DeepSeek-Prover-V2发布 - 公司发布DeepSeek-Prover-V2模型，包含7B和671B两个参数版本，专注于形式化定理证明，专为数学AI编程语言Lean 4打造 [3] - DeepSeek-Prover-V2-671B基于DeepSeek-V3-Base训练，7B版本基于DeepSeek-Prover-V1.5-Base构建，支持32K tokens上下文长度 [3] - 模型在MiniF2F测试中达到88.9%通过率，解决PutnamBench数据集中658道题中的49道，性能达到业内最佳 [15] 技术实现 - 采用递归定理证明流程，使用DeepSeek-V3分解复杂问题为子目标并生成形式化推理步骤，融合非形式化与形式化数学推理 [9][4] - 通过7B模型完成子目标证明以降低计算开销，整合子目标证明与DeepSeek-V3生成的思维链构建冷启动数据 [11] - 采用两阶段训练：非思维链（non-CoT）模式优化快速生成Lean代码，思维链（CoT）模式强调透明推理步骤 [17] 性能与基准测试 - DeepSeek-Prover-V2-671B在ProofNet-test上通过率37.1%（1024样本），PutnamBench解决49/658题，显著优于Goedel-Prover-SFT和STP等竞品 [23] - 7B版本在ProofNet-test通过率29.6%（1024样本），PutnamBench解决11/658题，展示小模型的高效性能 [23] - 发布ProverBench基准数据集，包含325道题目，涵盖AIME竞赛题及本科数学内容，支持高中至本科难度评估 [25][26] 行业影响 - 模型开源并公开技术细节，HuggingFace平台提供7B和671B版本下载链接，推动数学AI领域发展 [6][16] - 用户实测显示模型效果优于o4-mini和Grok-3，尤其在数学奥林匹克问题解决中表现突出 [31] - 子目标分解与推理融合的设计被类比为初级工程师问题解决技巧，潜在适用于代码生成等场景 [32]