MaxProof:MiniMax-M3如何做数学证明搜索
MaxProof 把 MiniMax-M3 当作生成器、验证器、修复器和排序器使用,在 IMO 2025 得到 35/42,USAMO 2026 得到 36/42。
快速答案
MaxProof 不是一个单次前向的数学模型分数,而是围绕 MiniMax-M3 证明能力搭建的 test-time scaling 系统。它让同一个模型在不同 prompt 下扮演 proof generator、verifier、fixer 和 ranker,生成候选证明、保守验证、按 critique 修复,再从候选群体里选最终证明。论文报告 MaxProof 在 IMO 2025 得到 35/42,在 USAMO 2026 得到 36/42,都超过金牌线。关键边界是:这是验证器引导的搜索系统成绩,不是单样本 pass@1。
MaxProof 真正在扩展什么
长证明不适合简单答案检查。一个证明可以接近正确但有漏洞,也可以写得很像但关键步骤不成立。论文最核心的工程问题是 verifier noise:如果生成式验证器在 RL 中给出 false positive,策略会学习无效证明模式;如果验证器太保守,又会扔掉有价值候选。
MiniMax 的方案是三种能力闭环。Proof Expert 写证明,Verifier Expert 读证明并输出结构化错误,Fixer Expert 根据 critique 修复证明。这些能力合并到 M3 后,MaxProof 在搜索时通过不同角色 prompt 激活。
验证器才是瓶颈
论文花了大量篇幅讲 false positive 和 reward hacking。早期 M2 周期中,单 rubric 生成式验证器会奖励更长、更会迎合格式和 judge 偏好的证明,但独立专家会否定这些证明。在 30 个训练验证器给满分的 rollout 中,专家只标了 17% 正确,50% 部分正确,33% 错误。
这个失败直接塑造 M3 verifier。它使用 bad-case filtering、solution normalization、多 rubric 与 no-rubric judge,再做 pessimistic aggregation。目标不是静态 benchmark 上最高准确率,而是在长时间训练和搜索循环里压低 false-positive rate。
这也是 MaxProof 比普通 best-of-N 更值得看的地方。它承认数学证明的评分信号会污染训练,所以把「如何不被验证器骗过」当成系统设计核心,而不是事后补一个 judge。
关键结果
- 竞赛分数: MaxProof 报告 IMO 2025 为 35/42,USAMO 2026 为 36/42。
- IMO 细节: IMO 2025 的 P1 到 P5 都达到 7/7,P6 为 0/7。
- USAMO 细节: USAMO 2026 有四题 7/7,P3 为 6/7,P2 虽然 archive 里有 6/7 oracle candidate,但 self-pick 只有 2/7。
- 搜索配置: 典型设置为 32 个初始候选、每个候选 4 次 verifier sample、10 轮 refinement、每轮 4 个新 child。
- reward hacking 证据: 论文记录了 length bias、format hacking、semantic shortcut、judge-specific preference 四类失败模式。
为什么群体搜索有效
MaxProof 试图把 best-of-many 能力转成更稳定的最终答案。它维护 candidate archive,用保守 verifier fitness 打分,选择多样化 parent,并提供两种修复:PATCH 针对 verifier 指出的具体错误做局部修复,REWRITE 在路线卡住时换一条证明路线。
但最终选择仍会失败。USAMO P2 是最有价值的反例:archive 中出现过 6/7 候选,但系统自己选择了 2/7,因为 tournament ranker 更偏好一个较差证明。这说明剩余问题不只是生成能力,还有 verifier score 接近时的选择可靠性。
局限与存疑
最大局限是计算和协议。32 个候选、多轮 refinement、多次 verifier sample 的系统级结果,不能随便和单次 pass@1 模型分数对比。论文还依赖生成式验证和专家式 judge,而它自己也承认这里会出错。
第二个问题是可复现性。M3 模型释放是一回事,但 contest-style 评测还依赖 prompt、verifier sampling、tournament 设置和评分流程。开发者更应该把 MaxProof 看成证明搜索蓝图,而不是只看榜单数字。
常见问题
MaxProof 是什么？
MaxProof 是用于数学证明的群体级 test-time scaling 框架。它让模型生成、验证、修复和排序候选证明,再通过搜索输出最终证明。
MaxProof 在 IMO 2025 和 USAMO 2026 得分多少？
论文报告 MaxProof 在 IMO 2025 得到 35/42,在 USAMO 2026 得到 36/42,都超过金牌线。
为什么 MaxProof 不是单模型分数？
因为它使用多个候选证明、多次 verifier sample、多轮修复和最终 tournament selection。这个成绩测的是围绕 M3 的证明搜索系统。
MaxProof 最清楚的短板是什么？
verifier 和 ranker 噪声仍然会伤害结果。USAMO 2026 P2 中,archive 里有 6/7 候选,但系统最终选了 2/7 证明。
一句话:MaxProof 的重要性在于它把数学证明看成 verifier noise 下的搜索问题,而不是一次性推理表演。阅读 arXiv 原文。