Resumen Técnico: MATHLIBPR – Una Referencia para la Preparación de Revisión de Bibliotecas Matemáticas Formales

1. Definición del Problema

El ecosistema de Lean y Mathlib se ha convertido en el estándar para el razonamiento formal asistido por modelos de lenguaje grandes (LLM), con éxitos recientes en la resolución de problemas de nivel olímpico (MiniF2F), matemáticas de competición (AlphaProof) y proyectos de formalización a gran escala (agente Gauss). Sin embargo, estos sistemas principalmente consumen Mathlib como dependencia en lugar de contribuir a ella. Aunque el código generado por LLM puede ser verificado en cuanto a su corrección por el núcleo de Lean, determinar si una contribución está "lista para fusionar" —es decir, si se adhiere a las convenciones de la comunidad, mantiene la coherencia de la biblioteca y es adecuada para el mantenimiento a largo plazo— requiere una revisión humana.

La revisión humana es actualmente el principal cuello de botella para el crecimiento de Mathlib, con una cola de aproximadamente 300 solicitudes de extracción (PR) y tiempos de espera medianos de dos semanas. La pregunta central abordada por este artículo es: ¿Pueden los LLM ayudar a revisar las PR de Mathlib? Específicamente, ¿pueden distinguir entre código que pasa la compilación y está listo para integración y código que pasa la compilación pero requiere revisión o será rechazado?

2. Metodología

2.1 Construcción del Conjunto de Datos: MATHLIBPR

Los autores introducen MATHLIBPR, una referencia construida a partir de historiales reales de PR de Mathlib4.

• Fuente: PR cerrados del repositorio leanprover-community/mathlib4 (a 5 de abril de 2026).
• Criterios de Selección: La referencia se centra exclusivamente en instantáneas que pasan la compilación. Esto elimina estrategias triviales basadas en errores de sintaxis o fallos de compilación, obligando a los modelos a juzgar basándose en la calidad del código y las convenciones.
• Etiquetas:
  • Listo para Fusionar: Instantáneas aceptadas en la rama master.
  • No Listo para Fusionar: Instantáneas que pasaron las verificaciones de compilación pero que fueron revisadas antes de su aceptación o pertenecieron a PR que nunca se fusionaron.
• Composición: El conjunto de datos final contiene 15.895 instantáneas etiquetadas de 12.063 PR (11.409 listas para fusionar, 4.486 no listas para fusionar). Incluye 3.687 pares dentro de PR (una instantánea anterior que pasa la compilación frente a la versión final aceptada) para probar el reconocimiento del progreso de revisión.

2.2 Protocolo de Evaluación

Los autores proponen un protocolo de evaluación de tres etapas que suministra progresivamente un contexto más rico a los modelos:

• Etapa 1: Evidencia local del código (diff, archivos modificados) y resúmenes compactos de las directrices de Mathlib (nomenclatura, estilo, documentación).
• Etapa 2: Añade diagnósticos estructurados (linting, importaciones, ubicación de declaraciones, ajuste de API) derivados de registros históricos de comprobaciones de GitHub o rellenados localmente.
• Etapa 3: Añade el título y la descripción de la PR como intención declarada.

2.3 Sistemas Evaluados

La referencia evalúa dos clases de sistemas:

1. Modelos LLM: DeepSeek-R1-Distill-Qwen, Qwen3-8B, Goedel-Prover-V2-32B (pre-ajustados finamente en Mathlib) y Kimina-Prover-Distill-8B.
2. Agentes LLM: Codex (GPT-5.4) y Claude Code (Claude Sonnet 4.6). Los agentes operan en una copia local de solo lectura del repositorio, restringidos de editar archivos, acceder a la web o recuperar resultados de PR.

2.4 Esquema de Salida y Métricas

Se requiere que los sistemas generen una revisión estructurada en JSON en lugar de texto libre. El esquema incluye:

• Veredicto: merge_ready, not_merge_ready o uncertain.
• Puntuación: Una puntuación escalar de preparación para fusión ($p_{merge\_ready}$).
• Ejes: Evaluaciones a través de ocho dimensiones de la rúbrica (nomenclatura, documentación, estructura local, ubicación de archivos, importaciones, legibilidad de pruebas, ajuste de API, superposición de repositorio).

Métricas:

• Recuperación MR/NMR: Recuperación para las clases listas para fusionar y no listas para fusionar (tratando uncertain y las salidas inválidas como errores).
• Precisión Equilibrada: Media de la recuperación MR y NMR.
• Tasa de Salida Válida: Porcentaje de salidas válidas según el esquema dentro de los presupuestos de tiempo de ejecución.
• AUROC: Área bajo la curva ROC basada en puntuaciones escalares.

3. Resultados Clave

3.1 Rendimiento General

