Resumen Técnico: Refactorización Lean

Declaración del Problema

Los Modelos de Lenguaje Grande (LLM) entrenados con aprendizaje por refuerzo (RL) para la demostración formal de teoremas en Lean a menudo generan pruebas que son correctas pero notoriamente verbosas, frágiles y computacionalmente costosas. Aunque existen esfuerzos de refactorización previos, enfrentan tres limitaciones fundamentales al aplicarse al ecosistema Lean:

1. Tensión Multiobjetivo: La refactorización en Lean es inherentemente multiobjetivo. Optimizar la longitud de la prueba a menudo entra en conflicto con la minimización del costo de compilación (por ejemplo, las pruebas más cortas pueden invocar tácticas pesadas que inflan el tiempo de compilación), y los métodos existentes carecen de mecanismos principistas para equilibrar estos compromisos o adaptarse a objetivos de usuario no vistos en el momento de la inferencia.
2. Fragilidad de Versión: Lean y su biblioteca estándar, Mathlib, evolucionan casi semanalmente con cambios frecuentes en la API y renombres de lemas. Los LLM de vanguardia tienen cortes de conocimiento estáticos, lo que lleva a alucinaciones de tácticas obsoletas e incompatibilidad con las cadenas de herramientas actuales.
3. Escasez de Datos: A diferencia de los lenguajes de programación convencionales, Lean carece de conjuntos de datos emparejados a gran escala (pares de código ruidoso-limpio) requeridos para pipelines de refactorización basados en entrenamiento. Además, los enfoques basados en entrenamiento requieren un ajuste fino repetido para cada nueva versión de LLM, fallando al escalar con el cambio de modelos o el ciclo de lanzamiento de Lean.

Metodología: Refactorización Lean

Los autores proponen Lean Refactor, un marco de agente aumentado por recuperación, plug-and-play, diseñado para refactorizar pruebas en Lean sin ajustar finamente el LLM subyacente. El sistema desacopla la lógica de refactorización del modelo externalizando el conocimiento en una base de datos estructurada y densamente anotada.

1. Banco de Estrategias Densamente Anotado

El núcleo del marco es una base de datos curada de 9.237 estrategias de refactorización únicas destiladas de más de 200.000 pares de pruebas largas-cortas.

• Estructura: Cada estrategia incluye un título, descripción, precondición ("cuándo aplicar"), guía de aplicación paso a paso y ejemplos abstractos antes/después.
• Metadatos: Crucialmente, cada estrategia está anotada con metadatos que el LLM no puede inferir de los datos de entrenamiento:
  • Reducción del Tiempo de Compilación: La aceleración relativa mediana observada al aplicar la estrategia.
  • Compatibilidad de Versión: Un conjunto de cadenas de herramientas Lean/Mathlib validadas (por ejemplo, v4.14.0, v4.16.0, v4.22.0) bajo las cuales la prueba refactorizada se compila con éxito. Esto se determina recompilando pruebas acortadas a través de múltiples versiones.

2. Recuperación y Reordenamiento Multiobjetivo

En la inferencia, el marco emplea un pipeline de recuperación que se adapta a objetivos especificados por el usuario sin reentrenamiento del modelo:

• Prueba Más Corta: Recupera estrategias basándose puramente en la similitud semántica (similitud del coseno) con el segmento de la prueba.
• Consciente del Tiempo de Compilación: Recupera un amplio conjunto de candidatos semánticamente similares y luego los reordena basándose en los metadatos anotados de reducción de costo de compilación.
• Específico de Versión: Filtra el conjunto de candidatos para incluir solo estrategias cuyos metadatos de compatibilidad incluyen la versión de Lean objetivo del usuario.

3. Bucle de Agente

El marco envuelve estos componentes en un bucle de agente agnóstico al modelo que consta de:

• Planificador: Descompone la tarea de refactorización en pasos específicos basados en las estrategias recuperadas.
• Refactorizador: Ejecuta el plan para generar una prueba más corta.
• Depurador: Utiliza la retroalimentación del compilador para reparar errores en un bucle cerrado (hasta $D$ rondas).
• Agnosticismo del Modelo Base: El planificador, el refactorizador y el depurador pueden ser instanciados por cualquier LLM de vanguardia congelado (por ejemplo, Gemini, Claude, serie GPT), permitiendo que el sistema se transfiera entre modelos sin reentrenamiento.

Contribuciones Clave

1. Lanzamiento de Conjunto de Datos: Los autores lanzan el mayor conjunto de datos de refactorización Lean hasta la fecha, que comprende más de 200K pares de pruebas largas-cortas y 9K estrategias de refactorización, cada una anotada con costo de compilación y compatibilidad de versión.
2. Rendimiento: Lean Refactor logra una compresión a nivel de token >70% en benchmarks de competencia (miniF2F, PutnamBench) y >20% en repositorios de investigación (Analysis, FLT, PhysLean). También reduce el tiempo de compilación hasta un 60% en benchmarks de competencia.
3. Controlabilidad y Robustez: El sistema soporta control multiobjetivo (longitud vs. velocidad vs. compatibilidad) mediante reglas de recuperación en lugar de pesos del modelo. Las pruebas refactorizadas exhiben una transferencia de versión zero-shot más fuerte hacia futuras versiones de Lean en comparación con sus contrapartes no refactorizadas y métodos de optimización anteriores.
4. Agnosticismo del Modelo: El marco mejora el rendimiento a través de diferentes modelos base LLM (Gemini 3 Flash, Claude Haiku 4.5) y supera a agentes de codificación de propósito general como Claude Code, incluso cuando este último tiene acceso a la misma herramienta de recuperación de estrategias.

Resultados Experimentales

• Reducción de Longitud: En benchmarks de competencia, Lean Refactor supera al estado anterior del arte, ProofOptimizer, logrando una reducción del 88,40% en miniF2F y del 70,38% en PutnamBench (frente al 57,20% de ProofOptimizer). En pruebas de nivel de investigación, logra una reducción promedio del 20–33%, superando significativamente a las líneas base de ablación.
• Tiempo de Compilación: Al reordenar estrategias basándose en metadatos de costo de compilación, el marco logra una reducción relativa del 42,62% en el tiempo de compilación en PutnamBench, comparado con el 37,11% del enfoque de recuperación estándar.
• Compatibilidad de Versión: Al apuntar a versiones específicas de Lean (por ejemplo, v4.16.0), la recuperación filtrada por versión produce consistentemente una mejor reducción de longitud que la recuperación sin filtrar. Las pruebas refactorizadas mantienen la capacidad de verificación de tipos a través de más futuras versiones de Lean (hasta v4.29.0) que las producidas por ProofOptimizer o las pruebas verbosas originales.
• Reducción de Dependencias: Las pruebas refactorizadas reducen las dependencias externas e intra-proyecto en el 42–67% de los casos, indicando una simplificación lógica genuina en lugar de una mera externalización a lemas pesados de bibliotecas.

Significado

El artículo argumenta que Lean Refactor aborda los cuellos de botella críticos del mantenimiento de bibliotecas matemáticas formales: la tensión entre la concisión de la prueba y la eficiencia de compilación, y la fragilidad del código a través de cadenas de herramientas en rápida evolución. Al externalizar el conocimiento de refactorización en un banco de estrategias rico en metadatos, el marco habilita una optimización multiobjetivo controlable sin la necesidad de un ajuste fino costoso del modelo. Este enfoque permite que el sistema permanezca robusto frente a la deriva de versiones de Lean/Mathlib y adaptable inmediatamente a nuevos modelos base LLM, sentando las bases para pruebas formales más mantenibles y resilientes a versiones.