FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?

El artículo presenta FormalProofBench, un benchmark privado que evalúa la capacidad de los modelos de IA para generar demostraciones matemáticas de nivel de posgrado formalmente verificadas en Lean 4, revelando que el mejor modelo alcanza un 33,5% de precisión y proporcionando un análisis exhaustivo de sus modos de fallo, costos y latencia.

Lo esencial

Imagina que tienes un grupo de estudiantes de matemáticas muy inteligentes (los modelos de IA) y les pides que resuelvan problemas de nivel universitario o de posgrado. Hasta ahora, para evaluarlos, les pedíamos que escribieran la solución en un cuaderno (lenguaje natural) y un profesor humano la leía para ver si tenía sentido.

El problema de este método es que un estudiante puede escribir una respuesta que suena muy convincente y lógica, pero que tiene un error oculto, como un paso que no existe o un caso que olvidó. El profesor humano podría no darse cuenta.

FormalProofBench es como un nuevo examen, pero con una regla estricta: no vale la pena si no está perfecto.

Aquí te explico cómo funciona, usando analogías sencillas:

1. El Examen: "La Prueba de Fuego"

En lugar de un cuaderno, los estudiantes deben escribir sus soluciones en un lenguaje de programación matemática llamado Lean 4.

• La analogía: Imagina que Lean 4 es un robot juez muy estricto. Si el estudiante escribe una sola coma mal, o si salta un paso lógico, el robot no solo lo corrige, sino que le dice: "No, esto no es una prueba válida".
• La diferencia: En los exámenes normales, si la idea es buena pero la redacción es un poco floja, el profesor te da puntos. En este examen, o el robot acepta tu código (¡Ganaste!) o lo rechaza (¡Perdiste!). No hay "casi".

2. La Herramienta: "El Taller de Reparación"

Los modelos de IA no tienen que escribir la respuesta de un solo golpe. Tienen un "taller" con herramientas:

• El Buscador (Loogle): Es como una biblioteca gigante donde pueden buscar definiciones y teoremas que ya existen.
• El Probador de Código (Lean Run Code): Es como un simulador de vuelo. Pueden probar una parte de su prueba, ver si el robot se queja de un error, y corregirlo antes de entregarla.
• El Turno: Tienen hasta 40 oportunidades (vueltas) para probar, fallar, buscar ayuda y corregir antes de entregar la prueba final.

3. Los Resultados: "Los Atletas de Élite"

Los autores probaron a los modelos de IA más potentes del mundo (como Claude, GPT-5, Gemini, etc.).

• El ganador: El modelo Claude Opus 4.5 fue el mejor, pero solo acertó el 33.5% de los problemas.
• La realidad: Esto suena bajo, pero es como si en una olimpiada de matemáticas de nivel doctoral, incluso el mejor estudiante solo resolviera 1 de cada 3 problemas correctamente. El resto de los modelos cayeron muy rápido en rendimiento.
• El secreto del éxito: Los modelos que ganaron no solo "pensaron" mucho; practicaron mucho. Los que usaron más el "Probador de Código" (ejecutaron más pruebas y vieron más errores) tuvieron más éxito. Los que solo buscaron en la biblioteca sin probar nada, se perdieron.

4. ¿Por qué es importante esto?

Hasta ahora, la IA era muy buena "hablando" de matemáticas, pero a veces alucinaba (inventaba cosas).

• La analogía: Es la diferencia entre un abogado que hace un discurso muy bonito en el tribunal y un abogado que realmente presenta las pruebas físicas que un juez puede verificar.
• El futuro: Si la IA puede pasar este examen, significa que pronto podrá ayudar a los matemáticos reales a descubrir cosas nuevas, asegurándose de que sus descubrimientos son 100% correctos y no solo "suena bien".

En resumen:
FormalProofBench es un examen de matemáticas de nivel avanzado donde la IA debe escribir código que un robot verifique automáticamente. Aunque los modelos actuales son muy inteligentes, todavía tienen dificultades para ser perfectos en matemáticas complejas. Sin embargo, la prueba nos dice que la clave para mejorar no es solo "pensar más", sino probar y corregir constantemente sus ideas.

Resumen técnico

Aquí tienes un resumen técnico detallado del artículo "FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?", presentado en la conferencia ICLR 2026.

1. Problema y Motivación

El avance de los modelos de lenguaje grandes (LLM) en el razonamiento matemático ha sido notable en benchmarks de estilo competitivo (como MATH o AIME). Sin embargo, existe una brecha crítica entre la competencia matemática aparente (soluciones en lenguaje natural) y la competencia verificada.

• Limitación actual: Las soluciones en lenguaje natural pueden ocultar errores lógicos sutiles, omisiones de casos críticos o invocación de lemas inexistentes, errores que incluso revisores expertos pueden pasar por alto.
• Necesidad: Se requiere una metodología de evaluación que elimine la ambigüedad. La verificación formal ofrece una señal binaria y automatizada: una prueba o compila (es correcta) o no lo hace.
• Objetivo: Evaluar si los modelos de IA pueden generar pruebas matemáticas formales de nivel universitario avanzado y de posgrado que sean aceptadas por un verificador de pruebas (kernel de Lean 4), superando el nivel de problemas de olimpiadas.

