DeepSeek-Prover — 大规模合成数据驱动的定理证明

DeepSeek-Prover

发布日期： 2024-05-22 来源： arXiv 2405.14333 工程范式： 用大规模合成数据（800 万条）将 LLM 定理证明能力提升至超越 GPT-4。

设计哲学

定理证明的核心瓶颈不是模型架构，而是训练数据。Lean 4 社区积累的正式证明数据极少，大幅限制了 LLM 在此领域的能力。DeepSeek-Prover 的思路是：从数学竞赛题目出发，用自然语言描述→自动形式化→筛选→自动证明这一管线批量生产训练数据。共生成 800 万条 Lean 4 正式语句及证明，低成本打破数据瓶颈。设计上选择 DeepSeekMath 7B 作为基座而非更大的通用模型，证明”数据工程 > 模型规模”在这一领域同样成立。

关键架构决策

• 基座： DeepSeekMath 7B（继承代码+数学能力）
• 数据管线： NL 问题 → 形式化翻译 → 质量过滤 → 可用性检查 → 自动证明生成，循环迭代
• 评估： miniF2F（高中竞赛水平）和 FIMO（IMO 题目）双基准
• 推理： 64 样本多数投票，搜索策略使用 top-p + 重试

关键结果

miniF2F test 上达 46.3%（Pass@64），累积成功率 52%，超越 GPT-4 的 23%（Pass@64）和树搜索 RL 方法的 41%。在 FIMO 上成功证明 5/148 题，GPT-4 为 0。这一结果证明：合成数据方法可以绕过传统自动定理证明需要人工标注的瓶颈。

范式对比

与 GPT-4（零样本证明）相比，DeepSeek-Prover 规模小 10 倍但效果翻倍，关键差异是领域专用数据。与 AlphaProof 等树搜索方法相比，DeepSeek-Prover 验证了”数据本身就能带来显著提升”，搜索是锦上添花而非必要条件。

可复用工程经验

1. 合成数据是突破训练数据瓶颈的最有效手段，尤其在数据稀缺的专用领域
2. 数学竞赛题目是形式化定理证明训练的优质种子数据
3. 形式化领域的”数据工程”效率远高于”模型工程”
4. 自动形式化+筛选的管线精度足够支撑大规模数据生产