SorryDB: Can AI Provers Complete Real-World Lean Theorems?

El artículo presenta SorryDB, un benchmark dinámico de tareas Lean extraídas de proyectos reales de GitHub para evaluar y alinear las herramientas de demostración automática con las necesidades de la comunidad, revelando que los enfoques actuales (modelos de lenguaje, agentes y demostradores simbólicos) son complementarios en lugar de uno ser estrictamente superior a los demás.

Lo esencial

Imagina que el mundo de las matemáticas es como una inmensa biblioteca en construcción. Los matemáticos son los arquitectos que están diseñando los planos de edificios increíbles (teoremas), pero a veces se atascan. En lugar de dejar el edificio a medias, dejan una nota que dice: "Aquí falta poner el ladrillo, lo haré más tarde". En el lenguaje de los ordenadores (específicamente en un programa llamado Lean), esa nota se llama sorry (que significa "lo siento" o "disculpa").

Hasta ahora, para probar si una Inteligencia Artificial (IA) era buena matemática, le dábamos exámenes de olimpiadas: problemas de lógica pura, tipo "resuelve este acertijo". Pero eso es como entrenar a un mecánico solo con rompecabezas de coches de juguete. Cuando llega un coche real, con piezas oxidadas y manuales confusos, el mecánico de juguete falla.

Aquí es donde entra SorryDB.

¿Qué es SorryDB?

SorryDB es como un termómetro en tiempo real de la construcción matemática real. En lugar de usar exámenes antiguos y resueltos, los autores de este paper crearon un sistema que vigila 78 proyectos de matemáticas reales que están activos en internet (en GitHub).

Cada vez que un matemático deja una nota de "lo siento" (sorry) en un proyecto real, SorryDB la captura. Es un banco de datos vivo y cambiante.

• La analogía: Imagina que en lugar de entrenar a un robot para que resuelva crucigramas de periódico, le pones a trabajar en una obra de construcción real, donde tiene que arreglar los huecos que dejaron los albañiles humanos. Si el robot puede poner el ladrillo correcto, significa que realmente entiende cómo se construye la casa.

¿Por qué es importante?

Los exámenes antiguos (como los de olimpiadas) están "saturados". Las IAs ya los han memorizado. Es como si un estudiante de matemáticas se hubiera aprendido de memoria las respuestas del examen final; saca un 10, pero no sabe matemáticas.

SorryDB evita esto porque:

1. Es nuevo: Los problemas son de proyectos que están ocurriendo ahora. Nadie tiene las respuestas guardadas.
2. Es real: Los problemas tienen "suciedad": dependen de otras partes del código, tienen nombres extraños y requieren entender el contexto, no solo la lógica pura.
3. Es dinámico: A medida que las IAs se vuelven mejores y resuelven los huecos, los matemáticos dejan huecos más difíciles. El examen se vuelve más difícil automáticamente, como un videojuego que sube de nivel contigo.

¿Qué descubrieron al probar las IAs?

Los autores probaron varias "fuerzas" de IA para ver quién podía rellenar esos huecos (sorry) en los proyectos reales.

1. Los "Héroes Solitarios" (Modelos Generales): IAs muy potentes como Gemini o Claude.

   • Resultado: Son buenas, pero si las dejas trabajar solas una sola vez, a veces fallan. Es como un genio que intenta resolver un problema de una sola vez sin consultar sus notas.

2. Los "Detectives" (IAs Agentes): IAs que pueden buscar en la biblioteca de matemáticas (llamada Mathlib) y probar varias veces.

   • Resultado: Son mucho mejores. La clave no es ser el más inteligente de una sola vez, sino ser persistente. Si fallan, miran el error, buscan una pista nueva y lo intentan de nuevo.
   • Analogía: Es la diferencia entre un estudiante que estudia de memoria y uno que, si no sabe una respuesta, busca en el libro, consulta a un compañero y vuelve a intentarlo hasta acertar.

3. La Sorpresa: Las IAs especializadas (entrenadas solo para matemáticas) no ganaron a las generales. De hecho, a veces fallaron porque estaban "entrenadas para olimpiadas" y no sabían cómo manejar la "suciedad" de un proyecto real.

