RMA：上下文编排的研究数学智能体

arXiv:2605.22875v2 公告类型：替换交叉版本 摘要：长时程数学推理之所以失败，较少是因为模型无法生成有效的下一步，更多是因为智能体未能在多轮迭代中维持并展示正确的语义状态。若缺乏管理，这会产生研究级证明：局部上看似可信，但整体上并不完整——某个关键引理尚未证明、某项假设未经检查、某条引用缺乏支持，或某个计算性结论未经验证。我们提出 Research Math Agents（RMA），一种面向长时程证明开发的智能体框架，其核心是持久化的类型化研究存储，以及一个从该存储中编译面向具体操作的上下文的编排器。Research Context Orchestrator 是连接持久化研究存储与每个局部范围证明操作的核心状态管理层：它检索与任务相关的材料，将其编译为有界上下文，调用适当的操作，并将生成的证明修改、问题更新、文献笔记、计划或评估结果写回存储。该过程旨在让证明修订、未解决问题、既有尝试、文献和评估结果在多轮过程中持续可用，同时仅向每个局部操作暴露与任务相关的状态。我们通过独立专家评估、数学家盲审、基于 LLM 的基准评估以及 Lean 4 内核验证，在多个互补的研究级场景中对 RMA 进行了评估。在经过独立评估的 SOOHAK Challenge Hard 集上，RMA 达到了 42.5% 的解决率；在人类专家评估中，RMA 在 First Proof B1 上获得了 10 题中 8 题的正确解答，并在 B2 上获得了 10 题中 8 题通过的解答；在 Formal Conjectures 中，RMA 使用 Lean 4 内核验证了抽样的 300 个 Research Solved 目标中的 213 个。