Resumen Técnico: Fallos en nuestros Benchmarks Formales

Planteamiento del Problema

Si bien los Modelos de Lenguaje de Gran Escala (LLM) han avanzado en la demostración automática de teoremas en Lean, la fiabilidad de los benchmarks utilizados para evaluarlos está comprometida. Una intuición común sugiere que los benchmarks de Lean son "autoverificables" porque el núcleo (kernel) de Lean certifica cada artefacto de prueba; sin embargo, este artículo argumenta que el kernel solo certifica que una prueba establece una declaración formal dada; no verifica que la declaración formal codifique fielmente el problema informal pretendido, ni que el entorno de evaluación sea robusto ante soluciones triviales o adversarias.

Consecuentemente, las puntuaciones de los benchmarks pueden ser engañosas debido a:

1. Errores de Especificación: La declaración formal omite hipótesis o restricciones necesarias, haciendo que los problemas sean más fáciles o vacuamente verdaderos.
2. Errores de Formalización: La traducción del lenguaje natural a Lean representa erróneamente el problema (por ejemplo, dominios incorrectos, cuantificadores incorrectos).
3. Vacíos de Evaluación (Loopholes): Fallos en el entorno de evaluación permiten que los modelos "aprueben" sin demostrar una capacidad genuina (por ejemplo, explotando sorry, tácticas inseguras o errores del kernel).
4. Degradación por Mantenimiento: La rápida evolución de Lean y sus librerías (mathlib) causa una deriva de versiones, haciendo que los conjuntos de datos dejen de ser compilables o sufran desplazamientos semánticos con el tiempo.

Metodología

Los autores realizaron una auditoría a escala de corpus de cinco benchmarks de demostración de teoremas en Lean ampliamente utilizados y sus derivados: miniF2F, ProofNet, FormalMath, CombiBench y ProverBench (cubriendo aproximadamente 10,000 variantes de problemas).

La metodología involucró tres componentes principales:

1. Desarrollo de la Taxonomía de Fallos: Los autores categorizaron los defectos según dónde entran en el pipeline del benchmark: Problemas de Fidelidad (durante la formalización), Vacíos de Evaluación (durante la comprobación/reporte de pruebas) y Problemas de Mantenimiento (errores de origen y deriva de versiones).
2. Verificadores Estáticos Automatizados: Implementaron 12 metaprogramas de Lean 4 para detectar peligros mecánicos. Estos verificadores utilizan la prueba de guardia semántica (mediante tácticas como omega, assumption y simp) para identificar problemas tales como:
   • Contraejemplos (valores concretos que refutan el teorema).
   • Teoremas vacuos (hipótesis insatisfechas).
   • Axiomas no válidos o uso de sorry en las pruebas.
   • Peligros aritméticos específicos de Lean (división por cero, sustracción de naturales truncada, violaciones de dominio analítico).
3. Auditoría Semántica Asistida por LLM: Reconociendo que el análisis estático no puede detectar desajustes semánticos (por ejemplo, hipótesis faltantes que están implícitas matemáticamente pero no presentes sintácticamente), los autores evaluaron LLMs en un conjunto de desafíos etiquetado de 92 problemas. Utilizaron prompting de pocos disparos (few-shot) para clasificar errores en seis categorías (por ejemplo, errores de especificación, desajustes de dominio, errores de formalización).

Resultados Clave

La auditoría reveló 4,833 hallazgos en los conjuntos de datos, de los cuales 398 portaban un certificado de no demostrabilidad o vacuidad comprobable por máquina.

• Distribución de Defectos:
  • FormalMath: 3,250 hallazgos (dominados por división por cero y problemas de sustracción de naturales).
  • ProverBench: 370 hallazgos (alta tasa de uso de axiomas y contraejemplos).
  • Variantes de miniF2F: 135–193 hallazgos por variante, resaltando problemas de formalización incompleta y proliferación de versiones.
  • ProofNet: 67–82 hallazgos, a menudo relacionados con la falta de especificación.
