Lean-GAP: A Dataset of Formalized Graduate Algebra Problems

Resumen Técnico de LEAN-GAP: Un Conjunto de Datos de Problemas de Álgebra de Posgrado Formalizados

Planteamiento del Problema
A pesar de los avances significativos en el razonamiento automatizado y los modelos de lenguaje de gran tamaño (LLMs), persiste una brecha sustancial entre el conocimiento matemático informal y sus contrapartes formales en asistentes de pruebas como Lean 4. Si bien esfuerzos recientes han logrado formalizar problemas de estilo de competición o teoremas altamente especializados, existe una escasez de conjuntos de datos representativos y estructurados que cubran material estándar de nivel de posgrado. Esta falta de datos curriculares fundacionales obstaculiza el desarrollo de sistemas de razonamiento automatizado, ya que a menudo se entrenan con "problemas desafiantes" sin el desarrollo conceptual sistemático que se encuentra en los libros de texto estándar. Además, aunque la autoformalización ha progresado, verificar que un enunciado formal generado capture fielmente el significado pretendido de un enunciado informal sigue siendo un cuello de botella crítico y no resuelto.

Metodología
Los autores presentan LEAN-GAP (Lean-Graduate Algebra Problems), un conjunto de datos derivado de 430 ejercicios formalizados del libro de texto Abstract Algebra de Dummit y Foote. El proyecto emplea un flujo de trabajo escalable de tres etapas:

1. Preprocesamiento de PDF-a-LATEX: Las páginas escaneadas en PDF del libro de texto se renderizan como imágenes, se recortan para eliminar elementos extraños y se procesan mediante la API Mathpix Convert para generar transcripciones iniciales de LATEX de los enunciados de los ejercicios.
2. Autoformalización de LATEX-a-Lean: Un enfoque basado en prompts utilizando varios LLMs traduce los enunciados de LATEX en código Lean 4. Los prompts imponen convenciones de nomenclatura consistentes (por ejemplo, DF_{sec}_{subsec}_{exercise_num}), compatibilidad con Mathlib e inclusión de marcadores de posición sorry para las demostraciones. Los autores evaluaron seis sistemas: cinco modelos de un solo paso (GPT-5, Gemma4-31B, Goedel-Formalizer-V2-32B, Qwen3.6-35B-A3B, DeepSeek-R1-Distill-Qwen-32B) y un bucle de agente iterativo (Codex).
3. Verificación de la Correspondencia Informal–Formal: Reconociendo que la compilación exitosa no garantiza la corrección semántica, los autores implementaron un riguroso flujo de trabajo de verificación con intervención humana (human-in-the-loop).
   • Fase de Contribuidor: Un contribuidor reescribe el ejercicio como un enunciado de teorema autónomo, lo formaliza en Lean y envía un Pull Request (PR).
   • Chequeo Automatizado: GitHub CI verifica que el código Lean se elabore contra una revisión fija de Mathlib.
   • Revisión de Mantenedor: Un mantenedor independiente realiza una revisión semántica, asegurando que la declaración de Lean capture el contenido matemático del enunciado informal.
   • Corrección Asistida por IA: Se utilizan herramientas como Claude Opus 4.7 y Aristotle como "segundos lectores" para detectar errores semánticos sutiles, como cuantificadores invertidos o restricciones faltantes (por ejemplo, $n \ge 2$) que los revisores humanos podrían pasar por alto inicialmente.

Contribuciones Clave

1. El Conjunto de Datos LEAN-GAP: Un corpus estructurado de 430 ejercicios de álgebra de posgrado formalizados, organizados por tema y dificultad, que cubren teoría de grupos, teoría de anillos, teoría de cuerpos y teoría de Galois.
2. Pipeline de Formalización Sistemática: Una metodología reproducible para convertir ejercicios de libros de texto en enunciados formales, destacando la necesidad de la supervisión humana en la etapa de verificación.
3. Análisis de los Desafíos de Formalización: Un examen detallado de los cuellos de botella recurrentes, incluyendo:
   • Argumentos geométricos: Los ejercicios que involucran construcciones con regla y compás son difíciles de formalizar debido a la falta de una infraestructura geométrica robusta en Mathlib.
   • Formalización con respuestas embebidas: Los problemas que requieren la enumeración de soluciones plantean desafíos para distinguir entre verificar una respuesta dada y descubrirla.
   • Definiciones faltantes: Los ejercicios que requieren conceptos aún no presentes en Mathlib (por ejemplo, grupos de Frobenius específicos) requieren definiciones personalizadas que deben construirse cuidadosamente para coincidir con la intención del libro de texto.
   • Ambigüedades sutiles: Los enunciados informales a menudo contienen restricciones implícitas (por ejemplo, $n \ge 2$) que, si se omiten, hacen que el enunciado formal sea falso en la lógica de Lean (por ejemplo, debido al comportamiento de la resta de números naturales).

Resultos
Los autores evaluaron el rendimiento de diferentes modelos de autoformalización sobre el conjunto completo de 1,966 ejercicios:

• Éxito de Elaboración: Codex (un bucle de agente iterativo) logró la tasa de éxito más alta con un 95.5%, superando significativamente a los modelos de un solo paso. GPT-5 lideró los modelos de un solo paso con un 44.1% de los ejercicios totalmente elaborados.
• Fidelidad Semántica: Aunque el éxito sintáctico (elaboración) es necesario, no es suficiente. Un juez semántico basado en LLM (Claude Opus 4.7) evaluó la fidelidad de los enunciados. GPT-5 alcanzó una puntuación media de 3.45/5, con un 45.1% de las salidas consideradas "fieles". En contraste, DeepSeek-R1 obtuvo una puntuación significativamente menor (1.15/5), fallando a menudo al emitir declaraciones o produciendo enunciados vacuos.
• Complementariedad de Modelos: Los modelos exhibieron un alto grado de desacuerdo; solo 7 ejercicios fueron resueltos por todos los sistemas, mientras que 654 fueron resueltos por exactamente uno. Esto subraya el valor de ejecutar modelos en paralelo.
• Necesidad de Verificación Humana: La etapa de verificación resultó ser la más laboriosa. Incluso con altas tasas de elaboración, muchos enunciados contenían errores semánticos (por ejemplo, nombres de grupos incorrectos, cuantificadores invertidos) que requirieron la intervención de expertos humanos para resolverse.

Significado
El artículo postula que LEAN-GAP aborda una brecha crítica en los datos de entrenamiento para sistemas de IA, yendo más allá de los benchmarks de competición hacia un currículo estándar de posgrado. El trabajo demuestra que, si bien los LLMs pueden automatizar la traducción inicial de texto matemático, aún no pueden servir como autoformalizadores de extremo a extremo para material estándar debido a persistentes brechas semánticas. Los autores argumentan que el futuro de la formalización reside en la colaboración productiva humano-IA, donde la IA actúa como un "segundo lector" para identificar errores sutiles e hipótesis no declaradas, mientras que los matemáticos humanos proporcionan la supervisión necesaria para la fidelidad semántica. Este enfoque ofrece una plantilla para escalar la formalización de materiales de formación matemática estándar, sirviendo potencialmente como base para el desarrollo de "estudiantes de matemáticas de IA" capaces de dominar currículos estándar.