企业官网建设流程全解析

DeepSeek-Prover-V2-671B是什么？88.9%通关MiniF2F的Lean 4形式化定理证明大模型完全指南

【免费下载链接】DeepSeek-Prover-V2-671B项目地址: https://ai.gitcode.com/hf_mirrors/deepseek-ai/DeepSeek-Prover-V2-671B

DeepSeek-Prover-V2-671B是深度求索开源的一款面向Lean 4 形式化定理证明的大语言模型，在数学推理基准 MiniF2F-test 上取得了88.9% 的通过率，是神经网络定理证明（Neural Theorem Proving）领域的标杆模型。它由 671B 参数的 MoE 架构驱动，基于 DeepSeek-V3-Base 训练，能够直接阅读自然语言题目并生成可被 Lean 4 证明助手机器验证的严格证明代码。

什么是形式化定理证明？为什么值得关注

很多人把"AI 会解数学题"理解为生成一段看起来对的解答，但 DeepSeek-Prover-V2-671B 走的是更硬核的路线——形式化证明：

• 🧮Lean 4是一个定理证明助手，证明不是"文字描述"，而是可被计算机逐行验证的逻辑代码
• 🤖 模型输出的是 Lean 4 证明代码，只要 Lean 4 接受，证明就绝对无误，不存在"步骤跳跃"
• ⚖️ 这项技术是数学自动化的核心方向，也是"AI 发现新定理"研究的基石

简而言之：普通大模型"说"自己证完了，DeepSeek-Prover-V2-671B 是"证给机器看"。

核心能力一览：88.9% 通关 MiniF2F 的神经网络定理证明模型

根据官方说明，DeepSeek-Prover-V2-671B 的关键成绩：

💡 值得一提的是，官方还把该模型在 miniF2F 数据集上的全部生成证明整理成了可下载的存档，供研究者逐条查验，这种"可验证的开源"在定理证明领域相当稀缺。

训练方法揭秘：递归定理证明流水线 + 强化学习

DeepSeek-Prover-V2 的训练流程分为两个阶段，这也是它超越前代的关键：

1️⃣ 用递归证明搜索合成"冷启动"推理数据

• 以 DeepSeek-V3 为统一工具，把复杂定理拆解成一系列子目标，并同时用 Lean 4 形式化这些证明步骤
• 用更小的7B 模型负责每个子目标的证明搜索，大幅降低算力开销
• 当一个难题的所有子目标都被解决后，把完整的分步形式化证明与 DeepSeek-V3 的思维链（Chain-of-Thought）配对，构成冷启动推理数据

2️⃣ 基于合成数据做强化学习（RL）

• 精选那些"7B 模型端到端解不了、但拆解后子目标全部可解"的难题，拼接子证明得到原命题的完整证明
• 微调后再进入强化学习阶段，以"对/错"二元反馈作为奖励信号，进一步打通非形式化推理 → 形式化证明的转换能力

这套"大模型拆题 → 小模型搜索 → 合成数据 → 强化学习"的闭环，让非形式化数学推理与形式化证明被统一进同一个模型。

架构参数一览：基于 DeepSeek-V3 的 MoE 结构

DeepSeek-Prover-V2-671B 与 DeepSeek-V3 共享同一架构，核心配置可从 config.json 直接读出：

对应的模型实现代码在 modeling_deepseek.py（DeepseekV3ForCausalLM类），配置类定义在 configuration_deepseek.py（DeepseekV3Config类）。

仓库里有什么：1.37TB 模型权重与关键文件

本仓库是 HuggingFace 上的官方镜像，包含完整的 671B 权重分片与推理所需全部文件：

• 📄 README.md —— 官方文档，含完整介绍、成绩、ProverBench 说明与推理示例
• ⚙️ config.json —— 模型架构超参数（上文表格的来源）
• 🧠 model-00001-of-000163.safetensors 至 model-00163-of-000163.safetensors —— 共163 个权重分片，总容量约1.37 TB（FP8）
• 🗂️ model.safetensors.index.json —— 91991 个张量到分片文件的映射索引
• 🔤 tokenizer.json 与 tokenizer_config.json —— 分词器
• 📜 LICENSE —— 模型使用许可（模型权重遵循 Model License）

💡 提示：671B 模型对硬件要求极高（FP8 权重约 1.4TB），普通单机难以部署；想本地体验可关注下文的 7B 版本。

快速上手：用 Transformers 跑通第一次定理证明

如果已下载到本地模型目录，可以直接用 HuggingFace Transformers 加载。官方 README.md 中给出了完整示例，核心流程如下：

from transformers import AutoModelForCausalLM, AutoTokenizer import torch model_id = "DeepSeek-Prover-V2-671B" # 本地目录或 Hub 地址 tokenizer = AutoTokenizer.from_pretrained(model_id) model = AutoModelForCausalLM.from_pretrained( model_id, device_map="auto", torch_dtype=torch.bfloat16, trust_remote_code=True ) # 将 Lean 4 定理填入提示词，要求模型先给出证明计划再补全证明 chat = [{"role": "user", "content": prompt.format(formal_statement)}] inputs = tokenizer.apply_chat_template(chat, tokenize=True, add_generation_prompt=True, return_tensors="pt").to(model.device) outputs = model.generate(inputs, max_new_tokens=8192) print(tokenizer.batch_decode(outputs))

官方示例中的题目是一道 algebra 题：

theorem mathd_algebra_10 : abs ((120 : ℝ) / 100 * 30 - 130 / 100 * 20) = 10 := by sorry

模型会先输出证明计划（关键思路、中间引理、证明结构），再补全sorry之后的正式 Lean 4 证明代码。

如果你只需要模型文件与文档，可以用镜像仓库获取：

git clone https://gitcode.com/hf_mirrors/deepseek-ai/DeepSeek-Prover-V2-671B

DeepSeek-Prover-V2-7B 与 671B 版本怎么选？

官方同时发布了两个规格：

另外，官方还配套发布了DeepSeek-ProverBench基准数据集：共325 道题，其中 15 道来自 AIME 24/25 竞赛题（数论与代数），其余 310 道来自教材与教程，覆盖线性代数（50）、微积分（90）、抽象代数（40）、实分析（30）等领域，是评估定理证明模型的实用工具。

常见问题 FAQ

Q1：DeepSeek-Prover-V2-671B 是免费开源的吗？模型权重已公开发布（本仓库即为镜像），但使用需遵守 LICENSE 中规定的模型协议，商用前请阅读条款。

Q2：它能直接帮我解数学作业题吗？它的强项是把已形式化的命题补全为可验证证明。你可以把题目翻译成 Lean 4 代码（或借助其他工具），再由模型完成证明，适合数学研究与 AI 系统学习实验。

Q3：MiniF2F 88.9% 意味着什么？MiniF2F 是形式化证明领域的通用"考试卷"，通过率越接近 100% 说明模型越接近完全掌握该证明体系。88.9% 代表了当前神经网络定理证明的最高水平。

小结

DeepSeek-Prover-V2-671B 用"递归证明搜索合成冷启动数据 + 强化学习"的组合拳，把非形式化推理与 Lean 4 形式化证明统一进一个 671B 的 MoE 模型，拿下 MiniF2F 88.9% 的 SOTA 成绩。无论你是想研究形式化定理证明、搭建AI 数学研究流水线，还是只是好奇"大模型如何证明数学定理"，这份开源模型 + ProverBench 基准的组合，都值得动手试一试 🚀

【免费下载链接】DeepSeek-Prover-V2-671B项目地址: https://ai.gitcode.com/hf_mirrors/deepseek-ai/DeepSeek-Prover-V2-671B