💻 computer science

MathAtlas: A Benchmark for Autoformalization in the Wild

Este artículo presenta MathAtlas, el primer benchmark de autoformalización a gran escala que comprende aproximadamente 52.000 conceptos matemáticos de nivel de posgrado de 103 libros de texto, lo cual revela la extrema dificultad de los modelos actuales para manejar matemáticas de investigación complejas y ricas en dependencias.

Autores originales: Nilay Patel, Noah Arias, Davit Babayan, Victoria Cochran, Timothy Libman, Hafsah Mahmood, Liam McCarty, Soli Munoz, Laurel Willey, Jeffrey Flanigan

Publicado 2026-05-15

📖 4 min de lectura☕ Lectura para el café

CC BY 4.0

Autores originales: Nilay Patel, Noah Arias, Davit Babayan, Victoria Cochran, Timothy Libman, Hafsah Mahmood, Liam McCarty, Soli Munoz, Laurel Willey, Jeffrey Flanigan

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina que tienes un traductor brillante que puede convertir historias humanas en un lenguaje estricto, legible por computadora, llamado "Lean". Durante mucho tiempo, este traductor solo ha sido probado con historias simples, como problemas de matemáticas de secundaria o acertijos básicos. La computadora podía traducirlos fácilmente porque las reglas eran sencillas y la computadora ya había visto reglas similares antes.

Pero, ¿qué sucede cuando le pides a este traductor que traduzca un artículo de investigación complejo de nivel de posgrado? Ese es el problema que MathAtlas aborda.

Aquí tienes una explicación sencilla de lo que hace el artículo, utilizando algunas analogías cotidianas:

1. El Problema: La "Biblioteca" es Demasiado Grande

Imagina que estás intentando construir una casa (una prueba formal) basándote en un plano (un libro de texto de matemáticas).

Antiguas Pautas de Referencia: Las pruebas anteriores solo pedían al traductor que construyera un pequeño cobertizo. Los materiales estaban todos ahí mismo en la caja de herramientas y las instrucciones eran cortas.
El Mundo Real: Las matemáticas de posgrado son como intentar construir un rascacielos. Para construir el piso superior, necesitas el piso 50. Para construir el piso 50, necesitas el 49, y así sucesivamente, hasta llegar a los cimientos.
El Problema: En matemáticas avanzadas, los "cimientos" (definiciones y teorías) a menudo aún no han sido construidos en el lenguaje de la computadora. Si el traductor no conoce la definición de un "álgebra de Lie" (un concepto complejo), no puede traducir el teorema que la utiliza.

2. La Solución: MathAtlas (El Mapa "Salvaje")

Los autores crearon MathAtlas, un nuevo conjunto de pruebas masivo.

La Escala: Recopilaron 103 libros de texto de matemáticas de nivel de posgrado. Es como tomar una biblioteca de 52.000 páginas de matemáticas avanzadas y convertirla en un mapa digital.
El "Gráfico de Dependencias": Este es el superpoder del artículo. Imagina un libro de "Elige tu propia aventura" donde cada página tiene flechas que apuntan a otras páginas que necesitas leer primero. MathAtlas dibuja estas flechas. Muestra que para entender la Proposición 15, primero necesitas entender los Anillos de Dedekind, que a su vez necesitan los Ideales Primos.
Por qué importa: Obliga a la IA a no solo traducir una oración, sino a averiguar: "¿Tengo las herramientas para construir esto? Si no, ¿puedo encontrar o construir las herramientas primero?".

3. Los Resultados: La IA Está Atascada en el Lodo

Los autores probaron los modelos de IA más inteligentes disponibles en MathAtlas, y los resultados fueron humildes.

La Puntuación: Incluso la mejor IA obtuvo menos del 10% de las declaraciones de teoremas correctas. Para las definiciones, fue alrededor del 16%.
La Trampa de la "Profundidad": Cuanto más profunda es el "árbol de dependencias" (más pasos debes retroceder para encontrar las definiciones), peor se desempeña la IA.
- Analogía: Si la IA tiene que consultar 10 conceptos anteriores para traducir una oración, se confunde y se rinde. En los problemas más difíciles (donde el árbol de dependencias era más profundo), la IA solo obtuvo un 2,6% de aciertos.
El Efecto "Mathlib": La IA se desempeñó ligeramente mejor cuando el concepto que necesitaba traducir ya estaba en una famosa biblioteca llamada "Mathlib" (que es como una caja de herramientas preconstruida que la IA probablemente ha estudiado). Si el concepto era nuevo y no estaba en esa biblioteca, la IA luchó mucho más.

4. La Prueba de "Confianza" (MA-Align)

El artículo también creó una nueva prueba llamada MA-Align.

