这项来自**Multimodal Art Projection（M-A-P）研究社区**的研究成果发表于2026年5月，论文编号为arXiv:2605.17283v1，有兴趣深入了解的读者可通过该编号在arXiv平台查询完整论文。M-A-P是一个非营利性开源人工智能研究社区，依靠捐助运营，专注于基础模型预训练、大规模数据处理以及编程、推理等应用方向。
一、先从一道数学题说起
假设你要在一张纸上证明一个数学定理，写完之后交给一位严格到极致的老师审阅。这位老师不会给你模糊的评语，而是精确地告诉你：第7行这里类型不对，第12行那个函数根本不存在，第15行逻辑跳跃了——然后把卷子还给你，让你继续改。你一轮一轮地改，每次都能从老师的具体指摘中学到东西，直到整道题无懈可击。
这个"改卷子"的场景，正是本文要介绍的OProver系统的核心工作方式。只不过扮演"学生"的是一个人工智能模型，扮演"严格老师"的是一套叫做Lean 4的形式化数学验证系统，而"卷子"则是一条条需要严格证明的数学定理。
形式化定理证明是一个听起来陌生但意义重大的领域。简单来说，它要求人们（或机器）把数学证明写得严格到每一个逻辑步骤都能被计算机核查——不是大概对，不是直觉上没问题，而是必须通过一个极其苛刻的自动验证程序。Lean 4就是这样一套验证系统，它就像数学界的"终极裁判"，只接受百分之百正确的答案。
现有的AI定理证明系统大多采用一种叫做"一次性生成"的策略：给模型看一个题目，让它一口气写出一个完整的证明，然后交给Lean验证，通过则通过，不通过就重新生成一个完全不同的证明，反复抽签碰运气。这种方式就像让人在不知道评分标准的情况下盲写答案，效率相当低。
M-A-P团队提出的OProver走了一条完全不同的路：让AI不仅能写证明，更能从失败中学习并修改，而且这个"修改能力"是通过专门训练得到的，而非临时拼凑的。这套系统在五个主流数学竞赛和大学级别的测试集上创下了开源模型的最好成绩。
二、为什么"一次性生成"不够用
要理解OProver解决的问题，得先弄清楚以前的系统卡在哪里。
当AI模型试图证明一个数学定理时，它本质上是在写一段特殊的"程序代码"，这段代码必须满足Lean 4的严格语法和逻辑规则。一个典型的证明可能包含几十甚至上百个步骤，任何一步出错——哪怕是变量名拼错、函数类型不对、或者两个数学对象的类型不兼容——整个证明都会被否定。
过去的主流做法是训练模型看大量"正确证明"，让它学会一次就写出完整答案。这就好比训练一个厨师的方式是只让他吃成品菜，从不告诉他哪些食材组合会失败，也不允许他在厨房里试错。这样训练出来的厨师面对新菜谱时，只能靠运气。
更深层的问题在于：模型在训练时看到的都是"最终成品证明"，但在实际使用时，它需要应对的情况是"写了一半失败了、Lean告诉我哪里错了、如何修改继续"。训练时的经历和使用时的处境完全不同，就像在泳池里练了一年的游泳姿势，结果被扔进了大海。
OProver团队把这个问题称为"训练与推理的不匹配"——模型在训练期间从来没见过Lean的错误提示，没有练习过如何根据反馈修改证明，所以即便临时给它看一些错误信息，它也不知道该怎么用。
解决方案听起来直觉上非常合理：从一开始就把"看着错误信息修改证明"这件事训练进模型里。但要做到这一点，需要两样东西——大量包含失败过程和修改轨迹的训练数据，以及一套能让这种训练循环运转的系统。这就是OProver和它配套的数据集OProofs诞生的原因。
三、OProofs：不只收藏正确答案，更记录"失败与重来"的过程
如果把现有的数学证明数据集比作一座图书馆，那这座图书馆里摆的全都是精装版的完成品——每一本书都是完美的最终版本，书店里买不到任何草稿、修改记录或被编辑否定的版本。OProofs的设计思路则是把这座图书馆改造成一个"出版社档案室"，不仅存放成品，还保留了从最初草稿到最终版本之间每一轮修改的完整历史。
OProofs数据集包含约177万条Lean 4数学定理陈述，以及686万条经过Lean编译器验证的正确证明。这些数字本身已经相当可观，但真正让OProofs与众不同的是它额外记录的信息：433万条证明带有"检索上下文"（也就是在写这条证明之前，系统去资料库里查到了哪些相似的参考证明），86.9万条证明带有之前失败时收到的编译器错误信息，以及107万条完整的"证明推进轨迹"，其中有16.4万条轨迹包含至少一次失败-修改循环，由此衍生出28万条"单轮修改训练样本"。
这些数据来自三个渠道。第一个渠道是整理现有的公开Lean资源，包括NuminaMath-LEAN、Lean-Workbook、Leanabell-FormalStmt、Goedel-Pset等多个开源数据集，团队对这些资源进行去重和筛选，然后用现有开源证明器对每条定理进行证明，只保留通过Lean验证的结果。第二个渠道是从互联网原始数学资料出发：用一个文本分类器从CommonCrawl网页和GitHub代码库中筛出数学内容，再通过一个叫做CriticLean的工具把这些自然语言数学陈述自动转写成Lean 4的形式化陈述，然后同样通过证明器生成并验证证明。第三个渠道则是OProver自身在训练和使用过程中产生的新证明和修改轨迹——随着模型能力提升，它会不断产生新的有效证明，这些证明随即被加入数据库，形成良性循环。
整个数据集覆盖了广泛的数学领域：代数占59.5%，分析学占13.8%，数论占13%，几何占6.8%，其余6.9%涵盖组合数学、逻辑、概率、拓扑和计算数学。难度分布从初等算术（27.1%）到高中数学（48.9%）、本科数学（19.2%）再到研究生级别（4.8%）。
与已有的同类数据集相比，OProofs的独特之处在于它是迄今为止唯一同时提供了正式陈述、验证证明、自然语言推理过程、编译器错误反馈、检索上下文以及多轮修改监督信号这六个维度信息的公开数据集。最接近的竞争者是Nemotron-Math-Proofs，它提供了前四项，但缺少检索上下文和多轮修改数据。
四、OProver如何工作：像侦探一样找线索、问证人、修正推断
OProver的证明过程可以用"侦探破案"这个框架来理解，而且这个比喻会贯穿接下来的所有描述。
每当OProver收到一道需要证明的数学定理，就相当于侦探接到了一个新案子。在开始推理之前，侦探要做的第一件事不是立刻凭空推断，而是去档案室查阅与这个案子最相似的历史案例——看看以前有没有类似的犯罪手法、相似的作案地点、可以复用的侦查方法。
在OProver里，这个"查档案"的步骤叫做检索增强。系统会把当前要证明的定理陈述送入一个专门训练的语义相似度模型（具体用的是Qwen3-8B-Embedding，这个选择经过了与另一个候选模型的严格对比测试：在1000个查询、9000个候选文档的评测中，用GPT-4o做裁判，Qwen3-8B-Embedding在667次对比中胜出），从OProofs数据库里找出最相似的几条已验证证明作为参考。这些参考证明就像侦探手头的"相似案件档案"，能给出有价值的方向提示：这类问题通常用什么数学工具、惯常的证明结构是什么、哪些引理可能有用。
接下来，侦探（也就是OProver的核心语言模型）综合手头的定理陈述和参考档案，给出一个初步的"破案推断"——也就是一段完整的Lean 4证明代码。然后，这段证明被交给Lean 4编译器这位"终极验证官"审查。
如果审查通过，案子结了，这条证明会被记录下来并加入档案库。如果审查不通过——这是大多数情况——验证官会给出详细的失败诊断：可能是某个变量类型不对，可能是某个数学函数在当前上下文中未定义，可能是某个战术步骤的前提条件不满足，可能是某个子目标没被完全解决。这些诊断信息就是侦探收到的"新证词"。
收到新证词之后，侦探不会把之前所有的推断全部推倒重来，而是针对问题进行局部修正，调整证明思路，重新提交。这个"提交-反馈-修改"的循环会持续进行，直到证明通过验证，或者用完预设的轮次预算。
有一个关键的工程细节值得关注：OProver在每一轮只记住最近一次的失败证明和对应的错误反馈，而不是把所有历史轮次的内容都积累在一起。这么做的理由是，证明修改通常是"局部性的"——你需要修的是上一版里具体的问题，而不是从头梳理所有历史；而且保持输入简洁能让模型更清晰地聚焦在当前最关键的问题上，避免被大量历史信息淹没。
五、训练：让侦探真正学会"根据证词修正推断"
OProver的证明能力不是凭空来的，而是通过一套精心设计的两阶段训练获得的。
第一阶段是"通识教育"，也就是论文里所说的持续预训练。研究团队在650亿个token的混合数据上对基础模型进行继续训练，这些数据由四类内容混合而成：约30%是OProofs里的Lean形式化数学数据，约20%是来自OpenCoder项目的代码数据，约40%是来自Nemotron-Math-4-Plus的数学推理数据，约10%是来自ProLong-64K项目的长思维链数据。这个阶段产出的叫做OProver-Base，相当于一个"通过了基础培训、具备数学和编程素养"的侦探新人。
第二阶段是"实战演练"，也就是迭代后训练。这个阶段分为监督微调和强化学习两个环节，两者交替进行，而且每轮训练完成后，模型新发现的证明和修改轨迹会被送回数据库，作为下一轮训练的新素材。
监督微调环节的逻辑非常直接：让当前版本的OProver去实际证明一批还没被可靠解决的定理，在这个过程中收集"单轮修改样本"——也就是（当前定理，参考证明，上一次失败的证明，Lean给出的错误信息）→（修改后的新证明）这样的四元组。每一个这样的四元组都是一个具体的"从失败学习"的例子，告诉模型在面对这种错误时应该怎么修改。模型在这些数据上训练，计算损失时只关注"修改后的新证明"部分，让模型专注于学会"如何修改"而不是死记硬背具体内容。
强化学习环节使用一个叫做GSPO（群序列策略优化）的方法。对每道定理，系统会让当前模型生成多个完整的多轮证明尝试（论文设定是每道题生成8组尝试，每组最多进行若干轮修改）。每一个尝试的每一轮都会得到一个奖励分数：如果那一轮的证明通过了Lean验证，得分是0.8加上一个最高0.2的格式规范奖励；如果没通过，得分为0。然后把同一道题所有尝试的所有轮次的奖励放在一起，计算相对优势，告诉模型哪些做法比平均水平好、哪些比平均水平差。
这种设计的聪明之处在于，它让模型同时从两个维度学习对比：一是不同起始尝试之间的对比（这次完全成功了，那次从第一轮就走错了方向），二是同一个尝试内部不同轮次之间的对比（第三轮的修改把第二轮的错误纠正了，说明这种修改策略是有效的）。通过筛选"成功率既不为0也不为1"的定理用于强化学习，系统集中火力训练模型在"有时能解决、有时解决不了"的中等难度问题上，避免在已经完全掌握或完全无法企及的问题上浪费训练资源。
这个训练-使用-反馈-再训练的循环，就像侦探在每破了一个案子之后，都会把这个案子的侦查过程整理成教学案例，自己再学习一遍，并把这个案子的线索加进档案室供以后查阅——随着破案经验积累，档案室越来越丰富，下次查档时能找到的参考也越来越精准，整个侦查能力形成持续提升的螺旋。
六、在五个数学测试集上的实际表现
理解了OProver的工作原理之后，接下来看它在实际测试中的表现。研究团队在五个标准测试集上进行了评估，这五个测试集代表了不同难度层次的数学挑战。
MiniF2F是最广泛使用的高中数学竞赛问题集，共244道题。ProverBench包含325道题，涵盖数学竞赛和本科数学内容。ProofNet包含186道本科水平的定理，来自教科书的形式化版本。MathOlympiadBench包含360道近年数学竞赛题，难度更高。PutnamBench是难度最大的一个，包含672道普特南数学竞赛（美国顶级本科数学竞赛）题目。
评估指标用的是Pass@32，意思是：对每道题，让模型独立生成若干个证明尝试，如果其中任何32个里有至少一个成功，就算通过——这个指标衡量的是"给足够多机会时的成功率"。
OProver-32B（参数量32亿的大版本）在MiniF2F上达到了93.3%，在ProverBench上达到了58.2%，在PutnamBench上达到了11.3%，这三项都是所有开源整体证明模型（whole-proof prover，即不用战术树搜索而是直接生成完整证明的模型）中的最高分。在MathOlympiadBench上得到22.8%，在ProofNet上得到33.2%，这两项是第二名。综合来看，OProver-32B在五个测试集上的排名分布（3个第一、2个第二）比所有其他参与对比的开源模型都要好。
对比一些具体数字能更好地感受这些成绩的含义。DeepSeek-Prover-V2是目前最强的竞争对手之一，其671B（6710亿参数）版本在MiniF2F上得了82.4%，在PutnamBench上得了3.3%。OProver-32B的参数量只有它的约二十分之一，却在MiniF2F上高出将近11个百分点，在PutnamBench上高出8个百分点。另一个强劲对手LongCat-Flash-Prover是一个5600亿参数的混合专家模型（实际激活参数约270亿），在启用"工具集成推理"模式后在MathOlympiadBench上得到27.5%，略高于OProver-32B的22.8%，这是OProver-32B唯一被超过的项目。
OProver-8B（较小的8亿参数版本）的表现同样值得关注：它在五个测试集上的得分全部高于Goedel-Prover-V2-32B，而后者的参数量是它的四倍。这表明OProver的架构设计本身带来的提升是实质性的，而不仅仅依赖参数规模。
七、多花一点"思考时间"能得到多少额外收益
研究团队还仔细研究了一个实际应用中非常关键的问题：如果给OProver更多的计算资源，它的表现会如何变化？更直接地说，同样的算力预算，应该用来多尝试几个独立的证明方向，还是应该集中在一个方向上进行更多轮的修改？
研究发现，随着可用预算（即总尝试次数）的增加，OProver在所有五个测试集上的成功率都单调上升，但增速逐渐放缓——这是一个典型的"边际收益递减"现象。在MiniF2F上，当预算从8增加到256时，OProver-32B的成功率从87.5%提升到92.8%；在PutnamBench上，从6.4%提升到11.3%；在MathOlympiadBench上，从15.5%提升到22.0%。每次将预算翻倍，带来的收益都比上一次翻倍要小，但始终是正的，没有出现饱和停滞的情况。
更有意思的是"深度与广度如何分配"这个问题。当总预算固定时，可以选择用16轮修改、8个独立尝试的策略，也可以选择用8轮修改、16个独立尝试的策略，效果并不一样。
在MiniF2F、MathOlympiadBench、ProofNet和ProverBench这四个测试集上，随着修改轮次从1增加到16，成功率持续上升，说明在这些难度中等偏下的题目上，更深的迭代修改是有价值的。在这些测试集上，当总预算达到16或以上时，"16轮修改配合相应数量的独立尝试"是最优分配策略。
PutnamBench则表现出完全不同的规律。这个测试集的题目极难，OProver每一条独立的证明尝试链的单次成功率只有5%到11%。在这种情况下，把太多预算集中在单条链的深度修改上，会导致用于"广撒网"的独立尝试数量不足，从而损失更多可能性。数据显示，在PutnamBench上，当总预算16或以上时，"8轮修改"比"16轮修改"效果更好——以预算256为例，8轮修改版本达到11.3%，16轮修改版本只有10.7%。这个发现对实际部署很有参考价值：难题应该多试方向而不是在一个方向上死磕。
八、如果把修改能力和检索能力都拿掉，会差多少
为了量化OProver两个核心组件——多轮编译器反馈和检索增强——各自的贡献，研究团队专门做了消融实验，也就是系统地"拆掉"某个功能，看成绩下降多少。
拿掉多轮编译器反馈（让模型只生成一轮证明，不做任何修改，但保留检索功能），效果下降非常显著。OProver-32B在MiniF2F上从93.3%降到88.4%，在ProofNet上从33.2%降到25.8%，在MathOlympiadBench上从22.8%降到16.5%，在ProverBench上从58.2%降到52.0%，在PutnamBench上从11.3%降到7.0%。这说明多轮编译器反馈是OProver性能提升的最主要来源。
在此基础上再拿掉检索功能（让模型既不修改也不查参考），成绩进一步下降，但幅度明显小于拿掉多轮反馈的效果。OProver-32B在MiniF2F上从88.4%再降到87.9%，在MathOlympiadBench上从16.5%再降到14.8%，在ProofNet上从25.8%降到24.7%，在ProverBench上从52.0%降到51.1%，在PutnamBench上从7.0%降到5.9%。检索的贡献是真实存在的，但比起多轮反馈修改机制，它的作用相对次要。这符合直觉：检索提供的是"出发前的方向感"，而编译器反馈提供的是"走错路之后的纠偏信号"，对于复杂的证明，纠偏能力更为关键。
九、三轮训练迭代的成长轨迹
研究团队详细记录了OProver在不同训练迭代阶段的成绩变化，以MiniF2F-Test上的Pass@32为指标。
OProver-8B在仅完成第一阶段持续预训练（尚未进行迭代后训练）时，成绩是79.5%。经过第一轮后训练迭代，提升到86.2%。第二轮迭代后达到87.0%。第三轮迭代后最终达到91.8%。从起点到终点，三轮迭代带来了12.3个百分点的提升。
OProver-32B进行了两轮后训练迭代（因为更大的模型每轮训练成本更高）。持续预训练完成后的基础成绩是84.7%，第一轮后训练迭代后提升到88.1%，第二轮后达到93.3%，共提升8.6个百分点。
这个单调递增的曲线验证了一个重要假设：把新证明和修改轨迹反馈回训练数据并不断扩充，确实能让每轮训练都产生更强的模型，而不是在第一轮之后就陷入停滞。数据库越来越丰富、检索越来越准确、训练样本越来越多样——这三个因素形成了正反馈，让OProver的能力随着迭代持续上升。
十、整件事的意义在哪里
说到底，OProver解决的是一个"学生如何真正学会解题"的问题——不是靠背答案，而是靠在反复尝试和失败中积累真实的解题经验。
对于数学自动化领域来说，这项研究给出了一个清晰的方向：单纯堆积更多的正确证明数据，效果是有限的；真正有价值的是那些记录了"为什么失败、如何修正"的过程数据。正是因为现有数据集里几乎没有这类过程数据，以往的系统才始终停留在"靠运气生成正确答案"的阶段。
对于AI推理领域来说，OProver展示了一个具有说服力的证据：把"使用工具的能力"从推理时的临时增强变成训练时就内化进模型的政策，带来的收益是实质性的。这个思路不仅适用于数学证明，也可能适用于其他需要与外部验证工具交互的任务，比如代码调试、科学实验设计等。
归根结底，OProver-32B是一个32亿参数的模型，却在五个数学测试集上超过了多个远大于自身的模型，其中包括参数量超过自身20倍的模型。这个结果本身就说明，在合适的训练框架和数据支持下，能力的提升空间远比参数规模更能决定上限。
当然，即使是当前最好的系统，在PutnamBench这样的顶级难题集上，成功率也不超过12%。绝大多数竞赛数学中的高难度题目，对当前所有AI系统来说依然是艰难的挑战。OProver的工作是在这个方向上推进了一步，而不是宣布终点已到。对于真正感兴趣的读者，完整的论文、代码和数据集都以开源方式发布，论文编号arXiv:2605.17283v1，可供查阅和复现。
Q&A
Q1：OProver和普通的AI证明系统有什么区别？
A：普通AI证明系统通常是一次性生成完整证明，失败就重新生成，不会从失败中学习。OProver不同，它会把Lean编译器给出的具体错误信息直接反馈给模型，让模型有针对性地修改，而且这种"看着错误修改"的能力是在训练阶段就专门练出来的，而不是临时加上去的。
Q2：OProofs数据集比其他Lean数据集多了什么？
A：大多数现有Lean数据集只保存最终正确的证明，OProofs额外记录了证明过程中失败的尝试、Lean编译器给出的错误信息、修改过程，以及每次证明前检索到的参考资料。这些"失败与修正"的过程数据是训练模型学会自我修改能力的关键，目前其他公开数据集基本没有提供这类信息。
Q3：OProver在最难的数学题上表现怎么样？
A：在最难的测试集PutnamBench（美国普特南大学生数学竞赛题）上，OProver-32B的Pass@32成功率是11.3%，是所有参与对比的开源整体证明模型中最高的，但绝对数值依然较低，说明顶级竞赛数学对所有现有AI系统来说仍是重大挑战。
热门跟贴