RMA：一个面向研究级数学问题的智能体系统
RMA: Context-Orchestrated Research Math Agents
AI总结：
提出Research Math Agents (RMA)框架，通过多角色多轮协作的智能体工作流，在First Proof基准上解决80%的研究级数学问题，优于GPT-5.2R等基线。
摘要：
我们提出了$ extbf{Research Math Agents (RMA)}$，一个用于研究级数学问题自动推理的智能体框架。与以往专注于竞赛数学或形式化定理证明的研究不同，RMA针对需要长程推理、文献依据和迭代证明改进的研究级数学问题。RMA将研究级证明求解分解为专门模块，包括问题分析、文献搜索与理解、公平比较、知识库构建和证明验证，所有这些都由初始化器、提议器和验证器智能体通过共享的结构化内存协调。在这个统一框架内，这些智能体以多角色、多轮工作流的方式运行，通过迭代反馈协作生成、改进和验证候选证明。我们在First Proof基准上评估了RMA，该基准由来自不同领域的专家数学家贡献的十个研究级问题组成。通过全面的专家评估，RMA在First Proof基准上优于强基线（包括GPT-5.2R和Aletheia），解决了十个研究问题中的八个，并生成了逻辑更合理、可读性更强的证明。我们的全面消融研究进一步表明，性能提升来自于结构化推理模块、迭代改进和基于验证器的反馈之间的交互，而非任何单一组件。我们的解决方案和实现将在论文被接收后公开。
英文摘要：
Long-horizon mathematical reasoning fails less often because a model cannot produce a valid next step than because an agent fails to maintain and expose the right semantic state across many iterations. Left unmanaged, this produces research-level proofs that are locally convincing yet globally incomplete: a key lemma unproved, an assumption unchecked, a citation unsupported, or a computational claim unverified. We present Research Math Agents (RMA), an agentic framework for long-horizon proof development built around a persistent, typed research store and an orchestrator that compiles operation-specific context from that store. The Research Context Orchestrator is the central state-management layer between the persistent research store and each locally scoped proof operation: it retrieves task-relevant artifacts, compiles them into a bounded context, invokes the appropriate operation, and writes the resulting proof edits, issue updates, literature notes, plans, or evaluations back to the store. This process is designed to keep proof revisions, unresolved issues, prior attempts, literature, and evaluations available across rounds while exposing only task-relevant state to each local operation. We evaluate RMA across complementary research-level settings using independent expert evaluation, blind mathematician review, LLM-based benchmark evaluation, and Lean 4 kernel verification. RMA achieves a 42.5% solve rate on the independently evaluated SOOHAK Challenge Hard set, obtains 8 of 10 correct solutions on First Proof B1 and 8 of 10 passing solutions on B2 under human-expert evaluation, and verifies 213 of 300 sampled Research Solved targets in Formal Conjectures with the Lean 4 kernel.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
