DeepSeek-Prover-V2-671B 模型正式发布，标志着 AI for Science 领域再次取得突破性进展。该模型并非通用对话系统，而是专注于 自动定理证明，借助大规模合成数据与强化学习，显著提升了机器在数学推理方面的能力。本教程将从模型特点、架构解析到背后的研究论文，逐步带你全面理解这一重要更新。

1. 模型特点及架构解析

DeepSeek-Prover-V2-671B 属于 DeepSeek-Prover 系列的最新版本，参数规模高达 6710亿（671B），被视作去年发布的 Prover-V1.5 的升级版。其核心特性包括：

• 更高效的文件格式：采用 safetensors 格式，训练与部署更加快速，且节省资源。
• 多精度支持：兼容多种计算精度，便于在不同硬件环境中灵活部署。
• FP8 量化：通过 FP8 量化 技术缩小模型体积，提高推理效率，降低显存占用。
• 超长上下文：最大位置嵌入达 163840，使其能够处理复杂的数学证明任务。

在模型架构层面，该模型沿用了 DeepSeek-V3 的 MoE（混合专家） 模式，具体配置如下：

• 61 层 Transformer 层
• 隐藏层维度 7168
• 采用 MoE 架构，激活部分专家以节省计算量

小提示：MoE 架构使模型能够在推理计算量不显著增加的前提下拥有庞大参数量，这已成为当前大模型的主流发展方向之一。

2. AI for Science 领域应用与挑战

自动定理证明是 AI for Science 的核心应用之一。传统数学证明依赖人类专家的灵感和经验，不仅耗时，而且容易出错。DeepSeek-Prover 系列模型的目标是让 大语言模型（LLM）学会用形式化语言（如 Lean 4） 自动生成可验证的证明，从而辅助数学家验证猜想、发现新定理。然而，这一领域面临的最大挑战是 训练数据极度匮乏——高质量的形式化证明数据远少于自然语言文本。为此，研究团队提出了一套大规模合成数据的方法。

3. 论文解读：大规模合成数据增强 LLMs 定理证明能力的方法

下面基于 DeepSeek 发布的论文，详细解析其核心方法。为了让理解更直观，我们借助 AI 辅助生成的解读（音频来自 NotebookLM，文字来自腾讯元宝），并结合打比方的形式说明其独特价值。

3.1 研究背景

• 背景介绍： 现代数学证明日益复杂，同行评审过程中错误难以被发现。形式化数学语言（如 Lean、Isabelle、Coq）允许计算机验证证明，但编写形式化证明需要大量专业知识，因此 自动化定理证明 的重要性与日俱增。
• 研究内容： 本文提出一种从非正式数学问题（高中数学竞赛题）生成大规模 Lean 4 证明数据的方法，并通过微调 DeepSeekMath 7B 模型来提升其定理证明性能。
• 文献综述： 相关工作（Polu et al., Jiang et al., Lample et al. 等）主要关注搜索算法与 LLM 结合，但缺乏足够的训练数据。Autoformalization 方法（如 Wu et al.）虽能生成合成数据，但规模仍然不足。

3.2 研究方法——四步训练流程

下图直观展示了整个数据生成与训练流程：

1. 自动形式化（Autoformalization）
   • 输入：大量非正式数学问题（例如来自高中、大学数学竞赛）。
   • 过程：使用基于 DeepSeekMath-Base 7B 的模型，将自然语言问题翻译成 Lean 4 的形式化语句。初始模型能力不足，因此先用 MMA 数据集（从 mathlib3 反向翻译的问答）进行微调。
   • 输出：初步的形式化数学语句。
2. 质量过滤（Quality Filtering）
   • 模型评分：用评分模型对每个形式化语句进行质量分类（“优秀”、“良好”、“高于平均”、“一般”、“较差”），排除“一般”和“较差”的语句。
   • 假设拒绝：尝试证明该语句的结论为假（即证明 P → False），若可证明则说明原假设不一致，予以剔除。
   • 输出：高质量的形式化语句。
3. 陈述证明（Statement Proving）
   • 使用 DeepSeek-Prover 模型为每个形式化语句搜索证明。为提高效率，并行证明原语句及其否定（同时尝试证明 T ⊢ P 和 T ⊢ ¬P）。
   • 每个证明搜索流最多尝试 k 次证明，一旦找到有效证明立即终止。
   • 用 Lean 4 验证器验证证明的正确性。
   • 输出：经过验证的语句及其证明。
4. 迭代增强（Iterative Enhancement）
   • 用新生成的证明数据微调 DeepSeek-Prover 模型。
   • 用微调后的模型进行新一轮的自动形式化、质量过滤和证明搜索。
   • 重复此过程，直到性能提升不再明显。

小提示：这种方法就像给 AI 准备了一个“超级题库”——最终生成了约 800 万道数学题（含证明），让模型通过反复训练显著提升能力。