La lección principal

El paper concluye que ninguna IA es perfecta por sí sola.

• Unas son buenas en problemas de lógica pura.
• Otras son buenas buscando información en libros.
• Otras son buenas corrigiendo sus propios errores.

La verdadera magia ocurre cuando las combinamos. Es como un equipo de fútbol: necesitas un portero, un delantero y un mediocampista. Si usas solo a un delantero, no ganarás el partido.

En resumen

SorryDB nos dice que para que la Inteligencia Artificial ayude realmente a los matemáticos, no debemos entrenarla con acertijos de papel, sino ponerla a trabajar en los proyectos reales donde la gente está construyendo el futuro de las matemáticas. Y lo más importante: la IA no necesita ser un genio infalible, necesita ser un colaborador persistente que sepa pedir ayuda, buscar en la biblioteca y no rendirse ante el primer error.

Es el paso de tener un "robot que sabe resolver exámenes" a tener un "asistente que sabe trabajar en equipo".

Resumen técnico

Resumen Técnico: SORRYDB

1. El Problema

El campo de la demostración automática de teoremas (ATP) ha avanzado significativamente, pero su evaluación actual adolece de limitaciones críticas:

• Saturación de Benchmarks: Los conjuntos de datos existentes (como miniF2F, PutnamBench) se basan en problemas de matemáticas competitivas (olimpiadas). Estos conjuntos están saturados, lo que dificulta medir el progreso real y permite que los modelos memoricen soluciones en lugar de razonar.
• Desalineación con la Realidad: Los problemas de competición a menudo carecen del contexto complejo, las dependencias de bibliotecas y la "suciedad" inherente a los proyectos de formalización reales. No reflejan el trabajo diario de un matemático que formaliza resultados de vanguardia.
• Fuga de Datos (Contamination): Al ser públicos y estáticos, es difícil distinguir si un modelo ha memorizado la solución o ha desarrollado habilidades de razonamiento general, especialmente con el auge de sistemas agénticos que utilizan LLMs estándar.
• Necesidad de Contexto: La formalización real requiere entender el contexto local del proyecto y las definiciones específicas, algo que los benchmarks fuera de contexto no evalúan adecuadamente.

2. Metodología: La Creación de SORRYDB

Los autores proponen SorryDB, un nuevo benchmark dinámico y en evolución, diseñado para evaluar la utilidad práctica de los demostradores de teoremas.

• Fuente de Datos: Se extraen obligaciones de prueba (placeholders sorry) de 78 proyectos activos de formalización en Lean alojados en GitHub. Un proyecto se considera "activo" si ha tenido al menos un commit en los últimos tres meses.
• Proceso de Extracción:
  1. Selección de Repositorios: Se filtran repositorios del registro de paquetes Reservoir de Lean, asegurando licencias abiertas y mantenimiento activo.
  2. Extracción de sorry: Se identifican todas las instancias de la palabra clave sorry (que marca teoremas no probados o pasos intermedios pendientes).
  3. Filtrado y Validación: Se eliminan duplicados y se asegura que el proyecto se pueda compilar. Se seleccionan solo aquellos sorry que requieren una prueba (tipo Prop), descartando definiciones simples.
  4. Actualización Continua: A diferencia de los benchmarks estáticos, SorryDB se actualiza dinámicamente. A medida que la comunidad resuelve los sorry, estos desaparecen del conjunto de pruebas y surgen nuevos desafíos más difíciles, evitando la saturación.
• Tarea de Evaluación: El objetivo es "rellenar el sorry" (fill-in-the-sorry). El modelo debe proporcionar el código que reemplace el placeholder para completar la prueba específica, manteniendo el contexto del archivo y el proyecto.
• Pipeline de Verificación: Se utiliza un mecanismo automatizado que clona el repositorio, reemplaza el sorry con la solución propuesta y verifica que el proyecto se compile correctamente sin errores y sin términos sorry residuales en ese estado.

3. Contribuciones Clave

