Benchmarking Testing in Automated Theorem Proving

1. Planteamiento del Problema

El rápido avance de los Modelos de Lenguaje Grandes (LLM) ha mejorado su capacidad para generar pruebas formales en sistemas como Lean. Sin embargo, los métodos de evaluación actuales adolecen de un defecto crítico: confunden la validez sintáctica con la corrección semántica.

• La Limitación de la Compilación: Las métricas existentes (por ejemplo, MiniF2F, ProofNet) evalúan principalmente a los modelos verificando si un teorema generado compila. Aunque la compilación verifica que el código sea sintácticamente válido y lógicamente consistente de forma aislada, no garantiza que el teorema capture el significado matemático intencionado.
• El Problema de la "Tautología": Un modelo puede generar una tautología trivial (por ejemplo, $a + b = a + b$) que compila con éxito pero falla al probar la afirmación no trivial pretendida (por ejemplo, la conmutatividad $a + b = b + a$).
• Insuficiencia de los Proxies: Los intentos existentes de medir la corrección semántica dependen de proxies poco fiables, como la superposición léxica (puntuaciones BLEU) frente a referencias anotadas manualmente o la inspección humana. Estos métodos son ruidosos, requieren costoso trabajo humano o no logran distinguir entre significados semánticos correctos e incorrectos.

2. Metodología

Los autores proponen un cambio de paradigma inspirado en las pruebas de integración en la ingeniería de software. En lugar de evaluar un teorema de forma aislada, lo evalúan basándose en cómo interactúa con el resto de la base de código.

Concepto Central: Pruebas de Teoremas (T2)

Basándose en la correspondencia de Curry-Howard (donde las pruebas corresponden a programas), los autores tratan un teorema generado como una función y los teoremas que dependen de él como "casos de prueba".

• Grafo de Dependencias: Construyen un grafo de dependencias donde un teorema objetivo ($t_{GT}$) tiene predecesores (definiciones/lemmas que utiliza) y sucesores (teoremas que lo invocan o construyen sobre él).
• Lógica de Pruebas de Integración: Si un teorema generado ($t_{fl}$) es semánticamente incorrecto (por ejemplo, define una tautología en lugar de la propiedad pretendida), cualquier teorema sucesor que dependa de él fallará al compilar.
• Analogía de Eliminación de Cortes: El proceso se fundamenta formalmente en el principio lógico de Eliminación de Cortes. Si una cadena de pruebas ($X \to Y \to Z \to W$) falla cuando el lema intermedio ($Y$) se reemplaza por un candidato generado, el candidato es semánticamente incorrecto.

El Benchmark T2

Los autores construyeron un benchmark a gran escala, T2, para facilitar esta evaluación:

• Fuente: Extraído de 5 repositorios reales de Lean 4 (que cubren álgebra, topología, teoría de números, etc.).
• Escala: 2.206 problemas, cada uno emparejado con un promedio de 41 teoremas sucesores.
• Subconjunto Difícil: Un subconjunto de 389 problemas "Difíciles" donde el modelo debe generar tanto la proposición (afirmación) como la prueba, en lugar de simplemente completar una prueba para una afirmación dada.
• Automatización: El pipeline de extracción es totalmente automatizado, sin requerir anotación humana para la estructura de dependencias. Las descripciones en lenguaje natural (LN) fueron generadas por un LLM potente (Claude Sonnet 4.5) y verificadas manualmente en una muestra.

La Métrica: Precisión de Pruebas (TA)

El artículo introduce la Precisión de Pruebas (TA) como la métrica de evaluación principal:
$$TA = E_{P \sim D} \left[ \prod_{i=1}^{k} \text{compiles}(t^{(i)}_{succ} \mid t_{fl}) \right]$$
Un teorema generado solo pasa si todos sus teoremas sucesores dependientes compilan con éxito cuando el teorema original se reemplaza por el generado.

3. Contribuciones Clave