• Verificación por LLM: Los verificadores estáticos produjeron falsos positivos cuando las guardias estaban embebidas en definiciones de tipos o estructuras. El filtrado por LLM (usando modelos como Gemini 3.0 Flash y GPT-5.2) redujo los hallazgos en un ~35% en ProverBench preservando todos los verdaderos positivos confirmados, logrando un ~83% de precisión.
• Rendimiento de la Auditoría Semántica: Los LLMs lograron una alta recuperación (recall) (0.80–0.91) pero baja precisión (0.20–0.30) al detectar errores semánticos. Fueron significativamente mejores detectando errores de especificación explícitos (F1 ~0.51) que errores de formalización profunda (F1 ~0.18), los cuales requieren comprensión de la intención matemática.
• Impacto en las Puntuaciones: Los autores demostraron que los defectos tienen efectos bidireccionales en las puntuaciones reportadas de los probadores:
  • Deflación: Las declaraciones no demostrables o falsas (debido a errores de origen) añaden elementos imposibles al denominador, bajando artificialmente las puntuaciones.
  • Inflación: Las formalizaciones debilitadas (falta de hipótesis) hacen que los problemas sean más fáciles, inflando artificialmente las puntuaciones.
  • Ejemplo: Corregir 20 problemas defectuosos en un subconjunto permitió que DeepSeek-Prover-V2-7B resolviera 3/20 y Kimina-Prover-8B resolviera 2/20, mientras que en los enunciados originales defectuosos resolvieron 0/20. Por el contrario, reparar los enunciados debilitados en ProofNet redujo las tasas de éxito de los probadores probados.

Principales Contribuciones

1. Auditoría Exhaustiva: Una auditoría sistemática y a gran escala de los cinco principales benchmarks de Lean, revelando que los defectos son sistemáticos y no anecdóticos.
2. Taxonomía de Fallos: Una clasificación estructurada de los defectos de los benchmarks en categorías de Fidelidad, Evaluación y Mantenimiento, aclarando que se requieren diferentes intervenciones para cada uno (por ejemplo, análisis estático para peligros de codificación vs. revisión humana para la intención semántica).
3. Suite de Herramientas:
   • Verificadores Estáticos: Una suite de 12 verificadores automatizados implementados como metaprogramas de Lean 4.
   • Prompts de Auditoría: Un conjunto de prompts orientados a la recuperación (recall) para LLMs con el fin de asistir en la auditoría semántica.
   • Instantáneas Corregidas: Lanzamiento de variantes de conjuntos de datos corregidos y resultados de la auditoría.
4. Estándares de Lanzamiento: Propuestas para la creación de benchmarks confiables, incluyendo:
   • Usar proof wanted en lugar de sorry para evitar que sorry actúe como un axioma.
   • Deshabilitar autoImplicit para forzar declaraciones de tipo explícitas.
   • Prohibir axiomas en los archivos de problemas.
   • Fijar (pinning) las versiones de Lean/mathlib para evitar la deriva.

Significancia y Reivindicaciones

El artículo sostiene que, si bien el kernel de Lean proporciona certeza matemática sobre la relación entre una prueba y una declaración formal, no garantiza la validez del benchmark en sí mismo. Los autores argumentan que el estado actual de la evaluación formal sufre de un "vacío de confianza" donde la fidelidad de la especificación y la robustez de la evaluación suelen pasarse por alto.

La significancia de este trabajo radica en:

• Reproducibilidad: Resaltar que la proliferación de versiones y los forks no documentados hacen que las comparaciones entre trabajos sean poco fiables.
• Integridad de la Evaluación: Demostrar que las puntuaciones reportadas en la demostración automática de teoremas son a menudo artefactos de los defectos de los datasets en lugar de una capacidad genuina del modelo.
• Remediación Accionable: Proporcionar un kit de herramientas práctico (verificadores, prompts, estándares) para ayudar a los creadores de benchmarks a identificar y corregir defectos antes del lanzamiento, mejorando así la calidad de los datos de entrenamiento y la confiabilidad de los resultados de evaluación.

Los autores se mantienen modestos, reconociendo que su auditoría no es una enumeración completa verificada por humanos de todos los defectos y que algunos problemas requieren un profundo conocimiento matemático o de Lean para resolverse. Sin embargo, afirman que su taxonomía y herramientas son suficientes para prevenir fallos de alto impacto y guiar la gestión futura de los datasets.