摘要：DeepSeek-Prover-V2 是一个开源的大型语言模型，专为 Lean 4 形式化定理证明而设计。该模型的初始化数据是通过 DeepSeek-V3 驱动的递归定理证明流程收集而来。其冷启动训练过程始于提示 DeepSeek-V3 将复杂问题分解为一系列

大家好，我是 Ai 学习的老章

DeepSeek 一贯的作风，先敲不作声放出模型文件，随后才公布技术细节。

1 小时前，DeepSeek 在其 GitHub 账号放出了部分技术文档和论文

1. 引言：形式化推理的挑战与 DeepSeek 的方案

DeepSeek-Prover-V2 是一个开源的大型语言模型，专为 Lean 4 形式化定理证明而设计。该模型的初始化数据是通过 DeepSeek-V3 驱动的递归定理证明流程收集而来。其冷启动训练过程始于提示 DeepSeek-V3 将复杂问题分解为一系列子目标。已解决子目标的证明被合成为思维链过程，结合 DeepSeek-V3 的逐步推理，为强化学习创建初始冷启动。这一过程使我们能够将非形式化和形式化数学推理整合到一个统一的模型中。

DeepSeek-Prover-V2 正是为了应对这一挑战而生，其核心创新在于：

结合非形式化与形式化推理：利用强大的基础模型 (DeepSeek-V3) 进行初始的非形式化推理（如生成证明思路、分解问题），然后将其与严谨的形式化证明步骤相结合。

强化学习优化：通过强化学习，特别是利用子目标分解的策略，进一步提升模型在形式化证明构建中的能力。

DeepSeek-Prover-V2 的训练过程独具特色，主要包含两个阶段：

a) 冷启动数据合成 (Synthesize Cold-Start Reasoning Data)

递归证明流水线：团队开发了一个简洁有效的递归定理证明流水线。首先，利用 DeepSeek-V3 将复杂的定理分解为高级别的证明草图（Proof Sketches）和一系列子目标（Subgoals）。

子目标证明：为了降低计算成本，使用一个较小的 7B 参数模型来处理每个子目标的证明搜索。

数据合成：当一个复杂问题的所有子目标都被解决后，将完整的、逐步的形式化证明（由子目标证明组合而成）与 DeepSeek-V3 生成的相应思维链（Chain-of-Thought, CoT，包含高级证明思路和引理分解）配对，形成用于模型初始训练的“冷启动”推理数据。这一过程巧妙地将非形式化的解题思路与形式化的证明步骤融为一体。

b) 基于合成数据的强化学习 (Reinforcement Learning with Synthetic Cold-Start Data)

筛选挑战性问题：选取一部分对于 7B 模型来说端到端无法解决、但其所有分解子目标都已被成功证明的难题。

数据增强：将这些难题的完整形式化证明（由子目标证明拼接而成）附加到 DeepSeek-V3 对应的 CoT 后面，生成更丰富的训练数据。

强化学习微调：在冷启动数据上进行初步微调后，采用强化学习进一步优化模型。奖励信号主要采用二元反馈（证明正确或错误），目标是增强模型连接非形式化推理和形式化证明构建的能力。

DeepSeek-Prover-V2 发布了两个尺寸的模型：

DeepSeek-Prover-V2-7B:基于 DeepSeek-Prover-V1.5-Base 构建，上下文长度扩展至 32K tokens。

DeepSeek-Prover-V2-671B:基于 DeepSeek-V3-Base 训练。

性能方面，DeepSeek-Prover-V2-671B表现出色，达到了当前神经定理证明领域的 SOTA (State-of-the-Art) 水平：

在MiniF2F-test数据集上达到88.9%的通过率。

解决了PutnamBench数据集中 658 个问题中的49个。

团队还公开了模型在 miniF2F 数据集上生成的证明，可供下载研究：minif2f-solutions.zip[1]

为了更全面地评估模型在不同难度数学问题上的能力，团队还推出了ProverBench基准测试集，包含 325 个问题：

15 个 AIME 问题：来自近两年的美国数学邀请赛 (AIME 24, 25) 的数论和代数题目，代表了真实的高中竞赛水平挑战。

310 个教科书/教程问题：来自精选的教科书案例和教育教程，提供了多样化且具有教学意义的形式化数学问题。

ProverBench 旨在覆盖从高中竞赛到本科水平的数学问题，为形式化推理模型的评估提供了更丰富的视角。

ProverBench 数据集地址：https://huggingface.co/datasets/deepseek-ai/DeepSeek-ProverBench[2]

5. 如何开始使用 DeepSeek-Prover-V2

模型下载：

7B 模型： https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-7B [3]

671B 模型： https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B [4]

架构说明：DeepSeek-Prover-V2-671B 与 DeepSeek-V3 共享相同架构，详细信息可参考 Hugging Face 上的 DeepSeek-V3 文档 [5] 。

制作不易，如果这篇文章觉得对你有用，可否点个关注。给我个三连击：点赞、转发和在看。若可以再给我加个，谢谢你看我的文章，我们下篇再见！

minif2f-solutions.zip: https://github.com/deepseek-ai/DeepSeek-Prover-V2/raw/master/minif2f-solutions.zip

https://huggingface.co/datasets/deepseek-ai/DeepSeek-ProverBench: https://huggingface.co/datasets/deepseek-ai/DeepSeek-ProverBench

https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-7B: https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-7B

https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B: https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B

[5]

Hugging Face 上的 DeepSeek-V3 文档: https://github.com/huggingface/transformers/blob/main/docs/source/en/model_doc/deepseek_v3.md

来源：科学大厦汇