💬 NLP

APE-Bench: Evaluating Automated Proof Engineering for Formal Math Libraries

Este artículo presenta APE-Bench, el primer marco y banco de pruebas sistemático para evaluar la ingeniería de pruebas automatizada en bibliotecas de matemáticas formales mediante la extracción de tareas del mundo real a escala de repositorio y la provisión de un entorno unificado para validar tanto la compilación sintáctica como la corrección semántica a través de diversas implementaciones de agentes.

Autores originales: Huajian Xin, Luming Li, Xiaoran Jin, Jacques Fleuriot, Wenda Li

Publicado 2026-02-03

📖 5 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Huajian Xin, Luming Li, Xiaoran Jin, Jacques Fleuriot, Wenda Li

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 estás intentando enseñarle a un robot cómo ser un maestro bibliotecario para una enorme y viva biblioteca de pruebas matemáticas. Esta biblioteca, llamada Mathlib, contiene millones de páginas. No es solo un libro estático; se está reescribiendo, expandiendo y corrigiendo constantemente por expertos humanos.

Durante mucho tiempo, los investigadores probaron a los robots en su capacidad para resolver acertijos matemáticos aislados y únicos (como "Demostrar que 2+2=4"). Pero en el mundo real, ser matemático no es solo resolver un acertijo aislado; se trata de ingeniería de pruebas. Esto significa navegar por toda la biblioteca, encontrar las herramientas adecuadas, arreglar páginas rotas y asegurarse de que tus nuevas adiciones encajen perfectamente con los millones de páginas ya existentes sin romper nada más.

Este artículo presenta una nueva forma de probar a los robots en estas habilidades del mundo real. Aquí está el desglose utilizando analogías sencillas:

1. El Proble Problema: El "Acertijo Aislado" frente a la "Biblioteca Viva"

La forma antigua (miniF2F): Imagina probar a un chef dándole una única tarjeta de receta y pidiéndole que cocine un plato. Si el plato sabe bien, aprueba. Esto no te dice si puede gestionar la cocina de todo un restaurante, pedir ingredientes o arreglar un horno roto.
La realidad: El trabajo matemático real es como gestionar ese restaurante. Tienes que coordinarte con otros chefs, usar herramientas específicas y asegurar que tu nuevo plato no arruine el menú.
La brecha: Las pruebas existentes solo comprobaban si el robot podía cocinar ese único plato. No comprobaban si el robot podía lidiar con el caos de una cocina real.

2. La Solución: APE-Bench (La prueba de la "Biblioteca Viva")

Los autores crearon APE-Bench, un nuevo campo de pruebas que imita el mantenimiento de una biblioteca de la vida real.

Cómo funciona: En lugar de darle al robot un acertijo falso, el sistema observa la historia real de la biblioteca Mathlib. Encuentra un momento en el que un experto humano realizó un cambio (un "commit"), oculta ese cambio y le pregunta al robot: "Aquí está la biblioteca antes del cambio. Aquí hay una nota que dice lo que el humano quería hacer. ¿Puedes realizar ese cambio?"
El giro: El robot no solo es calificado por si el código "funciona" (sintaxis). Es calificado por dos cosas:
1. Compilación: ¿Realmente compiló el código sin errores? (¿Se quemó el plato?)
2. Verificación Semántica: ¿Realmente hizo el robot lo que se le pidió? (¿Arregló el problema correcto, o simplemente cambió líneas al azar?)

3. La Infraestructura: APE-Harness (La "Cocina Universal")

Para ejecutar estas pruebas de manera justa, construyeron un sistema llamado APE-Harness. Piensa en esto como un simulador de cocina universal.

