深度求索（DeepSeek）于 2025 年 4 月 30 日发布的新一代数学推理大模型 DeepSeek-Prover-V2，在数学定理证明领域实现了技术范式的突破。该模型基于 DeepSeek-V3 架构，通过递归子目标分解与强化学习的结合，将复杂数学问题拆解为可验证的子目标链，并生成对应的 Lean 4 形式化代码框架，实现了自然语言推理与形式化证明的深度融合。其核心技术突破包括采用递归子目标分解架构，将费马大定理等复杂定理分解为椭圆曲线模性定理等子目标，由 7B 轻量模型递归解决后拼接成完整证明；双模式推理机制则通过快速模式（non-CoT）直接生成精炼的 Lean 4 代码，30 秒内解决 AIME 竞赛题，逻辑模式（CoT）则逐步阐述推理过程，确保逻辑透明。模型采用 GRPO 强化学习算法，从 32 种候选方案中自主选择最优解，训练数据通过 “失败回撤 - 路径重组” 机制自动生成，摆脱对人工标注的依赖。
在性能表现上，Prover-V2 的 671B 版本在 MiniF2F-test 中通过率达 88.9%，较前代提升 47%，解决 PutnamBench 数据集 658 题中的 49 道，远超竞品的 23 题。7B 版本在 PutnamBench 中解决 13 个 671B 模型未解决的问题，支持本地设备运行，推理速度达 60 tokens / 秒，且通过 FP8 量化技术节省 35% 显存。跨领域泛化能力方面，模型在 ProofNet（本科数学问题）和 CombiBench（组合数学）测试中表现优异，尤其在有限基数问题中使用特定数学工具 Cardinal.toNat 等，展现差异化推理能力。
应用场景上，Prover-V2 已在教育、科研、工业等领域落地。新东方、猿辅导等机构利用其 7B 版本实时解析 3.2 万字符的数学证明，辅助智能教辅系统；MIT 团队用其辅助完成代数几何领域顶刊论文，验证猜想并生成形式化证明。工业领域中，华为将其应用于 5G 协议栈的自动化审计，解决形式化验证中的 “组合爆炸” 难题；Fermat-1 量化平台基于 Prover-V2 的算法实现年化 36% 的超额收益。模型已在 Hugging Face 开源，提供 7B 和 671B 版本，并配套发布 ProverBench 测试集，吸引超 10 万开发者参与，形成 “模型 - 工具 - 社区” 闭环。
行业评价认为，Prover-V2 的发布标志着 AI 从解题工具向探索伙伴转型，其 “神经符号结合” 架构为通用人工智能（AGI）发展提供关键支撑。技术报告详细披露训练流程与性能数据，被 MLCommons 列为基准测试参考模型。下一代旗舰模型 R2 计划扩展至 1.2 万亿参数，支持 “文本 + 视觉” 跨模态推理，目标覆盖科研辅助、金融建模等场景。
