🤖 AI

Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement

Goedel-Architect es un marco de agentes para la demostración de teoremas en Lean 4 que utiliza una estrategia de generación y refinamiento de planos para lograr un rendimiento de vanguardia en evaluaciones matemáticas desafiantes como MiniF2F, Putnam e IMO con costos significativamente menores que los pipelines existentes.

Autores originales: Jui-Hui Chung, Ziyang Cai, Zihao Li, Qishuo Yin, Rohit Agarwal, Simon Park, Rodrigo Porto, Narutatsu Ri, Ziran Yang, Shange Tang, Xingyu Dang, Hongzhou Lin, Mengdi Wang, Danqi Chen, Chi Jin, Liam H Fo

Publicado 2026-06-05

📖 5 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Jui-Hui Chung, Ziyang Cai, Zihao Li, Qishuo Yin, Rohit Agarwal, Simon Park, Rodrigo Porto, Narutatsu Ri, Ziran Yang, Shange Tang, Xingyu Dang, Hongzhou Lin, Mengdi Wang, Danqi Chen, Chi Jin, Liam H Fowl, Sanjeev Arora

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 construir un castillo enorme e intrincado con piezas de LEGO. Tienes un plano, pero no es un dibujo; es una lista de instrucciones que dice: "Para construir la torre, primero necesitas un cimiento, luego una pared, luego una ventana".

El problema es que, si intentas construir toda la torre de un solo salto gigante, podrías quedarte atascado, o podrías darte cuenta a mitad de camino de que el cimiento se construyó mal.

Goedel-Architect es un nuevo equipo de robots inteligentes diseñado para construir estos "castillos" matemáticos (pruebas formales) en un lenguaje llamado Lean 4. En lugar de intentar construir todo el castillo de una sola vez, utiliza una estrategia llamada Generación y Refinamiento de Planos.

Así es como funciona, desglosado en pasos sencillos:

1. El Plano (El Plan Maestro)

Antes de que el robot comience a construir, dibuja un Plano.

¿Qué es? Piensa en esto como un mapa de dependencias. Enumera cada uno de los pequeños pasos (llamados "lema") necesarios para probar el gran problema matemático.
Cómo funciona: Dibuja flechas que muestran qué pasos dependen de otros. Por ejemplo: "No puedes construir el techo hasta que las paredes estén terminadas".
El giro: A veces, si el problema matemático es muy difícil, se le da al robot una Prueba en Lenguaje Natural. Esto es como si un matemático humano le diera al robot un boceto aproximado o una historia sobre cómo resolverlo. El robot utiliza esta historia para dibujar un plano mejor y más preciso desde el principio.

2. El Equipo de Construcción (Pruebas en Paralelo)

Una vez que el plano está listo, el robot no construye un paso a la vez. Envía a todo un equipo de constructores especializados (un "probador de Lean") para trabajar en todos los pequeños pasos al mismo tiempo.

Cada constructor solo observa su paso específico y los pasos que tiene permitido utilizar (sus "dependencias").
Intentan construir su parte. Si tienen éxito, convierten esa parte del plano en Verde.
Si fallan, la convierten en Azul (atascado) o Roja (roto).

3. El Bucle de Reparación (Refinamiento)

Aquí es donde Goedel-Architect es diferente de otros robots.

La forma antigua: Muchos otros sistemas de IA intentan resolver un problema, se quedan atascados y luego intentan romper esa única pieza atascada en partes más pequeñas una y otra vez. Esto es como intentar arreglar una pared rota simplemente martillando con más fuerza en el mismo lugar. A menudo conduce a un callejón sin salida.
El método Goedel: Si un constructor se queda atascado, todo el equipo se detiene y observa el plano completo.
- Diagnóstico: El robot pregunta: "¿Por qué falló esto?".
  - Caso A (Rojo): "¡Ah, este paso es en realidad falso!" (El plano tenía una idea errónea). El robot corrige la afirmación.
  - Caso B (Azul): "Este paso es verdadero, pero es demasiado difícil de construir en este momento". El robot divide este paso grande en dos o tres pasos auxiliares más pequeños y fáciles.
- Revisión: El robot reescribe el plano con estos nuevos pasos más pequeños y envía al equipo de nuevo.
- Eficiencia: Crucialmente, cualquier parte del castillo que ya se haya construido con éxito (Verde) permanece Verde. El robot no desecha el buen trabajo; simplemente arregla las partes rotas y añade nuevos pasos auxiliares.

¿Por qué es esto importante?

