Resumen Técnico: Los "sorries" no son la parte difícil

Planteamiento del problema

La narrativa predominante en la formalización semi-autónoma se centra en la completitud de la prueba: la capacidad de un agente para generar código que un asistente de pruebas (por ejemplo, Lean) acepte como un teorema verificado. Sin embargo, los autores argumentan que un teorema verificado es distinto de una contribución reutilizable a una biblioteca. La matemática moderna depende de bibliotecas interconectadas donde las definiciones deben combinarse, los enunciados de los teoremas deben poseer la generalidad adecuada y las API deben facilitar el razonamiento futuro sin obligar a los usuarios a desplegar las implementaciones.

El problema central identificado es que, si bien los Modelos de Lenguaje de Gran Escala (LLM) son cada vez más capaces de cerrar brechas locales de prueba (eliminar los "sorries"), tienen dificultades con las decisiones de diseño global requeridas para producir formalizaciones de alta calidad y mantenibles. Específicamente, los agentes suelen fallar al elegir definiciones apropiadas, diseñar enunciados de teoremas generalizables o construir API limpias, lo que resulta en un código que pasa el núcleo (kernel) pero falla la revisión de expertos como contribución a una biblioteca.

Metodología

El artículo presenta un estudio de caso detallado de una formalización semi-autónoma del teorema de la vanishing de Grothendieck (Hartshorne, 1977, Cap. III, Teo. 2.7) en Lean 4. El teorema establece que para un espacio topológico noetérico $X$ y un entero $n$ mayor que la dimensión de Krull topológica de $X$, la $n$-ésima cohomología de un haz de grupos abelianos en $X$ se anula.

El estudio sigue un diseño experimental de antes y después:

1. Estado A (Formalización Inicial): Un agente (Claude Code), guiado por un enunciado de teorema suministrado por un humano y un extracto en PDF de la demostración de Hartshorne, generó una formalización que compiló con cero "sorries" (objetivos no probados).
2. Revisión de Expertos: Un experto en Lean/mathlib revisó el Estado A, identificando problemas en las definiciones, la generalidad del teorema, la organización de archivos y el diseño de la API.
3. Estado B (Formalización Refactorizada): Se le encargó al agente abordar la lista de verificación del experto. Esto implicó un "refactor dirigido por la revisión" y una fase posterior de "compresión y pulido" para alinearse con las convenciones de mathlib.
4. Segunda Revisión: El mismo experto revisó el Estado B.

El análisis compara los dos estados a través de cuatro dimensiones: definiciones, enunciados de teoremas, pruebas y estructura de archivos/API. La línea de tiempo del proyecto, el uso de tokens y las interacciones con las herramientas se reconstruyeron a partir de los registros de commits y la telemetría para comprender los patrones de comportamiento del agente.

Hallazgos Clave y Resultados

1. Definiciones: El Principal Punto de Falla

Las definiciones fueron identificadas como el componente más débil y el área donde el agente mostró la menor mejora entre el Estado A y el Estado B.

• Estado A: El agente generó 62 definiciones personalizadas. Solo una (TopCat.closedIncl) fue considerada correcta y reutilizable. El resto fueron "ad hoc", a menudo envolviendo construcciones de la biblioteca estándar con nombres específicos del contexto de la prueba actual (por ejemplo, sheafH_filtered_colimit_h1_sectionsFunctor en lugar de usar sheafSections existentes).
• Consecuencias: Estas definiciones crearon "costes de transporte futuros", obligando a usuarios posteriores a probar equivalencias triviales para usar los objetos. También dificultaron el rendimiento de los tácticos (por ejemplo, simp) al oscurecer la sintaxis subyacente.
• Estado B: El agente no logró mejorar significativamente su capacidad para crear definiciones generales y reutilizables. Continuó creando objetos específicos e innecesarios en lugar de diseñar construcciones generales con especializaciones convenientes.

2. Diseño de API: Mejora Parcial

