Formally Solving Answer-Construction Problems in Lean

Resumen Técnico: Resolución Formal de Problemas de Construcción de Respuestas en Lean

Definición del Problema
Los problemas de competición matemática generalmente se dividen en dos categorías: demostración de teoremas (verificar una proposición dada) y construcción de respuestas (construir un objeto específico que satisfaga una propiedad). Si bien los avances recientes en los Modelos de Lenguaje de Gran Escala (LLM) han mejorado significamente la demostración formal de teoremas, la construcción formal de respuestas sigue estando poco explorada. Existe una brecha crítica entre los sistemas de razonamiento informal, que son fuertes en la formulación de conjeturas pero débiles en la verificación formal, y los LLM de demostración formal, que están optimizados para las pruebas pero tienen dificultades para descubrir los testigos necesarios para eliminar los cuantificadores existenciales.

Un desafío específico al formalizar la construcción de respuestas es la admisibilidad. Los verificadores de pruebas estándar de Lean verifican que un término de prueba tenga el tipo correcto, pero no imponen inherentemente que el testigo construido sea una respuesta canónica de forma cerrada. Por ejemplo, una prueba podría satisfacer una sentencia existencial $\exists x, P(x)$ devolviendo un término no canónico como sInf PropertySet (el ínfimo del conjunto definido) en lugar de un número natural explícito (por ejemplo, 245). Tales testigos "circulares" o de forma no cerrada son matemáticamente válidos dentro de la lógica, pero inadmisibles como respuestas de concurso.

Metodología: Enumerar-Conjeturar-Probar (ECP)
Para abordar estos desafíos, los autores introducen Enumerate-Conjecture-Prove (ECP), un marco neuro-simbólico diseñado para la construcción de respuestas de extremo a extremo con demostraciones formales en Lean 4. ECP separa el proceso en etapas distintas manteniendo un bucle de verificación formal:

1. Formalización del Problema y Verificación de Admisibilidad:

   • Los problemas se formalizan como tareas de síntesis funcional: encontrar una función $\Psi$ tal que $\forall X, P(X) \to Q(X, \Psi(X))$.
   • Se implementa un verificador de admisibilidad para asegurar que la respuesta sintetizada utilice solo un "vocabulario admisible" predefinido (por ejemplo, constantes específicas, operadores aritméticos y constructores estándar). Este extrae estructuralmente las constantes semánticas del término de Lean y filtra las constantes administrativas (como instancias de clases de tipos o artefactos generados por el compilador) y las definiciones no canónicas (como sInf).

2. Etapa de Enumeración (Exploración Asistida por Herramientas):

   • Un LLM de propósito general (por ejemplo, GPT-5.4) está equipado con capacidades de ejecución de herramientas de Python.
   • El LLM escribe y ejecuta código Python para realizar una enumeración acotada sobre dominios pequeños para encontrar tuplas que satisfagan las restricciones del problema.
   • Estos trazos de ejecución sirven como evidencia empírica para identificar patrones, invariantes y formas funcionales.

3. Etapa de Conjetura (Síntesis de Respuesta):

   • Utilizando la evidencia de la etapa de Enumeración, el mismo LLM general sintetiza una función de respuesta candidata $\Psi'$.
   • La candidata se somete a dos filtros antes de proceder:
     • Verificación Sintáctica: El término debe compilar en Lean con el tipo correcto.
     • Verificación de Admisibilidad: El término debe utilizar únicamente constantes del vocabulario permitido.
   • Si una candidata falla, el sistema itera incluyendo el mensaje de error en el prompt.

4. Etapa de Demostración (Verificación Formal):

   • Una vez construida una candidata válida $\Psi'$, el sistema intenta demostrar el teorema instanciado $Stmt(T)|_{\Psi=\Psi'}$.
   • Bucle de Refutación: Antes de intentar una demostración, el sistema intenta refutar la candidata probando su negación. Si la refutación tiene éxito, la candidata se descarta y el sistema regresa a la etapa de Conjetura.
   • Generación de Demostración: Si la refutación falla, el sistema intenta probar la sentencia positiva utilizando una combinación de la automatización integrada de Lean (tácticas como simp, aesop, ring, norm_num) y un LLM de demostración especializado (por ejemplo, Goedel-Prover-V2). Si la automatización falla, se invoca al LLM de demostración con un bucle de reparación para generar o corregir la prueba.

