論文の概要: Danus: Orchestrating Mathematical Reasoning Agents with Fact-Graph Memory

• arxiv url: http://arxiv.org/abs/2607.06447v1
• Date: Tue, 07 Jul 2026 16:11:30 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-07-08 21:24:51.58317
• Title: Danus: Orchestrating Mathematical Reasoning Agents with Fact-Graph Memory
• Title（参考訳）: Danus: ファクトグラフメモリを用いた数学的推論エージェントのオーケストレーション
• Authors: Jihao Liu, Guoxiong Gao, Zeming Sun, Bin Wu, Shurui Liu, Jiedong Jiang, Haocheng Ju, Leheng Chen, Ronnie Cheng, Xiping Zhang, Bin Dong,
• Abstract要約: Danusは、共有事実グラフを中心とした研究レベルの数学的推論のためのオーケストレーションシステムである。 検証された各事実は証明と論理的依存関係と共に格納され、システムは長い引数を構築できる。
• 参考スコア（独自算出の注目度）: 7.10978537067254
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.
• Abstract（参考訳）: 最近のLSMに基づく数学的推論エージェントは、研究レベルの問題に取り組み始めており、いくつかのケースでは、オープンな問題の解決に寄与している。 しかし,中間クレームの整理と信頼性を維持しながら並列証明探索の調整が困難であることから,このようなエージェントのスケーリングとオーケストレーションは依然として困難である。 本稿では,グローバルメモリ管理機構として共有ファクトグラフを中心とした研究レベルの数学的推論のためのオーケストレーションシステムであるDanusを提案する。 Danusは、計画と調整を行うメインエージェントと、並列に証明検索を実行する複数のワーカーエージェントと、事実グラフに入る前に提案された数学的クレームをチェックするステートレス検証器で構成される。 各証明された事実は証明と論理的依存関係と共に格納されるため、システムは共有された証明状態を整理しながら、長い議論を段階的に構築することができる。 主エージェントは、進化する証明状態を定期的に要約し、有望な方向を越えて労働者をリダイレクトし、進捗報告を通じて人間数学者との相互作用をサポートする。 我々はダヌスを、代数幾何学、特異性理論、コンビネータ学の6つの研究レベルのケーススタディを通じて評価し、ファクトグラフ記憶機構がダヌスにどのように長く詳細な数学的証明を構築することができるかを説明する。 この結果から, ファクトグラフに基づくオーケストレーションは, 長期的研究問題に対する数学的推論エージェントのスケーリングに有効な方法であることが示唆された。 Danusはhttps://github.com/frenzymath/Danus.comでオープンソース公開されている。

関連論文リスト

• MechMath Agent Team: LLM Driven Agents for Mathematical Research [17.23955320294417]
  MechMath Agent Team (MMAT) は、数学研究の全サイクルを通して共同パイロットとして機能するように設計された大規模言語モデル駆動エージェントである。 我々は、システムの責任をコントロール、実行、拡張プレーンに分離する三部構成のハーネスアーキテクチャを設計する。 我々は、数論、代数的複素性理論、微分代数、作用素代数、不等式における開問題に関するMMATを評価する。
  論文  参考訳（メタデータ） (2026-07-05T16:37:40Z)
• Artificial Intelligence for Mathematical Reasoning: An Integrated Survey of Language Models, Neuro-symbolic Systems, and Verified Discovery [3.9943798586374784]
  この調査は、この分野の進化の統一的な説明を提供する。 i)テキストや図面に対する非公式な推論、MWPの解法、マルチモーダル幾何、RLMの解法、(ii)自動形式化、戦術予測、コンパイラ誘導修理、証明探索を含む証明アシスタントの形式的推論、(iii)システム構築の提案、境界の改善、オープンな問題に対する攻撃を支援する数学的発見、(iv)CoTプロンプト、ツールの使用、プロセス報酬モデル、VLVRなど、推論およびトレーニング時のテクニック。
  論文  参考訳（メタデータ） (2026-06-07T16:50:07Z)
• LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization [104.06650149974585]
  信頼性の高い研究レベルのLean AutoformalizationのためのマルチエージェントハーネスであるLeanMarathonを紹介します。 4つのコントラクトスコープエージェントがこの青写真を構築し、監査し、証明し、修復する。 我々は4つのErds問題にまたがる最近の2つの研究論文でLeanMarathonを評価した。
  論文  参考訳（メタデータ） (2026-06-03T20:09:39Z)
• Discovering mathematical concepts through a multi-agent system [3.820195410658766]
  計算数学的発見のための新しいマルチエージェントモデルを提案する。 我々のシステムは、研究を念頭に考え、独自の予想を示し、それを証明しようと試みる。 局所過程の正しい組み合わせの最適化は、驚くほどよく整合した数学的面白さの概念に繋がると主張している。
  論文  参考訳（メタデータ） (2026-03-04T19:13:36Z)
• Towards Autonomous Mathematics Research [48.29504087871558]
  Aletheiaは、自然言語のエンドツーエンドの解を反復的に生成し、検証し、修正する数学研究エージェントである。 具体的には、AletheiaはGemini Deep Thinkの高度なバージョンで、推論の問題に挑戦している。 我々は、オリンピアード問題から博士レベルのエクササイズまで、AI支援数学研究におけるいくつかのマイルストーンを通じて、アレクシアを実証する。
  論文  参考訳（メタデータ） (2026-02-10T18:50:15Z)
• Stationary Processes, Wiener-Granger Causality, and Matrix Spectral Factorization [0.3626013617212666]
  本稿では,Grangerの因果関係を詳細に概説し,その歴史的発展を辿り,近年の計算技術の進歩が様々な分野への応用をいかに促進するかを考察する。 提案手法の今後の方向性について,特に大規模データ分析の文脈で論じる。
  論文  参考訳（メタデータ） (2024-12-25T13:29:39Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• GeoQA: A Geometric Question Answering Benchmark Towards Multimodal Numerical Reasoning [172.36214872466707]
  我々は、テキスト記述、視覚図、定理知識の包括的理解を必要とする幾何学的問題を解くことに注力する。 そこで本研究では,5,010の幾何学的問題を含む幾何学的質問応答データセットGeoQAを提案する。
  論文  参考訳（メタデータ） (2021-05-30T12:34:17Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。