3.3 实验设置与结果

• 基础模型：DeepSeekMath-Base 7B，额外在 1200 亿数学相关 token 上预训练。
• 微调参数：全局批量大小 512，学习率 1×10⁻⁴ ，包含 6000 个热身步骤。
• 评估指标：pass@k（k 次采样中的成功率）。
• 对比基线：GPT-3.5、GPT-4、GPT-f 等。

关键结果：

• 在 Lean 4 miniF2F 测试集上，微调后的模型在 64 个样本下完整证明生成准确率 46.3%，累积达 52%，远超 GPT-4 的 23.0% 和树搜索强化学习方法的 41.0%。
• 在 Lean 4 FIMO 基准（形式化国际数学奥林匹克问题）上，该模型成功证明了 148 个问题中的 5 个，而 GPT-4 一个都没证明出来。

3.4 消融实验与发现

• 大规模自动形式化有效：用自动生成数据训练的模型比仅用 mathlib 数据训练的模型性能更好。
• 质量过滤有效：用高质量证明数据训练的模型比用低质量数据训练的性能提升 4.5%。
• 迭代增强有效：随着迭代次数增加，模型性能持续提升。
• 数据规模与效果正相关：数据量越大，模型在 miniF2F 上的性能越好。

3.5 常见问题（AI 自问自答）

以下整理了几个关键问答，帮助你快速理解论文的贡献：

1. 这篇论文主要解决了什么问题？
   在数学定理证明中，LLM 因缺乏训练数据而进展受限。本文提出一种方法，从竞赛问题生成大量 Lean 4 证明数据来解决数据缺乏的问题。
2. 它是怎么解决数据缺乏问题的？
   从网上抓取竞赛自然语言问题，用 LLM 翻译成 Lean 4 语句，经过质量过滤后，用模型生成证明，再微调模型并迭代增强。
3. 这种方法效果如何？
   在 miniF2F 上准确率远超 GPT-4；在 FIMO 上成功证明 5 题（GPT-4 为零）。
4. 论文提出的方法有何独特之处？
   多步骤质量保证（评分+假设拒绝）和并行证明加速，以及迭代框架。
5. 对数学领域有什么贡献？
   创建并开源了大规模高质量形式化数学证明数据集，有助于自动定理证明研究和教育。
6. 对人工智能领域有什么意义？
   展示 LLM 在自动定理证明上的巨大潜力，为相关研究提供新思路。
7. 论文中的实验如何设置？
   以 DeepSeekMath-Base 7B 为基础，微调参数具体给出，与 GPT-4 等对比。
8. 除了准确率，还有什么发现？
   消融实验证实自动形式化、质量过滤、迭代增强和数据规模都至关重要。
9. 案例研究有什么作用？
   展示了模型成功证明以及识别错误假设的能力，比如自动发现并修正形式化中的错误。
10. 未来展望是什么？
    目前聚焦中学/大学的代数和数论，未来将扩大问题多样性，提高通用性。

3.6 独特的价值（打比方版）

• 像“教AI做数学题”一样训练模型
  先让 AI 学会把题目翻译成机器语言（Lean 4），再自己尝试解题，做错了纠正，反复训练，直到独立解题。
• 像“刷题库”一样提升AI的数学能力
  生成了 800 万道数学题和答案，相当于给 AI 准备了一个超级题库，疯狂刷题，能力自然提升。
• 像“错题本”一样优化训练
  把错题整理分析，剔除错误假设，避免下次再犯。
• 像“双保险”一样提高解题效率
  同时证明原命题和反命题，快速排除错误命题，节省计算资源。

3.7 作者为什么要做这篇论文？（打比方版）

• 解决AI数学解题的“卡脖子”问题：数据不够是主要瓶颈，作者自己造数据。
• 让AI像数学家一样思考：希望 AI 先理解题目，再有逻辑地推导，而非暴力破解。
• 推动AI自动定理证明的发展：让 AI 未来能帮数学家验证猜想、发现新定理。
• 让更多人能用上AI数学工具：开源数据和方法，促进研究和应用。

总结

DeepSeek-Prover-V2-671B 模型及其背后的论文，为我们展示了一条通过大规模合成数据 + 迭代微调来大幅提升 LLM 自动定理证明能力的可行路径。它不仅刷新了 Lean 4 基准测试的成绩，更重要的是开源了高质量的证明数据集和方法，为数学与 AI 的深度融合开启了新篇章。未来，随着数据规模的扩大和方法的通用性提升，AI 在数学研究中的角色将越来越重要。

常见问题补充： 如果你对“自动形式化”的具体实现感兴趣，可以查阅论文中关于 MMA 数据集和模型评分机制的详细描述。也可以直接尝试 DeepSeek 开源的模型在 Lean 4 环境进行推理测试。