기술 요약: Danus – 사실 그래프 메모리를 통한 수학적 추론 에이전트의 오케스트레이션

문제 정의

최근 대규모 언어 모델(LLM) 기반의 에이전트들은 연구 수준의 수학적 문제를 해결하며 오픈 퀘스천을 해결하는 능력을 보여주었습니다. 그러나 이러한 시스템을 장기적인 연구 과제(long-horizon research tasks)로 확장하는 것은 여전히 큰 도전 과제입니다. 기존의 멀티 에이전트 시스템은 특화된 역할을 가진 "생성-검증-수정" 루프에 의존하는 경우가 많지만, 병렬적인 증명 탐색을 효과적으로 조정하는 데 어려움을 겪습니다. 여러 에이전트가 단일 증명에 기여하려고 할 때 견고한 메모리 관리 체계가 없다면, 공유된 컨텍스트가 혼란에 빠지거나 무관하거나 오류가 있는 중간 산출물이 전파되어 성능이 저하될 수 있습니다. 핵심 문제는 어떻게 하면 에이전트 군집(swarm)을 조율하여 신뢰할 수 있는 진실의 상태를 유지하면서 길고 상세한 수학적 증명을 협력적으로 구축하게 할 것인가 하는 점입니다.

방법론

본 논문은 글로벌 메모리 관리 메커니즘으로서 공유된 **사실 그래프(Fact Graph)**를 통해 수학적 추론을 확장하도록 설계된 오케스트레이션 시스템인 Danus를 제안합니다. 이 시스템 아키텍처는 세 가지 구별된 에이전트 유형 간의 엄격한 권력 분립을 강제합니다.

1. 메인 에이전트 (The Main Agent):

   • 역할: 글로벌 계획 수립, 조정 및 인간 수학자와의 전략적 상호작용을 수행합니다. 상세한 유도를 직접 수행하지는 않습니다.
   • 기능: 문제를 해석하고, 필요 시 고수준 전략 모델(예: GPT-5.5-pro)을 참조하며, 문제를 분해하고 워커 에이전트에게 방향을 할당합니다.
   • 상태 관리: 주기적으로 사실 그래프와 글로벌 메모리 로그를 읽어 현재 증명의 상태를 요약하고, 막다른 길(dead end)을 식별하며, 유망한 방향으로 워커를 재배치합니다. 인간의 가이드를 위한 인터페이스 역할을 합니다.

2. 워커 에이전트 (Worker Agents - Swarm):

   • 역할: 병렬적으로 상세한 증명 탐색을 수행합니다.
   • 기능: Rethlas 생성 에이전트를 기반으로, 워커들은 문제를 여러 각도(구성적 및 반증적 측면)에서 동시에 탐색합니다. 각 워커는 전체 증명이 아닌 특정 주장(보조정리, 반례, 토이 예시 등)에 집중합니다.
   • 상호작용: 워커들은 검증자에게 뒷받침되는 증명을 포함한 문장을 제안합니다. 이들은 현재의 주장을 뒷받침하기 위해 사실 그래프에서 관련 사실을 검색하지만, 그래프를 직접 수정하지는 않습니다.

3. 무상태 검증자 (The Stateless Verifier):

   • 역할: 정당성에 대한 유일한 권위자입니다.
   • 기능: 사실이 사실 그래프에 수용되기 전, 제안된 수학적 주장을 확인하는 무상태 서비스입니다. 의존성 및 인용된 참조를 확인하기 위해 사실 그래프를 읽습니다.
   • 신뢰성: 생략된 단계나 잘못된 참조가 있는 증명을 거부하도록 설계되어, 사실상 거짓 양성(false positive)을 발생시키지 않습니다.

사실 그래프 (핵심 혁신)

사실 그래프는 시스템의 단일 진실 공급원(single source of truth) 역할을 하는 유향 비순환 그래프(DAG)입니다.

• 구조: 노드는 검증된 사실(수학적 문장 + 검증자가 확인한 증명)을 나타냅니다. 엣지는 논리적 의존성(즉, 사실 B는 사실 A에 의존함)을 나타냅니다.
• 장점 (단일 블루프린트 대비): 모든 워커가 전체 누적 컨텍스트를 모두 떠안아야 하는 기존의 단일 마크다운 파일 방식과 달리, 사실 그래프를 사용하면 워커가 현재 작업에 관련된 특정 사실만을 검색할 수 있습니다. 이를 통해 컨텍스트 창을 작고 집중적으로 유지하여 환각(hallucination)과 간섭을 줄입니다.
• 병렬성: 여러 워커가 파일 잠금 충돌 없이 동시에 그래프에 기여할 수 있습니다.
• 철회(Revocation): 만약 어떤 사실이 나중에 잘못된 것으로 판명되면(예: 결함이 있는 참조로 인해), 해당 사실과 그에 의존하는 모든 사실이 그래프에서 제거되어 남은 구조의 무결성을 보장합니다.

메모리 아키텍처

• 사실 그래프 (Fact Graph): 검증된 진실만을 저장합니다.
• 글로벌 메모리 (Global Memory): 중간 산출물(계획, 막다른 길, 유망한 방향, 구축된 예시 등)과 외부 모델과의 상담 로그를 포함하며, 메인 에이전트와 워커가 공유하는 컨텍스트입니다.
• 로컬 메모리 (Local Memory): 개별 워커가 자신의 특정 추론 이력을 추적하기 위한 개인 로그입니다.

워크플로우

