各位五一快乐！（顺便星标⭐️一下本号，最近很多朋友反应不能及时看到内容更新，只有关注并且⭐️才会第一时间收到更新）
让 AI 理解并进行严格的数学推理，尤其是形式化证明（就是用像 Lean、Coq 这样的证明辅助语言写的、机器可验证的证明），一直是个挑战。这不仅需要逻辑能力，还需要某种程度的“数学直觉”来分解复杂问题。
今天DeepSeek 正式开源了他们最新的 DeepSeek-Prover-V2 模型，专门用于 Lean 4 形式化定理证明。这次不仅仅是一次模型的迭代（对DeepSeek-Prover-V1.5），更带来了一种结合大语言模型（LLM）的直觉和强化学习（RL）严谨性的新思路
DeepSeek这次开源了两个模型版本
DeepSeek-Prover-V2-7B：基于 DeepSeek-Prover-V1.5-Base 构建，上下文长度扩展到 32K tokens
DeepSeek-Prover-V2-671B：基于 DeepSeek-V3-Base 训练，还附有详细的论文，论文题目《DeepSeek-Prover-V2：通过强化学习推进子目标分解的形式数学推理》
性能 SOTA：DeepSeek-Prover-V2-671B模型，在标准测试集 MiniF2F-test 上达到了 88.9% 的通过率，这是目前的最佳水平
挑战难题：在更难的 PutnamBench（基于普特南数学竞赛题）上，它成功解决了 49 个 问题（总共 658 个）。从图表看，这个成绩也显著优于之前的 BFS-Prover 7B、STP 7B 等模型
Hugging Face (模型下载):
https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B
https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-7B
论文链接:
https://github.com/deepseek-ai/DeepSeek-Prover-V2/blob/main/DeepSeek_Prover_V2.pdf
核心思路：两步走，联通直觉与形式
DeepSeek-Prover-V2 的训练方法很有意思，可以概括为两个关键阶段：
一,冷启动数据合成：用大模型“拆解”问题
他们先利用 DeepSeek-V3 这个强大的基础模型。通过精心设计的 Prompt，让 V3 同时做两件事：
-
• 分解定理：把一个复杂的证明目标，拆解成一系列更小的、更容易处理的子目标（Subgoals），并给出高级证明草图（Proof Sketch）。这模拟了人类数学家的“直觉”或“规划”能力 -
• 同步形式化：在分解的同时，尝试将这些证明步骤形式化为 Lean 4 代码片段，形成一系列子目标
然后，他们用一个较小的 7B 参数模型（DeepSeek-Prover-V2-7B 或类似模型）去搜索每个子目标的具体形式化证明。这样做的好处是，针对小目标的搜索计算成本更低
一旦所有子目标都被解决了，就把这些子目标的证明组合起来，形成原始问题的完整形式化证明。
最后，将这个完整的形式化证明与 DeepSeek-V3 最初生成的“分解思路+形式化草稿”（Chain-of-Thought）配对，构成一份高质量的“冷启动”训练数据。这份数据既包含了宏观的解题策略，也包含了微观的、严格的证明步骤
二，强化学习：用合成数据“教会”模型连接思路与证明
筛选出一部分“有挑战性”的问题：这些问题是 7B 模型无法直接端到端解决，但其分解出的所有子目标都能被成功证明的。用这些问题对应的“合成证明”（由子目标证明拼接而成）和 DeepSeek-V3 的思路链，来构建 RL 的初始数据
用这些合成数据对 Prover 模型进行微调
然后进入 强化学习阶段。目标是进一步提升模型将非形式化推理（如 V3 给出的解题思路）转化为形式化证明的能力。训练目标很直接：对于模型生成的证明，系统反馈一个二元信号（正确或错误）作为奖励，驱动模型学习生成正确的证明
新基准：ProverBench，更全面的评测
为了更全面地评估模型在不同数学领域和难度上的能力，DeepSeek 还推出了一个新的基准测试集 ProverBench。
组成：共 325 个问题
-
• 15 个 来自近两年的 AIME（美国数学邀请赛）的数论和代数题，代表了真实的高中竞赛挑战 -
• 310 个 来自精心挑选的教科书和教程，覆盖了数论 (40), 初等代数 (30), 线性代数 (50), 抽象代数 (40), 微积分 (90), 实分析 (30), 复分析 (10), 泛函分析 (10), 概率论 (10) 等多个本科及以上数学领域
目标：提供一个能同时评估高中竞赛水平和本科基础数学能力的、更多样化、更贴近教育场景的评测平台
快速上手：自己跑试试看
想自己跑跑看？很简单：
模型可以通过 Hugging Face 的 transformers 库直接加载使用
DeepSeek-Prover-V2-671B 与 DeepSeek-V3架构相同，可以直接参考 DeepSeek-V3 在 Hugging Face 上的文档
仓库里提供了一个基础的 miniF2F 推理示例代码：输入形式化的定理描述，设置好 Prompt（要求模型先提供详细证明计划，再生成 Lean 4 代码），模型就能输出证明思路和代码
# 示例代码片段 (关键部分)
from transformers import AutoModelForCausalLM, AutoTokenizer
import torch
model_id = "deepseek-ai/DeepSeek-Prover-V2-7B" # or 671B
tokenizer = AutoTokenizer.from_pretrained(model_id)
model = AutoModelForCausalLM.from_pretrained(model_id, ...)
formal_statement = """
import Mathlib ...
theorem mathd_algebra_10: abs ((120 : ℝ) / 100 * 30 - 130 / 100 * 20) = 10 := by
sorry
""".strip()
prompt = """
Complete the following Lean 4 code:
```lean4
{}
Before producing the Lean 4 code to formally prove the given theorem, provide a detailed proof plan...
""".strip()
chat = [{"role": "user", "content": prompt.format(formal_statement)}]
inputs = tokenizer.apply_chat_template(chat, ...)
outputs = model.generate(**inputs, ...)参考：
https://github.com/deepseek-ai/DeepSeek-Prover-V2
⭐
（文：AI寒武纪）