• Baja Precisión: Ningún sistema distingue de manera fiable las instantáneas listas para fusionar de las no listas para fusionar. El modelo de mejor rendimiento (DeepSeek) logró una Precisión Equilibrada del 36,0% en la Etapa 3, significativamente por debajo de la línea base del 50% de azar para una tarea equilibrada (aunque el conjunto de datos está desequilibrado, las métricas de recuperación destacan el fallo).
• Asimetría de Clases: Los sistemas muestran un fuerte sesgo hacia predecir merge_ready.
  • DeepSeek (Etapa 3): 69,8% de recuperación MR, pero solo 2,3% de recuperación NMR.
  • Qwen (Etapa 3): 48,3% de recuperación MR, 0,0% de recuperación NMR.
  • Codex (Agente): 92,0% de recuperación MR, pero solo 12,0% de recuperación NMR.
• Impacto del Contexto: Añadir diagnósticos e intención de la PR (Etapa 2 y 3) produjo ganancias limitadas y desiguales. Por ejemplo, la precisión equilibrada de DeepSeek mejoró del 18,1% al 36,0%, pero su capacidad para identificar código no listo para fusionar permaneció cerca de cero.

3.2 Rendimiento Agente vs. Modelo

• Agentes: Aunque Codex mostró una alta fiabilidad operativa (99,9% de tasa de salida válida) y alta recuperación MR, falló en identificar código no listo para fusionar. Claude Code tuvo una fiabilidad menor (56,4% de tasa válida) y una recuperación NMR igualmente pobre.
• Modelos Especializados: Goedel y Kimina, a pesar de estar entrenados en pruebas formales, rindieron mal. La tasa de salida válida de Goedel colapsó del 68,3% (Etapa 1) al 13,5% (Etapa 3), y ambos modelos produjeron frecuentemente salidas inválidas (prosa o bloques de código) en lugar del esquema JSON requerido.

3.3 Análisis Dentro de PR

En una comparación controlada de instantáneas anteriores que pasan la compilación frente a instantáneas finales aceptadas de la misma PR:

• Los modelos apenas superan al azar. La precisión por pares de DeepSeek se estabilizó en 51,1% (Etapa 3), y Qwen se mantuvo cerca de 49,1%.
• Esto indica que los modelos no pueden detectar de manera fiable las mejoras específicas que llevaron a la aceptación de una PR, incluso al comparar dos versiones de la misma contribución.

3.4 Análisis de Errores

• Abstención: Los sistemas a menudo se abstienen (uncertain) en los ejes de documentación o legibilidad de pruebas.
• Salidas Inválidas: Una parte significativa de las salidas de modelos especializados (Goedel, Kimina) y agentes (Claude Code) fue inválida debido a violaciones del esquema, tiempos de espera o fallo en la producción de JSON. Esto sugiere una desconexión entre los objetivos de entrenamiento de los modelos (demostración de teoremas) y la interfaz de revisión estructurada.

4. Contribuciones

1. Referencia MATHLIBPR: La primera referencia para evaluar LLMs en la preparación para fusión de contribuciones a Mathlib que pasan la compilación, derivada de historiales reales de PR.
2. Protocolo de Evaluación por Etapas: Un protocolo que prueba sistemáticamente si un contexto más rico (diagnósticos, intención de la PR) mejora el juicio similar al de un revisor.
3. Estudio Empírico: Una evaluación exhaustiva que muestra que los LLM y agentes actuales luchan por distinguir el código listo para fusionar del código que pasa la compilación pero requiere revisión, destacando una brecha entre la corrección del código y la calidad de la integración en la biblioteca.

5. Significado y Afirmaciones

El artículo afirma que MATHLIBPR proporciona un paso hacia asistentes de revisión y modelos de recompensa para bibliotecas matemáticas formales.

• Estado Actual: Los resultados demuestran que juzgar la preparación para fusión es una capacidad sustancialmente más difícil que detectar errores de sintaxis o fallos de compilación. Los sistemas actuales no logran capturar las normas de revisión matizadas requeridas para curar una biblioteca matemática integrada.
• Utilidad Futura: La referencia está destinada a ser utilizada para:
  • Asistencia al Revisor: Triaje y puesta en primer plano de posibles bloqueos para revisores humanos.
  • Modelado de Recompensa: Entrenar modelos de recompensa utilizando la estructura de pares dentro de PR (prefiriendo la instantánea final aceptada sobre una anterior que pasa la compilación) para orientar a los LLM hacia la generación de código que no solo sea correcto, sino también mantenible y listo para fusionar.
• Limitaciones: Los autores reconocen que la referencia cubre un segmento selectivo de la historia de PR y que las etiquetas se derivan de decisiones históricas de los mantenedores, las cuales pueden incluir factores no técnicos. Declaran explícitamente que el objetivo no es reemplazar a los revisores humanos, sino proporcionar una señal de asesoramiento.

En conclusión, aunque los LLM han tenido éxito en generar pruebas correctas, la transición a contribuir a Mathlib requiere un nivel de juicio sobre el estilo del código, la documentación y la adecuación a la biblioteca que los modelos actuales aún no han dominado. MATHLIBPR establece la línea base para medir el progreso en esta dirección.