5 月 1 日消息，深度求索（DeepSeek）昨日在 AI 开源社区 Hugging Face 上发布了名为 DeepSeek-Prover-V2-671B 的新模型，并在 GitHub 等平台上公布了相关论文信息。该模型专注于形式化数学推理，旨在提升数学定理证明的能力。
DeepSeek-Prover-V2 是一款基于 DeepSeek-V3-0324，通过递归定理证明管道生成初始数据的开源大型语言模型。DeepSeek 推出了 DeepSeek-Prover-V2-671B（结合 V3 基础大模型）、DeepSeek-Prover-V2-7B（增强模型）两个模型，以及 DeepSeek-ProverBench 数据集。DeepSeek-Prover-V2-671B 采用和 DeepSeek V3-0324 相同的架构，并非用于常规对话或者推理，而是用于形式化定理证明、专门增强数学能力的模型。
DeepSeek 团队首先引导 DeepSeek-V3 模型将复杂定理分解为一系列子目标（subgoals），整合非形式与形式化数学推理，在 Lean 4 平台上形式化证明步骤。接着，利用一个较小的 7B 参数模型处理子目标的证明搜索，减轻计算负担。最终，结合完整的逐步证明与 DeepSeek-V3 的思维链（chain-of-thought），形成强化学习的 “冷启动” 数据。
在训练过程中，团队筛选出一批 7B 模型无法直接解决但子目标已被证明的难题，通过整合子目标证明，形成完整的形式化证明，并与 DeepSeek-V3 的推理过程对接，生成合成数据。随后，模型微调这些数据，并通过强化学习进一步提升能力，以二元反馈（正确或错误）作为奖励机制。最终，DeepSeek-Prover-V2-671B 在神经定理证明领域创下新高，在 MiniF2F-test 数据集上通过率达 88.9%，在 PutnamBench 数据集中解决 658 个问题中的 49 个。
团队还发布了 ProverBench 基准数据集，包含 325 个形式化数学问题。其中，15 个问题源自近期 AIME 竞赛（AIME 24 和 25），涉及数论与代数，代表高中竞赛难度。其余 310 个问题则来自精选教材和教学内容，涵盖线性代数、微积分、概率等多个领域。这一数据集旨在为高中竞赛和本科数学提供全面评估标准，推动模型在多样化场景下的测试与应用。
DeepSeek-Prover-V2-671B 的发布，标志着形式化数学推理领域的重大进步。通过先进的模型架构和强化学习技术，该模型在神经定理证明领域取得了显著成绩。发布的 ProverBench 数据集也为教育和竞赛提供了重要的评估标准，推动了模型在多样化场景中的应用和测试。