1. El Dataset SorryDB: Un conjunto de datos dinámico extraído de proyectos reales, alineado con las necesidades de la comunidad de formalización y libre de contaminación por soluciones preexistentes en la mayoría de los casos (ya que son tareas pendientes).
2. Marco de Evaluación Automatizado: Un pipeline robusto que valida la corrección de las soluciones mediante compilación real en el entorno del proyecto, sin necesidad de etiquetas manuales.
3. Evaluación Exhaustiva: Se presenta una línea base evaluando una instantánea estática de 1000 tareas (corte en enero de 2026) contra una variedad de enfoques:
   • Tácticas deterministas (ej. grind, linarith).
   • Modelos de lenguaje generales (GPT-5.2, Claude Opus 4.5, Gemini Flash 3, Qwen 3).
   • Modelos especializados en demostración (Kimina Prover, Goedel Prover).
   • Enfoques iterativos y agénticos (con autocomprobación y búsqueda de herramientas).

4. Resultados Principales

La evaluación sobre la muestra de 1000 tareas revela hallazgos cruciales:

• Complementariedad de los Modelos: No existe un único modelo que resuelva todos los problemas. Los demostradores son complementarios; un modelo puede fallar en una tarea donde otro tiene éxito. La tasa de éxito combinada (cualquier modelo resolviendo la tarea) alcanza un 35.7%, mucho mayor que la de cualquier modelo individual.
• Superioridad de los Enfoques Iterativos y Agénticos:
  • Los enfoques de "un solo intento" (pass@1 o pass@32) tienen un rendimiento modesto (ej. ~10-20% para los mejores LLMs).
  • Los enfoques con retroalimentación iterativa (autocomprobación o agentes) superan drásticamente a los métodos de un solo paso. Por ejemplo, Gemini Flash 3 (Agente) alcanza un 30.3% de éxito, y Claude Opus 4.5 (Autocomprobación) llega al 27.1%.
  • Esto demuestra que el acceso al entorno de compilación y la capacidad de corregir errores basados en mensajes de error son más valiosos que simplemente aumentar el presupuesto de razonamiento o el tamaño del modelo.
• Dificultad por Categoría:
  • Los repositorios pedagógicos son los más fáciles de resolver.
  • Los proyectos de formalización (teoremas de vanguardia) son los más difíciles.
  • Los modelos especializados (como Goedel Prover) funcionan bien en benchmarks de competición pero tienen dificultades para generalizar a proyectos de formalización complejos, posiblemente debido a la desincronización de versiones de Lean o a su entrenamiento enfocado en matemáticas competitivas.
• Fracasos Comunes:
  • Sobre-dependencia de herramientas: Algunos agentes fallan al buscar lemas inexistentes en la biblioteca en lugar de construir la prueba desde cero.
  • Falta de contexto: Los modelos a menudo no entienden las definiciones locales del proyecto y fallan al intentar aplicar lemas de bibliotecas externas que no son relevantes.

5. Significado e Impacto

• Cambio de Paradigma en la Evaluación: SorryDB marca un paso away de las matemáticas competitivas hacia la utilidad práctica. Evalúa si un sistema de IA puede contribuir realmente a proyectos matemáticos en desarrollo, no solo si puede resolver acertijos aislados.
• Herramienta para el Progreso Sostenible: Al ser un benchmark en movimiento, SorryDB evita la saturación. A medida que los modelos mejoran, el conjunto de tareas se vuelve más difícil (los sorry fáciles se resuelven y desaparecen), proporcionando una métrica robusta para medir el avance real en la demostración automática.
• Insights para el Desarrollo de Agentes: El estudio confirma que para la demostración de teoremas en entornos reales, la arquitectura de agentes con retroalimentación de compilación es superior a los modelos estáticos. La capacidad de iterar sobre errores de compilación es el factor dominante en el rendimiento.
• Comunidad y Colaboración: Al basarse en proyectos de código abierto reales, el dataset fomenta el desarrollo de herramientas que son directamente útiles para matemáticos e ingenieros de software que utilizan Lean, cerrando la brecha entre la investigación en IA y la aplicación práctica.

En conclusión, el artículo establece que, aunque los modelos actuales no son perfectos, los enfoques agénticos iterativos son prometedores para la formalización real, y SorryDB proporciona la infraestructura necesaria para guiar el desarrollo futuro de asistentes de demostración más capaces y útiles.