107 lines
11 KiB
Markdown
107 lines
11 KiB
Markdown
# DeepSeek-Prover：用大规模合成数据推进大模型的定理证明
|
||
|
||
> **原文标题**：DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data
|
||
> **arXiv**：[2405.14333](https://arxiv.org/abs/2405.14333) ｜ **发布**：23 May 2024
|
||
> **作者/机构**：Huajian Xin、Daya Guo、Zhihong Shao、Zhizhou Ren、Qihao Zhu、Bo Liu、Chong Ruan、Wenda Li、Xiaodan Liang（DeepSeek（深度求索）、中山大学、爱丁堡大学、MBZUAI）
|
||
> **原文 PDF**：[01-DeepSeek-Prover-2405.14333.pdf](./01-DeepSeek-Prover-2405.14333.pdf)
|
||
|
||
## 一、摘要（全文翻译）
|
||
|
||
像 Lean 这样的证明助手已经彻底改变了数学证明的验证方式，保证了高准确性与高可靠性。尽管大语言模型（Large Language Model, LLM）在数学推理上展现出潜力，但其在形式化定理证明方面的进展受到了训练数据不足的阻碍。为解决这一问题，我们提出了一种方法，用于生成大量源自高中与本科水平数学竞赛题目的 Lean 4 证明数据。该方法包括：将自然语言问题翻译为形式化陈述、过滤掉低质量陈述、并生成证明以构建合成数据。在由 800 万条带证明的形式化陈述构成的合成数据集上对 DeepSeekMath 7B 模型进行微调后，我们的模型在 Lean 4 miniF2F 测试集上取得了整证明生成（whole-proof generation）准确率 46.3%（64 个样本）与累计 52% 的成绩，超过了 64 个样本下为 23.0% 的基线 GPT-4，以及达到 41.0% 的树搜索强化学习方法。此外，我们的模型在 Lean 4 形式化国际数学奥林匹克（Formalized International Mathematical Olympiad, FIMO）基准上成功证明了 148 道题中的 5 道，而 GPT-4 一道也没能证明。这些结果展示了利用大规模合成数据增强 LLM 定理证明能力的潜力。合成数据集与模型都将公开，以促进该领域的进一步研究。
|
||
|
||
## 二、核心贡献
|
||
|
||
1. **提出可迭代的合成数据生成流水线**：自动形式化 → 质量过滤 → 证明生成 → 迭代精炼，单轮产出 800 万条「定理–证明」对，同时提升合成数据的规模与质量。
|
||
2. **刷新 miniF2F 与 FIMO 的 SOTA**：miniF2F 测试集整证明生成达 64 样本 46.3%、累计 52%，超过 GPT-4（23.0%）与树搜索强化学习（41.0%）；FIMO 上证明 5/148 题，GPT-4 为 0。
|
||
3. **用「否定命题并行证明」解决不可证陈述的资源浪费**：同时搜索原命题与否定命题，任一被证明即终止搜索，既加速又充当数据增强。
|
||
4. **开源数据集与模型**：公开高质量形式化数学证明数据集，推动自动定理证明（Automated Theorem Proving, ATP）社区研究。
|
||
5. **完整消融**：验证数据来源、陈述打分、迭代轮次、数据规模各自的增益，其中迭代 4 轮使 miniF2F 验证集从 38.1% 升至 59.4%。
|
||
|
||
## 三、方法与技术要点
|
||
|
||
整体流程由四个关键环节构成（论文 Figure 1）：**自动形式化 → 质量过滤 → 陈述证明 → 迭代增强**，循环往复直至模型提升变得微弱。
|
||
|
||
### 3.1 自动形式化（Autoformalization）
|
||
|
||
形式化证明数据的前提是海量形式化陈述，而人工撰写代价极高，因此转向互联网上丰富的自然语言数学题。作者的观察是：**条件明确、目标清晰的问题比需要复杂定义与构造的高等数学主题更易形式化**，所以本文聚焦高中与本科竞赛题，重点在代数与数论。通过网页抓取与清洗，最终得到 **869,659** 道高质量自然语言数学题。
|
||
|
||
初始的 DeepSeek-Prover 基于 DeepSeekMath-Base 7B；因模型起初难以把非形式问题转成形式陈述，作者先用 **MMA 数据集**（来自 Lean 4 mathlib 的形式陈述，由 GPT-4 反向翻译为自然语言描述）微调，再以固定模板要求模型只输出核心声明：
|
||
|
||
````text
|
||
Mathematical Problem in Natural Language:
|
||
{$informal_statement_with_answers}
|
||
Translate the problem to Lean 4 (only the core declaration):
|
||
```lean4
|
||
{$formal_statement}
|
||
```
|
||
````
|
||
|
||
### 3.2 质量过滤（Quality Filtering）
|
||
|
||
自动形式化结果存在两类主要缺陷，对应两种过滤手段：
|
||
|
||
1. **陈述过于简单**：作者设计评分标准，并以 miniF2F-valid 样例作少样本示例，引导模型用思维链（Chain-of-Thought）从前沿相关性、复杂度与深度、跨学科潜力、社区需求缺口、创新性五个维度打分，等级为 "excellent"/"good"/"above average"/"fair"/"poor"，**"fair" 与 "poor" 直接剔除**；人工复核确认模型评分与人类直觉高度一致。
|
||
2. **假设自相矛盾导致空虚结论**：例如模型生成的 `example (θ : ℝ) (h₀ : ∀ z : ℂ, z^2 = -1 ∧ z^3 = -1 ∧ z^6 = 1) ... : θ = 5 * Real.pi / 3`，其对所有复数成立的前提显然为假，结论在数学上无意义（虚真）。为此提出**假设否定（Hypothesis Rejection）**：让模型尝试证明以 `False` 为结论的同一陈述（如用 `simpa using h₀ 1`）——证明成功即说明假设无效，剔除该陈述。
|
||
|
||
双策略共同作用后，得到 **712,073** 条高质量形式化陈述。
|
||
|
||
### 3.3 陈述证明（Statement Proving）与否定并行搜索
|
||
|
||
传统做法是暴力重复尝试直到找到证明或算力耗尽，这在自动形式化场景下代价极高：即便经过质量过滤，作者观察到**至少 20% 的生成陈述仍是错误的**，而对假命题任何可靠证明系统都不可能给出证明。
|
||
|
||
为此利用陈述与否定之间的逻辑对称性加速：对每条合成陈述同时启动两条搜索，一条证明 $\Gamma \vdash P$，另一条证明 $\Gamma \vdash \neg P$；**任一条先找到有效证明即终止整个搜索**，因为证明其中一个就决定性地说明另一个不可证。每条搜索流最多尝试 $k$ 个证明。所有被 Lean 4 验证器（`leanprover/lean4:v4.7.0-rc2`）接受的证明——无论对应原命题还是其否定——都被汇总继续训练，因此这一双重搜索同时构成**数据增强**。
|
||
|
||
### 3.4 迭代增强（Iterative Enhancement）
|
||
|
||
整条流水线高度依赖 DeepSeek-Prover 本身，故每轮之后提升模型能力至关重要：用新生成的数据持续微调，再把更新后的模型用于下一轮自动形式化，循环直到不再有增益。其洞见是模型每轮精炼后都有增量提升，产出的定理–证明对质量逐轮上升，形成正反馈。
|
||
|
||
### 3.5 训练设置
|
||
|
||
DeepSeek-Prover 基于 DeepSeekMath-Base 7B（decoder-only transformer，预训练语料含 **1200 亿**数学相关 token）。微调使用全局批大小 **512**、恒定学习率 $1\times 10^{-4}$、**6,000** 步 warmup。评测指标为 pass@k，即前 $k$ 次尝试中至少找到一个有效证明。
|
||
|
||
## 四、主要实验结果
|
||
|
||
| 基准 / 任务 | 本模型 | 对比对象 | 说明 |
|
||
|---|---|---|---|
|
||
| miniF2F-test（整证明生成，累计） | **52.0%** | GPT-4-turbo 0409：22.95%（原文 23.0%）；Hypertree Proof Search (600M)：41.0% | 累计口径为不同采样预算的并集 |
|
||
| miniF2F-valid（累计） | **60.2%** | GPT-4-turbo 0409：25.4%；Hypertree Proof Search：58.6% | 本文领先所有对比方法 |
|
||
| miniF2F-test，64 次采样 | **46.3%** | GPT-4-turbo 0409：23.0%；DeepSeekMath-Base 7B：27.5%（128 次） | 整证明生成（非树搜索） |
|
||
| miniF2F-test，greedy / 8192 / 65536 次 | 30.0% / 48.8% / **50.0%** | — | 性能随采样预算单调提升 |
|
||
| FIMO（149 道 IMO 短名单题） | 100 次采样证明 4 题；4096 次采样证明 **5 题** | GPT-4：0 题 | 摘要与引言中的 5/148 对应 4096 次采样口径 |
|
||
| 消融：数据来源（pass@128） | 自动形式化陈述（3.108B token）：valid 48.8% / test 42.6% | Mathlib（0.238B token）：30.3% / 31.2%；基线：25.4% / 27.5% | 大规模自动形式化数据远胜仅用 mathlib 数据 |
|
||
| 消融：陈述打分（pass@128） | 高分档（excellent/good/above average）：48.8% / 42.6% | 低分档（fair/poor）：41.4% / 38.1% | 高分数据领先 4.5% |
|
||
| 消融：迭代轮次（pass@128，validation） | iteration 0→4：38.1%、45.1%、49.2%、54.5%、**59.4%** | test 同步为 34.0%、39.3%、41.4%、45.1%、46.3% | 每轮迭代稳定带来增益 |
|
||
| 消融：数据规模（pass@128） | 1K→8,066,621 条：valid 22.95%→42.62%，test 24.18%→40.16% | — | 性能随数据量指数增长而近似成比例提升 |
|
||
|
||
DeepSeek-Prover 在 miniF2F 上全面领先：累计口径下 valid 60.2%、test 52.0%，明显高于 GPT-4 的 25.41% 与 22.95%；即便最强的树搜索方法 Hypertree Proof Search（600M）也只在 valid 上达到 58.6%、test 上 41.0%。可扩展性突出：从 greedy 的 30.03% 到 65536 次采样的 50.0% 持续上升。差距仍在——test 累计准确率（52.0%）尚未过半，FIMO 上 4096 次采样也只解出 5/148 题，说明竞赛级难题的形式化证明仍是短板。
|
||
|
||
## 五、结论、局限与影响
|
||
|
||
- **结论**：从高中与本科数学竞赛题生成大规模合成证明数据——自然语言转形式陈述、低质量过滤、迭代式证明生成——构建 800 万条证明数据，显著提升 DeepSeekMath 7B 的定理证明表现，在 miniF2F 与 FIMO 上超过 GPT-4 及其他方法，并开源数据集与模型。
|
||
- **局限性**：论文自述当前工作**主要聚焦中学与本科水平的代数与数论**，未来将扩展问题多样性以提升方法的通用适用性；论文未明确给出除「过滤后至少 20% 陈述仍错误」以外的错误率统计。
|
||
- **影响**：表明大规模合成数据可有效缓解形式化证明语料稀缺这一核心瓶颈，为神经定理证明器提供可复制的数据构造范式；开源代码、模型与数据有助于提升证明验证可靠性，并为学生与研究者提供教育资源。作者在「更广泛影响」中强调负责任使用，并关注数据隐私与知识产权合规。
|
||
|
||
## 六、关键术语对照表
|
||
|
||
| English | 中文 |
|
||
|---|---|
|
||
| Automated Theorem Proving (ATP) | 自动定理证明 |
|
||
| Autoformalization | 自动形式化 |
|
||
| Formal Statement | 形式化陈述 |
|
||
| Informal Problem | 非形式化问题 |
|
||
| Whole-Proof Generation | 整证明生成 |
|
||
| Proof Assistant (Lean 4) | 证明助手（Lean 4） |
|
||
| Formal Verifier | 形式化验证器 |
|
||
| Hypothesis Rejection | 假设否定 / 假设排斥 |
|
||
| Quality Filtering | 质量过滤 |
|
||
| Statement Scoring | 陈述打分 |
|
||
| Iterative Enhancement | 迭代增强 |
|
||
| negation $\Gamma \vdash \neg P$ | 否定式（证明否定命题） |
|
||
| vacuous conclusion | 空虚结论（虚真结论） |
|
||
| pass@k | pass@k（前 k 次尝试中至少一次成功） |
|
||
| miniF2F | miniF2F 基准 |
|
||
| FIMO (Formalized International Mathematical Olympiad) | 形式化国际数学奥林匹克 |
|
||
| Expert Iteration | 专家迭代 |
|
||
| Tree Search | 树搜索 |
|
||
| mathlib | mathlib 数学库 |
|