Danus: 사실 그래프 메모리를 활용한 수학적 추론 에이전트 오케스트레이션

Danus: Orchestrating Mathematical Reasoning Agents with Fact-Graph Memory

최근의 LLM 기반 수학적 추론 에이전트는 연구 수준의 문제를 해결하기 시작했으며, 일부 경우에는 미해결 문제 해결에 기여하기도 했습니다. 그러나 이러한 에이전트를 효과적으로 확장하고 관리하는 것은 여전히 어려운 과제이며, 이는 중간 단계의 주장을 체계적이고 신뢰성 있게 유지하면서 병렬 증명 탐색을 조정하는 데 어려움이 있기 때문입니다. 본 논문에서는 연구 수준의 수학적 추론을 위한 오케스트레이션 시스템인 Danus를 제안합니다. Danus는 전역 메모리 관리 메커니즘으로 공유된 사실 그래프를 중심으로 설계되었습니다. Danus는 계획 및 조정을 수행하는 주요 에이전트, 병렬로 증명 탐색을 수행하는 여러 작업 에이전트, 그리고 제안된 수학적 주장을 사실 그래프에 포함하기 전에 검증하는 상태 없는 검증기로 구성됩니다. 각 검증된 사실은 증명과 논리적 의존성과 함께 저장되어 시스템이 공유된 증명 상태를 체계적으로 유지하면서 장기간에 걸쳐 점진적으로 복잡한 논증을 구축할 수 있도록 합니다. 주요 에이전트는 주기적으로 진화하는 증명 상태를 요약하고, 작업 에이전트를 유망한 방향으로 재분배하며, 진행 상황 보고서를 통해 인간 수학자와의 상호 작용을 지원합니다. 우리는 대수 기하학, 특이점 이론 및 조합론 분야의 6가지 연구 수준 사례 연구를 통해 Danus를 평가하여 사실 그래프 메모리 메커니즘이 Danus가 장황하고 상세한 수학적 증명을 구축하도록 어떻게 지원하는지 보여줍니다. 우리의 결과는 사실 그래프 기반 오케스트레이션이 장기적인 연구 문제를 위한 수학적 추론 에이전트를 확장하는 효과적인 방법임을 시사합니다. Danus는 https://github.com/frenzymath/Danus 에서 오픈 소스로 제공됩니다.

Recent LLM-based mathematical reasoning agents have begun to tackle research-level problems and, in several cases, have contributed to the resolution of open problems. However, scaling and orchestrating such agents effectively remains challenging, due to the difficulty of coordinating parallel proof search while keeping intermediate claims organized and reliable. In this paper, we propose Danus, an orchestration system for research-level mathematical reasoning centered on a shared fact graph as a global memory-management mechanism. Danus consists of a main agent that performs planning and coordination, multiple worker agents that carry out proof search in parallel, and a stateless verifier that checks proposed mathematical claims before they are admitted into the fact graph. Each verified fact is stored together with its proof and logical dependencies, allowing the system to build long arguments incrementally while keeping the shared proof state organized. The main agent periodically summarizes the evolving proof state, redirects workers across promising directions, and supports interaction with human mathematicians through progress reports. We evaluate Danus through six research-level case studies in algebraic geometry, singularity theory, and combinatorics, illustrating how the fact-graph memory mechanism enables Danus to construct long, detailed mathematical proofs. Our results suggest that fact-graph-based orchestration provides an effective route toward scaling mathematical reasoning agents for long-horizon research problems. Danus is open source at https://github.com/frenzymath/Danus.