Les chercheurs proposent Danus, un système d'orchestration pour le raisonnement mathématique de niveau recherche qui utilise un graphe de faits partagé comme mécanisme de gestion de la mémoire globale. Le système coordonne un agent principal pour la planification et plusieurs agents ouvriers effectuant une recherche de preuve parallèle, en utilisant un vérificateur sans état pour vérifier les affirmations avant qu'elles n'entrent dans le graphe.
- Danus stocke les faits vérifiés avec leurs preuves et dépendances logiques pour construire des arguments longs de manière incrémentale tout en gardant l'état de preuve partagé organisé.
- L'agent principal résume périodiquement l'état de preuve évolutif, redirige les ouvriers vers des directions prometteuses et soutient l'interaction avec les mathématiciens humains grâce à des rapports d'avancement.
- L'évaluation à travers six études de cas de niveau recherche en géométrie algébrique, théorie des singularités et combinatoire illustre comment le mécanisme de graphe de faits permet la construction de preuves mathématiques longues et détaillées.
Les résultats suggèrent que l'orchestration basée sur un graphe de faits fournit une voie efficace vers l'échelle des agents de raisonnement mathématique pour les problèmes de recherche à long terme.