模型发布与版本 - DeepSeek在Hugging Face正式发布DeepSeek-Prover-V2，同步上线模型卡及示例代码，共推出两个版本：7B和671B [1][4] - DeepSeek-Prover-V2-7B基于上一代V1.5模型，支持最长32K上下文输入 [4] - DeepSeek-Prover-V2-671B在DeepSeek-V3-Base基础上训练，推理性能最强 [4] 训练方法与技术 - 训练核心采用"递归+强化学习"组合，由DeepSeek-V3拆解复杂定理生成子目标和推理思路，再通过GRPO算法从候选方案中学习最优解 [3] - 训练分为两阶段：第一阶段采用"专家迭代"方法，模型通过解决难题反哺自身 [5]；第二阶段迁移DeepSeek-V3数学知识并引入形式化数据，构建复杂推理路径 [6] - GRPO强化学习算法引导模型在32个候选证明方案中选择被Lean验证系统判定为正确的答案（奖励1分，否则0分） [8][9] 模型能力与特点 - 671B模型能力被"蒸馏"到7B模型，使小模型在资源有限设备上获得接近大模型的数学推理能力 [10][11] - 提供两种解题风格：快速模式（non-CoT）直接生成精炼答案；逻辑模式（CoT）详细展示推理过程 [12] - DeepSeek-V3负责拆解定理生成推理草图，7B模型完成子证明并拼接完整推理，形成"模糊思考+精确证明"机制 [14][15] 性能评估与数据集 - DeepSeek-Prover-V2-671B在MiniF2F测试中通过率达88.9%，成功解出PutnamBench数据集49道难题 [17] - 推出全新数学形式化数据集ProverBench，包含325道题目，涵盖AIME竞赛题、数论、代数、微积分等10个领域 [18][19] - 在15道AIME竞赛题中，DeepSeek-Prover-V2解出6道，DeepSeek-V3通过多数投票解决8道 [20] 行业趋势与方向 - 大型语言模型在"非正式数学推理"与"正式数学推理"间的表现差距明显缩小，逐步学会写出规范可验证的数学证明 [21][22] - 模型从生成内容迈向生成结构化逻辑，可能最早触碰通用人工智能的底层结构，推理能力成为知识系统边界的关键 [32][33][34] 商业化与部署 - 新模型遵循公开许可证，可通过Hugging Face平台免费下载并支持Transformers接口部署 [23][24] - Novita AI成为首批上线Prover-V2-671B推理服务的第三方提供商 [24]