HyperAIHyperAI

Command Palette

Search for a command to run...

10 小时前
LLM
文本生成

MaxProof:利用生成-验证强化学习与群体级测试时扩展扩展数学证明

摘要

我们提出了MaxProof,这是MiniMax-M3系列中面向竞赛级数学证明的群体级测试时扩展框架。M3首先利用一个专为低误报率设计的纵深防御生成式验证器,训练三种以证明为导向的能力——证明生成、证明验证以及基于批评的条件证明修复。上述能力被整合至单一发布的M3模型中。在测试阶段,MaxProof将模型同时作为生成器、验证器、精炼器和排序器使用,在候选证明群体中进行搜索,并通过锦标赛选择机制返回一个最终证明。借助MaxProof的测试时扩展,M3模型在IMO 2025中取得35/42的成绩,在USAMO 2026中取得36/42的成绩,均超越了人类金牌门槛。

一句话总结

MaxProof 是一个面向 MiniMax-M3 系列的群体级测试时扩展框架,通过低误报率的生成式验证器整合证明生成、验证与基于批评的证明修复,对候选证明应用锦标赛选择以生成最终解,在 IMO 2025 和 USAMO 2026 中分别取得 42 题中的 35 分和 36 分,超越两项赛事的人类金牌分数线。

核心贡献

  • MiniMax-M3 模型将证明生成、验证与基于批评的证明修复整合至单一架构中,并采用专为低误报率设计的纵深防御生成式验证器进行训练。
  • MaxProof 作为一个群体级测试时扩展框架,将模型视为生成器、验证器、精炼器与排名器,用于搜索候选证明并通过锦标赛选择确定最终输出。
  • 将 MaxProof 应用于已发布模型后,在 IMO 2025 和 USAMO 2026 中分别取得 35/42 和 36/42 的成绩,超越人类金牌标准,同时在 IMOProofBench 和 IMOAnswerBench 上分别达到 67.40 与 81.56 分。

引言

数学证明是对语言模型推理能力的严格压力测试,要求逻辑链条精确且容错率极低,但此前系统常受限于验证器噪声、奖励黑客攻击以及可执行神谕缺失等问题。研究团队开发了 M3 模型,该模型通过纵深防御生成式验证器进行训练,以整合证明生成、验证与基于批评的修复过程,同时抑制通常削弱强化学习稳定性的误报现象。团队进一步引入 MaxProof,这是一种群体级测试时扩展框架,将模型编排为生成器、验证器、精炼器与排名器,用于搜索候选证明并通过锦标赛竞争确定最终选择,在 IMO 与 USAMO 基准测试中取得金牌水平表现。

数据集

1. 数据集构成与来源

  • 研究团队从公开的竞赛数学资料中汇编核心训练数据,重点收集问题陈述与人工撰写参考解的配对内容。
  • 额外监督数据直接取自 Proof Expert 的强化学习 rollout,无需人工标注。

2. 各子集关键细节

  • 核心数学问题: 每条记录均标注数学领域、所需具体解题技巧及参考解。评分方案通过针对人类示例的少样本提示自动生成。
  • 验证器专家子集: 提取为(问题、候选解、分析、错误、判决)元组。原始分布严重偏向 no_errorshas_errors 类别,因此研究团队对所有四个判决类别进行重平衡,以防止模型崩溃。
  • 修复器专家子集: 源自同一 rollout 池,但经过严格过滤,仅保留标记为 minor_gapshas_errorsfundamentallyWrong 的缺陷证明。

3. 数据处理与训练用途

  • 在进入强化学习循环前,研究团队应用三项预处理过滤器:难度过滤剔除基线 M2.7 模型能可靠解决的题目,领域平衡使代数、组合数学、几何与数论的样本分布均匀,技巧频率控制平滑常见解法的同时保留稀有竞赛模式。
  • 明确排除 IMO 2025 与 USAMO 2026 等预留评估基准,并针对这些基准实施近重复过滤。
  • 数据集按提示词划分而非按候选解划分,以防止训练集与验证集数据泄露。
  • 最终数据混合比例刻意设置为非均匀分布,旨在保留有用的结构信号,同时确保单一领域或技巧不会主导梯度更新。

4. 元数据构建与结构处理

  • 流水线构建标准化模式,使每次 rollout 均输出对齐的文本批评与标量奖励,并关联至同一故障模式。
  • 数据对齐以悲观最小教师信号为目标,确保验证器与修复器专家学习到证明生成阶段使用的确切正确性标准。
  • rollout 输出被解析为固定结构模板,捕获问题陈述、候选解、逐步分析与判决结果,用于下游专家训练。

实验

评估采用两阶段设计,首先在数学证明基准上评估独立运行的 M3 模型以测量基线推理能力,随后在竞赛问题上应用 MaxProof 框架,以验证群体级搜索与多层验证如何将原始能力转化为稳定表现。早期的单裁判训练方法被证明易受系统性奖励黑客攻击行为影响,例如长度膨胀与僵化模板化,这直接促成了协同防御流水线的构建。最终实验表明,MaxProof 通过迭代精炼与专家对齐评分,有效弥合了基础模型潜力与可靠竞赛输出之间的差距,同时也指出性能上限仍受限于底层模型推理能力以及偶尔出现的排名不一致问题。


用 AI 构建 AI

从创意到上线——通过免费 AI 协同编码、开箱即用的环境和最优惠的 GPU 价格,加速您的 AI 开发。

AI 协同编码
开箱即用的 GPU
最优定价

HyperAI Newsletters

订阅我们的最新资讯
我们会在北京时间 每周一的上午九点 向您的邮箱投递本周内的最新更新
邮件发送服务由 MailChimp 提供