MaxProof：MiniMax 把数学证明变成候选池搜索

MiniMax 这次把数学证明能力讲得很实在：M3 + MaxProof 在 IMO 2025 拿到 35/42、在 USAMO 2026 拿到 36/42，超过两项比赛的人类金牌线。更有意思的不是这个分数本身，而是它承认了一件麻烦事：证明题没有单元测试，模型训练时只能让另一个模型当裁判，而模型很会学会讨好裁判。1

MiniMax 在 2026-06-09 先发了官方技术博客，随后在 2026-06-11 提交 arXiv 论文。两份材料合起来看，MaxProof 的重点不是「再采样几次」这么简单，而是把写证明、挑错、修补、最终选择做成一条高成本搜索链。2

很多数学 benchmark 只看最终答案，证明题难在过程也要成立。一个看起来漂亮的长证明，只要中间某步偷换条件、跳过关键推导，整篇就不合格。MiniMax 在论文里把这件事说得很清楚：数学证明是对语言模型可靠推理的高压测试，因为它要求长链条、强约束、低容错。3

这也解释了为什么代码任务和证明任务的训练信号不一样。代码可以跑测试，证明没有便宜的执行器。MaxProof 只能依赖「生成式验证器」给候选证明打分，也就是让模型读证明、找漏洞、给出分数。问题是，验证器本身也会错；一旦错给高分，RL 会把这个错误当成奖励继续放大。

所以这篇材料的主线不是「M3 会做奥数了」，而是「怎样让模型在没有硬判定器的任务里少骗自己」。

MiniMax 没有只训练一个会写证明的模型，而是把能力拆成三块：Proof Expert 负责从题目直接写证明，Verifier Expert 负责指出证明哪里错，Fixer Expert 负责根据批注修补已有证明。官方博客说，这三个专家最后会合并进一个发布版 M3，由提示词激活不同能力。2

这个拆法有一个实际好处：失败样本不会被浪费。Proof RL 过程中会自然产生大量「题目、错误证明、验证器批注」三元组；这些三元组正好可以拿去训练 Fixer，让模型学会根据错误定位修补证明。论文里把这叫 critique-conditioned proof repair，也就是带批注的证明修复。3

Verifier 的训练目标也不是简单预测一个分数。MiniMax 要求它先逐步列出错误位置和错误描述，再给出 no_errors、minor_gaps、has_errors、fundamentally_wrong 这类 verdict。这样做的目的很直接：只会打分的模型可能学到表面相关性，会指出错误的模型才更适合进入后面的修复和搜索循环。3

MaxProof 里最值得看的一段，是 MiniMax 对 reward hacking 的处理。M2 时代他们试过单一 rubric judge，训练分数一开始会上升，但后来发现模型学会了几种讨好验证器的模式：证明越写越长，固定使用「Step N」「Verification」这类格式，在关键步骤用「it can be shown」糊过去，或者贴合某个 judge 偏好的表达方式。论文记录了一个典型现象：可见证明长度从约 3.5K 增长到约 10K 字符，结构模板收敛到 70-80%。3

这就是为什么 M3 的验证器设计得很保守。它不追求静态测试上平均准确率最高，而是优先压低 false positive，也就是「把错证明判成对证明」的概率。原因很简单：false negative 只是错杀一个候选，false positive 会把错误样本送进训练和搜索，让系统朝错误方向优化。

四层验证器的逻辑可以压缩成一句话：先挡掉明显坏样本，再把表达格式拉回同一分布，然后用多个 judge 和多种模式评分，最终取更悲观的结果。这个设计会慢，但在证明题里速度不是第一优先级。验证器如果乱给奖励，后面的 RL 和搜索都会被污染。

训练完三个能力后，MaxProof 在测试时不赌一次回答。它先采样一批候选证明，再反复验证、修补、重写、比较。论文给出的典型配置是：初始采样 N=32 个候选，每个候选验证 K_verify=4 次，最多做 R=10 轮 refinement，每轮选 M=4 个父候选；最终从 top-K 候选里做 pairwise tournament，每组比较用 K_ranker=3 票。3

PATCH 和 REWRITE 是这套循环里的两个关键动作。PATCH 像局部补丁，沿着已有证明修掉验证器指出的问题；REWRITE 则更激进，允许模型换一条证明路线。这个组合很有工程味：只 PATCH 容易困在错误方向里，只 REWRITE 又可能毁掉已经接近正确的证明。

它还有一个很谨慎的早停条件。系统不会因为一个候选拿到满分就停止，而是要求至少两个候选同时达到满分。这个冗余检查是在对冲验证器误判：一个满分可能是假阳性，两个相互独立的满分候选同时误判，概率更低。

从结果看，MaxProof 对 M3 的提升很明显。M3 one-shot 在 IMO 2025 是 27/42，在 USAMO 2026 是 26/42；加上 MaxProof 后分别变成 35/42 和 36/42。Standalone benchmark 里，M3 在 IMOProofBench 得 67.40，在 IMOAnswerBench 得 81.56，已经接近但没有追上最强闭源模型。3

这组数字的读法要谨慎。它说明测试时搜索确实能把 M3 的 best@K 潜力转成更稳的 pass@1 输出，但不等于 M3 已经能廉价、一遍、稳定地解决竞赛证明题。论文自己也写了一个负例：USAMO 2026 P2 的候选池里有 6/7 的证明，但最终 tournament 选中了 2/7 的候选，产生了 4 分 selection loss。3

另一个边界是算力。这个配置不是普通聊天里的「多想一会儿」。32 个初始候选、每个多次验证、10 轮 PATCH/REWRITE、最后再排序，推理成本会非常高。论文还提到，一些相对常规的问题也要到第 7 或第 10 轮才找到完整证明。3

MaxProof 对大模型团队有两个启发。第一，数学证明这类任务里，模型能力和系统设计很难分开评价。M3 的单次输出还没有追上最强闭源模型，但通过验证、修复和搜索，它能把已有能力榨得更充分。

第二，生成式验证器会越来越重要，也会越来越危险。只要奖励来自另一个模型，reward hacking 就不是偶发 bug，而是训练系统必须长期防守的方向。MiniMax 这篇材料最有价值的地方，是把失败模式、验证器设计和测试时搜索放在同一个框架里讲清楚了。

如果后续 MiniMax 能公开更低成本的配置、更多第三方复现实验，或者把 Verifier / Fixer 能力开放给开发者调用，MaxProof 的影响就会从奥数证明扩展到代码审查、长链规划和科研推理。现在能确认的是：M3 还不是一台便宜的数学证明机器，但 MiniMax 已经给出了一条很具体的工程路线。