1. 초기화: 인간이 문제를 제공합니다. 메인 에이전트는 계획을 수립하고 워커 군집에 작업을 할당합니다.
2. 병렬 탐색: 워커들이 주장과 증명을 생성하여 검증자에게 제출합니다. 검증된 사실들은 사실 그래프에 추가됩니다.
3. 오케스트레이션: 메인 에이전트는 주기적으로 상태를 요약하고, 전략을 위해 외부 모델을 참조하며, 진행 상황이나 정체에 따라 워커를 재지시합니다.
4. 종료: 목표 정리(theorem) 또는 그 반증이 그래프에 검증된 사실으로 등장할 때까지 루프가 지속됩니다.
5. 합성: 메인 에이전트는 사실 그래프를 논문 스타일의 원고로 변환합니다. 이 초안은 사실들을 선형적인 산문으로 압축하는 과정에서 발생하는 오류를 수정하기 위해 최종 검증 과정을 거칩니다.

주요 기여

1. 사실 그래프 오케스트레이션: 워커의 컨텍스트를 글로벌 증명 상태로부터 분리함으로써, 단일 파일 방식에서 나타나는 "컨텍스트 팽창"과 간섭을 방지하고 확장 가능한 병렬 증명 탐색을 가능하게 하는 DAG 기반 메모리 메커니즘을 도입했습니다.
2. 권력 분립: 계획, 실행, 검증이 엄격히 분리된 구조를 확립하여, 오케스트레이터가 검증되지 않은 수학적 내용을 도입하는 것을 방지합니다.
3. 인간 참여형 설계 (Human-in-the-Loop): 인간이 고수준의 가이드와 최종 검토를 제공하는 동안, 시스템은 탐색, 분해, 합성을 처리하는 협업 구조를 촉진합니다.
4. 견고한 검증 파이프라인: 무상태 검증자가 사실 그래프가 신뢰할 수 있는 진실의 원천이 되도록 보장함으로써, 긴 의존성 체인(실험에서 최대 54단계)을 안전하게 축적할 수 있음을 입증했습니다.

결과

시스템은 대수 기하학, 특이점 이론, 조합론 분야의 6가지 연구 수준 사례 연구를 통해 평가되었습니다. 모든 경우에서 베이스라인인 GPT-5.5-pro 웹 인터페이스는 의미 있는 결과를 내는 데 실패했습니다.

• Foliations의 Optimal Bend-and-Break: Danus는 서로 다른 참조 문헌들로부터 기법을 합성하여 최적의 상수 $r+1$을 증명했습니다. 또한 만족스럽지 못한 참조를 독립적으로 식별하고 더 나은 참조를 찾아냈습니다.
• Shokurov의 Global Index Conjecture (3D): Danus는 문제를 다섯 가지 클래스로 자율적으로 분해하고 세 가지 클래스에 대해 Lie 이론적 해법을 발견했습니다. 나머지 두 클래스를 해결하기 위해 고수준의 힌트(foliated minimal model program)만을 필요로 했습니다.
• Families에서의 Total Cartier Indices: Danus는 대수 기하학, 가환 대수학, 실 대수 기하학을 연결하여 유계성(boundedness)을 증명했습니다. 또한 인간의 개입을 통해 PDF 소스에서 잘못 읽은 가설을 바로잡았습니다.
• Matryoshka Numbers Asymptotics: Danus는 이 조합론적 문제를 문제 제기부터 완성된 원고에 이르기까지 인간의 수학적 가이드 없이 완전히 자율적으로 해결했습니다.
• Logarithmic Vector Fields를 통한 Weighted Homogeneity: Danus는 인간 전문가들이 예상치 못한 경로를 통해 증명을 생성했습니다. 인간에 의해 결함이 있는 참조가 식별되었을 때, Danus는 의존적인 사실들을 성공적으로 철회하고 증명을 재구축했습니다.
• Matroids의 Tangent Classes: 이전 모델인 Rethlas와의 통제된 비교에서, Danus는 Rethlas가 세 번의 시도 끝에도 해결하지 못한 복잡한 문제를 해결했습니다. 사실 그래프 덕분에 Danus는 3,157개의 검증된 사실과 최대 54단계의 의존성 체인을 관리할 수 있었던 반면, Rethlas는 서로 다른 수학적 개념을 혼동했습니다.

의의 및 주장

본 논문은 사실 그래프 기반의 오케스트레이션이 장기적인 연구 문제를 위한 수학적 추론 에이전트를 확장하는 효과적인 경로를 제공한다고 주장합니다.

• 확장성: 시스템은 너비(많은 방향의 병렬 탐색)와 깊이(검증된 추론의 긴 체인 축적) 모두에서 테스트 시간 계산(test-time computation)을 성공적으로 확장합니다.
• 신뢰성: 엄격한 검증 프로토콜은 사실 그래프가 신뢰할 수 있는 진실의 원천이 되도록 보장하며, 단일 모델 패스로는 불가능한 길고 복잡한 증명 구축을 가능하게 합니다.
• 협업: Danus는 AI 에이전트가 분해, 합성, 오류 수정을 처리하는 동안 인간 수학자가 문제 선택, 누락된 고수준 아이디어 제공, 최종 전문가 검토를 수행하며 증명 구축에 실질적으로 기여할 수 있음을 보여줍니다.
• 한계: 저자들은 시스템이 여전히 가장 어려운 개념적 도약을 위해 인간의 개입을 필요로 한다는 점과, 생성된 원고가 검증되었음에도 불구하고 표기법 및 인용 관례를 위해 인간의 조정이 필요할 수 있다는 점을 겸허히 언급했습니다. 시스템은 새로운 수학적 아이디어를 무(無)에서 창조하는 것이 아니라, 해결책으로 가는 경로를 찾는 데 탁월합니다.

결론적으로, Danus는 AI 에이전트가 인간의 판단과 통합되어 열린 연구 문제를 해결하는 협업적 수학 연구 시스템을 향한 한 단계임을 나타냅니다.