ProofCouncil: An LLM Agent for Solving Open Mathematical Problems

Resumen Técnico: ProofCouncil

Planteamiento del Problema
Los modelos de lenguaje de gran tamaño (LLM) han demostrado una capacidad creciente para resolver problemas matemáticos abiertos, sin embargo, su rendimiento carece a menudo de la rigurosidad y el refinamiento iterativo característicos de la práctica matemática real. El desafío radica en crear agentes autónomos capaces de abordar problemas abiertos —específicamente aquellos que no poseen soluciones públicamente disponibles— dentro de entornos restringidos (por ejemplo, ventanas de 24 horas, presupuestos fijos) utilizando únicamente herramientas públicas. El desafío FirstProof, un benchmark compuesto por 10 de estos problemas no resueltos, sirve como el principal terreno de evaluación para este trabajo. Además, los autores buscaron evaluar el rendimiento en un conjunto más amplio de 30 problemas abiertos recolectados directamente de investigadores matemáticos.

Metodología: Arquitectura de ProofCouncil
Los autores introducen ProofCouncil, un sistema agéntico diseñado en torno a una arquitectura de autor-crítico para simular el proceso iterativo de la investigación matemática. El sistema opera a través de los siguientes componentes:

1. Agente Autor: Responsable de generar y revisar una demostración. Utiliza GPT-5.5-Pro (xhigh) con acceso a ejecución de código y búsqueda web. El autor mantiene tres archivos canónicos:

   • answer.tex: El documento de demostración principal en LaTeX.
   • research notes.tex: Un cuaderno de notas persistente para ideas, intentos fallidos y resultados parciales.
   • references.bib: Un archivo BibTeX para citas.
     El autor actualiza iterativamente estos archivos basándose en la retroalimentación y puede emitir etiquetas XML estructuradas para solicitar ayuda auxiliar.

2. Agente Crítico: También utilizando GPT-5.5-Pro (xhigh), el crítico evalúa la corrección de la demostración actual, identificando brechas, errores o justificaciones faltantes.

   • Con estado vs. Fresco: El crítico es típicamente con estado (stateful), reteniendo el historial de la conversación para proporcionar retroalimentación consistente. Sin embargo, para reducir la dependencia de la trayectoria, el historial del crítico se reinicia cada $k$ rondas (donde $k=3$ en los experimentos).
   • Protocolo de Verificación: Si un crítico con estado acepta una demostración, un crítico "fresco" (inicializado con una nueva conversación) realiza una auditoría independiente. Una solución solo se devuelve si tanto el autor la marca como lista como preparada como el crítico fresco la acepta.

3. Componentes Auxiliares:

   • Consejo de LLM (LLM Council): Un grupo opcional de modelos independientes (Gemini 3.1 Pro, Claude Opus 4.7, GPT-5.5-Pro) que proporcionan retroalimentación específica sobre sub-preguntas concretas cuando el autor lo solicita.
   • Nodo de Cómputo: Un agente especializado (Codex con GPT-5.5) con acceso a Sistemas de Álgebra Computacional (CAS) como SageMath, GAP, Singular y Pari. Maneja computación pesada, recuperación de literatura y verificación independiente de afirmaciones.

4. Biblioteca Subyacente (Agentes como DAGs):
   ProofCouncil está construido sobre una biblioteca de código abierto que representa sistemas agénticos como grafos acíclicos dirigidos (DAG) condicionales.

   • Estructura: Los nodos representan llamadas a LLM, bloques de Python, agentes de CLI o puertas de flujo de control. Las aristas codifican las dependencias.
   • Condicionalidad: Las aristas pueden tener condiciones, permitiendo que la ejecución de los nodos descendentes dependa de salidas intermedias (por ejemplo, llamar al Consejo solo si el autor emite una etiqueta específica).
   • Desenrollado de Bucles (Loop Unrolling): Aunque el flujo de trabajo contiene bucles de retroalimentación, la biblioteca los representa como bloques de repetición acotados, desenrollándolos efectivamente en un DAG condicional finito para su ejecución.
   • Humano en el Bucle (Human-in-the-Loop): La biblioteca permite insertar nodos humanos en el DAG, permitiendo a los investigadores revisar demostraciones intermedias o responder preguntas durante la ejecución.

Contribuciones Clave

