前些天到处都在流传着 DeepSeek-R2 即将发布的传言，DeepSeek 确实有新动作，不过大家没等来 R2，等来的是 DeepSeek-Prover-V2，它当然也是开源的。
Prover-V2 在定理证明赛道上实现了业内最佳性能，在 MiniF2F 测试中达到了 88.9% 的通过率，在 AIME 24、25 上也有不错的分数。在 4 月 30 日晚，机器学习协作平台 HuggingFace 上就更新了 DeepSeek-Prover-V2 的一些技术细节。
这次 DeepSeek 团队发布了两个版本的 DeepSeek-Prover-V2 模型，参数规模分别为 7B 和 671B。其中，DeepSeek-Prover-V2-671B 是在 DeepSeek-V3-Base 基础上训练而成，而 DeepSeek-Prover-V2-7B 则基于 DeepSeek-Prover-V1.5-Base 构建，并支持最长 32K tokens 的上下文长度扩展。
- DeepSeek-Prover-V2-7B 链接：DeepSeek-Prover-V2-7B
- DeepSeek-Prover-V2-671B 链接：DeepSeek-Prover-V2-671B
要一句话总结 DeepSeek-Prover-V2 到底是什么？它是一款专为「数学 AI 编程语言」Lean 4 打造的开源大语言模型，专注于形式化定理证明。
它的初始化数据通过一个由 DeepSeek-V3 驱动的递归定理证明流程收集而来。在冷启动训练阶段，首先通过提示 DeepSeek-V3 将复杂问题分解成一系列可以解决的子目标。每解决一个子目标就会将这些证明整合成「思维链」。并融合 DeepSeek-V3 的逐步推理轨迹，共同构建出用于强化学习的初始训练数据。
这一策略的精妙之处在于：它能够将非形式化和形式化的数学推理融合到一个统一的模型中，让模型既能像人一样灵活思考，也能像机器一样严谨论证，真正实现了数学推理的一体化融合。
技术概述#
通过递归式证明搜索生成冷启动推理数据#
为了构建冷启动数据集，DeepSeek 团队设计了一条简洁高效的递归定理证明流程，使用 DeepSeek-V3 作为统一工具，既负责子目标的拆解，也负责推理步骤的形式化表达。其中具体的过程则是通过提示引导 DeepSeek-V3 将定理拆解为高层次的证明草图，并在此过程中同时将这些推理步骤用 Lean 4 语言形式化，最终生成一系列结构清晰、逻辑严密的子目标。
DeepSeek-Prover-V2 使用冷启动数据收集过程概览。降低计算开销一直是 DeepSeek 团队的强项，这次也不例外。他们使用一个更小的 7B 模型来完成每个子目标的证明搜索，从而降低计算负担。当复杂问题被拆解的各个步骤都成功解决后，他们将完整的形式化逐步证明与 DeepSeek-V3 生成的思维链相对应，组合成冷启动推理数据。
基于合成冷启动数据的强化学习#
DeepSeek 团队挑选了一部分具有挑战性的定理问题。7B 证明模型虽然没法将它们端到端的解决，但是能够拿捏拆解出来的一系列子目标。整合所有子目标的证明就可以构建出原始问题的完整形式化证明。随后，将该正式证明附加到 DeepSeek-V3 所生成的思维链，这条思维链展示了对应的引理拆解过程，从而形成了一份将非形式化推理与后续形式化过程紧密融合的训练数据。
在对证明模型进行合成冷启动数据的微调后，研究团队进一步引入强化学习阶段，进一步提升模型将非形式化推理转化为形式化证明的能力。在训练过程中，遵循推理模型的通用目标，采用「对 / 错」二值反馈作为主要的奖励信号。
最终得到的模型 DeepSeek-Prover-V2-671B 在神经定理证明任务中达到了当前最先进的性能，在 MiniF2F-test 上的通过率达到 88.9%，并成功解决了 PutnamBench 数据集中 658 道题中的 49 道。DeepSeek-Prover-V2 在 miniF2F 数据集上生成的所有证明已整理为 ZIP 文件，开放下载。
- 下载链接：miniF2F 解决方案