1. Benchmark T2: El primer benchmark a gran escala, rico en dependencias, para la demostración de teoremas formales que va más allá de problemas aislados hacia contextos de repositorios del mundo real.
2. Precisión de Pruebas (TA): Una métrica novedosa, automática y libre de referencias que verifica directamente la corrección semántica mediante la compilación de módulos dependientes.
3. Análisis de Brecha Empírica: Evaluación exhaustiva de 18 modelos de última generación (tanto de código abierto como cerrado) que revela una desconexión masiva entre el éxito de la compilación y la corrección semántica.
4. Perspectivas Contextuales: Demostró que proporcionar teoremas sucesores como contexto mejora significativamente la corrección semántica, mientras que proporcionar solo pruebas en lenguaje natural no lo hace.

4. Resultados Experimentales

Los autores evaluaron 18 modelos (incluyendo GPT-5, Claude-Sonnet-4.5, Llama-3.1 y modelos matemáticos especializados como DeepSeek-Prover) en el benchmark T2.

• La Brecha Semántica:

  • Precisión de Compilación: Los modelos lograron altas tasas de compilación (por ejemplo, Claude-Sonnet-4.5: 80.3% en el conjunto completo).
  • Precisión de Pruebas (TA): Los mismos modelos lograron puntuaciones de TA drásticamente más bajas (por ejemplo, Claude-Sonnet-4.5: 38.9% en el conjunto completo; 4.5% en el conjunto Difícil).
  • Falsos Positivos: Hasta un 93.1% de los teoremas compilables resultaron ser semánticamente incorrectos al probarlos contra los sucesores.

• Fallo de las Métricas Existentes:

  • BLEU: Una alta similitud léxica (puntuaciones BLEU) mostró casi ninguna correlación con la corrección semántica (Correlación: 0.123). Los modelos podían generar pruebas textualmente similares pero lógicamente erróneas.
  • Modelos Especializados: Los modelos ajustados específicamente para la demostración de teoremas a menudo lograron tasas de compilación más altas, pero rindieron peor o de manera similar a los modelos de propósito general en TA, lo que sugiere que se sobreajustan a la sintaxis en lugar de a la semántica.

• Impacto del Contexto:

  • Proporcionar Teoremas Sucesores como contexto de entrada mejoró consistentemente la TA (por ejemplo, +4.9% para Claude-Sonnet-4.5).
  • Proporcionar solo Pruebas en LN sin sucesores no mejoró el rendimiento y a veces lo degradó.
  • El aprendizaje con pocos ejemplos (few-shot prompting) y el refinamiento iterativo (usando retroalimentación del compilador) produjeron mejoras insignificantes en el conjunto Difícil, lo que indica que la dificultad radica en el razonamiento semántico profundo, no solo en el formato de la tarea.

5. Significado y Conclusión

Este artículo desafía fundamentalmente el estado actual de la evaluación de la Demostración Automática de Teoremas (ATP).

• Redefinición del Éxito: Demuestra que la "compilación" es una condición necesaria pero insuficiente para la generación de teoremas. Un modelo puede ser sintácticamente perfecto pero semánticamente inútil.
• Confiabilidad: El benchmark T2 y la métrica TA proporcionan una forma rigurosa y automática de evaluar si un LLM comprende verdaderamente conceptos matemáticos o si simplemente está alucinando código sintácticamente válido.
• Dirección Futura: El trabajo sugiere que los futuros sistemas de ATP deben evaluarse en su capacidad para integrarse en bases de código existentes (generación consciente de dependencias) en lugar de resolver acertijos aislados. También destaca que proporcionar el "conjunto de pruebas" (teoremas sucesores) al modelo durante la generación es una estrategia crucial para mejorar la alineación semántica.

En resumen, el artículo argumenta que las pruebas de integración son el eslabón perdido en la evaluación de LLMs para las matemáticas formales, revelando que los modelos actuales de última generación están lejos de lograr una corrección semántica fiable en la demostración de teoremas.