論文の概要: MechMath Agent Team: LLM Driven Agents for Mathematical Research

• arxiv url: http://arxiv.org/abs/2607.04394v1
• Date: Sun, 05 Jul 2026 16:37:40 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-07-07 22:26:29.913824
• Title: MechMath Agent Team: LLM Driven Agents for Mathematical Research
• Title（参考訳）: MechMath Agent Team: 数学研究のためのLLM駆動エージェント
• Authors: Yichuan Cao, Ruichen Qiu, Junqi Liu, Jiaqi Wang, Dakai Guo, Ruyong Feng, Lihong Zhi, Xiao-Shan Gao,
• Abstract要約: MechMath Agent Team (MMAT) は、数学研究の全サイクルを通して共同パイロットとして機能するように設計された大規模言語モデル駆動エージェントである。 我々は、システムの責任をコントロール、実行、拡張プレーンに分離する三部構成のハーネスアーキテクチャを設計する。 我々は、数論、代数的複素性理論、微分代数、作用素代数、不等式における開問題に関するMMATを評価する。
• 参考スコア（独自算出の注目度）: 17.23955320294417
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: AI reasoning has become a central focus in contemporary artificial intelligence, largely driven by the success of large language models. However, mathematical research, which is characterized by non-linear derivation paths, rigorous logical requirements, and protracted exploration cycles, poses severe challenges for existing reasoning systems. To overcome these limitations, we present the MechMath Agent Team (MMAT), which is a large language model driven agent designed to serve as a co-pilot throughout the full cycle of mathematical research. We design a tripartite Harness Architecture that decouples system responsibilities into Control, Execution, and Augmentation planes, thereby reconciling rigorous logical control with the agility demanded by open-ended research. Building upon this framework, we instantiate three specialized agents: a Knowledge Base Manager, a Natural Language Prover, and a Formal Language Prover, all operating in a closed loop to produce formally certified mathematical proofs. We evaluate MMAT on open problems in Number Theory, Algebraic Complexity Theory, Differential Algebra, Operator Algebra, and Inequalities. Across a two-month deployment, 11 problems have been solved, demonstrating its capacity to act as a co-pilot throughout the entire research cycle. The contributions are threefold: a general decoupled Harness Architecture for multi-agent mathematical reasoning, its concrete instantiation in the MMAT system, and empirical validation on a diverse suite of open problems.
• Abstract（参考訳）: AI推論は、主に大きな言語モデルの成功によって、現代の人工知能において中心的な焦点となっている。 しかし, 線形導出経路, 厳密な論理的要求, 長期探索サイクルを特徴とする数学的研究は, 既存の推論システムに深刻な課題をもたらす。 これらの制限を克服するために,数学研究の全サイクルを通じて共同パイロットとして機能するように設計された大規模言語モデル駆動エージェントであるMechMath Agent Team (MMAT)を提案する。 我々は、システムの責任をコントロール、実行、拡張プレーンに分離する三部構成のハーネスアーキテクチャを設計し、これにより、オープンエンドリサーチで要求されるアジリティと厳密な論理的制御を整合させる。 この枠組みに基づいて、我々は、知識ベースマネージャ、自然言語プロバー、フォーマル言語プロバーの3つの特殊エージェントをインスタンス化し、全てクローズドループで動作し、正式に認定された数学的証明を生成する。 我々は、数論、代数的複素性理論、微分代数、作用素代数、不等式における開問題に関するMMATを評価する。 2ヶ月のデプロイメントで11の問題が解決され、研究サイクル全体を通じて共同パイロットとして機能する能力が実証された。 コントリビューションは、マルチエージェントな数学的推論のための一般的な分離されたハーネスアーキテクチャ、MMATシステムにおける具体的なインスタンス化、様々なオープンな問題に対する経験的検証である。

関連論文リスト

• 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)
• Automated Conjecture Resolution with Formal Verification [21.763678203045973]
  本研究では,研究レベルの数学的問題に対処するためのフレームワークを提案する。 我々のフレームワークは、非公式な推論エージェントであるRethlasと、正式な検証エージェントであるArchonの2つのコンポーネントで構成されている。 このフレームワークを使用することで、可換代数におけるオープンな問題を自動で解決し、人間による関与なしにLean 4における結果の証明を正式に検証します。
  論文  参考訳（メタデータ） (2026-04-04T16:35:16Z)
• Thinking Machines: Mathematical Reasoning in the Age of LLMs [0.0]
  大規模言語モデル(LLM)は構造化推論や記号的タスクにおいて顕著な能力を示している。 この記事では、最近のモデルとベンチマークに焦点を当て、機械学習と数学的認知の交差における3つの中心的な課題について考察する。
  論文  参考訳（メタデータ） (2025-08-01T09:31:48Z)
• Large Language Models for Mathematical Analysis [3.7325315394927023]
  この研究は、数学的推論における重要なギャップに対処し、信頼できるAIの進歩に寄与する。 DEMI-MathAnalysisデータセットを開発した。 また,LLMの問題解決能力を高めるためのガイドフレームワークも設計した。
  論文  参考訳（メタデータ） (2024-12-28T20:37:55Z)
• Formal Mathematical Reasoning: A New Frontier in AI [60.26950681543385]
  我々は公式な数学的推論を提唱し、AI4Mathを次のレベルに進めるには不可欠であると主張している。 既存の進捗を要約し、オープンな課題について議論し、将来の成功を測るための重要なマイルストーンを想定します。
  論文  参考訳（メタデータ） (2024-12-20T17:19:24Z)
• LeanAgent: Lifelong Learning for Formal Theorem Proving [85.39415834798385]
  フォーマルな定理証明のための新しい生涯学習フレームワークであるLeanAgentを紹介する。 LeanAgentは継続的に一般化し、拡張可能な数学的知識を改善します。 これは23のリーンリポジトリにわたる155の定理の正式な証明を生成する。
  論文  参考訳（メタデータ） (2024-10-08T17:11:24Z)
• Evaluating LLMs' Mathematical and Coding Competency through Ontology-guided Interventions [47.83142414018448]
  算術的推論とコード生成という,2つの一般的な推論タスクに注目します。 i) 数学やコーディング問題に対する摂動の一般的なオントロジー, (ii) 摂動を応用するための半自動手法, (iii) 2つのデータセットを紹介する。 混乱した質問に対して、すべてのモデルで大幅なパフォーマンス低下を示します。
  論文  参考訳（メタデータ） (2024-01-17T18:13:07Z)
• math-PVS: A Large Language Model Framework to Map Scientific Publications to PVS Theories [10.416375584563728]
  本研究では,大規模言語モデル(LLM)の高度な数学的概念の定式化への適用性について検討する。 我々は、研究論文から数学的定理を抽出し、形式化する、Emphmath-PVSと呼ばれる自動過程を構想する。
  論文  参考訳（メタデータ） (2023-10-25T23:54:04Z)

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

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