論文の概要: 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 : 研究レベル数学問題のためのエージェントシステム
- Authors: Zelin Zhao, Bo Yuan, Jaemoo Choi, Yongxin Chen,
- 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つを解決し、より論理的に健全で読みやすい証明を生み出した。
包括的アブレーション研究により、単一のコンポーネントではなく、構造化推論モジュール、反復的洗練、検証者に基づくフィードバックの相互作用により、性能が向上することが示された。
私たちのソリューションと実装は、受け入れ次第公開します。
関連論文リスト
- 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) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。