El "Contrato": Cada prueba viene con un contrato estricto. Dice: "Estás en esta versión específica de la biblioteca. Solo puedes tocar estos archivos. Debes demostrar que hiciste el trabajo".
Los "Andamios": El sistema está diseñado para que puedas conectar diferentes robots (como Claude Code, Codex o su propio APE-Agent) en la misma cocina. Debido a que las reglas de la cocina (el contrato) son las mismas para todos, puedes comparar justamente quién es realmente el mejor chef, en lugar de solo ver quién tuvo suerte con las instrucciones.
El truco del "Viaje en el Tiempo": La biblioteca tiene 67 versiones diferentes (como 67 ediciones distintas de un libro). Almacenar todas ellas tomaría una cantidad masiva de espacio. Los autores construyeron un ingenioso sistema de "deduplicación". Si una página es igual en la Versión 1 y en la Versión 67, el sistema la almacena una sola vez y simplemente apunta a ella. Esto les ahorró un 85% del espacio de almacenamiento y un 98% del dinero necesario para procesar los datos.

4. Los Resultados: ¿Quién pasó la prueba?

Probaron tres modelos de IA de alto nivel (GPT-5.2, Gemini 3 Pro y Gemini 3 Flash) en este nuevo y más difícil test.

La dificultad: El nuevo test fue mucho más difícil que los antiguos tests de "acertijo único".
- En los tests antiguos, los robots obtenían un 80–90% de aciertos.
- En el nuevo test de "Mantenimiento de Biblioteca", el mejor robot solo obtuvo un 47% de aciertos.
El ganador: Gemini 3 Flash fue el más eficiente. Resolvió la mayoría de los problemas con el menor costo. Los otros modelos intentaron esforzarse más (más turnos de conversación), pero se quedaron sin su "presupuesto" antes de terminar.
La lección: Los robots son excelentes resolviendo problemas matemáticos aislados, pero todavía luchan con la tarea desordenada y compleja de gestionar un código base enorme y en evolución.

5. Por qué esto es importante

El artículo afirma que esta es la primera vez que tenemos una forma sistemática y automatizada de probar si una IA puede realizar "ingeniería de software para pruebas".

Cambia el objetivo de "¿Puede la IA resolver un problema matemático?" a "¿Puede la IA trabajar como un matemático profesional en un entorno de equipo?".
Proporciona un campo de juego justo donde diferentes sistemas de IA pueden ser comparados utilizando exactamente las mismas reglas y herramientas.

En resumen: Los autores construyeron una simulación realista de una biblioteca matemática gigante y desordenada, junto con un conjunto de reglas para probar si la IA puede arreglarla. Descubrieron que, aunque la IA está mejorando, todavía tiene un largo camino por recorrer antes de poder gestionar de forma fiable proyectos matemáticos complejos en el mundo real por sí sola.

Resumen Técnico: APE-Bench: Evaluando la Ingeniería de Pruebas Automatizada para Librerías de Matemáticas Formales

Declaración del Problema

Los benchmarks de evaluación actuales para matemáticas formales basadas en Modelos de Lenguaje de Gran Escala (LLM), como miniF2F y FATE, se centran primordialmente en la demostración de teoremas aislados. Estos benchmarks requieren que los agentes sinteticen un término de prueba para un enunciado formal dado que sea verificable por tipos. Sin embargo, la práctica del desarrollo de matemáticas formales en entornos de producción (por ejemplo, Mathlib) ha evolucionado hacia la ingeniería de pruebas a escala de repositorio. El desarrollo en el mundo real implica coordinación entre múltiples archivos, evolución de la librería, gestión de dependencias entre archivos y mantenimiento ante cambios; tareas que los benchmarks de demostración de teoremas aislados no logran capturar. Las herramientas existentes para el mantenimiento de pruebas (por ejemplo, iCoq, REPLICA) siguen siendo mayoritariamente heurísticas y requieren un esfuerzo manual significativo. Existe una falta de un marco sistemático para evaluar agentes de IA en las actividades de ingeniería de repositorios a escala que caracterizan el desarrollo real de las matemáticas formales.

Metodología

1. Formulación de la Ingeniería de Pruebas Automatizada (APE)

