32B超越671B，M-A-P全开源数学定理证明模型OProver，五项评测三项第一
OProver：让AI学会“改卷子”的数学证明机器
传统AI证明系统就像个只会“一次性写完答案”的学生——给一个题目，它一口气写出一段完整证明，交给Lean 4编译器验证，不行就重新写一份完全不同的，反复碰运气。这种“抽签式”证明效率极低，因为模型从不知道自己的答案错在哪里。
M-A-P研究团队推出的OProver彻底改写了规则：它让AI既能写证明，更能从每轮失败中“看懂”Lean编译器给出的具体错误提示，然后有针对性地修改，直到通过验证。就像学生把草稿交给一位严格到极致的老师，老师会明确指出“第7行类型不对，第12行函数未定义”——OProver做的就是把这些诊断信号内化为自身能力，让模型在训练阶段就学会如何根据反馈进行局部修正，而不是推理时才临时拼凑。
OProofs：一座记录失败与修正的数学证明档案馆
如果现有数学证明数据集是只收藏精装成品的图书馆，那么OProofs就是保留从草稿到终版全部修改历史的“出版社档案室”。这个由M-A-P团队构建的数据集包含约177万条Lean 4定理陈述和686万条经过验证的正确证明，但真正让它与众不同的是额外记录的“过程”信息：433万条证明带有检索上下文，86.9万条证明带有所次失败时收到的编译器错误信息，以及107万条完整的证明推进轨迹（其中16.4万条包含至少一次失败-修改循环）。
这些数据来自三个渠道：整理现有开源Lean资源并用证明器重新验证；从CommonCrawl网页和GitHub中自动筛选数学内容并转写为形式化陈述；以及OProver自身在训练中使用过程中产生的新证明和修改轨迹——随着模型能力提升，数据库不断扩充，形成良性循环。OProofs覆盖代数、分析、数论、几何等广泛领域，难度从初等算术到研究生级别，是目前唯一同时提供正式陈述、验证证明、自然语言推理过程、编译器错误反馈、检索上下文和多轮修改监督信号六个维度信息的公开数据集。
OProver的训练秘诀：从侦探查案到自我修炼的螺旋上升
OProver的工作方式可以形象地比作侦探破案：接到定理题目后，首先通过语义相似度模型（Qwen3-8B-Embedding）从OProofs数据库中检索最相似的已验证证明作为参考，这一步叫做检索增强；然后核心模型综合定理和参考，输出一段完整Lean 4证明代码；接着让Lean 4编译器充当“终极验证官”，要么通过，要么给出详细失败诊断；收到诊断后，OProver不会全盘推翻，而是进行局部修改，继续提交。系统每轮只记住最近一次的失败证明和对应错误，避免被历史信息淹没，让模型聚焦在最关键的问题上。
训练过程分为两大阶段：第一阶段是“通识教育”，在650亿token的混合数据（形式化数学、代码、数学推理、长思维链）上进行持续预训练，产出一个具备数学和编程基础素养的OProver-Base。第二阶段是“实战演练”，包含监督微调和强化学习的迭代后训练。监督微调收集“单轮修改样本”——（当前定理，参考证明，上一次失败的证明，Lean错误信息）→（修改后新证明）这样的四元组，让模型学会“如何改”；强化学习使用群序列策略优化（GSPO），对每道题生成多组多轮尝试，按每轮是否通过Lean验证赋予奖励，让模型同时从“不同尝试之间”和“同一尝试内不同轮次之间”两个维度学习对比。每轮训练完成后，新发现的证明和修改轨迹被送回数据库，用作下一轮的新素材——这个“训练-使用-反馈-再训练”的循环，就像侦探每破一案后都把侦破过程整理成教学案例，自身再学习一遍，档案室越来越丰富，侦查能力螺旋上升。
32B碾压671B：五项评测三项第一的成绩单
OProver-32B在五个主流数学定理证明测试集上的表现令人瞩目：MiniF2F（高中竞赛题）93.3%、ProverBench（竞赛+本科题）58.2%、PutnamBench（美国顶级本科竞赛题）11.3%，这三项均是所有开源整体证明模型中的最高分；在MathOlympiadBench上获得22.8%、ProofNet上33.2%，均为第二名。综合排名3个第一、2个第二，优于所有参与对比的开源模型。
对比具体数字更能体会差距：之前最强的开源模型DeepSeek-Prover-V2-671B（6710亿参数）在MiniF2F上仅82.4%，在PutnamBench上3.3%；OProver-32B参数量只有其约二十分之一，却在这两项上分别高出近11个和8个百分点。另一劲敌LongCat-Flash-Prover（5600亿参数混合专家模型，实际激活约270亿）在启用工具集成推理后在MathOlympiadBench上得到27.5%，略超OProver-32B的22.8%，这是OProver-32B唯一被超越的项目。较小的OProver-8B同样出色，在五套测试集上全部高于参数量是其四倍的Goedel-Prover-V2-32B，证明能力提升主要来自架构设计而非参数规模。
研究还探讨了“深度与广度如何分配”：在总预算固定时，对于MiniF2F等中等难度测试集，增加修改轮次（深度）能持续提升成功率，“16轮修改+相应数量独立尝试”是最优策略；但在极难的PutnamBench上，单次尝试成功率仅5%-11%，此时过多深度会挤占“广撒网”的独立尝试空间，所以“8轮修改”比“16轮”效果更好——难题应该多试方向，而非在一个方向上死磕。
消融实验揭示：多轮反馈才是真正的“纠偏神器”
为了量化核心组件贡献，研究团队做了系统的消融实验：首先拿掉多轮编译器反馈（让模型只生成一轮证明，不做任何修改，保留检索），成绩断崖式下降——OProver-32B在MiniF2F从93.3%降到88.4%，在ProofNet从33.2%降到25.8%，在PutnamBench从11.3%降到7.0%。在此基础上再拿掉检索（既不修改也不查参考），成绩进一步下降，但幅度明显更小。这说明多轮编译器反馈是性能提升的最主要来源，检索提供的是“出发前的方向感”，而编译器反馈提供的是“走错路之后的纠偏信号”，对于复杂证明，纠偏能力更为关键。
后训练迭代效果同样直观：OProver-8B经过三轮迭代，从持续预训练后的79.5%提升到91.8%，共提升12.3个百分点；OProver-32B经过两轮迭代，从84.7%提升到93.3%，提升8.6个百分点。每轮新数据和模型能力形成的正反馈，让这一数字单调递增，证明“把新证明和修改轨迹反馈回训练”的思路是可持续的。这项研究给AI证明领域指出了明确方向：真正有价值的不是堆积正确答案，而是记录“为什么失败、如何修正”的过程数据。OProver-32B以32B参数超越20倍于己的模型，证明在合适训练框架下，能力上限远比参数规模更能决定未来。