El Problema: A veces una IA traduce una oración a un código que parece perfecto y se ejecuta sin errores, pero en realidad significa algo completamente diferente al matemático original. Es como traducir "El gato se sentó en la alfombra" a un programa informático que dice "El perro comió la pizza". El programa funciona, pero está mal.
La Prueba: Pidieron a jueces de IA que verificaran si la traducción era "fiable" (fiel al significado). Descubrieron que incluso los mejores jueces de IA a menudo eran engañados, especialmente con definiciones complejas de nivel de posgrado.

La Conclusión

El artículo concluye que, aunque la IA está mejorando en matemáticas simples, actualmente es terrible traduciendo matemáticas complejas y reales de nivel de posgrado. El principal cuello de botella no es solo traducir palabras; es comprender la inmensa red de conexiones entre ideas y saber cómo construir las "herramientas" necesarias (definiciones) antes de construir la "casa" (teoremas).

MathAtlas ahora está abierto para que todos lo utilicen como un curso de desafío para ayudar a la IA a aprender a manejar estas dependencias profundas y complejas.

Resumen Técnico: MathAtlas: Una referencia para la formalización automática en el mundo real

Declaración del Problema

Las referencias actuales de formalización automática se centran principalmente en dominios más simples, como las matemáticas de olimpiadas o de pregrado, donde el material previo es limitado y a menudo ya está formalizado en bibliotecas como Mathlib. Sin embargo, las matemáticas de nivel de posgrado e investigación siguen siendo poco exploradas. En estos dominios avanzados, la formalización automática es significativamente más compleja debido a:

Profundidad de los Prerrequisitos: Las matemáticas avanzadas dependen de una teoría previa extensa, gran parte de la cual aún no ha sido formalizada. Un sistema efectivo debe no solo formalizar la declaración objetivo, sino también recuperar o sintetizar las teorías dependientes necesarias.
Brecha de Definición: Las referencias existentes ignoran en gran medida la formalización de definiciones matemáticas. Los sistemas que solo pueden manejar declaraciones de teoremas están limitados por la teoría formal existente; no pueden formalizar teoremas que involucren conceptos para los cuales no existen definiciones.
Falta de Datos del Mundo Real: Existe una escasez de referencias a gran escala y del mundo real que capturen la complejidad "en el mundo real" de las matemáticas de nivel de posgrado, incluidas las dependencias contextuales ricas y las relaciones entre entidades.

Metodología

Construcción del Conjunto de Datos: MathAtlas

Los autores introducen MathAtlas, la primera referencia a gran escala para formalización automática de matemáticas de nivel de posgrado.

Material de Origen: El conjunto de datos se extrae de 103 libros de texto de matemáticas de nivel de posgrado que cubren 87 campos distintos (por ejemplo, análisis real, geometría diferencial, teoría de categorías, grupos cuánticos).
Escala y Composición: MathAtlas contiene aproximadamente 52,052 entidades, que comprenden:
- ~18,000 teoremas
- ~10,000 ejercicios
- ~10,000 definiciones
- ~10,000 demostraciones
- ~5,000 ejemplos
Grafo de Dependencia: Una característica clave es el enriquecimiento del conjunto de datos con un grafo de dependencia matemática que contiene ~178,000 relaciones. Este grafo vincula entidades a:
- Referencias a Objetos: Conceptos matemáticos nombrados (por ejemplo, "anillo de Dedekind") que requieren definiciones externas.
- Referencias a Entidades: Referencias a otros teoremas o definiciones específicos dentro del texto.
- Referencias a Variables Locales: Símbolos utilizados sin una introducción local explícita.
- Profundidad de Dependencia: La altura máxima del árbol de dependencia de una entidad (profundidad promedio de 30, con un rango de hasta 80), que varía significativamente según el campo (por ejemplo, el álgebra de Lie tiene árboles más profundos que la teoría de conjuntos).

Pipeline de Construcción:

Conversión: Los PDFs se convierten a Markdown Matemático (MMD) utilizando Nougat.
Extracción: Un modelo de lenguaje grande (LLM) con pocas muestras (gpt-oss-120b) extrae entidades (definiciones, teoremas, etc.) y sus identificadores.
Extracción de Referencias: Un segundo modelo identifica referencias a objetos, entidades y variables locales dentro del texto extraído.
Extracción de Relaciones: Un sistema empareja las referencias con entidades objetivo (utilizando LeanSearch para la fundamentación en Mathlib y LLMs para el emparejamiento interno) para construir el grafo de dependencia.
Control de Calidad: La evaluación humana en muestras aleatorias indica un 90.4% de validez para la extracción de entidades y una puntuación F1 del 94.8% para la extracción de relaciones.

Métricas de Evaluación

El artículo evalúa el rendimiento de la formalización automática utilizando una métrica compuesta llamada Correctitud, que requiere que una formalización satisfaga dos condiciones:

