Resumen Técnico: Más allá de la compilación: Evaluando la formalización fiel de enunciados de lenguaje natural a Lean

1. Planteamiento del problema

El artículo aborda la tarea de la formalización de enunciados de lenguaje natural a Lean: traducir automáticamente enunciados matemáticos informales en declaraciones de teoremas válidas en Lean 4. Esta tarea es distinta de la demostración de teoremas. En los entornos de prueba de teoremas (por ejemplo, MiniF2F, LeanDojo), el enunciado formal es fijo y confiable; el objetivo del sistema es generar una demostración que sea aceptada por el verificador. En la formalización de enunciados, el sistema debe generar el enunciado mismo.

El desafío central es que la compilación es una condición necesaria pero insuficiente para el éxito. Una declaración de Lean puede tipificarse (compilar) mientras:

• Omite hipótesis críticas.
• Cambia el dominio de discurso.
• Fortalece o debilita la afirmación.
• Codifica una versión vacua del resultado.

Los trabajos previos a menudo han dependido de las tasas de compilación o de métricas de equivalencia basadas en referencias (por ejemplo, BEq, retro-traducción). Este artículo argumenta que la compilación por sí sola crea una "brecha de paso de compilación" donde los sistemas parecen exitosos pero fallan en preservar el significado matemático pretendido. Los autores definen el problema central como la evaluación de la formalización fiel de enunciados: generar declaraciones que tanto compilen como preserven la intención semántica de la entrada de lenguaje natural.

2. Metodología

2.1 Construcción del Benchmark

Los autores curaron un benchmark de nivel de posgrado que consta de 400 enunciados de lenguaje natural derivados de notas de clase y libros de texto de código abierto en LaTeX. El conjunto de datos está equilibrado en cuatro dominios:

• Análisis Real (100 entradas)
• Análisis Complejo (100 entradas)
• Topología (100 entradas)
• Álgebra (100 entradas)

Crucialmente, estos enunciados no tienen declaraciones de Lean "gold" (de referencia) acompañantes, lo que asegura que la tarea represente una traducción genuina en lugar de una recuperación.

2.2 Protocolo de Evaluación

El artículo propone una métrica de Consenso de LLM como Juez, calibrada por expertos humanos, para evaluar la fidelidad. El protocolo involucra dos etapas:

1. Verificación del Compilador: Cualquier código que falle al compilar se considera inmediatamente infiel.
2. Consenso Semántico: Para el código que compila, dos jueces de LLM independientes (GPT-5.2 y Gemini-2.5-Pro) comparan la declaración de Lean generada contra el enunciado original de lenguaje natural. Asignan una puntuación de fidelidad (0–10).
   • Métrica de Éxito: Una traducción se considera Fiel si y solo si compila Y ambos jueces le asignan una puntuación $\ge 9$.
   • Este enfoque de consenso estricto está diseñado como un punto de operación conservador para la comparación de sistemas, no como una prueba formal de equivalencia.

2.3 Calibración Humana

Para validar la métrica automatizada, los autores realizaron auditorías humanas:

• Consenso-Positivo: El 96.0% de las salidas etiquetadas como fieles por el consenso estricto fueron confirmadas como fieles por los revisores humanos.
• Consenso-Negativo (Paso de Compilación): El 82.4% de las salidas que compilaron pero fueron rechazadas por el consenso fueron confirmadas como fallos semánticos genuinos por los humanos.
  Esto confirma que la métrica es un filtro de alta precisión y conservador que identifica eficazmente la deriva semántica.

2.4 Configuración Experimental: Diseño Factorial

Los autores evaluaron varios sistemas (LLMs de propósito general, formalizadores especializados, modelos orientados a la demostración y agentes aumentados por herramientas) utilizando un diseño factorial $2^3$ para descomponer los efectos de tres intervenciones comunes:

1. Borrador de Experto Paramétrico (T): Usar un modelo ajustado (Herald) para generar un borrador inicial.
2. Búsqueda de Conocimiento (S): Usar herramientas para consultar Mathlib (búsqueda de símbolos, resolución de espacios de nombres) y realizar búsquedas web para la fundamentación.
3. Retroalimentación de Elaboración de Lean (F): Usar un REPL para compilar código de forma iterativa y recibir mensajes de error para su reparación.

La arquitectura del agente utiliza un orquestador central (GPT-5.2) que mantiene el estado y decide qué herramientas invocar basándose en la configuración.

3. Resultados Clave

3.1 La Brecha de Paso de Compilación

El hallazgo empírico más significativo es la divergencia entre las tasas de compilación y la fidelidad semántica:

