DeepSeek-Prover-V2 登场：AI 数学推理新王者，88.9% 通过率设新标杆

图片地址：https://img.ithome.com/newsuploadfiles/2025/5/e0437141-c17d-4052-8119-f8819ad2eb68.jpg?x-bce-process=image/format,f_auto

IT之家 5 月 1 日消息，深度求索（DeepSeek）昨日（4 月 30 日）在 AI 开源社区 Hugging Face 上，发布名为 DeepSeek-Prover-V2-671B 的新模型，随后在 GitHub等平台上公布了论文信息。IT之家援引论文介绍，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 模型无法直接解决但子目标已被证明的难题。通过整合子