研究者らは、グローバルなメモリ管理メカニズムとして共有事実グラフを利用する、研究レベルの数学的推論のためのオーケストレーションシステムであるDanusを提案する。このシステムは、計画用のメインエージェントと並列証明探索を行う複数のワーカーエージェントを調整し、ステートレス検証器を使用して主張がグラフに入る前にそれらを検証する。

  • Danusは、共有された証明状態を整理しながら、長い議論を段階的に構築するために、証明と論理的依存関係とともに検証済みの事実を保存する。
  • メインエージェントは定期的に進化している証明状態を要約し、有望な方向へワーカーをリダイレクトし、進捗報告を通じて人間の数学者との対話をサポートする。
  • 代数幾何学、特異点理論、組み合わせ論における6つの研究レベルのケーススタディを通じた評価は、事実グラフメカニズムがいかにして長く詳細な数学的証明の構築を可能にするかを示している。

結果は、事実グラフベースのオーケストレーションが、長期の研究問題に対する数学的推論エージェントのスケーリングに向けた効果的な道筋を提供することを示唆している。