Improving Lean4 Autoformalization via Cycle Consistency Fine-tuning

Resumen Técnico: Mejora de la Autoformalización en Lean4 mediante Ajuste Fino de Consistencia de Ciclo

1. Planteamiento del Problema

La autoformalización es el proceso de traducir automáticamente textos matemáticos en lenguaje natural (NL) a lenguajes de prueba formal como Lean4. Aunque los Grandes Modelos de Lenguaje (LLM) han avanzado en razonamiento, la autoformalización sigue siendo un desafío crítico:

• Los modelos suelen generar código Lean4 que es sintácticamente válido (compila) pero semánticamente incorrecto (no captura el significado matemático deseado).
• La evaluación tradicional depende de compiladores o verificadores simbólicos, que pueden ser costosos computacionalmente o no estar disponibles para todos los tipos de problemas.
• Existe la necesidad de métodos de entrenamiento que optimicen la fidelidad semántica sin depender exclusivamente de recompensas de compilación estrictas.

2. Metodología

El autor aborda el problema como una tarea de traducción secuencia-a-secuencia, utilizando un enfoque de aprendizaje por refuerzo (RL) basado en la consistencia de ciclo.

• Modelos Base: Se utiliza Qwen3.5-2B como modelo principal, ajustado con LoRA (Low-Rank Adaptation) restringido a las subcapas de la red neuronal (FFN) para mantener la eficiencia computacional (9.4M parámetros entrenables de un total de 2B). También se incluye una comparación con Qwen3.5-9B.

• Arquitectura de Ciclo:

  1. Modelo $f_\theta$ (NL $\to$ Lean4): El modelo entrenable que formaliza la declaración matemática.
  2. Modelo $g_\phi$ (Lean4 $\to$ NL): Un modelo "traductor inverso" (back-translator) que se entrena inicialmente pero se congela durante la fase de RL.
  3. Métrica de Consistencia: Se define la puntuación de consistencia de ciclo $C_\theta(s)$ como la similitud coseno entre la declaración original $s$ y la reconstrucción $g_\phi(f_\theta(s))$, utilizando embeddings de oraciones del modelo all-MiniLM-L6-v2.

• Estrategias de Entrenamiento Comparadas:

  1. Ajuste Fino Supervisado (SFT) con Currículo: Entrenamiento secuencial ordenado por dificultad (1 a 10).
  2. SFT sin Currículo: Entrenamiento en el mismo conjunto de datos pero mezclado aleatoriamente.
  3. RL con GRPO (Group Relative Policy Optimization): Se utiliza el algoritmo GRPO para optimizar la política del modelo $f_\theta$ maximizando la recompensa de consistencia de ciclo. La recompensa se calcula como la similitud coseno mencionada anteriormente, evitando el costo de latencia de un REPL de Lean4.

• Datos:

  • FineLeanCorpus (FLC): 509k pares NL/Lean4 con etiquetas de dificultad. Se aplicó limpieza de datos (deduplicación, eliminación de errores de compilación) y descontaminación contra PutnamBench.
  • PutnamBench: 660 problemas de competencia de alto nivel utilizados como conjunto de evaluación fuera de distribución (held-out).

3. Contribuciones Clave

1. Pipeline de Ajuste Fino con LoRA: Implementación eficiente de un pipeline de autoformalización en Qwen3.5-2B con descontaminación rigurosa de datos.
2. Estudio de Ablación de Currículo: Demostración de que, para la escala de modelo (2B) y tamaño de datos utilizados, el ordenamiento por dificultad (currículo) no proporciona beneficios significativos en comparación con el entrenamiento aleatorio.
3. RL con Recompensa de Consistencia de Ciclo: Propuesta de un método de RL basado en GRPO que utiliza la consistencia semántica (NL $\to$ Lean4 $\to$ NL) como señal de recompensa. Esto logra mejoras sustanciales en la fidelidad semántica con un costo mínimo en la capacidad de modelado del lenguaje (pérdida de entropía cruzada).

4. Resultados Principales

Los resultados se evaluaron en el conjunto de datos FLC (700 ejemplos retenidos) y PutnamBench (660 problemas).

• Rendimiento Superior del RL: El modelo entrenado con RL (GRPO) superó significativamente a ambas variantes de SFT.
  • En FLC: Mejora de la consistencia de ciclo media de 0.513 (SFT) a 0.669 (RL).
  • En PutnamBench: Mejora de 0.422 (SFT) a 0.561 (RL).
  • Las diferencias son estadísticamente significativas ($p < 10^{-56}$).
• Impacto del Currículo: No hubo diferencia estadísticamente significativa entre el SFT con currículo y el SFT sin currículo (p > 0.3 en ambos conjuntos), indicando que el ordenamiento no compensa la capacidad limitada del modelo de 2B en esta tarea.
• Comparación de Escala: El modelo de 9B con SFT (0.585 en FLC) superó al de 2B con SFT, pero el modelo de 2B con RL (0.669) superó al de 9B con SFT, demostrando que el RL ofrece una mejora mayor que simplemente aumentar el tamaño del modelo en este contexto.
• Estabilidad del Lenguaje: El aumento en la pérdida de entropía cruzada (CE) fue mínimo (0.011 nats), lo que indica que el modelo no degradó su capacidad básica de modelado de lenguaje al optimizar la consistencia.
• Análisis por Dominio: El RL mejoró consistentemente en todos los dominios matemáticos. Los dominios discretos (teoría de números, álgebra) obtuvieron puntuaciones más altas que los continuos (cálculo, análisis), debido a que las estructuras algebraicas se traducen y retrotraducen de manera más limpia.

5. Significado y Limitaciones

• Significado: Este trabajo demuestra que la consistencia de ciclo es una señal de recompensa viable y potente para el entrenamiento por refuerzo en tareas de formalización matemática. Permite mejorar la calidad semántica de las formalizaciones sin depender exclusivamente de compiladores costosos o verificadores simbólicos complejos durante el entrenamiento.
• Limitaciones Identificadas:
  • Hacking de Recompensa: La métrica de consistencia puede ser engañada si el modelo genera código Lean4 que, al ser retrotraducido, devuelve el texto original casi verbatim (especialmente en problemas con patrones estructurales simples), inflando la puntuación sin garantizar la corrección matemática profunda.
  • Sesgo del Traductor Inverso: Dado que el mismo modelo congelado se usa para calcular la recompensa y evaluar el resultado, cualquier sesgo sistemático en la retrotraducción afecta a todos los modelos por igual.
  • Falta de Verificación de Pruebas: Los ejemplos generados utilizan sorry (marcador de posición), por lo que la compilación exitosa solo garantiza validez sintáctica, no corrección matemática real.

Conclusión

El proyecto concluye que el ajuste fino mediante RL con GRPO y recompensas de consistencia de ciclo es una estrategia superior a la SFT tradicional para la autoformalización en Lean4, logrando una fidelidad semántica significativamente mayor. Además, sugiere que, para modelos de tamaño medio (2B), la complejidad del ordenamiento de datos (currículo) es menos crítica que la optimización directa de la fidelidad semántica mediante RL.