MiniF2F数据集解决方案：DeepSeek-Prover-V2自动生成证明代码全解析

【免费下载链接】DeepSeek-Prover-V2 项目地址: https://gitcode.com/gh_mirrors/de/DeepSeek-Prover-V2

DeepSeek-Prover-V2是一款专为Lean 4形式化定理证明设计的开源大语言模型，通过强化学习实现子目标分解，显著提升了MiniF2F等数学问题的自动证明能力。本文将全面解析其核心技术、性能表现及使用方法，帮助新手快速掌握这一强大工具。

1. 什么是DeepSeek-Prover-V2？

DeepSeek-Prover-V2是基于DeepSeek-V3开发的新一代定理证明模型，采用递归定理证明 pipeline 收集初始化数据。其冷启动训练过程通过提示DeepSeek-V3将复杂问题分解为一系列子目标，将已解决子目标的证明合成思维链，结合逐步推理创建强化学习的初始起点，实现了非形式化与形式化数学推理的统一。

图：DeepSeek-Prover-V2在MiniF2F-test、PutnamBench和ProverBench-AIME等数据集上的性能表现对比

2. 核心技术：从冷启动数据到强化学习

2.1 递归证明搜索合成冷启动推理数据

• 开发了简单高效的递归定理证明 pipeline，利用DeepSeek-V3作为子目标分解和形式化的统一工具
• 提示DeepSeek-V3将定理分解为高层证明框架，同时在Lean 4中形式化这些证明步骤，生成子目标序列
• 使用较小的7B模型处理每个子目标的证明搜索，降低计算负担
• 将挑战性问题的分解步骤与DeepSeek-V3的思维链配对，创建冷启动推理数据

2.2 基于合成冷启动数据的强化学习

• 精选7B证明器模型无法端到端解决但所有分解子目标已成功解决的挑战性问题子集
• 通过组合所有子目标的证明，构建原始问题的完整形式化证明
• 将证明附加到DeepSeek-V3的思维链中，产生非形式化推理与后续形式化的 cohesive 合成
• 在合成冷启动数据上微调证明器模型后，执行强化学习阶段，使用二元正确/不正确反馈作为主要奖励监督

3. 性能表现：MiniF2F数据集88.9%通过率

DeepSeek-Prover-V2-671B在神经定理证明方面实现了最先进的性能：

• 在MiniF2F-test上达到88.9%的通过率
• 解决了PutnamBench中658个问题中的49个
• 为miniF2F数据集生成的证明可通过minif2f-solutions.zip下载

4. ProverBench：AIME与教科书问题的形式化基准

ProverBench是包含325个问题的基准数据集，其中：

• 15个来自最近AIME竞赛（AIME 24和25）的数论和代数问题，提供真实的高中竞赛级挑战
• 310个来自精选教科书示例和教育教程，提供多样化且有教学基础的形式化数学问题集合

该基准旨在实现对高中竞赛问题和本科数学的更全面评估。

5. 模型与数据集下载

DeepSeek-Prover-V2提供两种模型规模：

• 7B参数模型：基于DeepSeek-Prover-V1.5-Base构建，上下文长度扩展至32K tokens
• 671B参数模型：在DeepSeek-V3-Base基础上训练

要开始使用，可通过以下步骤克隆仓库：

git clone https://gitcode.com/gh_mirrors/de/DeepSeek-Prover-V2

6. 快速开始：使用Huggingface Transformers进行推理

你可以直接使用Huggingface的Transformers库进行模型推理。DeepSeek-Prover-V2-671B与DeepSeek-V3共享相同架构。以下是为miniF2F数据集问题生成证明的基本示例：

from transformers import AutoModelForCausalLM, AutoTokenizer
import torch
torch.manual_seed(30)

model_id = "DeepSeek-Prover-V2-7B"  # 或使用 DeepSeek-Prover-V2-671B
tokenizer = AutoTokenizer.from_pretrained(model_id)

# 形式化命题
formal_statement = """
import Mathlib
import Aesop

set_option maxHeartbeats 0

open BigOperators Real Nat Topology Rat

/-- What is the positive difference between $120\%$ of 30 and $130\%$ of 20? Show that it is 10.-/
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 outlining the main proof steps and strategies. The plan should highlight key ideas, intermediate lemmas, and proof structures that will guide the construction of the final formal proof. """.strip()

chat = [ {"role": "user", "content": prompt.format(formal_statement)}, ]

加载模型并生成证明

model = AutoModelForCausalLM.from_pretrained(model_id, device_map="auto", torch_dtype=torch.bfloat16, trust_remote_code=True) inputs = tokenizer.apply_chat_template(chat, tokenize=True, add_generation_prompt=True, return_tensors="pt").to(model.device)

import time start = time.time() outputs = model.generate(inputs, max_new_tokens=8192) print(tokenizer.batch_decode(outputs)) print(time.time() - start)

## 7. 许可证信息

DeepSeek-Prover-V2模型的使用受[模型许可证](https://link.gitcode.com/i/05f91c40957fdf06dc2808c1e8b226b8)约束。

## 8. 获取更多帮助

如需了解更多详细信息和支持的功能，请参考[DeepSeek-Prover-V2论文](https://link.gitcode.com/i/7c6ecb8024b01d7ba4230b51b1e041de)。如有任何问题，可以提出issue或通过[service@deepseek.com](mailto:service@deepseek.com)联系开发团队。

【免费下载链接】DeepSeek-Prover-V2 项目地址: https://gitcode.com/gh_mirrors/de/DeepSeek-Prover-V2