論文の概要: RMA: an Agentic System for Research-Level Mathematical Problems
- arxiv url: http://arxiv.org/abs/2605.22875v1
- Date: Wed, 20 May 2026 04:54:22 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-05-25 17:29:20.014887
- Title: RMA: an Agentic System for Research-Level Mathematical Problems
- Title（参考訳）: RMA : 研究レベル数学問題のためのエージェントシステム
- Abstract要約: 研究数学エージェント(Research Math Agents、RMA)は、研究レベルの数学的問題に対する自動推論のためのエージェントフレームワークである。
RMAは、研究レベルの証明を、問題解析、文献検索と理解、公正比較、知識銀行構築、証明検証のための特殊なモジュールに分解する。
- 参考スコア（独自算出の注目度）: 30.952480229786236
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: We present $\textbf{Research Math Agents (RMA)}$, an agentic framework for automated reasoning on research-level mathematical problems. Unlike prior studies centered on competition mathematics or formal theorem proving, RMA targets research-level mathematical problems that require long-horizon reasoning, literature grounding, and iterative proof refinement. RMA decomposes research-level proof solving into specialized modules for problem analysis, literature search and understanding, fair comparison, knowledge-bank construction, and proof verification, all coordinated by initializer, proposer, and verifier agents through a shared structured memory. Within this unified framework, these agents operate in a multi-role, multi-round workflow, collaboratively generating, refining, and verifying candidate proofs through iterative feedback. We evaluate RMA on the First Proof benchmark, which consists of ten research-level problems contributed by expert mathematicians across diverse domains. Through comprehensive expert evaluation, RMA outperforms strong baselines on the First Proof benchmark, including GPT-5.2R and Aletheia, solving eight out of ten research problems and producing more logically sound and readable proofs. Our comprehensive ablation studies further show that performance gains arise from the interaction of structured reasoning modules, iterative refinement, and verifier-based feedback, rather than any single component. Our solutions and implementations will be made publicly available upon acceptance.
- Abstract（参考訳）: 我々は、研究レベルの数学的問題に対する自動推論のためのエージェントフレームワークである$\textbf{Research Math Agents (RMA)$を提示する。
競争数学や形式的定理証明を中心とした以前の研究とは異なり、RMAは長い水平推論、文学的根拠、反復的証明の洗練を必要とする研究レベルの数学問題をターゲットにしている。
RMAは、問題解析、文献検索および理解、公正比較、知識銀行構築、証明検証のための特殊なモジュールに研究レベルの証明を分解する。
この統合されたフレームワーク内では、これらのエージェントは複数ロールで複数ラウンドのワークフローで動作し、反復的なフィードバックを通じて候補の証明を生成し、精査し、検証する。
各種領域にまたがる専門家数学者が提案する10種類の研究レベルの問題からなる第1ProofベンチマークでRMAを評価する。
総合的な専門家評価を通じて、RMAはGPT-5.2Rやアレテアを含むファーストプロフのベンチマークにおいて強い基準線を上回り、10つの研究問題のうち8つを解決し、より論理的に健全で読みやすい証明を生み出した。
包括的アブレーション研究により、単一のコンポーネントではなく、構造化推論モジュール、反復的洗練、検証者に基づくフィードバックの相互作用により、性能が向上することが示された。
私たちのソリューションと実装は、受け入れ次第公開します。
関連論文リスト
- MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research [62.221184989046826]
MathCoPilotは、数学研究のための新しいAI共生パラダイムを具現化したループシステムである。
MathCoPilotは3つのコア機能を統合する: 証明をナビゲート可能なステップに分解するインタラクティブな証明青写真、適応的な知識ベース検索とリーン統合された反復検証を備えた自動証明スキルオーケストレーション、トピック駆動の紙検索と自動形式化を検証可能なリーン知識ベースに統合する。
論文 参考訳（メタデータ） (2026-07-16T05:22:40Z) - From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier [109.93387172162984]
AI4Mathシステムの次の飛躍は、事前に定義された問題解決者から研究エージェントへの決定的なシフトを必要とする。
この分野の体系的なレビューを行い、データセット、自動形式化、証明合成について紹介する。
論文 参考訳（メタデータ） (2026-07-08T17:46:36Z) - 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) - Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics [9.38309744591661]
フォーマル・コンジェクチャ(Formal Conjectures)は、Lean 4.0で形式化された2615の数学的問題文の進化ベンチマークである。
このデータセットは、数学的な証明発見のためのゼロ汚染ベンチマークを提供する1029のオープンリサーチ予想を特徴としている。
我々は,これらの形式化の正しさを保証するためのアプローチを,アクティブなコミュニティからのコントリビューションを生かしたオープンソースプロジェクトとして紹介する。
論文 参考訳（メタデータ） (2026-05-13T08:33:15Z) - Automated Conjecture Resolution with Formal Verification [21.763678203045973]
本研究では,研究レベルの数学的問題に対処するためのフレームワークを提案する。
我々のフレームワークは、非公式な推論エージェントであるRethlasと、正式な検証エージェントであるArchonの2つのコンポーネントで構成されている。
このフレームワークを使用することで、可換代数におけるオープンな問題を自動で解決し、人間による関与なしにLean 4における結果の証明を正式に検証します。
論文 参考訳（メタデータ） (2026-04-04T16:35:16Z) - Dr.Mi-Bench: A Modular-integrated Benchmark for Scientific Deep Research Agent [52.876617746453995]
ミ・ベンチ博士(Dr.Mi-Bench)は、科学深層研究(DR)エージェントのためのモジュール統合ベンチマークである。
Dr.Mi-Evalはモジュラー統合評価パラダイムである。
論文 参考訳（メタデータ） (2025-11-30T17:16:47Z) - Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics [1.2978846076301875]
Ax-Proverは、リーンにおける自動定理証明のためのマルチエージェントシステムである。
様々な科学的領域にまたがる問題を解決し、自律的または協調的に人間の専門家と操作することができる。
我々は,2つの公的な数学ベンチマークと,抽象代数学と量子論の分野において導入される2つのリーンベンチマークにおいて,フロンティア LLM と特殊証明モデルに対するアプローチをベンチマークする。
論文 参考訳（メタデータ） (2025-10-14T17:57:04Z) - A Comprehensive Survey on Benchmarks and Solutions in Software Engineering of LLM-Empowered Agentic System [56.40989626804489]
この調査は、Large Language Modelsを使ったソフトウェアエンジニアリングに関する、最初の総合的な分析を提供する。
本稿では,150以上の最近の論文をレビューし,(1)素早い,微調整,エージェントベースのパラダイムに分類した解法,(2)コード生成,翻訳,修復などのタスクを含むベンチマークという2つの重要な側面に沿った分類法を提案する。
論文 参考訳（メタデータ） (2025-10-10T06:56:50Z) - MOSAIC: Multi-agent Orchestration for Task-Intelligent Scientific Coding [5.470408942595905]
MOSAICは訓練のないフレームワークで、特別に設計されたエージェントで、生徒-教師のパラダイム内で、自己表現し、合理性を作り、コードを作り、デバッグする。
我々はMOSAICを科学的符号化ベンチマークで評価し、我々の特殊エージェントフレームワークが既存の手法よりも精度、堅牢性、解釈可能性で優れていることを示した。
論文 参考訳（メタデータ） (2025-10-09T20:35:23Z) - MLR-Bench: Evaluating AI Agents on Open-Ended Machine Learning Research [70.72318131988102]
MLR-Benchは、オープンエンド機械学習研究においてAIエージェントを評価するための包括的なベンチマークである。
MLR-Benchは,(1)NeurIPS, ICLR, ICMLのさまざまなMLトピックを対象としたワークショップから得られた201のリサーチタスク,(2)LLMベースのレビュアーと慎重に設計されたレビュールーリックを組み合わせた自動評価フレームワーク,(3)MLR-Agent,研究タスクを4段階(アイデア生成,提案定式化,実験,論文執筆)で完了するモジュールエージェントの足場である。
論文 参考訳（メタデータ） (2025-05-26T13:18:37Z) - LLaMA-Berry: Pairwise Optimization for O1-like Olympiad-Level Mathematical Reasoning [56.273799410256075]
このフレームワークはMonte Carlo Tree Search (MCTS)と反復的なSelf-Refineを組み合わせて推論パスを最適化する。
このフレームワークは、一般的なベンチマークと高度なベンチマークでテストされており、探索効率と問題解決能力の点で優れた性能を示している。
論文 参考訳（メタデータ） (2024-10-03T18:12:29Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。