1. Sistema ProofCouncil: Un agente matemático diseñado para resolver problemas abiertos complejos mediante un bucle de autor-crítico con soporte auxiliar.
2. Biblioteca de Código Abierto: Una biblioteca para construir sistemas agénticos como DAGs condicionales, proporcionando una interfaz flexible para definir flujos de trabajo, prompts y lógica de ejecución.
3. Evaluación Empírica: Una evaluación exhaustiva del sistema tanto en el desafío FirstProof como en un conjunto de datos personalizado de problemas proporcionados por investigadores.

Resultados

• Desafío FirstProof:

  • ProofCouncil fue enviado a la segunda tanda del desafío FirstProof (10 problemas).
  • Rendimiento: Las propuestas para 6 de 10 problemas (P1, P2, P3, P5, P7, P9) fueron juzgadas por los revisores como correctas hasta un máximo de revisiones menores. Esto representó el mejor rendimiento entre los equipos participantes.
  • Costo: La ejecución incurrió en aproximadamente $350 por problema (un total de $3,186 para 9 problemas analizados), significativamente mayor que una línea base de una sola consulta ($12/problema), pero logrando una tasa de resolución más alta (6/9 frente a 4/9).
  • Modos de Fallo: Un problema (P6) falló debido a tiempos de espera de la API. P4 y P8 fueron rechazados; P8 falló debido a una afirmación técnica no soportada, y P4 fue rechazado por otras razones.

• Problemas Proporcionados por Investigadores:

  • El sistema fue probado en 30 problemas abiertos recolectados de investigadores matemáticos (más 3 problemas públicos de Erdős).
  • Retroalimentación: Entre 21 revisiones humanas recibidas:
    • 5 fueron juzgadas como soluciones completas y correctas.
    • 2 fueron consideradas prometedoras pendientes de verificación final.
    • 8 contenían progreso parcial útil.
    • 4 no contenían errores pero ofrecían poco progreso sustantivo.
    • 2 fueron juzgadas como la resolución de versiones más fáciles de los problemas planteados (malinterpretación).
  • Observación Notable: Ningún experto reportó que un resultado que afirmaba resolver un problema fuera matemáticamente falso. El principal modo de fallo identificado fue la interpretación del problema, donde el agente resolvió una versión diferente y más fácil del mismo.
  • Costo: Aproximadamente $213 por intento de problema.

• Utilidad de los Componentes:

  • El Nodo de Cómputo fue más útil para verificar afirmaciones concretas y encontrar contraejemplos.
  • El Consejo de LLM proporcionó perspectivas diversas, siendo GPT-5.5-Pro el contribuyente más decisivo.
  • El Crítico fue crucial para evitar que se aceptaran soluciones incorrectas, aunque ocasionalmente sufrió de falsos positivos (aceptar soluciones incorrectas) o falsos negativos (rechazar soluciones correctas).

Significado y Limitaciones
El artículo afirma que ProofCouncil demuestra el potencial de los flujos de trabajo agénticos para mejorar el rendimiento de los LLM en problemas matemáticos abiertos, logrando resultados de vanguardia en el desafío FirstProof. La publicación de la biblioteca subyacente basada en DAG tiene como objetivo facilitar la investigación futura en la construcción de sistemas agénticos complejos.

Sin embargo, los autores son modestos sobre las capacidades actuales del sistema:

• Costo: El sistema es costoso, impulsado por llamadas repetidas a modelos de frontera y agentes auxiliares.
• Interpretación: El sistema tiene dificultades con enunciados de problemas ambiguos, resolviendo a menudo interpretaciones más fáciles sin detección.
• Legibilidad: Las demostraciones generadas son densas y optimizadas para la corrección más que para la legibilidad humana, requiriendo a menudo una expansión para no expertos.
• Evaluación: Los resultados dependen en gran medida del juicio humano en lugar de la verificación formal, y la evaluación en problemas de investigadores involucró un desarrollo adaptativo (ajuste de prompts basado en ejecuciones anteriores) en lugar de una configuración congelada.

El trabajo concluye que, si bien ProofCouncil representa un paso significativo hacia adelante en el razonamiento matemático autónomo, los desafíos en la eficiencia de costos, la interpretación de problemas y el pulido de los resultados siguen siendo áreas abiertas para la investigación futura.