Resumen:Presentamos FormalProofBench, un punto de referencia privado diseñado para evaluar si los modelos de IA pueden producir pruebas matemáticas formalmente verificadas a nivel de posgrado. Cada tarea combina un problema de lenguaje natural con una declaración formal de Lean~4, y un modelo debe generar una prueba de Lean aceptada por el verificador de Lean 4. FormalProofBench está dirigido a matemáticas avanzadas de pregrado y posgrado, con problemas extraídos de exámenes de calificación y libros de texto estándar sobre temas que incluyen análisis, álgebra, probabilidad y lógica. Evaluamos una variedad de modelos de frontera con un arnés agente y descubrimos que el modelo básico con mejor rendimiento logra una precisión del 33,5 %, y el rendimiento cae rápidamente después de eso. Además de las cifras de precisión, también proporcionamos análisis empíricos del uso de herramientas, modos de falla, costo y latencia, brindando así una evaluación exhaustiva de las capacidades de demostración de teoremas formales de los modelos de frontera.
Publicado originalmente en export.arxiv.org el 30 de marzo de 2026.
Ver fuente original