Los autores introducen la Ingeniería de Pruebas Automatizada (APE) como una formulación de tarea que operacionaliza la ingeniería de pruebas a escala de repositorio. Una tarea APE se define por tres componentes:

Entorno Fijado (Pinned Environment): Un commit específico del repositorio y una versión de la cadena de herramientas (toolchain).
Instrucción en Lenguaje Natural: Una descripción del objetivo de ingeniería (por ejemplo, "refactorizar", "añadir automatización").
Verificación Dual:
- Corrección Sintáctica: El código modificado debe compilarse con éxito dentro del entorno fijado.
- Corrección Semántica: La solución debe satisfacer los requisitos de lenguaje natural y mantener el control del alcance (evitando cambios gratuitos), validado mediante un LLM-como-Juez (LLM-as-Judge).

Esta formulación refleja el paradigma SWE-bench para la ingeniería de software, pero lo adapta para las matemáticas formales reemplazando las pruebas unitarias con validación basada en juicios, ya que las tareas de prueba a menudo carecen de suites de pruebas preexistentes.

2. Infraestructura APE-Harness

Para soportar una evaluación sistemática, los autores construyeron la infraestructura de ejecución APE-Harness basada en la Abstracción de Contrato de Tarea.

Contratos de Tarea: Especificaciones declarativas que separan los requisitos de la tarea (objetivos, límites, vínculos de entorno, protocolos de verificación) de las estrategias de ejecución. Esto permite que diferentes andamiajes (scaffolds) de agentes ejecuten la misma tarea bajo las mismas restricciones.
Servicios de Infraestructura:
- Servicios de Ejecución: Compilan el código del agente contra instalaciones de librerías objetivo inmutables.
- Servicios de Recuperación: Permiten la búsqueda semántica acotada a versiones específicas de la librería.
- Aislamiento de Espacio de Trabajo: Impone acceso de solo lectura a las librerías objetivo y acceso de escritura a espacios de trabajo de prueba (scratch workspaces).
Eficiencia Multi-Versión: El sistema utiliza almacenamiento direccionable por contenido (hashing criptográfico) para deduplicar archivos idénticos a través de 67 versiones diferentes de la librería, logrando ahorros de recursos de un orden de magnitud en almacenamiento y costos de incrustación (embedding).

3. Construcción de APE-Bench

APE-Bench es un pipeline automatizado que extrae tareas de ingeniería de pruebas de los historiales de commits reales de Mathlib.

Proceso: Filtra los commits por modificaciones sustantivas a nivel de archivo (5–100 líneas), luego utiliza un agente para sintetizar instrucciones en lenguaje natural a partir de los diffs.
Validación: El pipeline asegura que las tareas sean resolubles y que el parche original satisfaga la instrucción generada bajo la verificación dual.
Dataset: La liberación inicial contiene 100 tareas extraídas de 67 commits (con fecha de 2026-01-01 en adelante) para asegurar la contaminación cero de datos de entrenamiento para los modelos de frontera.

4. Andamiajes de Evaluación (Evaluation Scaffolds)

El marco soporta la intercambiabilidad de andamiajes. Los autores proporcionan APE-Agent (un andamiaje tipo ReAct con verificación integrada) y lo evalúan junto con Claude Code y Codex CLI para demostrar que la infraestructura puede comparar de manera justa diferentes implementaciones de agentes.

Contribuciones Clave

Formulación y Benchmark de APE: La primera infraestructura completa para la evaluación de la ingeniería de pruebas a escala de repositorio, que cuenta con un pipeline automatizado (APE-Bench) que mina tareas de la evolución real de librerías.
Benchmark de Validación por LLM-como-Juez: Un conjunto de datos de 64 soluciones de agentes anotadas por expertos con calificaciones tridimensionales de calidad (corrección semántica, alineación de requisitos y control de alcance) para validar la fiabilidad de los jueces LLM.
APE-Harness: Una infraestructura de ejecución basada en contratos de tarea que permite la evaluación unificada de diversos andamiajes, soporta flujos de trabajo funcionales (como la síntesis de instrucciones) y permite la intercambiabilidad de andamiajes.
APE-Agent: Un andamiaje de caja blanca, tipo ReAct, con herramientas integradas de sistema de archivos y verificación para facilitar la investigación y comparación.
Servicios de Ejecución Multi-Versión: Implementación de servicios eficientes de compilación y recuperación a través de múltiples versiones de librerías utilizando deduplicación de contenido.

