首页 > 科学

DeepSeek新数学模型刷爆记录！7B小模型自主发现671B模型不会的新技能

DeepSeek 放大招！新模型专注数学定理证明，大幅刷新多项高难基准测试。

在普特南测试上，新模型 DeepSeek-Prover-V2 直接把记录刷新到49 道。

目前的第一名在 657 道题中只做出10 道题，为 Kimi 与合作成果 Kimina-Prover。

而未针对定理证明优化的 DeepSeek-R1 只做出1 道。

让还没发布的 R2 更令人期待了。

除测评结果之外，论文中特别报告了 " 通过强化学习发现新技能 " 现象。

正如 R1 带来了 " 啊哈时刻 "，Prover-V2 也有令人意想不到的能力。

具体来说，在普特南测试中，参数量较小的 DeepSeek-Prover-V2-7B 用非 CoT 生成模式成功解决了 13 个 671B 模型未能解决的问题。

团队仔细检查该模型的输出后发现，其推理方法存在一个独特模式：7B 模型处理涉及有限基数的问题时，经常使用 Cardinal.toNat 和 Cardinal.natCast_inj，而 671B 模型生成的输出中明显没有这些内容。

要注意，7B 模型是在 DeepSeek-Prover-V1.5-Base 模型基础上，先使用 671B 模型在强化学习阶段收集的数据微调，再执行强化学习得来的。

也就是说，7B 模型学会了 671B 模型没有学会的新技能。

那么，DeepSeeK-Prover-V2 如何炼成的呢？与前代相比又有哪些改进？

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

DeepSeek 数学定理证明 DeepSeek-Prover 系列模型已推出 3 款：

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。

整合 DeepSeek-V3 的高上下文窗口和强大的自然语言推理能力，把形式化和非形式化数学证明统一到一个模型中。

Prover-V2 还继承了 Prover-V1.5 提出的 CoT 和非 CoT 生成两种模式。

接下来，详细介绍 Prover-V2 的各主要环节。

通过递归证明搜索合成冷启动推理数据

利用 DeepSeek-V3 作为子目标分解和形式化的统一工具构建冷启动数据集，提示 DeepSeek-V3 将定理分解为高级证明草图，同时在 Lean 4 中将这些证明步骤形式化，从而产生一系列子目标。

使用一个较小的 70 亿参数模型来处理每个子目标的证明搜索，从而减轻相关的计算负担。一旦一个具有挑战性的问题的分解步骤得到解决，就将完整的逐步形式化证明与来自 DeepSeek-V3 的相应思维链进行配对，以创建冷启动推理数据。

使用合成冷启动数据进行子目标分解的强化学习

团队精心挑选了一组具有挑战性的问题，这些问题无法由 70 亿参数量的证明器模型以端到端的方式解决，但所有分解后的子目标都已成功解决。

通过组合所有子目标的证明，为原始问题构建了一个完整的形式化证明。

然后，将此证明附加到 DeepSeek-V3 的思维链中，该思维链概述了相应的引理分解，从而实现了非形式化推理与后续形式化的有机结合。

在合成冷启动数据上对证明器模型进行微调后进行强化学习阶段，进一步增强其将非正式推理与形式化证明构建相衔接的能力。遵循推理模型的标准训练目标，使用二元的正确或错误反馈作为奖励监督的主要形式。

具体训练细节

两阶段训练：

DeepSeek-Prover-V2 分两阶段建立互补证明生成模式。

第一阶段用高效非思维链（non-CoT）模式，聚焦快速生成 Lean 证明代码，加快迭代和数据收集。

第二阶段基于第一阶段成果，采用高精度思维链（CoT）模式，阐述中间推理步骤，用冷启动思维链数据强化学习，提升复杂问题推理能力。

专家迭代：

其中非 CoT 模式训练遵循专家迭代范式，用最佳证明策略为难题生成证明尝试，经 Lean 验证，成功的纳入监督微调（SFT）数据集。与之前版本相比，训练问题分布有调整，引入了额外问题和子目标分解生成的问题。

监督微调：

对 DeepSeek-V3-Base-671B 做监督微调，训练语料库包含两个互补来源的数据：

一是通过专家迭代收集的非 CoT 数据，这些数据生成的 Lean 代码不包含中间推理步骤，主要用于强化模型在 Lean 定理证明生态系统中的形式验证技能。

二是冷启动 CoT 数据，这些数据将 DeepSeek-V3 的先进数学推理过程提炼为结构化的证明路径，明确地模拟了将数学直觉转化为形式证明结构的认知过程。

强化学习：

采用 GRPO 算法，与传统的 PPO 不同，GRPO 无需单独的裁判模型，它通过为每个定理提示采样一组候选证明，并根据它们的相对奖励来优化策略。

训练过程中使用二元奖励机制，即生成的 Lean 证明若被验证正确则获得奖励 1，否则为 0。

为确保学习效果，精心挑选训练提示，仅包含那些有足够挑战性但又能被监督微调后的模型解决的问题。

蒸馏 DeepSeek-Prover-V2 7B

将 DeepSeek-Prover-V1.5-Base-7B 上下文窗口扩展到 32768 个 token，用 DeepSeek-Prover-V2-671B 数据微调，融入非 CoT 证明数据，以便利用小模型生成简洁的形式化输出，提供一种经济高效的证明选项。

此外，对 DeepSeek-Prover-V2-7B 执行与 671B 模型训练中相同的强化学习阶段，以进一步提升其性能。

ProverBench：AIME 和教科书问题的形式化

与 Prover-V2 一起推出 ProverBench，这是一个包含 325 个问题的基准数据集。其中，有 15 个问题是从近期美国数学邀请赛（AIME 24 和 25）的数论与代数题目中形式化而来，提供了真实的高中竞赛水平挑战。其余 310 个问题则取自精心挑选的教科书示例和教学教程，构成了一套多样化且基于教学需求的形式化数学问题集合。该基准旨在能够对高中竞赛问题和本科阶段数学问题进行更全面的评估。