El artículo afirma que este enfoque es un "cambio de juego" por dos razones principales:

Es increíblemente inteligente y preciso:
- En una prueba estándar de problemas matemáticos de secundaria (MiniF2F), resolvió el 99.2% de ellos. Con un poco de ayuda de una historia de lenguaje natural, resolvió el 100%.
- En matemáticas de nivel universitario más difíciles (PutnamBench), resolvió el 75.6% por su cuenta, y el 88.8% con un poco de ayuda.
- Incluso resolvió problemas de competiciones muy recientes y difíciles (como IMO 2025 e IMO 2025) que ningún otro robot de código abierto había resuelto antes.
Es increíblemente barato:
- Otros robots de primer nivel que resuelven estos problemas suelen utilizar modelos de "caja negra" que cuestan miles de dólares de ejecutar.
- Goedel-Architect utiliza un cerebro de código abierto más económico (DeepSeek-V4-Flash).
- El Costo: Para resolver la prueba completa de PutnamBench, Goedel-Architect costó aproximadamente $294. El siguiente mejor competidor de código abierto costó alrededor de $163,000. Es un ahorro de 500 veces.

La Conclusión

Goedel-Architect es como un maestro arquitecto que no se limita a intentar clavar un clavo; dibuja un mapa, envía a un equipo para construir en paralelo y, cuando algo se rompe, vuelve a dibujar todo el mapa para corregir la lógica, manteniendo las partes buenas y cambiando solo lo necesario. Demuestra que no necesitas la IA más cara y secreta para resolver los problemas matemáticos más difíciles; solo necesitas una forma más inteligente de organizar el trabajo.

Resumen Técnico: Goedel-Architect

Planteamiento del Problema

El artículo aborda el desafío de la demostración formal de teoremas en Lean 4, con el objetivo específico de cerrar la brecha entre los sistemas propietarios de alto rendimiento y las canalizaciones (pipelines) de código abierto accesibles. Mientras que los sistemas de IA de vanguardia han demostrado capacidades matemáticas significativas (por ejemplo, medallas de oro en la IMO, resolviendo problemas abiertos de Erdős), la verificación de estas demostraciones requiere una formalización rigurosa. Las soluciones existentes de pesos abiertos suelen tener dificultades con benchmarks difíciles como PutnamBench (puntuando <15%), mientras que los sistemas de alto rendimiento dependen de modelos no lanzados o de costosas API propietarias (que cuestan miles de dólares por cada ejecución de benchmark). La dificultad central radica en descomponer eficientemente teoremas complejos en lemas demostrables sin quedar atrapado en callejones sin salida recursivos o incurrir en costos computacionales prohibitivos.

Metodología

Goedel-Architect es un marco agéntico centrado en la generación y el refinamiento de planos (blueprints). A diferencia de los enfoques que dependen de la descomposición recursiva descendente o de la generación de demostraciones de un solo paso, este sistema opera sobre un grafo de dependencias global.

1. Generación del Plano (Blueprint Generation)

El proceso comienza con la generación de un plano, definido como un grafo de dependencias de definiciones y lemas formulados formalmente que construyen progresivamente hacia el teorema objetivo.

Estructura: El teorema objetivo es el sumidero único del grafo. Cada nodo representa una definición o lema, y las aristas representan las dependencias declaradas (es decir, qué lemas tiene permitido utilizar una demostración).
Entrada: La declaración formal del teorema siempre inicia la generación. Opcionalmente, para problemas difíciles, una demostración en lenguaje natural (generada por un modelo más fuerte o proporcionada como solución) puede actuar como una guía estructural.
Validación: El generador itera contra el compilador de Lean para asegurar que el archivo emitido se parsee, que todos los nodos estén bien tipados y que el grafo sea acíclico y conectado.

2. Demostración de Teoremas en Paralelo

Una vez generado el plano inicial ( $G_0$ ), el sistema distribuye cada nodo de lema a un demostrador de Lean equipado con herramientas en paralelo.

Contexto: El demostrador de un lema específico ve solo el lema mismo y sus dependencias declaradas (disponibles como hechos), no el grafo completo.
Herramientas: El demostrador utiliza el compilador de Lean para la comprobación de tipos y un servicio de recuperación de Mathlib para la búsqueda de lemas.
Diagnóstico: Si un lema falla, el demostrador devuelve un diagnóstico estructurado. Este incluye:
- Negación: Si el demostrador encuentra un contraejemplo, registra una demostración de la sentencia negada.
- Análisis de Brechas (Gap Analysis): Si el lema no ha sido demostrado pero se cree verdadero, el demostrador identifica dónde se rompe la cadena de la demostración.