Resultados

Rendimiento de los Modelos

Los autores evaluaron modelos de frontera (GPT-5.2, Gemini 3 Pro, Gemini 3 Flash) en APE-Bench, miniF2F y miniCTX utilizando un presupuesto fijo de $3 por tarea.

Dificultad de APE-Bench: La ingeniería a escala de repositorio resultó ser significativamente más difícil que la demostración aislada. En APE-Bench, Gemini 3 Flash logró una tasa de éxito del 47.0%, superando a GPT-5.2 (27.0%) y Gemini 3 Pro (24.0%).
Comparación con la Demostración Aislada: En miniF2F y miniCTX, los modelos alcanzaron tasas de éxito mucho más altas (73–94%), indicando que la dificultad en APE-Bench proviene de la complejidad de la ingeniería (coordinación, control de alcance) más que de la capacidad pura de demostración de teoremas.
Eficiencia: Las brechas de rendimiento fueron impulsadas por la eficiencia de costos. Gemini 3 Flash logró tasas de éxito más altas no por un razonamiento superior por turno, sino por evitar el agotamiento prematuro del presupuesto causado por llamadas a herramientas costosas o prompts verbosos.

Análisis de Andamiaje y Herramientas

Intercambiabilidad de Andamiaje: APE-Agent superó significativamente a Claude Code y Codex CLI (por 15–23 puntos porcentuales) en tareas idénticas.
- Razones: La verificación integrada de APE-Agent (edición atómica + compilación) redujo las llamadas redundantes. En contraste, Claude Code y Codex incurrieron en costos más altos debido a prompts verbosos, llamadas de ejecución separadas y patrones de recuperación conservadores.
Ablación de Herramientas: Eliminar la recuperación, la shell o las operaciones de archivos resultó en caídas de rendimiento solo marginales (rango de 44–47%). Esto sugiere que el cuello de botella principal son las capacidades de razonamiento de los modelos para tareas a escala de repositorio, no la disponibilidad de herramientas específicas.

Fiabilidad del Juez

El pipeline de LLM-como-Juez demostró una alta precisión (90.6% general) frente a las anotaciones de expertos humanos en las dimensiones de corrección semántica, alineación de requisitos y control de alcance, validando su uso para la evaluación automatizada.

Eficiencia de la Infraestructura

La deduplicación de contenido redujo los requisitos de almacenamiento de 67 versiones de la librería de 480GB a 71GB (una reducción del 85%) y redujo los costos de incrustación para los servicios de recuperación en un 98.5% ( $12.9K a$ 197).

Significado

El artículo afirma establecer una base para la evaluación sistemática de agentes de IA en el desarrollo de matemáticas formales a escala de repositorio. Al cambiar el paradigma de evaluación de la demostración de teoremas aislados a la ingeniería de pruebas, APE-Bench aborda la brecha entre las capacidades actuales de la IA y las demandas reales de mantener librerías de matemáticas formales de producción. El trabajo demuestra que:

La ingeniería de pruebas a escala de repositorio es una tarea distinta y significativamente más desafiante que la demostración de teoremas aislados.
La abstracción de contrato de tarea permite una comparación justa y estandarizada de diversos arquitecturas de agentes.
Los modelos de frontera actuales muestran promesa pero enfrentan obstáculos sustanciales en disciplina de ingeniería, control de alcance y eficiencia de costos cuando se aplican al mantenimiento de librerías del mundo real.

Los autores liberan todo el código y el dataset de benchmark como código abierto para facilitar la investigación posterior en este dominio.