Resumen Técnico: Compile to Compress

1. El Problema

La demostración formal de teoremas asistida por Grandes Modelos de Lenguaje (LLM) ha avanzado significativamente, pero enfrenta un cuello de botella crítico en la escalabilidad. Los métodos actuales de vanguardia (State-of-the-Art) a menudo requieren una cantidad prohibitiva de cómputo en tiempo de prueba (test-time compute) mediante:

• Despliegues masivos (Roll-outs): Generar miles de intentos de prueba independientes.
• Ventanas de contexto extendidas: Mantener historiales largos de intentos fallidos para la autocorrección, lo que satura los límites de memoria y aumenta la latencia.

Los enfoques existentes suelen tratar los mensajes de error del compilador (como Lean) como señales binarias (éxito/fracaso) o texto plano simple, ignorando la estructura rica que estos mensajes contienen. Esto obliga a los modelos a depender de correcciones iterativas acumulativas, lo que es ineficiente y costoso.

2. Metodología Propuesta

Los autores proponen un marco de "Aprendizaje para Refinar" (Learning-to-Refine) basado en una observación fundamental: el compilador actúa como un compresor de dimensiones.

2.1. Compresión de Dimensiones por el Compilador

Aunque el espacio de programas Lean es combinatoriamente vasto y casi ilimitado, el compilador mapea una gran variedad de intentos de prueba fallidos a un conjunto compacto y estructurado de modos de fallo (mensajes de error).

• Hipótesis: Muchos programas sintácticamente distintos pero semánticamente incorrectos generan las mismas firmas de error.
• Implicación: En lugar de aprender a generar soluciones desde cero para cada problema, el modelo puede aprender a refinar intentos fallidos basándose en el tipo de error estructural (el mensaje del compilador).

2.2. Marco de Aprendizaje para Refinar

El sistema transforma el proceso de demostración en un proceso de refinamiento markoviano:

1. Entrada: Un intento de prueba fallido ($c$) y su mensaje de error del compilador ($\Phi(c)$).
2. Salida: Un análisis de la causa del error y el programa Lean corregido.
3. Entrenamiento:
   • Síntesis de Datos en Frío (Cold-Start): Se utiliza un modelo externo (Claude-3.7-Sonnet) para generar "pensamientos" (razonamiento) que explican cómo corregir errores específicos, creando un dataset de pares (estado fallido $\to$ corrección).
   • Iteración de Expertos: Se entrena al modelo mediante Fine-Tuning Supervisado (SFT) y luego se mejora mediante iteración de expertos, donde el modelo corrige sus propios fallos en un bucle, generando datos de entrenamiento on-policy.

2.3. Cadena de Distribuciones (Chain of Distributions - CoD)

A diferencia de la generación directa, que muestrea desde una única distribución fija $D_{direct}$, el refinamiento induce una cadena de distribuciones condicionales.

• Cada paso de corrección mueve la probabilidad hacia regiones del espacio de programas que contienen soluciones correctas, basándose en el feedback del compilador.
• Esto permite escapar de los modos locales donde la generación directa se estanca.

2.4. Estrategia de Búsqueda en Tiempo de Prueba

Para gestionar el presupuesto computacional, se introduce una búsqueda en árbol guiada por valores:

• Se entrena una función de valor neuronal que estima el potencial de un nodo (un intento de prueba) para llevar a una solución.
• La búsqueda alterna dinámicamente entre:
  • BFS (Búsqueda en Amplitud): Generar nuevos intentos desde cero.
  • DFS (Búsqueda en Profundidad): Refinar un intento fallido previo.
• La función de valor decide cuándo es más eficiente intentar una nueva prueba o corregir una existente, optimizando el uso de recursos.

3. Contribuciones Clave

1. Nueva Perspectiva Teórica: Identificar al compilador no solo como un validador, sino como un compresor de dimensiones que revela una estructura latente en los modos de fallo, permitiendo generalizar estrategias de corrección entre problemas diferentes.
2. Marco de Refinamiento Markoviano: Un enfoque que elimina la necesidad de mantener historiales largos de contexto, reduciendo el costo de inferencia y permitiendo un aprendizaje más eficiente de estrategias de reparación.
3. Búsqueda Guiada por Valores: Un algoritmo de búsqueda que combina generación directa y refinamiento iterativo, utilizando una función de valor aprendida para priorizar las ramas más prometedoras del árbol de búsqueda.
4. Rendimiento Escalable: Demostración de que este método escala consistentemente con el tamaño del modelo y el presupuesto de cómputo, sin depender de arquitecturas masivas o costos de inferencia desproporcionados.

4. Resultados Experimentales

Los autores evaluaron su método en dos modelos base: Kimina-Prover-Distill-8B y Goedel-Prover-V2-32B, sobre cuatro benchmarks estándar: MiniF2F, ProofNet, MathOlympiadBench y PutnamBench.

• Mejoras Generales: Los probadores aumentados superaron consistentemente a sus contrapartes base en todos los benchmarks. En Goedel-32B, se observaron mejoras relativas superiores al 50% en ProofNet, MathOlympiadBench y PutnamBench.
• Rendimiento en PutnamBench (Estado del Arte):
  • Modelo 32B: El probador Goedel-32B refinado resolvió 110 problemas, superando a todas las soluciones de escala comparable (incluyendo Ax-Prover y la versión original de Goedel-V2).
  • Modelo 8B: El probador Kimina-8B refinado resolvió 25 problemas, ocupando el primer lugar entre los probadores de tamaño similar.
• Eficiencia de Búsqueda: La búsqueda guiada por valores superó a la búsqueda aleatoria y a las estrategias puras de generación directa, especialmente en problemas difíciles donde la corrección iterativa es necesaria.
• Análisis de Distribuciones: Pruebas estadísticas confirmaron que el refinamiento explora regiones del espacio de programas que son inalcanzables para la generación directa, validando la hipótesis de la "Cadena de Distribuciones".

5. Significado e Impacto

Este trabajo ofrece un paradigma escalable para la próxima generación de razonamiento guiado por verificadores.

• Eficiencia: Reduce drásticamente la necesidad de cómputo en tiempo de prueba al evitar la acumulación de contextos largos y los despliegues masivos.
• Generalización: Al centrarse en los modos de fallo estructurales (mensajes de error) en lugar de la sintaxis superficial, el modelo aprende a corregir errores de manera más robusta y transferible entre problemas.
• Futuro: Establece una base para sistemas de demostración de teoremas que no dependen exclusivamente del tamaño del modelo, sino de la inteligencia en la gestión de la búsqueda y el aprendizaje de estrategias de corrección.

En resumen, "Compile to Compress" demuestra que explotar la estructura de los mensajes de error del compilador permite transformar la demostración de teoremas de un proceso de generación ciega a uno de corrección dirigida y eficiente, logrando un rendimiento de vanguardia con recursos computacionales moderados.