Resumen Técnico: Danus – Orquestación de Agentes de Razonamiento Matemático con Memoria de Grafo de Hechos

Planteamiento del Problema

Los recientes agentes basados en Grandes Modelos de Lenguaje (LLM) han demostrado la capacidad de abordar problemas matemáticos de nivel de investigación, resolviendo en ocasiones cuestiones abiertas. Sin embargo, escalar estos sistemas para manejar tareas de investigación de largo horizonte sigue siendo un desafío significativo. Los sistemas multi-agente existentes suelen depender de un bucle de "generar–verificar–revisar" con roles especializados, pero tienen dificultades para coordinar búsquedas de pruebas en paralelo de manera efectiva. Cuando múltiples agentes intentan contribuir a una única prueba sin una gestión de memoria robusta, los contextos compartidos pueden confundirse, y los artefactos intermedios irrelevantes o erróneos pueden propagarse, degradando el rendimiento. El problema central es cómo orquestar un enjambre de agentes para construir colaborativamente pruebas matemáticas largas, detalladas y correctas, manteniendo un estado de verdad fiable.

Metodología

El artículo propone Danus, un sistema de orquestación diseñado para escalar el razonamiento matemático a través de un Grafo de Hechos compartido que sirve como mecanismo global de gestión de memoria. La arquitectura del sistema impone una estricta separación de poderes entre tres tipos distintos de agentes:

1. El Agente Principal:

   • Rol: Realiza la planificación global, la coordinación y la interacción estratégica con matemáticos humanos. No realiza derivaciones detalladas.
   • Función: Interpreta el problema, consulta modelos de estrategia de alto nivel (por ejemplo, GPT-5.5-pro) cuando es necesario, descompone el problema y asigna direcciones a los agentes trabajadores.
   • Gestión de Estado: Lee periódicamente el Grafo de Hechos y los registros de memoria global para resumir el estado actual de la prueba, identificar callejones sin salida y reasignar trabajadores a direcciones prometedoras. Actúa como la interfaz para la guía humana.

2. Agentes Trabajadores (Enjambre):

   • Rol: Llevan a cabo la búsqueda de pruebas detalladas en paralelo.
   • Función: Basándose en los agentes de generación de Rethlas, los trabajadores exploran el problema desde múltiples ángulos (constructivos y refutacionales) simultáneamente. Cada trabajador se enfoca en afirmaciones específicas (lemas, contraejemplos, ejemplos de juguete) en lugar de en la prueba completa.
   • Interacción: Los trabajadores proponen enunciados con pruebas de apoyo al verificador. Recuperan hechos relevantes del Grafo de Hechos para respaldar su afirmación actual, pero no editan el grafo directamente.

3. El Verificador Sin Estado:

   • Rol: Es la única autoridad sobre la corrección.
   • Función: Un servicio sin estado que comprueba las afirmaciones matemáticas propuestas antes de que sean admitidas en el Grafo de Hechos. Lee el Grafo de Hechos para verificar dependencias y referencias citadas.
   • Fiabilidad: Diseñado para producir esencialmente cero falsos positivos; rechaza pruebas con pasos omitidos o referencias erróneas.

El Grafo de Hechos (Innovación Central)

El Grafo de Hechos es un Grafo Acíclico Dirigido (DAG) que sirve como la única fuente de verdad del sistema.

• Estructura: Los nodos representan hechos verificados (un enunciado matemático + una prueba verificada por el verificador). Las aristas representan dependencias lógicas (es decir, el Hecho B depende del Hecho A).
• Ventajas sobre los Planos Únicos: A diferencia de los sistemas anteriores que utilizaban un único archivo Markdown (que obliga a todos los trabajadores a cargar con todo el contexto acumulado), el Grafo de Hechos permite a los trabajadores recuperar solo los hechos específicos relevantes para su tarea actual. Esto mantiene la ventana de contexto pequeña y enfocada, reduciendo las alucinaciones y la interferencia.
• Paralelismo: Múltiples trabajadores pueden contribuir al grafo simultáneamente sin conflictos de bloqueo de archivos.
• Revocación: Si un hecho resulta ser incorrecto posteriormente (por ejemplo, debido a una referencia defectuosa), este y todos los hechos que dependen de él son eliminados del grafo, asegurando la integridad de la estructura restante.

Arquitectura de Memoria

• Grafo de Hechos: Almacena solo verdades verificadas.
• Memoria Global: Un contexto compartido para el Agente Principal y los trabajadores que contiene productos intermedios (planes, callejones sin salida, direcciones prometedoras) y registros de consultas con modelos externos.
• Memoria Local: Registros privados para cada trabajador individual para rastrear su propio historial de razonamiento.

Flujo de Trabajo

