DeepSeek-Prover-V2：开源形式化数学定理证明模型

DeepSeek发布Prover-V2，用强化学习分解子目标，提升形式化数学推理能力，性能卓越，并在MiniF2F测试中达到88.9%通过率，模型及数据集可在Hugging Face下载。

• DeepSeek-Prover-V2 发布： 深寻科技发布了 DeepSeek-Prover-V2，一款用于形式化数学定理证明的开源大型语言模型。

• 核心能力： 通过强化学习进行子目标分解，从而推进形式化数学推理。

• 训练方式：

  • 利用 DeepSeek-V3 将复杂问题分解为子目标。
  • 将已解决子目标的证明合成为连贯的思维链，结合 DeepSeek-V3 的逐步推理，为强化学习提供初始数据。
  • 整合非形式化和形式化数学推理到一个统一的模型中。

• 冷启动数据集构建：

  • 使用 DeepSeek-V3 作为统一工具，进行子目标分解和形式化。
  • DeepSeek-V3 将定理分解为高级证明草图，并同步用 Lean 4 形式化这些步骤，生成一系列子目标。
  • 使用较小的 7B 模型处理每个子目标的证明搜索，降低计算负担。
  • 将完整的形式化证明与 DeepSeek-V3 的思维链配对，创建冷启动推理数据。

• 强化学习阶段：

  • 选择 7B 证明模型无法端到端解决，但所有分解的子目标已成功解决的难题。
  • 组合所有子目标的证明，构建原始问题的完整形式化证明。
  • 将此证明添加到 DeepSeek-V3 的思维链中，综合非形式化推理和后续形式化。
  • 使用二元正确/错误反馈作为主要奖励监督，进行强化学习，提高模型连接非形式化推理和形式化证明构建的能力。

• 模型性能：

  • DeepSeek-Prover-V2-671B 在神经定理证明方面达到最先进的性能。
  • 在 MiniF2F-test 上达到 88.9% 的通过率。
  • 解决了 PutnamBench 中的 658 个问题中的 49 个。

• ProverBench 基准数据集：

  • 包含 325 个问题。
  • 15 个来自 AIME 竞赛中的数论和代数问题（AIME 24 和 25）。
  • 310 个来自教科书示例和教育教程。
  • 旨在更全面地评估高中竞赛问题和本科水平的数学问题。

• 模型和数据集下载：

  • 提供 7B 和 671B 两种模型尺寸。
  • DeepSeek-Prover-V2-671B 基于 DeepSeek-V3-Base 训练。
  • DeepSeek-Prover-V2-7B 基于 DeepSeek-Prover-V1.5-Base 构建，具有高达 32K tokens 的扩展上下文长度。
  • Hugging Face 上提供模型和数据集下载。

• 快速开始：

  • 使用 Hugging Face 的 Transformers 进行模型推理。
  • DeepSeek-Prover-V2-671B 与 DeepSeek-V3 共享相同的架构。
  • 提供使用示例，展示如何为 miniF2F 数据集中的问题生成证明。