2. Metodología: FormalProofBench

A. Construcción del Benchmark

• Naturaleza: Es un benchmark privado (para evitar contaminación de datos en el entrenamiento) que consta de 200 problemas.
• Fuentes: Los problemas provienen de exámenes de calificación (qualifying exams) y libros de texto estándar de nivel de posgrado.
• Dominios: Cubre áreas avanzadas como análisis real y funcional, teoría de la medida, álgebra conmutativa, geometría algebraica, teoría de números, probabilidad y lógica.
• Formalización: Cada tarea empareja una declaración de problema en lenguaje natural con su formalización correspondiente en Lean 4 (utilizando la biblioteca Mathlib).
• Control de Calidad:
  • Los problemas fueron formalizados por seis expertos (estudiantes de doctorado y expertos en Lean).
  • Se implementó un proceso de revisión secundaria (code review en GitHub) para detectar "misformalizaciones" (cuando la declaración formal no refleja fielmente la intención del problema informal).

B. Configuración de Evaluación (Agentic Harness)

A diferencia de evaluaciones de un solo paso, el benchmark utiliza un entorno de agente que permite la iteración:

• Entrada: El modelo recibe el problema en lenguaje natural, la declaración formal en Lean, y los encabezados necesarios.
• Herramientas:
  • lean_loogle: Búsqueda de teoremas y definiciones en Mathlib.
  • lean_run_code: Ejecución de código Lean para obtener retroalimentación inmediata (errores de sintaxis, tipos, metas no resueltas).
  • submit_proof: Envío final de la prueba.
• Iteración: Los modelos tienen hasta 40 turnos por problema. En cada turno, pueden realizar múltiples llamadas a herramientas y razonamiento antes de intentar enviar la prueba final.
• Criterio de Éxito: La prueba debe compilarse exitosamente en el kernel de Lean 4 (versión v4.25.2) sin usar axiomas locales o sorry.

3. Contribuciones Clave

1. Nuevo Benchmark Determinista: Presenta un conjunto de datos no contaminado, de nivel realista y de evaluación determinista para medir el rendimiento de modelos de lenguaje en matemáticas formales.
2. Evaluación Exhaustiva: Proporciona una evaluación detallada de modelos de vanguardia (frontier models) en pruebas formales de posgrado utilizando 200 problemas cuidadosamente formalizados.
3. Análisis de Costos y Latencia: Ofrece métricas sobre el costo económico y el tiempo de latencia en un entorno de agente multiturno con acceso a herramientas de búsqueda y ejecución de código.
4. Hallazgos sobre el Uso de Herramientas: Descubre patrones críticos en el uso de herramientas, específicamente la correlación entre la iteración mediante ejecución de código y el éxito.

4. Resultados Principales

Se evaluaron modelos de OpenAI, Anthropic, xAI, Zhipu AI, Google y DeepSeek.

• Rendimiento General: El rendimiento es bajo en comparación con benchmarks informales. El modelo mejor clasificado, Claude Opus 4.5 (Thinking), alcanzó una precisión del 33.5%.
• Caída de Rendimiento: Existe una caída rápida en el rendimiento después del primer lugar; el segundo modelo (Gemini 3 Pro) obtuvo un 18.5%, y los modelos posteriores descendieron rápidamente hasta el 3-4%.
• Análisis de Herramientas:
  • Éxito: Los modelos más fuertes tienden a ejecutar código (lean_run_code) temprano en el proceso para obtener retroalimentación y corregir errores, utilizando la búsqueda (lean_loogle) solo para llenar lagunas específicas.
  • Fallo: Un patrón de fallo común es el "espiral de búsqueda", donde los modelos realizan llamadas repetidas a la herramienta de búsqueda intentando encontrar lemas inexistentes, sin ejecutar código para verificar sus hipótesis.
• Costo y Latencia:
  • El costo por prueba varía de ~$0.10 a más de $1.30.
  • La latencia es significativa: el promedio por prueba supera a menudo la hora (ej. ~4000 segundos para el modelo líder), debido a los múltiples turnos de interacción y ejecución de código.

5. Significado e Implicaciones

• Barrera de Formalización: El estudio revela que, aunque los modelos pueden razonar matemáticamente, la capacidad de traducir ese razonamiento a una sintaxis formal verificable sigue siendo un cuello de botella significativo.
• Herramientas para Matemáticos: El rápido ritmo de mejora sugiere que estamos acercándonos a un umbral donde los sistemas de IA podrían convertirse en herramientas prácticas para matemáticos en activo, permitiendo la exploración rápida de estrategias de prueba con retroalimentación inmediata de corrección.
• Democratización: El éxito en la verificación formal podría democratizar el acceso a métodos formales, que actualmente están restringidos a una pequeña comunidad de expertos en asistentes de prueba.
• Futuro: A medida que los modelos mejoren en benchmarks como FormalProofBench, la verificación formal podría pasar de ser una técnica especializada a un componente estándar en la caja de herramientas de la investigación matemática.

En resumen, FormalProofBench establece un nuevo estándar riguroso para evaluar la capacidad real de la IA en matemáticas avanzadas, demostrando que, aunque el progreso es real, la generación de pruebas formalmente verificadas de nivel de posgrado sigue siendo un desafío formidable para los modelos actuales.