• Un agente completo aumentado por herramientas logró una tasa de compilación del 89.5%.
• Sin embargo, bajo la métrica de consenso estricto, solo el 60.5% de las salidas fueron consideradas fieles.
• Esto deja una brecha de 29.0 puntos donde las salidas compilan pero fallan en las verificaciones semánticas. Las auditorías humanas confirmaron que la mayoría de estos casos de "paso de compilación, negativo en consenso" son fallos semánticos reales (por ejemplo, falta de hipótesis, afirmaciones vacuas).

3.2 Rendimiento de los Modelos

• Formalizadores Especializados y Modelos de Demostración: Los formalizadores de enunciados dedicados (por ejemplo, Herald, Kimina-Autoformalizer) y los modelos orientados a la demostración (por ejemplo, Goedel-Prover, Kimina-Prover) tuvieron un desempeño pobre en la generación de enunciados cuando el objetivo formal no era suministrado. Sus tasas de fidelidad oscilaron entre el 4.0% y el 12.3%.
• LLMs de Propósito General: Los LLMs de propósito general de un solo paso (one-shot) alcanzaron una fidelidad del 19.8–28.0%.
• Agentes Aumentados por Herramientas: El marco de agente completo superó significativamente a los baselines de un solo paso, alcanzando un 60.5% de fidelidad. Sin embargo, diferentes orquestadores (Sonnet 4.5, Gemini-2.5-Pro) convergieron a niveles de rendimiento similares (60–65%) a pesar de diferentes baselines, lo que sugiere que las ganancias son estructurales al enfoque aumentado por herramientas más que específicas del modelo orquestador.

3.3 Descomposición Factorial de las Intervenciones

El estudio aisló el impacto de las tres herramientas:

• Retroalimentación de Elaboración (F): Fue el mayor impulsor de la validez (compilación), aumentando significamente la tasa de compilación. Sin embargo, también expandió el grupo de "paso de compilación pero infiel", ya que permitió que más enunciados sintácticamente correctos pero semánticamente desviados pasaran.
• Búsqueda (S): La búsqueda mejoró principalmente la fundamentación y la selectividad. Redujo la brecha de paso de compilación (es decir, ayudó a filtrar enunciados semánticamente incorrectos que lograban compilar) y mejoró la eficiencia al reducir el número de iteraciones de REPL necesarias. Su beneficio marginal fue mayor cuando la retroalimentación estaba ausente.
• Borrador de Experto (T): El borrador previo de un modelo ajustado fue en gran medida sustituible una vez que la retroalimentación y la fundamentación estuvieron disponibles. De hecho, con retroalimentación completa, el borrador previo afectó ligeramente el rendimiento, sugando que un orquestador fuerte con retroalimentación del compilador puede superar a un borrador especializado en este stack de herramientas específico.

3.4 Variaciones Específicas de Dominio

• Análisis Complejo mostró las mayores ganancias de la retroalimentación del compilador (+54.2 puntos en fidelidad), probablemente debido a la madurez de la cobertura de Mathlib.
• Análisis Real y Álgebra mostraron ganancias menores, indicando un soporte de librería limitado o una mayor dificultad intrínseca de formalización.
• Topología exhibió desafíos específicos con conceptos avanzados (por ejemplo, espacios de recubrimiento), donde la retroalimentación a menudo conducía a enunciados válidos pero semánticamente desplazados.

4. Significado y Reivindicaciones

El artículo afirma que la formalización de enunciados debe evaluarse como preservación de significado, no meramente como aceptación de Lean. Las contribales principales son:

1. Una Nueva Métrica: Una métrica basada en el consenso y calibrada por humanos, que expone la "brecha de paso de compilación", revelando que muchos sistemas generan enunciados sintácticamente válidos pero semánticamente incorrectos.
2. Descomposición Diagnóstica: Un análisis factorial que muestra que las herramientas no son adiciones monótonas. Mientras que la retroalimentación arregla la sintaxis, puede oscurecer los errores semánticos; la búsqueda mejora la fundamentación pero tiene rendimientos decrecientes cuando la retroalimentación está presente; y el borrador especializado no siempre es necesario en un bucle rico en retroalimentación.
3. Comparación de Sistemas: Evidencia de que los modelos orientados a la demostración y los formalizadores especializados actuales no transfieren automáticamente sus capacidades de demostración a la generación de enunciados semánticamente fieles sin un entrenamiento explícito centrado en el enunciado o protocolos aumentados por herramientas.

Los autores conclizan que los sistemas futuros deben emparejar una fuerte retroalimentación de Lean con la evaluación semántica y políticas que decidan cuándo buscar, reparar o detenerse, en lugar de confiar únicamente en las ganancias de precisión promedio. El artículo evita explícitamente reclamar que su métrica sea una prueba formal de equivalencia, posicionándola en su lugar como un límite de decisión conservador y escalable para la comparación de sistemas.