1. Inicialización: Un humano proporciona un problema. El Agente Principal formula un plan y asigna tareas al enjambre de trabajadores.
2. Búsqueda en Paralelo: Los trabajadores generan afirmaciones y pruebas, enviándolas al Verificador. Los hechos verificados se añaden al Grafo de Hechos.
3. Orquestación: El Agente Principal resume periódicamente el estado, consulta modelos externos para la estrategia y redirige a los trabajadores basándose en el progreso o el estancamiento.
4. Terminación: El bucle continúa hasta que el teorema objetivo (o su refutación) aparece como un hecho verificado en el grafo.
5. Síntesis: El Agente Principal convierte el Grafo de Hechos en un manuscrito con estilo de artículo académico. Este borrador se somete a una fase final de verificación para corregir errores introducidos durante la compresión de los hechos en prosa lineal.

Contribuciones Clave

1. Orquestación mediante Grafo de Hechos: Introduce un mecanismo de memoria basado en DAG que permite una búsqueda de pruebas paralela y escalable al desacoplar el contexto del trabajador del estado global de la prueba, evitando la "inflación de contexto" e interferencia observadas en los enfoques de archivo único.
2. Separación de Poderes: Establece una arquitectura rigurosa donde la planificación, la ejecución y la verificación están estrictamente separadas, evitando que el orquestador introduzca matemáticas no verificadas.
3. Diseño con Humano en el Bucle (Human-in-the-Loop): Facilita la interacción donde los humanos proporcionan guía de alto nivel y revisión final, mientras el sistema se encarga del trabajo pesado de búsqueda, descomposición y síntesis.
4. Pipeline de Verificación Robusto: Demuestra un sistema donde un verificador sin estado asegura que el Grafo de Hechos siga siendo una fuente de verdad fiable, permitiendo la acumulación segura de largas cadenas de dependencia (hasta 54 niveles de profundidad en experimentos).

Resultados

El sistema fue evaluado en seis casos de estudio de nivel de investigación en geometría algebraica, teoría de singularidades y combinatoria. En todos los casos, una interfaz web de GPT-5.5-pro base no pudo producir resultados significativos.

• Optimal Bend-and-Break para Foliaciones: Danus sintetizó técnicas de diferentes referencias para demostrar que la constante óptima es $r+1$. Identificó de forma independiente referencias insatisfactorias y buscó mejores.
• Conjetura del Índice Global de Shokurov (3D): Danus descompuso autónomamente el problema en cinco clases y descubrió una solución de tipo Lie para tres de ellas. Solo requirió una pista de alto nivel (programa de modelo mínimo foliado) para resolver las dos restantes.
• Índices de Cartier Totales en Familias: Danus unió la geometría algebraica, el álgebra conmutativa y la geometría algebraica real para demostrar la acotación. Corrigió una hipótesis mal leída de una fuente en PDF tras la intervención humana.
• Asintótica de Números Matryoshka: Danus resolvió este problema combinatorio de forma totalmente autónoma, desde el enunciado del problema hasta el manuscrito terminado, con cero guía matemática humana.
• Homogeneidad Ponderada vía Campos Vectoriales Logarítmicos: Danus produjo una prueba a través de una ruta no anticipada por expertos humanos. Cuando los humanos identificaron una referencia defectuosa, Danus logró revocar los hechos dependientes y reconstruir la prueba.
• Clases Tangentes de Matroides: En una comparación controlada contra su predecesor (Rethlas), Danus resolvió un problema complejo que Rethlas no pudo resolver en tres intentos. El Grafo de Hechos permitió al sistema gestionar 3,157 hechos verificados y cadenas de dependencia de hasta 54 niveles, mientras que Rethlas confundió conceptos matemáticos distintos.

Significado y Reivindicaciones

El artículo afirma que la orquestación basada en grafos de hechos proporciona una ruta efectiva para escalar los agentes de razonamiento matemático para problemas de investigación de largo horizonte.

• Escalabilidad: El sistema escala con éxito el cómputo en tiempo de ejecución tanto en anchura (exploración paralela de muchas direcciones) como en profundidad (acumulación de largas cadenas de razonamiento verificado).
• Fiabilidad: El estricto protocolo de verificación asegura que el Grafo de Hechos siga siendo una fuente de verdad confiable, permitiendo la construcción de pruebas demasiado largas y complejas para una sola pasada de un modelo.
• Colaboración: Danus demuestra que los agentes de IA pueden contribuir sustancialmente a la construcción de pruebas, manejando la descomposición, la síntesis y la reparación de errores, mientras que los matemáticos humanos siguen siendo esenciales para la selección de problemas, el suministro de ideas de alto nivel faltantes y la revisión experta final.
• Limitaciones: Los autores señalan modestamente que el sistema aún requiere intervención humana para los saltos conceptuales más difíciles y que la generación del manuscrito final, aunque verificada, puede seguir requiriendo ajustes humanos para las convenciones de notación y citación. El sistema no crea ideas matemáticas ex nihilo, sino que destaca encontrando caminos hacia las soluciones cuando estas existen.

El artículo concluye que Danus representa un paso hacia sistemas de investigación matemática colaborativa donde los agentes de IA se integran con el juicio humano para resolver problemas de investigación abiertos.