3. Refinamiento del Plano

Si algún lema permanece sin demostrar, un modelo de refinamiento reescribe el plano global ( $G_{k+1}$ ) basándose en las señales de fallo.

Estrategias: El refinamiento incluye la descomposición de lemas difíciles en lemas auxiliares, el reajuste de dependencias para otorgar acceso a resultados necesarios, o la alteración/eliminación de sentencias que el demostrador ha probado como falsas.
Preservación: Los lemas demostrados con éxito de la iteración anterior se preservan (nodos verdes) con su firma intacta, asegurando que el esfuerzo computacional no se descarte.
Iteración: El plano revisado se vuelve a demostrar en paralelo. Este bucle continúa hasta que todos los nodos se resuelven o se agota el presupuesto de iteración.

Contribuciones Clave

Arquitectura Centrada en el Plano: El artículo introduce un enfoque de grafo de dependencias global que contrasta con la descomposición recursiva. Esto permite que los intentos de demostración en paralelo compartan contexto y permite que el refinamiento actúe sobre toda la estrategia simultáneamente en lugar de hacerlo localmente.
Estado del Arte de Pesos Abiertos: El sistema logra un rendimiento de vanguardia utilizando el modelo de pesos abiertos DeepSeek-V4-Flash (284B-A13B) como base, evitando la necesidad de modelos no lanzados o de fronteras propietarias.
Eficiencia de Costos: La canalización es significativamente más rentable que los sistemas comparables de alto rendimiento. El artículo reporta un costo por problema de ~$0.44, lo que es hasta 500 veces menos que otras canalizaciones de código abierto y órdenes de magnitud más barato que las alternativas propietarias.
Semilla de Lenguaje Natural: El marco demuestra que las demostraciones opcionales en lenguaje natural pueden servir como andamios estructurales efectivos para el plano inicial, particularmente para problemas con estructuras no locales (por ejemplo, sumas cíclicas, cadenas de divisibilidad), ayudando a anclar la estrategia para el bucle de refinamiento.

Resultados Experimentales

El sistema fue evaluado en cinco benchmarks: MiniF2F-test, PutnamBench, IMO 2025, Putnam 2025 y USAMO 2026.

MiniF2F-test: Logró un 99.2% pass@1 (242/244 problemas) sin guía de lenguaje natural. Con la semilla de lenguaje natural opcional, resolvió todos los 244 problemas (100%), estableciendo un nuevo récord para sistemas de pesos abiertos.
PutnamBench: Logró un 75.6% pass@1 (508/672 problemas), superando a la canalización de Hilbert (70.0% en pass@1840) y a AxProverBase (54.7% en pass@1). Con la guía de lenguaje natural (pass@4), la tasa de resolución aumentó al 88.8% (597/672).
IMO 2025: Resolvió 4/6 problemas.
Putnam 2025: Resolvió 11/12 problemas.
USAMO 2026: Resolvió 3/6 problemas (un benchmark libre de contaminación, ya que los problemas son posteriores a las fechas de corte de entrenamiento del modelo).

Análisis de Costos: En PutnamBench, Goedel-Architect resolvió el conjunto completo de 672 problemas por $294 en costos de API. En contraste, la siguiente mejor canalización abierta (Hilbert) reportó haber gastado entre ~ $163k y ~$ 170k para una sola ejecución, resaltando una brecha de eficiencia masiva.

Significado y Reivindicaciones

Los autores afirman que Goedel-Architect establece una nueva frontera de Pareto para la demostración formal de teoremas. Demuestra que se puede lograr un rendimiento de alto nivel (rivalizando con sistemas propietarios masivos como AlphaProof o sistemas que utilizan Claude Opus 4.5) con un modelo de base altamente eficiente de pesos abiertos y un diseño de canalización novedoso.

El artículo enfatiza que la combinación del grafo de dependencia global (que permite el refinamiento holístico) y el modelo de pesos abiertos (DeepSeek-V4-Flash) es el motor clave de este éxito. El sistema cierra efectivamente la brecha entre la accesibilidad académica y el rendimiento de vanguardia, haciendo que la demostración formal de alto nivel sea factible a una fracción del costo anterior. Los autores señalan que, si bien la guía de lenguaje natural aumenta significamente el rendimiento en los problemas más difíciles, el núcleo de la canalización sigue siendo robusto y efectivo sin ella en los benchmarks estándar.