Resumen Técnico: ImProver 2

Enunciado del Problema

La rápida expansión de las bibliotecas de matemáticas formales (por ejemplo, Mathlib de Lean) ha creado un doble desafío: la mantenibilidad de estas bibliotecas se ve amenazada por estilos de prueba heterogéneos y una baja modularidad, mientras que la calidad de los datos de entrenamiento para los demostradores de teoremas neuronales se degrada debido a pruebas que son correctas pero estructuralmente subóptimas. Los métodos existentes de optimización automática de pruebas enfrentan obstáculos significativos, incluidos objetivos heterogéneos y definidos heurísticamente, datos de optimización de alta calidad escasos y los costos prohibitivos de entrenamiento e inferencia para modelos a gran escala. Además, trabajos anteriores a menudo dependían de modelos de propósito general de código cerrado o se centraban estrechamente en la cantidad de tokens, sin abordar métricas estructurales más amplias como la modularidad y la gestión de dependencias.

Metodología

Los autores presentan ImProver 2, un marco neurosimbólico diseñado para mejorar iterativamente de forma autónoma modelos de lenguaje pequeños (SLM) para la optimización de pruebas en Lean 4. El sistema opera mediante una tubería de múltiples componentes:

1. Aumento Neurosimbólico (Andamiaje)

Para cerrar la brecha entre el razonamiento informal y la verificación formal, el marco expone al modelo a un contexto rico del entorno Lean. Este "andamiaje" ($\Psi$) incluye:

• Rebanadas de Contexto: Definiciones, teoremas y lemas relevantes referenciados directamente por la prueba objetivo, serializados con metadatos.
• Cadenas de Estados (CoS): Rastros explícitos de los estados de la meta antes y después de cada paso de táctica, intercalados como comentarios para revelar el flujo lógico de la prueba.
• Auto-informalización: Resúmenes en lenguaje natural de los pasos de la prueba, generados traduciendo la prueba formal a una secuencia de descripciones de alto nivel.

2. Métricas de Optimización

El sistema apunta a tres objetivos estructurales distintos, definidos como funciones computables $\mu$:

• Longitud: Minimizar el número de tácticas utilizadas ("golfing" de pruebas).
• Dependencias: Minimizar la cantidad de lemas externos únicos nombrados explícitamente en la prueba, fomentando pruebas autocontenidas.
• Modularidad: Maximizar el número de "metas generadas efectivas" (subpruebas independientes introducidas mediante have, calc, etc.), lo que sirve como un proxy para la descomposición de pruebas y la mantenibilidad.

3. Tubería de Optimización de Preferencias Iterativa (IRPO)

ImProver 2 emplea un bucle de entrenamiento iterativo para arrancar SLM:

1. Generación: El modelo actual $G_t$ genera $n$ reescrituras candidatas para cada teorema en el conjunto de entrenamiento, utilizando el andamiaje neurosimbólico.
2. Filtrado y Reproducción: Los candidatos se puntúan según la corrección (verificación del núcleo de Lean) y la mejora de la métrica. Se utiliza un búfer de reproducción para equilibrar los datos recién generados con los datos históricos, evitando el colapso del modelo y asegurando una mejora monótona. Se filtran problemas triviales o de baja calidad.
3. Construcción de Pares de Preferencia: El conjunto de datos se divide en "ganadores" (pruebas que se compilan y tienen alta mejora) y "perdedores" (fallos o pruebas con baja mejora). Se forman dos tipos de pares de preferencia: ganador–ganador (ordenados por magnitud de mejora) y ganador–perdedor.
4. Entrenamiento: El modelo se actualiza utilizando Optimización de Preferencias de Razonamiento Iterativa (IRPO), que combina una pérdida de Optimización de Preferencias Directa (DPO) con una pérdida de verosimilitud negativa (NLL) en las pruebas ganadoras. Este proceso se repite hasta la convergencia o el agotamiento del presupuesto.

Contribuciones Clave

