DeepSeek系列论文解读四之DeepSeek Prover V2
一、研究背景与目标
近年来，大语言模型（LLMs）在数学推理、问答和代码生成等领域展现了惊人的推理能力，特别是在自然语言条件下的“思维链”（Chain-of-Thought, CoT）推理。然而，将这类能力应用于形式化定理证明（如 Lean、Coq 等系统）仍面临巨大挑战：
- 自然语言推理具有模糊性、跳步性、不严格；
- 形式化系统则要求每一步证明都无歧义、可验证；
- LLMs 能否成为严谨数学证明助手，是一个关键科学问题。
本论文提出了 DeepSeek-Prover-V2，一个面向 Lean 4 的、具备递归子目标分解能力的大语言模型，通过强化学习与课程学习联合训练，在多个数学基准测试上达到当前最强性能。
二、技术方法详解
2.1 子目标分解策略（Subgoal Decomposition）
- 借鉴人类证明策略：将复杂定理分解为一系列中间引理（子目标）；
- 使用 DeepSeek-V3 模型生成自然语言思维链，并将子目标形式化为 Lean 语句；
- 每个子目标用
sorry占位，由后续 7B 小模型解决； - 子目标之间具备依赖关系，可通过
have链接组合为完整定理证明。
这种方式实现了复杂推理任务的结构化、模块化与并行化求解。
2.2 冷启动数据构建（Bootstrapping Formal Reasoning）
- 利用子目标成功率高的事实：先解子目标，再自动组合成完整定理；
- 合并 DeepSeek-V3 提供的 CoT 推理与子目标证明，形成高质量训练样本；
- 相比于以往直接采集自然语言→形式化对照，本方法反向建模：形式化先 → 自然语言补足，更适合 LLM 模拟人类推理。
2.3 双模型策略（CoT 与 non-CoT）
📗 Non-CoT 模型
- 专注于 Lean 证明代码生成；
- 无需中间解释步骤，执行速度快；
- 适合大规模并发尝试，支持专家迭代数据采集（Expert Iteration）。
📘 CoT 模型
- 展示自然语言推理路径 + Lean 形式化步骤；
- 提高可解释性；
- 在训练后期结合强化学习进行优化。
2.4 强化学习优化（RL with Structural Rewards）
- 使用 Group Relative Policy Optimization (GRPO) 算法；
- 奖励信号基于是否通过 Lean 验证；
- 引入“结构一致性奖励”，鼓励模型保留关键中间步骤（如每个
have）； - 实验证明对多步骤复杂定理效果显著。
2.5 课程学习策略（Curriculum Learning）
- 通过已解决子目标构建“伪定理”（即中间命题）；
- 随着模型能力增强，逐步加入更复杂结构；
- 类似人类学习路径，从简单引理到复杂定理逐步提升。
三、实验评估与结果
模型在多个主流和新提出的数据集上进行测试：
| 数据集 | 模型/设置 | 成绩 | 说明 |
|---|---|---|---|
| MiniF2F-test | 671B + CoT | 88.9% (Pass@8192) | SOTA，竞赛级定理证明 |
| MiniF2F-valid | 课程学习 + 子目标 | 90.2% | 与最终模型相当，验证子目标分解有效性 |
| ProofNet-test | 671B + CoT | 37.1% (Pass@1024) | 本科教材 Lean 证明集 |
| PutnamBench | 671B + CoT | 49 / 658 | 美国本科竞赛题集，覆盖多数学科 |
| + 7B non-CoT | +13 题，共 62 | 发现技能补偿，7B 模型表现出独特强项 | |
| AIME 2024-2025 | 671B + CoT | 6 / 15 | 高中顶尖数学竞赛题 |
| DeepSeek-V3 | 8 / 15 | 非正式推理结果，显示能力接近 | |
| CombiBench | 671B + CoT | 12 / 77 | 组合数学 Lean 形式化 |
| ProverBench | 325 题混合集（教材+AIME） | 多基准强势表现 | 覆盖 9 类课程内容和竞赛场景 |
四、创新点总结
| 创新点 | 贡献描述 |
|---|---|
| 冷启动推理数据生成方法 | 形式化优先，反向配对非正式语言，构建更严谨的训练样本 |
| 子目标驱动的递归证明流程 | 支持复杂定理分层解构，大幅提升模型效率与可扩展性 |
| 非 CoT + CoT 模型协同训练策略 | 兼顾速度与解释性，适应多场景使用 |
| 结构奖励强化学习框架（GRPO） | 强化“多步逻辑链”保留，提升复杂任务稳定性 |
| ProverBench 数据集 | 首次引入教材与竞赛混合评测集，扩大了评估覆盖范围 |
五、未来工作展望
- 向 IMO（国际数学奥林匹克）级别的挑战进发；
- 构建具备完整证明流程的 AlphaProof 级系统；
- 探索更强的子目标推理规划能力与长期结构记忆机制；
- 融合多模态（图形/自然语言/符号逻辑）以支持更广泛的数学活动。
📝 本文为构建类人类智能数学系统提供了切实路径：从推理分解、知识重组到代码级验证，每一步都向“具备数学能力的通用智能”迈出实质性一步。