DeepSeek-Prover-V2 — 子目标分解强化学习的形式推理突破

DeepSeek-Prover-V2

发布日期： 2025-04-30 来源： arXiv 2504.21801 工程范式： 用 RL 连接非正式推理与形式证明——子目标分解 + 课程学习 + 大模型冷启动。

设计哲学

从 V1 到 V1.5 再到 V2，核心思路发生了根本性转变。V1 靠合成数据，V1.5 靠 RL+搜索。V2 的洞察是：形式定理证明的瓶颈在于”从非正式思维到形式化步骤的翻译”。解决方式是让 DeepSeek-V3（671B 通用大模型）先生成自然语言证明草稿并同时写出 Lean 代码骨架（含 have 语句和 sorry 占位符），然后用一个 7B 小模型递归解决每个子目标。这个管线既利用了通用大模型的推理能力，又避免了用完整大模型穷举搜索的巨额开销。RL 阶段用 GRPO 附加一致性奖励来约束证明结构，防止模型偏离子目标分解模式。

关键架构决策

• 冷启动数据： DeepSeek-V3 生成 NL 证明 + Lean 骨架（have + sorry）→ 7B prover 递归解子目标 → 合并为 CoT 训练数据
• 课程学习： 将子目标转化为独立的定理，逐步提高难度纳入训练
• RL： GRPO + 一致性奖励（惩罚偏离子目标结构的证明），256 问题/迭代，32 候选/问题
• 蒸馏： 7B 变体从 671B 的 rollout 数据微调，上下文窗口扩展至 32768
• 两种推理模式： non-CoT（快速简洁）和 CoT（结构化推理，含中间步骤）

关键结果

miniF2F test Pass@8192 达 88.9%（IMO 50%、AIME 93.3%、MATH Algebra 100%、Number Theory 96.7%）。PutnamBench 671B CoT 解决 49/658。ProverBench（新数据集）AIME 24-25 解决 6/15。7B non-CoT 模型发现了 13 个 671B 模型无法解决的问题——小模型在特定技术路径上可能超越大模型。

范式对比

与 V1.5（RL+搜索）相比，V2 的子目标分解策略使 miniF2F 从 63.5% 跃升至 88.9%，提升 25pp。与 AlphaProof 的 test-time RL 思路本质相同但更高效——通过冷启动数据预先学习问题分解结构。

可复用工程经验

1. 子目标分解是连接非正式和形式推理的最有效桥接策略
2. 用大模型做分解+小模型做子目标搜索是计算效率最优解
3. 课程学习（逐步提高子目标难度）能持续提升模型上限
4. 一致性奖励防止 RL 过程偏离有益的结构化推理模式