1. SLM de Auto-mejora para Refactorización: El artículo demuestra que la optimización de preferencias iterativa puede arrancar eficazmente modelos de lenguaje pequeños (específicamente un modelo de 7 mil millones de parámetros) para optimizar pruebas en bibliotecas de investigación especializadas, haciéndolos competitivos con modelos significativamente más grandes.
2. Métricas de Optimización Estructural: Más allá de la simple reducción de longitud, los autores introducen y evalúan métricas de modularidad y dependencia. Estas métricas aprovechan la estructura de la prueba y el contexto de la biblioteca para abordar objetivos de refactorización distintos relevantes para la mantenibilidad de la biblioteca.
3. Aumento Neurosimbólico: El marco extrae e integra rastros de estados de meta, contexto relevante y auto-informalizaciones. Los autores muestran que este aumento mejora significativamente el rendimiento tanto para modelos pequeños como de vanguardia, facilitando el descubrimiento de reescrituras válidas y de alto valor.

Resultados Experimentales

El sistema se evaluó en miniCTX-v2, una referencia de matemáticas a nivel de investigación escritas por humanos, utilizando un modelo base de 7 mil millones de parámetros (DeepSeek-R1-Distill-Qwen-7B).

• Rendimiento vs. Escala: ImProver 2 supera al modelo DeepSeek-R1 de 671 mil millones de parámetros, mucho más grande, en las tres métricas (Longitud, Modularidad, Dependencia) cuando no tiene andamiaje. Por ejemplo, en modularidad, ImProver 2 logró una mejora media de 0.143 en comparación con 0.055 para el modelo de 671B.
• Comparación con Modelos de Vanguardia: El modelo ImProver 2 de 7B es competitivo con modelos de vanguardia de nivel medio (por ejemplo, GPT-5-mini) en métricas de longitud y dependencia. Lidera a todos los sistemas evaluados sin andamiaje en modularidad.
• Impacto del Andamiaje: Añadir el andamiaje neurosimbólico mejora significativamente el rendimiento en todas las familias de modelos. Por ejemplo, la puntuación de mejora de longitud del modelo de 7B aumentó de 0.118 (base) a 0.236 (con andamiaje). Incluso modelos grandes como GPT-5-high vieron ganancias sustanciales (de 0.660 a 0.875) con el andamiaje.
• Dinámica de Iteración: La mayoría de las ganancias de rendimiento ocurren dentro de las primeras 2–3 iteraciones de IRPO. El sistema muestra que los modelos pequeños pueden aprender a reestructurar pruebas a nivel de investigación de manera efectiva, aunque el rendimiento eventualmente se estabiliza a medida que el modelo absorbe patrones de refactorización comunes.
• Compensaciones de Precisión: El artículo nota una compensación entre la optimización y la precisión de compilación. Si bien las pruebas optimizadas a menudo producen mayores mejoras en las métricas, pueden tener tasas de compilación ligeramente inferiores a las reescrituras conservadoras, reflejando la naturaleza más arriesgada de las transformaciones estructurales.

Significado y Afirmaciones

El artículo postula que la optimización de pruebas no es únicamente una función de la escala del modelo, sino que está impulsada significativamente por la especialización específica de la tarea y la auto-mejora iterativa. Al combinar una tubería de optimización de preferencias con búfer de reproducción con un andamiaje neurosimbólico, ImProver 2 establece que modelos pequeños y accesibles pueden reestructurar eficazmente pruebas complejas a nivel de investigación.

Los autores afirman que su trabajo establece la optimización de pruebas como una tarea escalable y aprendible. Argumentan que su enfoque aborda la necesidad crítica de mantener bibliotecas formales y mejorar la calidad de los datos de entrenamiento para futuros demostradores, ofreciendo un camino para automatizar la refactorización de pruebas para la mantenibilidad sin depender exclusivamente de modelos de vanguardia masivos y costosos. El trabajo destaca que, con el andamiaje y el entrenamiento adecuados, los modelos pequeños pueden igualar o superar el rendimiento de sistemas sustancialmente más grandes en objetivos estructurales específicos.