DeepSeek-Prover：基于强化学习的数学定理证明模型，在普特南测试与miniF2F中展现卓越性能，7B参数小模型竟自主发现连671B大模型也望尘莫及的新技能！

DeepSeek再次展现强大实力！全新推出的数学定理证明模型大幅提升了多个高难度基准测试的表现。在普特南测试中，新模型DeepSeek-Prover-V2成功解决了49道题目，成为当前表现最为突出的模型之一。相比之下，目前排名第一的Kimina-Prover（由Kimi与AIME2024冠军团队Numina合作开发）仅在657道题中解出10道。而未针对定理证明优化的DeepSeek-R1则仅解出1道题，这使得尚未发布的R2备受期待。

此外，在研究论文中还特别提到了“通过强化学习发现新技能”的现象。例如，参数量较小的DeepSeek-Prover-V2-7B在非链式思维（non-CoT）生成模式下，成功解决了671B模型未能解决的13个问题。经过深入分析发现，7B模型在处理有限基数相关问题时，频繁使用Cardinal.toNat和Cardinal.natCast_inj，而671B模型的输出中并未包含这些。这一现象表明，7B模型通过强化学习掌握了671B模型未能学会的新技能。

那么，DeepSeek-Prover-V2是如何实现如此卓越性能的呢？它与前代相比有哪些改进？

统一形式化与非形式化数学证明的模型

DeepSeek-Prover系列目前已推出三款模型：
– 2024年3月的DeepSeek-Prover（简称Prover-V1）
– 2024年8月的DeepSeek-Prover-V1.5（简称Prover-V1.5）
– 2025年5月的DeepSeek-Prover-V2（简称Prover-V2）

Prover-V1主要探索了通过大规模合成数据集微调DeepSeek-Math-7B来推进定理证明的能力。Prover-V1.5在此基础上增加了证明助手反馈的强化学习（RLPAF）和蒙特卡洛树搜索方法。而Prover-V2则进一步引入了“子目标分解的强化学习”，并且将基础模型从DeepSeek-Math-7B升级到DeepSeek-V3，实现了形式化与非形式化数学证明的统一。

Prover-V2的主要环节

1. 递归证明搜索合成冷启动推理数据
利用DeepSeek-V3作为子目标分解和形式化的统一工具，构建冷启动数据集。通过提示DeepSeek-V3将定理分解为高级证明草图，并在Lean 4中形式化这些步骤，从而生成一系列子目标。随后，使用一个较小的70亿参数模型进行每个子目标的证明搜索，以减少计算负担。

2. 使用合成冷启动数据进行强化学习
精心挑选一组具有挑战性的问题，这些问题无法通过70亿参数证明器模型以端到端方式解决，但所有分解后的子目标均已成功解决。通过组合所有子目标的证明，为原始问题构建完整的形式化证明。然后，将此证明附加到DeepSeek-V3的思维链中，实现非形式化推理与形式化的有机结合。

3. 两阶段训练
– 第一阶段采用高效非链式思维（non-CoT）模式，专注于快速生成Lean证明代码，加快迭代和数据收集速度。
– 第二阶段基于第一阶段成果，采用高精度链式思维（CoT）模式，阐述中间推理步骤，利用冷启动思维链数据进行强化学习，提升复杂问题的推理能力。

4. 专家迭代与监督微调
非CoT模式训练遵循专家迭代范式，通过最佳证明策略为难题生成证明尝试，并经Lean验证后纳入监督微调（SFT）数据集。监督微调数据来源包括通过专家迭代收集的非CoT数据和冷启动CoT数据。

5. 强化学习与模型蒸馏
使用GRPO算法进行强化学习，无需单独的裁判模型，而是通过为每个定理采样一组候选证明并根据其相对奖励优化策略。此外，DeepSeek-Prover-V2-7B通过对DeepSeek-Prover-V2-671B的数据进行蒸馏，融合非CoT证明数据，提供一种经济高效的证明选项。

基准测试与成果

Prover-V2在miniF2F测试中的通过率达到88.9%，并在普特南测试中成功解决49道题目。同时，DeepSeek还推出了ProverBench基准数据集，包含325个问题，涵盖高中竞赛水平和本科阶段数学问题，为评估模型性能提供了全面的参考。

团队与社区反响

Prover-V2的研发团队共有18人，核心成员包括Z.Z. Ren、邵智宏、辛华剑等，他们曾参与过DeepSeek多个重要项目。新加入的研究者如Shirong Ma、Zhe Fu、Yuxuan Liu也为项目贡献了关键力量。

Prover-V2发布后迅速引发广泛关注，GitHub仓库在12小时内获得350+星标。普林斯顿大学助理教授Chi Jin表示：“恭喜这项惊人的工作！在miniF2F上攻克最后10%-20%的问题标志着能力上的重大飞跃。”网友们最关心的问题仍然是：“R2什么时候发布？”

本文来源：