Deepseek Prover V2 671B GGUF

🚀 DeepSeek-Prover-V2-671B

DeepSeek-Prover-V2-671B是一個專為Lean 4形式定理證明設計的開源大語言模型。它通過遞歸定理證明管道收集初始化數據，將非正式和正式的數學推理集成到統一模型中，在神經定理證明領域達到了先進水平。

🚀 快速開始

你可以直接使用 Huggingface的Transformers 進行模型推理。DeepSeek-Prover-V2-671B與DeepSeek-V3架構相同。詳細信息和支持的功能，請參考 Hugging Face上的DeepSeek-V3文檔。

以下是為miniF2F數據集中的問題生成證明的基本示例：

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

model_id = "DeepSeek-Prover-V2-7B"  # or 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)

## ✨ 主要特性
### 合成冷啟動推理數據的遞歸證明搜索
- 為構建冷啟動數據集，我們開發了一個簡單而有效的遞歸定理證明管道，利用DeepSeek-V3作為子目標分解和形式化的統一工具。我們促使DeepSeek-V3將定理分解為高級證明草圖，同時在Lean 4中對這些證明步驟進行形式化，從而得到一系列子目標。
- 我們使用一個較小的7B模型來處理每個子目標的證明搜索，從而減輕相關的計算負擔。一旦一個具有挑戰性的問題的分解步驟得到解決，我們將完整的逐步形式證明與DeepSeek-V3相應的思維鏈配對，以創建冷啟動推理數據。

### 合成冷啟動數據的強化學習
- 我們精心挑選了一組具有挑戰性的問題，這些問題無法由7B證明器模型以端到端的方式解決，但所有分解的子目標都已成功解決。通過組合所有子目標的證明，我們為原始問題構建了一個完整的形式證明。然後，將此證明附加到DeepSeek-V3的思維鏈上，該思維鏈概述了相應的引理分解，從而產生了非正式推理和後續形式化的連貫合成。
- 在合成冷啟動數據上對證明器模型進行微調後，我們進行了強化學習階段，以進一步增強其將非正式推理與形式證明構建相銜接的能力。遵循推理模型的標準訓練目標，我們使用二元正確或錯誤反饋作為主要的獎勵監督形式。
- 由此產生的模型DeepSeek-Prover-V2-671B在神經定理證明中達到了最先進的性能，在MiniF2F測試中達到了88.9%的通過率，並解決了PutnamBench中658個問題中的49個。DeepSeek-Prover-V2為miniF2F數據集生成的證明可作為 [ZIP存檔](https://github.com/deepseek-ai/DeepSeek-Prover-V2/blob/master/minif2f-solutions.zip) 下載。

### ProverBench：AIME和教科書問題的形式化
我們引入了ProverBench，這是一個包含325個問題的基準數據集。其中，15個問題是從最近AIME競賽（AIME 24和25）中的數論和代數問題形式化而來，提供了真實的高中競賽級挑戰。其餘310個問題來自精心挑選的教科書示例和教育教程，構成了一個多樣化且具有教學基礎的形式化數學問題集合。這個基準旨在能夠對高中競賽問題和本科水平的數學進行更全面的評估。

| 領域 | 數量 |
| ---- | ---- |
| AIME 24&25 | 15 |
| 數論 | 40 |
| 初等代數 | 30 |
| 線性代數 | 50 |
| 抽象代數 | 40 |
| 微積分 | 90 |
| 實分析 | 30 |
| 複分析 | 10 |
| 泛函分析 | 10 |
| 概率 | 10 |
| 總計 | 325 |

## 📦 安裝指南
文檔未提及安裝步驟，故跳過該章節。

## 💻 使用示例
### 基礎用法
以下是為miniF2F數據集中的問題生成證明的基本示例：
```python
from transformers import AutoModelForCausalLM, AutoTokenizer
import torch
torch.manual_seed(30)

model_id = "DeepSeek-Prover-V2-7B"  # or 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)

### 高級用法
文檔未提及高級用法示例，故跳過該部分。

## 📚 詳細文檔
### 模型與數據集下載
我們發佈了兩種模型大小的DeepSeek-Prover-V2：7B和671B參數。DeepSeek-Prover-V2-671B是在DeepSeek-V3-Base的基礎上進行訓練的。DeepSeek-Prover-V2-7B基於DeepSeek-Prover-V1.5-Base構建，並具有長達32K標記的擴展上下文長度。

| **模型** | **下載地址** |
| ---- | ---- |
| DeepSeek-Prover-V2-7B | [🤗 HuggingFace](https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-7B) |
| DeepSeek-Prover-V2-671B | [🤗 HuggingFace](https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B) |

| **數據集** | **下載地址** |
| ---- | ---- |
| DeepSeek-ProverBench | [🤗 HuggingFace](https://huggingface.co/datasets/deepseek-ai/DeepSeek-ProverBench) |

## 🔧 技術細節
### 合成冷啟動推理數據的遞歸證明搜索
- 為構建冷啟動數據集，我們開發了一個簡單而有效的遞歸定理證明管道，利用DeepSeek-V3作為子目標分解和形式化的統一工具。我們促使DeepSeek-V3將定理分解為高級證明草圖，同時在Lean 4中對這些證明步驟進行形式化，從而得到一系列子目標。
- 我們使用一個較小的7B模型來處理每個子目標的證明搜索，從而減輕相關的計算負擔。一旦一個具有挑戰性的問題的分解步驟得到解決，我們將完整的逐步形式證明與DeepSeek-V3相應的思維鏈配對，以創建冷啟動推理數據。

### 合成冷啟動數據的強化學習
- 我們精心挑選了一組具有挑戰性的問題，這些問題無法由7B證明器模型以端到端的方式解決，但所有分解的子目標都已成功解決。通過組合所有子目標的證明，我們為原始問題構建了一個完整的形式證明。然後，將此證明附加到DeepSeek-V3的思維鏈上，該思維鏈概述了相應的引理分解，從而產生了非正式推理和後續形式化的連貫合成。
- 在合成冷啟動數據上對證明器模型進行微調後，我們進行了強化學習階段，以進一步增強其將非正式推理與形式證明構建相銜接的能力。遵循推理模型的標準訓練目標，我們使用二元正確或錯誤反饋作為主要的獎勵監督形式。
- 由此產生的模型DeepSeek-Prover-V2-671B在神經定理證明中達到了最先進的性能，在MiniF2F測試中達到了88.9%的通過率，並解決了PutnamBench中658個問題中的49個。DeepSeek-Prover-V2為miniF2F數據集生成的證明可作為 [ZIP存檔](https://github.com/deepseek-ai/DeepSeek-Prover-V2/blob/master/minif2f-solutions.zip) 下載。

### ProverBench：AIME和教科書問題的形式化
我們引入了ProverBench，這是一個包含325個問題的基準數據集。其中，15個問題是從最近AIME競賽（AIME 24和25）中的數論和代數問題形式化而來，提供了真實的高中競賽級挑戰。其餘310個問題來自精心挑選的教科書示例和教育教程，構成了一個多樣化且具有教學基礎的形式化數學問題集合。這個基準旨在能夠對高中競賽問題和本科水平的數學進行更全面的評估。

## 📄 許可證
DeepSeek-Prover-V2模型的使用需遵循 [模型許可證](LICENSE-MODEL)。

## 📞 聯繫我們
如果您有任何問題，請提出問題或通過 [service@deepseek.com](mailto:service@deepseek.com) 與我們聯繫。