🚀 DeepSeek-Prover-V2
DeepSeek-Prover-V2 是一個用於 Lean 4 形式定理證明的開源大語言模型。它藉助由 DeepSeek-V3 驅動的遞歸定理證明管道收集初始化數據,將非正式和正式的數學推理集成到統一模型中,在神經定理證明領域取得了卓越的性能。
🚀 快速開始
你可以直接使用 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"
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) 下載。
## 📦 安裝指南
文檔未提及安裝步驟,故跳過此章節。
## 💻 使用示例
### 基礎用法
```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)
### 高級用法
文檔未提及高級用法相關代碼示例,故跳過此部分。
## 📚 詳細文檔
### ProverBench:AIME 和教科書問題的形式化
我們引入了 ProverBench,這是一個包含 325 個問題的基準數據集。其中,15 個問題是從最近的 AIME 競賽(AIME 24 和 25)中的數論和代數問題形式化而來,提供了真實的高中競賽級別的挑戰。其餘 310 個問題來自精心挑選的教科書示例和教育教程,構成了一個多樣化且具有教學基礎的形式化數學問題集合。這個基準旨在能夠對高中競賽問題和本科水平的數學進行更全面的評估。
<div align="center">
| 領域 | 數量 |
| ---- | ---- |
| AIME 24&25 | 15 |
| 數論 | 40 |
| 初等代數 | 30 |
| 線性代數 | 50 |
| 抽象代數 | 40 |
| 微積分 | 90 |
| 實分析 | 30 |
| 複分析 | 10 |
| 泛函分析 | 10 |
| 概率論 | 10 |
| 總計 | 325 |
</div>
### 模型與數據集下載
我們發佈了兩種模型大小的 DeepSeek-Prover-V2:7B 和 671B 參數。DeepSeek-Prover-V2-671B 是在 DeepSeek-V3-Base 上進行訓練的。DeepSeek-Prover-V2-7B 基於 DeepSeek-Prover-V1.5-Base 構建,並具有長達 32K 標記的擴展上下文長度。
<div align="center">
| **模型** | **下載地址** |
| ---- | ---- |
| 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) |
</div>
<div align="center">
| **數據集** | **下載地址** |
| ---- | ---- |
| DeepSeek-ProverBench | [ü§ó HuggingFace](https://huggingface.co/datasets/deepseek-ai/DeepSeek-ProverBench) |
</div>
## 🔧 技術細節
文檔未提及技術實現細節相關內容,故跳過此章節。
## 📄 許可證
使用 DeepSeek-Prover-V2 模型需遵循 [模型許可證](LICENSE-MODEL)。
## 📞 聯繫我們
如果您有任何問題,請提出問題或通過 [service@deepseek.com](mailto:service@deepseek.com) 與我們聯繫。