• Estado A: El agente no construyó una API para la cohomología de haces (Sheaf.H), sino que desplegó repetidamente la definición en archivos posteriores.
• Estado B: El agente creó un archivo de API dedicado, lo que limpió las demostraciones posteriores. Sin embargo, la API en sí era "ruidosa y saturada", conteniendo ~800 líneas y 24 lemas altamente específicos en lugar de una interfaz destilada y basada en principios.
• Contraste: El agente se desempeñó mejor en la API para topologicalKrullDim (una definición más simple), lo que sugiere que puede diseñar buenas API cuando se le presentan tareas específicas y acotadas, pero tiene dificultades con el diseño abierto.

3. Enunciados de Teoremas: Local vs. Global

• Estado A: El agente probó exactamente lo que se necesitaba para la demostración inmediata, utilizando a menudo hipótesis excesivamente específicas (por ejemplo, requiriendo una "presentación inyectiva" cuando una secuencia exacta corta general habría bastado).
• Estado B: El agente logró generalizar los enunciados de los teoremas cuando se le solicitó explícitamente en la lista de verificación de la revisión. Sin embargo, no logró identificar las generalizaciones necesarias por sí mismo. El agente destaca en arreglos sintácticos locales pero carece del juicio global para anticipar necesidades de reutilización futura.

4. Pruebas: Mejora Desigual

• Estado A: Las pruebas contenían "muros de sentencias have", uso frecuente de igualdad definicional y despliegue directo de definiciones.
• Estado B: Las pruebas mejoraron, particularmente en los archivos que utilizaban objetos existentes de mathlib. El agente adoptó sub-lemas con nombre para descomponer pruebas complejas, un patrón reforzado por las restricciones de "latido" (rendimiento).
• Limitación: Las pruebas que dependían de las propias definiciones deficientes del agente (por ejemplo, en los archivos de colimit de filtrado) siguieron siendo difíciles de leer y mantener.

5. Dinámicas del Proceso

• Adaptación a la Retroalimentación: El agente se adaptó bien a la retroalimentación con predicados de completitud nítidos (por ejemplo, "renombra este archivo", "generaliza esta hipótesis"). Tuvo dificultades con la retroalimentación que requería juicio contrafáctico (por ejemplo, "diseña una API que sea útil en el futuro").
• Vías de Escape: Los agentes tendían a declarar tareas como "bloqueadas" o a culpar a la infraestructura (por ejemplo, "brecha de mathlib") al enfrentar decisiones de diseño difíciles. Fue necesario utilizar prompts explícitos que prohibieran estas frases para forzar la descomposición.
• Métricas: "Cerrar sorries" es una métrica insuficiente para la calidad. El proyecto continuó evolucionando significativamente (en términos de líneas de código y estructura) mucho después de que el recuento de sorries llegara a cero.

Significación y Reivindicaciones

El artículo sostiene que la evaluación de la autoformalización debe extenderse más allá de la completitud binaria de la prueba. Los autores afirman:

1. La aceptación del núcleo es incompleta: Un teorema puede ser verificado por el núcleo mientras obliga a los futuros usuarios a pasar por coerciones extrañas, definiciones duplicadas y APIs inmanejables.
2. La Brecha de Reutilización: Existe una división clara entre la capacidad de un agente para cerrar objetivos locales y su capacidad para elegir definiciones y diseñar APIs. Esto último requiere un juicio sobre la reutilización futura del que carecen los LLM actuales.
3. Estándar de Evaluación: Los autores proponen que los sistemas de IA para matemáticas deben ser evaluados por si la formalización resultante sobrevive a la revisión de expertos. Específicamente, tras verificar una prueba, un experto debe revisar las definiciones públicas, los enunciados de los teoremas, los espacios de nombres y las superficies de la API para medir la capacidad del sistema para responder al feedback de diseño.

El estudio concluye que, sin un armazón sofisticado para el diseño global, los LLM son capaces de producir "artefactos verificados" pero aún no "contribuciones reutilizables a una biblioteca". El camino a seguir implica utilizar a expertos humanos para definir las especificaciones de calidad (definiciones, interfaces) y a los agentes para manejar las refactorizaciones estrechas y mecánicamente comprobables.