Contribuciones Clave

• Marco para la Construcción de Respuestas: ECP es el primer marco que separa explícitamente la construcción de la respuesta de la generación de la demostración, imponiendo restricciones de admisibilidad dentro de un bucle de verificación formal.
• Imposición de Admisibilidad: El artículo introduce un método estructural para filtrar testigos no canónicos (por ejemplo, definiciones circulares) que los verificadores estándar de Lean aceptarían de otro modo, asegurando que la salida coincida con los requisitos del concurso.
• Integración Neuro-Simbólica: El marco combina eficazmente el razonamiento exploratorio de los LLM generales con herramientas de Python y las rigurosas capacidades de demostración de los LLM de demostración especializados.
• Benchmarks y Autoformalización: Los autores autoformalizaron 75 problemas de las Competiciones de Respuesta Final de MathArena 2026 (AIME, HMMT, APEX) y 346 problemas de construcción de respuestas de PutnamBench, creando un nuevo estándar de evaluación para este tipo de problema.

Resultados Experimentales
El sistema fue evaluado en MathArena 2026 (75 problemas) y PutnamBench (346 problemas) frente a líneas de base que incluyen LLM de generación de demostración directa (GPT-5.4, Goedel-Prover-V2).

• Rendimiento de Extremo a Extremo: ECP superó a las líneas de base de generación de demostración directa.
  • MathArena: ECP resolvió 18/75 problemas (Pass@32), comparado con 13/75 para la mejor línea de base de solo LLM (GPT-5.4).
  • PutnamBench: ECP resolvió 17/346 problemas (Pass@32), comparado con 8/346 para GPT-5.4 y 7/346 para Goedel-Prover-V2-32B.
• Precisión de Solo Respuesta: La construcción de respuestas asistida por herramientas mejoró significativamente la precisión de los LLM generales al generar candidatos correctos. Para GPT-5.4, el uso de herramientas aumentó la construcción de respuestas correctas en PutnamBench de 290/346 a 303/346.
• Impacto de la Admisibilidad: El análisis reveló que muchas pruebas generadas por las líneas de base eran compilables en Lean pero contenían respuestas inadmisibles (por ejemplo, testigos circulares). La verificación de admisibilidad explícita de ECP fue crucial para filtrar estas.
• Estudios de Ablación:
  • Eliminar el paso de corrección del LLM de demostración redujo el rendimiento en MathArena (18 $\to$ 16) y PutnamBench (17 $\to$ 16).
  • Eliminar la automatización de Lean tuvo un impacto severo en MathArena (18 $\to$ 11) pero menos en PutnamBench en la ejecución específica, sugiriendo que los problemas de MathArena dependen más de las tácticas de automatización mientras que PutnamBench depende más de la capacidad del demostrador.
  • Usar un demostrador más pequeño (8B) mantuvo el rendimiento de MathArena pero redujo significativamente los resultados de PutnamBench (17 $\to$ 7), indicando que los problemas de Putnam están más limitados por la búsqueda de la demostración.

Significado y Reivindicaciones
El artículo afirma que ECP logra cerrar la brecha entre la generación de respuestas informales y la demostración de teoremas formal. Al manejar explícitamente la fase de "construcción de la respuesta" e imponer la admisibilidad, ECP resuelve instancias que actualmente son intratables para los enfoques de generación de demostración directa. Los autores enfatizan que su enfoque es particularmente efectivo para problemas que requieren la construcción de un testigo específico (cuantificación existencial) en lugar de solo verificar una conclusión fija.

El trabajo destaca que los benchmarks formales actuales suelen omitir la dificultad de la construcción de respuestas, centrándose en su lugar en las versiones de los problemas "con respuesta". ECP demuestra que combinar LLM generales con la ejecución de herramientas para la enumeración, seguido de LLM de demostración especializados para la verificación, es un camino viable para resolver problemas matemáticos complejos y abiertos en sistemas formales. Los autores señalan limitaciones respecto a la naturaleza heurística del etiquetado del vocabulario admisible y el potencial de explosión combinatoria en la etapa de enumeración para problemas de combinatoria altamente complejos.