연구자들은 글로벌 메모리 관리 메커니즘으로 공유 fact-graph를 활용하는 연구 수준의 수학적 추론을 위한 오케스트레이션 시스템인 Danus를 제안합니다. 이 시스템은 계획을 위한 메인 에이전트와 병렬 증명 검색을 수행하는 여러 워커 에이전트를 조정하며, stateless 검증기를 사용하여 주장을 graph에 입력하기 전에 확인합니다.
- Danus는 공유된 proof 상태를 정리하면서 긴 논증을 점진적으로 구축하기 위해 proof와 논리적 의존성과 함께 검증된 fact를 저장합니다.
- 메인 에이전트는 진화하는 proof 상태를 주기적으로 요약하고, 유망한 방향으로 워커들을 리디렉션하며, 진행 보고를 통해 인간 수학자와의 상호작용을 지원합니다.
- 대수기하학, 특이점 이론, 조합론에서의 여섯 가지 연구 수준 사례 연구를 통한 평가는 fact-graph 메커니즘이 어떻게 길고 상세한 수학적 증명의 구축을 가능하게 하는지를 보여줍니다.
결과는 fact-graph 기반 오케스트레이션이 장기적인 연구 문제를 위한 수학적 추론 에이전트의 확장성을 향한 효과적인 경로를 제공한다는 것을 시사합니다.