Compilación: El código Lean 4 generado debe compilarse con éxito.
Fidelidad Semántica: La declaración formal debe ser semánticamente equivalente a la fuente informal.
- Para medir la fidelidad, los autores introducen MA-Align, una referencia de clasificación binaria de 200 entidades (declaraciones y definiciones) de MathAtlas, anotadas como "alineadas" o "desalineadas".
- Evalúan sistemas existentes de "LLM como juez" (por ejemplo, CriticLean) y descubren que, aunque funcionan bien en referencias anteriores (ConsistencyCheck, CriticLeanBench), su precisión disminuye significativamente en MA-Align, destacando una brecha en la evaluación de definiciones de nivel de posgrado.

Configuración Experimental

Los autores probaron varias líneas base en MathAtlas, incluyendo:

Modelos con Prompts: Prompts de cero y pocas muestras con gpt-oss-20b y gpt-oss-120b.
Modelos Ajustados: Herald, Kimina, ATLAS-L, Goedel y ReForm.
Estudios de Ablación: Prueba del impacto del contexto local (los 500 tokens anteriores), prompts diseñados y ejemplos de entrenamiento específicos.
Subconjunto MA-Hard: Un subconjunto específico de ~700 entidades con los árboles de dependencia más profundos (profundidad promedio >50) para probar los límites de los sistemas actuales.

Resultados Clave

Rendimiento General

MathAtlas resulta ser una referencia extremadamente desafiante. Las líneas base fuertes alcanzan tasas bajas de correctitud:

Declaraciones (Teoremas, Ejemplos, Ejercicios): La mejor línea base (ReForm 8B) alcanza solo un 9.8% de correctitud.
Definiciones: La mejor línea base (gpt-oss-120b con prompts de pocas muestras) alcanza un 16.7% de correctitud.
Disparidad: Existe una brecha significativa entre las tasas de compilación y la correctitud (por ejemplo, Kimina 7B compila el 27.3% de las declaraciones, pero solo el 2.3% son fieles), lo que indica que el éxito sintáctico no garantiza la precisión semántica.

Profundidad de Dependencia y Dificultad

El rendimiento se degrada sustancialmente a medida que aumenta la profundidad de la dependencia:

En MA-Hard (las 700 entidades con los árboles de dependencia más profundos), el mejor modelo alcanza solo un 2.6% de correctitud.
El análisis estadístico (prueba de Kolmogorov–Smirnov) confirma una diferencia significativa en las distribuciones de correctitud entre árboles de dependencia poco profundos y profundos ( $p < 0.001$ ).

Contexto y Fundamentación

Contexto Local: Añadir contexto local (los 500 tokens anteriores) al prompt disminuyó el rendimiento para los modelos con prompts (bajando del 20.3% al 17.4% en definiciones), lo que sugiere que los modelos actuales luchan por integrar el contexto de largo alcance de manera efectiva.
Fundamentación en Mathlib: Las entidades que podían fundamentarse en formalizaciones existentes en Mathlib tenían una probabilidad significativamente mayor de ser formalizadas correctamente (27.9% frente al 16.8% para definiciones no fundamentadas), lo que sugiere que los LLM se benefician de la exposición previa a teorías formalizadas en sus datos de entrenamiento.

Significado y Contribuciones

El artículo afirma el siguiente significado para el campo:

Primera Referencia de Nivel de Posgrado: MathAtlas es la primera referencia a gran escala y "en el mundo real" para matemáticas de nivel de posgrado, superando las restricciones de los conjuntos de datos de olimpiadas y pregrado.
Evaluación Consciente de la Dependencia: Es la primera referencia que incluye grafos de dependencia ricos y relaciones entre entidades, permitiendo la evaluación de sistemas que deben manejar teoría previa y síntesis de definiciones.
Destacar la Brecha de Definición: Los resultados demuestran que los modelos actuales de vanguardia luchan significativamente con definiciones y cadenas de dependencia profundas, revelando un cuello de botella crítico para escalar la formalización automática a las matemáticas avanzadas.
Limitaciones de la Métrica de Fidelidad: La introducción de MA-Align y los experimentos subsiguientes muestran que las métricas existentes de fidelidad semántica (como CriticLean) no se generalizan bien a las definiciones de nivel de posgrado, lo que hace necesarias nuevas aproximaciones de evaluación.
Recurso para la Comunidad: Los autores lanzan MathAtlas, MA-Align y el código experimental para facilitar la investigación futura sobre la formalización automática consciente de la dependencia y la formalización de conceptos matemáticos avanzados.

Los autores concluyen que, aunque los sistemas actuales muestran promesa, la brecha entre las capacidades existentes y los requisitos de las matemáticas de nivel de posgrado sigue siendo vasta, particularmente en lo que respecta a la síntesis de teoría previa y la formalización de definiciones.