Los investigadores proponen Danus, un sistema de orquestación para razonamiento matemático a nivel de investigación que utiliza un grafo de hechos compartido como mecanismo de gestión de memoria global. El sistema coordina un agente principal para la planificación y múltiples agentes trabajadores que realizan búsqueda paralela de pruebas, utilizando un verificador sin estado para verificar afirmaciones antes de que entren en el grafo.
- Danus almacena hechos verificados con sus pruebas y dependencias lógicas para construir argumentos largos de forma incremental mientras mantiene organizado el estado compartido de las pruebas.
- El agente principal resume periódicamente el estado evolutivo de la prueba, redirige a los trabajadores hacia direcciones prometedoras y soporta la interacción con matemáticos humanos a través de informes de progreso.
- La evaluación a través de seis estudios de caso a nivel de investigación en geometría algebraica, teoría de singularidades y combinatoria ilustra cómo el mecanismo del grafo de hechos permite la construcción de pruebas matemáticas largas y detalladas.
Los resultados sugieren que la orquestación basada en grafos de hechos proporciona una ruta efectiva hacia el escalado de agentes de razonamiento matemático para problemas de investigación a largo plazo.