Update README.md
Browse files
README.md
CHANGED
|
@@ -1,170 +1,162 @@
|
|
| 1 |
-
<!-- markdownlint-disable first-line-h1 -->
|
| 2 |
-
<!-- markdownlint-disable html -->
|
| 3 |
-
<!-- markdownlint-disable no-duplicate-header -->
|
| 4 |
-
|
| 5 |
-
<div align="center">
|
| 6 |
-
<img src="https://github.com/deepseek-ai/DeepSeek-V2/blob/main/figures/logo.svg?raw=true" width="60%" alt="DeepSeek-V3" />
|
| 7 |
-
</div>
|
| 8 |
-
<hr>
|
| 9 |
-
<div align="center" style="line-height: 1;">
|
| 10 |
-
<a href="https://www.deepseek.com/"><img alt="Homepage"
|
| 11 |
-
|
| 12 |
-
<a href="https://
|
| 13 |
-
|
| 14 |
-
<a href="https://
|
| 15 |
-
|
| 16 |
-
<
|
| 17 |
-
<
|
| 18 |
-
|
| 19 |
-
<a href="https://github.com/deepseek-ai/DeepSeek-
|
| 20 |
-
|
| 21 |
-
<a href="https://
|
| 22 |
-
|
| 23 |
-
|
| 24 |
-
<a href="
|
| 25 |
-
|
| 26 |
-
<a href="
|
| 27 |
-
|
| 28 |
-
<
|
| 29 |
-
<a href="
|
| 30 |
-
</
|
| 31 |
-
|
| 32 |
-
|
| 33 |
-
|
| 34 |
-
|
| 35 |
-
|
| 36 |
-
|
| 37 |
-
|
| 38 |
-
|
| 39 |
-
|
| 40 |
-
|
| 41 |
-
|
| 42 |
-
##
|
| 43 |
-
|
| 44 |
-
|
| 45 |
-
|
| 46 |
-
|
| 47 |
-
|
| 48 |
-
|
| 49 |
-
|
| 50 |
-
|
| 51 |
-
|
| 52 |
-
---
|
| 53 |
-
|
| 54 |
-
**
|
| 55 |
-
|
| 56 |
-
-
|
| 57 |
-
|
| 58 |
-
-
|
| 59 |
-
|
| 60 |
-
|
| 61 |
-
|
| 62 |
-
|
| 63 |
-
|
| 64 |
-
|
| 65 |
-
|
| 66 |
-
|
| 67 |
-
|
| 68 |
-
|
| 69 |
-
|
| 70 |
-
|
| 71 |
-
|
| 72 |
-
|
| 73 |
-
|
| 74 |
-
|
| 75 |
-
|
| 76 |
-
|
| 77 |
-
|
|
| 78 |
-
|
|
| 79 |
-
|
|
| 80 |
-
|
|
| 81 |
-
|
|
| 82 |
-
|
| 83 |
-
|
| 84 |
-
|
| 85 |
-
|
| 86 |
-
|
| 87 |
-
|
| 88 |
-
|
| 89 |
-
|
| 90 |
-
|
| 91 |
-
|
| 92 |
-
|
| 93 |
-
|
| 94 |
-
|
| 95 |
-
|
| 96 |
-
|
| 97 |
-
|
| 98 |
-
|
| 99 |
-
|
| 100 |
-
|
|
| 101 |
-
|
|
| 102 |
-
| DeepSeek-
|
| 103 |
-
|
| 104 |
-
</div>
|
| 105 |
-
|
| 106 |
-
|
| 107 |
-
|
| 108 |
-
|
| 109 |
-
|
| 110 |
-
|
| 111 |
-
|
| 112 |
-
|
| 113 |
-
|
| 114 |
-
|
| 115 |
-
|
| 116 |
-
|
| 117 |
-
|
| 118 |
-
|
| 119 |
-
|
| 120 |
-
|
| 121 |
-
import
|
| 122 |
-
|
| 123 |
-
|
| 124 |
-
|
| 125 |
-
|
| 126 |
-
|
| 127 |
-
|
| 128 |
-
|
| 129 |
-
|
| 130 |
-
|
| 131 |
-
|
| 132 |
-
|
| 133 |
-
|
| 134 |
-
|
| 135 |
-
|
| 136 |
-
|
| 137 |
-
|
| 138 |
-
|
| 139 |
-
|
| 140 |
-
|
| 141 |
-
|
| 142 |
-
|
| 143 |
-
|
| 144 |
-
{}
|
| 145 |
-
|
| 146 |
-
|
| 147 |
-
|
| 148 |
-
|
| 149 |
-
|
| 150 |
-
|
| 151 |
-
|
| 152 |
-
|
| 153 |
-
|
| 154 |
-
|
| 155 |
-
|
| 156 |
-
|
| 157 |
-
|
| 158 |
-
|
| 159 |
-
|
| 160 |
-
|
| 161 |
-
|
| 162 |
-
|
| 163 |
-
````
|
| 164 |
-
|
| 165 |
-
## 6. License
|
| 166 |
-
The use of DeepSeek-Prover-V2 models is subject to [the Model License](LICENSE-MODEL).
|
| 167 |
-
|
| 168 |
-
## 7. Contact
|
| 169 |
-
|
| 170 |
-
If you have any questions, please raise an issue or contact us at [[email protected]](mailto:[email protected]).
|
|
|
|
| 1 |
+
<!-- markdownlint-disable first-line-h1 -->
|
| 2 |
+
<!-- markdownlint-disable html -->
|
| 3 |
+
<!-- markdownlint-disable no-duplicate-header -->
|
| 4 |
+
|
| 5 |
+
<div align="center">
|
| 6 |
+
<img src="https://github.com/deepseek-ai/DeepSeek-V2/blob/main/figures/logo.svg?raw=true" width="60%" alt="DeepSeek-V3" />
|
| 7 |
+
</div>
|
| 8 |
+
<hr>
|
| 9 |
+
<div align="center" style="line-height: 1;">
|
| 10 |
+
<a href="https://www.deepseek.com/"><img alt="Homepage" src="https://github.com/deepseek-ai/DeepSeek-V2/blob/main/figures/badge.svg?raw=true"/></a>
|
| 11 |
+
<a href="https://chat.deepseek.com/"><img alt="Chat" src="https://img.shields.io/badge/🤖%20Chat-DeepSeek%20V3-536af5?color=536af5&logoColor=white"/></a>
|
| 12 |
+
<a href="https://huggingface.co/deepseek-ai"><img alt="Hugging Face" src="https://img.shields.io/badge/%F0%9F%A4%97%20Hugging%20Face-DeepSeek%20AI-ffc107?color=ffc107&logoColor=white"/></a>
|
| 13 |
+
<br>
|
| 14 |
+
<a href="https://discord.gg/Tc7c45Zzu5"><img alt="Discord" src="https://img.shields.io/badge/Discord-DeepSeek%20AI-7289da?logo=discord&logoColor=white&color=7289da"/></a>
|
| 15 |
+
<a href="https://github.com/deepseek-ai/DeepSeek-V2/blob/main/figures/qr.jpeg?raw=true"><img alt="Wechat" src="https://img.shields.io/badge/WeChat-DeepSeek%20AI-brightgreen?logo=wechat&logoColor=white"/></a>
|
| 16 |
+
<a href="https://twitter.com/deepseek_ai"><img alt="Twitter Follow" src="https://img.shields.io/badge/Twitter-deepseek_ai-white?logo=x&logoColor=white"/></a>
|
| 17 |
+
<br>
|
| 18 |
+
<a href="https://github.com/deepseek-ai/DeepSeek-V3/blob/main/LICENSE-CODE"><img alt="Code License" src="https://img.shields.io/badge/Code_License-MIT-f5de53?&color=f5de53"/></a>
|
| 19 |
+
<a href="https://github.com/deepseek-ai/DeepSeek-V3/blob/main/LICENSE-MODEL"><img alt="Model License" src="https://img.shields.io/badge/Model_License-Model_Agreement-f5de53?&color=f5de53"/></a>
|
| 20 |
+
<br>
|
| 21 |
+
<a href="https://github.com/deepseek-ai/DeepSeek-Prover-V2/blob/master/DeepSeek_Prover_V2.pdf"><b>Paper Link</b>👁️</a>
|
| 22 |
+
</div>
|
| 23 |
+
<p align="center">
|
| 24 |
+
<a href="#2-model-summary">Model Summary</a> |
|
| 25 |
+
<a href="#3-proverbench">ProverBench</a> |
|
| 26 |
+
<a href="#4-model-dataset-downloads">Model&Dataset Download</a> |
|
| 27 |
+
<a href="#5-quick-start">Quick Start</a> |
|
| 28 |
+
<a href="#6-license">License</a> |
|
| 29 |
+
<a href="#7-contact">Contact</a>
|
| 30 |
+
</p>
|
| 31 |
+
|
| 32 |
+
# DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition
|
| 33 |
+
|
| 34 |
+
## 1. Introduction
|
| 35 |
+
|
| 36 |
+
We introduce DeepSeek-Prover-V2, an open-source large language model designed for formal theorem proving in Lean 4, with initialization data collected through a recursive theorem proving pipeline powered by DeepSeek-V3. The cold-start training procedure begins by prompting DeepSeek-V3 to decompose complex problems into a series of subgoals. The proofs of resolved subgoals are synthesized into a chain-of-thought process, combined with DeepSeek-V3's step-by-step reasoning, to create an initial cold start for reinforcement learning. This process enables us to integrate both informal and formal mathematical reasoning into a unified model.
|
| 37 |
+
|
| 38 |
+
<p align="center">
|
| 39 |
+
<img width="100%" src="figures/performance.png">
|
| 40 |
+
</p>
|
| 41 |
+
|
| 42 |
+
## 2. Model Summary
|
| 43 |
+
|
| 44 |
+
---
|
| 45 |
+
|
| 46 |
+
**Synthesize Cold-Start Reasoning Data through Recursive Proof Search**
|
| 47 |
+
|
| 48 |
+
- To construct the cold-start dataset, we develop a simple yet effective pipeline for recursive theorem proving, utilizing DeepSeek-V3 as a unified tool for both subgoal decomposition and formalization. We prompt DeepSeek-V3 to decompose theorems into high-level proof sketches while simultaneously formalizing these proof steps in Lean 4, resulting in a sequence of subgoals.
|
| 49 |
+
|
| 50 |
+
- We use a smaller 7B model to handle the proof search for each subgoal, thereby reducing the associated computational burden. Once the decomposed steps of a challenging problem are resolved, we pair the complete step-by-step formal proof with the corresponding chain-of-thought from DeepSeek-V3 to create cold-start reasoning data.
|
| 51 |
+
|
| 52 |
+
---
|
| 53 |
+
|
| 54 |
+
**Reinforcement Learning with Synthetic Cold-Start Data**
|
| 55 |
+
|
| 56 |
+
- We curate a subset of challenging problems that remain unsolved by the 7B prover model in an end-to-end manner, but for which all decomposed subgoals have been successfully resolved. By composing the proofs of all subgoals, we construct a complete formal proof for the original problem. This proof is then appended to DeepSeek-V3's chain-of-thought, which outlines the corresponding lemma decomposition, thereby producing a cohesive synthesis of informal reasoning and subsequent formalization.
|
| 57 |
+
|
| 58 |
+
- After fine-tuning the prover model on the synthetic cold-start data, we perform a reinforcement learning stage to further enhance its ability to bridge informal reasoning with formal proof construction. Following the standard training objective for reasoning models, we use binary correct-or-incorrect feedback as the primary form of reward supervision.
|
| 59 |
+
- The resulting model, DeepSeek-Prover-V2-671B, achieves state-of-the-art performance in neural theorem proving, reaching $88.9$% pass ratio on the MiniF2F-test and solving 49 out of 658 problems from PutnamBench. The proofs generated by DeepSeek-Prover-V2 for the miniF2F dataset are available for download as a [ZIP archive](https://github.com/deepseek-ai/DeepSeek-Prover-V2/blob/master/minif2f-solutions.zip).
|
| 60 |
+
|
| 61 |
+
---
|
| 62 |
+
|
| 63 |
+
## 3. ProverBench: Formalization of AIME and Textbook Problems
|
| 64 |
+
|
| 65 |
+
we introduce ProverBench, a benchmark dataset comprising 325 problems. Of these, 15 are formalized from number theory and algebra questions featured in the recent AIME competitions (AIME 24 and 25), offering authentic high-school competition-level challenges. The remaining 310 problems are drawn from curated textbook examples and educational tutorials, contributing a diverse and pedagogically grounded collection of formalized mathematical problems. This benchmark is designed to enable more comprehensive evaluation across both high-school competition problems and undergraduate-level mathematics.
|
| 66 |
+
|
| 67 |
+
<div align="center">
|
| 68 |
+
|
| 69 |
+
| Area | Count |
|
| 70 |
+
| :---------------------: | :-------: |
|
| 71 |
+
| AIME 24&25 | 15 |
|
| 72 |
+
| Number Theory | 40 |
|
| 73 |
+
| Elementary Algebra | 30 |
|
| 74 |
+
| Linear Algebra | 50 |
|
| 75 |
+
| Abstract Algebra | 40 |
|
| 76 |
+
| Calculus | 90 |
|
| 77 |
+
| Real Analysis | 30 |
|
| 78 |
+
| Complex Analysis | 10 |
|
| 79 |
+
| Functional Analysis | 10 |
|
| 80 |
+
| Probability | 10 |
|
| 81 |
+
| Total | 325 |
|
| 82 |
+
|
| 83 |
+
</div>
|
| 84 |
+
|
| 85 |
+
## 4. Model & Dataset Downloads
|
| 86 |
+
|
| 87 |
+
We release DeepSeek-Prover-V2 in two model sizes: 7B and 671B parameters. DeepSeek-Prover-V2-671B is trained on top of DeepSeek-V3-Base. DeepSeek-Prover-V2-7B is built upon DeepSeek-Prover-V1.5-Base and features an extended context length of up to 32K tokens.
|
| 88 |
+
|
| 89 |
+
<div align="center">
|
| 90 |
+
|
| 91 |
+
| **Model** | **Download** |
|
| 92 |
+
| :-----------------------------: | :----------------------------------------------------------: |
|
| 93 |
+
| DeepSeek-Prover-V2-7B | [🤗 HuggingFace](https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-7B) |
|
| 94 |
+
| DeepSeek-Prover-V2-671B | [🤗 HuggingFace](https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B) |
|
| 95 |
+
|
| 96 |
+
</div>
|
| 97 |
+
|
| 98 |
+
<div align="center">
|
| 99 |
+
|
| 100 |
+
| **Dataset** | **Download** |
|
| 101 |
+
| :-----------------------------: | :----------------------------------------------------------: |
|
| 102 |
+
| DeepSeek-ProverBench | [🤗 HuggingFace](https://huggingface.co/datasets/deepseek-ai/DeepSeek-ProverBench) |
|
| 103 |
+
|
| 104 |
+
</div>
|
| 105 |
+
|
| 106 |
+
## 5. Quick Start
|
| 107 |
+
|
| 108 |
+
You can directly use [Huggingface's Transformers](https://github.com/huggingface/transformers) for model inference. DeepSeek-Prover-V2-671B shares the same architecture as DeepSeek-V3. For detailed information and supported features, please refer to [the DeepSeek-V3 documentation on Hugging Face](https://github.com/huggingface/transformers/blob/main/docs/source/en/model_doc/deepseek_v3.md).
|
| 109 |
+
|
| 110 |
+
The following is a basic example of generating a proof for a problem from the miniF2F dataset:
|
| 111 |
+
````python
|
| 112 |
+
from transformers import AutoModelForCausalLM, AutoTokenizer
|
| 113 |
+
import torch
|
| 114 |
+
torch.manual_seed(30)
|
| 115 |
+
|
| 116 |
+
model_id = "DeepSeek-Prover-V2-7B" # or DeepSeek-Prover-V2-671B
|
| 117 |
+
tokenizer = AutoTokenizer.from_pretrained(model_id)
|
| 118 |
+
|
| 119 |
+
formal_statement = """
|
| 120 |
+
import Mathlib
|
| 121 |
+
import Aesop
|
| 122 |
+
|
| 123 |
+
set_option maxHeartbeats 0
|
| 124 |
+
|
| 125 |
+
open BigOperators Real Nat Topology Rat
|
| 126 |
+
|
| 127 |
+
/-- What is the positive difference between $120\%$ of 30 and $130\%$ of 20? Show that it is 10.-/
|
| 128 |
+
theorem mathd_algebra_10 : abs ((120 : ℝ) / 100 * 30 - 130 / 100 * 20) = 10 := by
|
| 129 |
+
sorry
|
| 130 |
+
""".strip()
|
| 131 |
+
|
| 132 |
+
prompt = """
|
| 133 |
+
Complete the following Lean 4 code:
|
| 134 |
+
|
| 135 |
+
```lean4
|
| 136 |
+
{}
|
| 137 |
+
```
|
| 138 |
+
|
| 139 |
+
Before producing the Lean 4 code to formally prove the given theorem, provide a detailed proof plan outlining the main proof steps and strategies.
|
| 140 |
+
The plan should highlight key ideas, intermediate lemmas, and proof structures that will guide the construction of the final formal proof.
|
| 141 |
+
""".strip()
|
| 142 |
+
|
| 143 |
+
chat = [
|
| 144 |
+
{"role": "user", "content": prompt.format(formal_statement)},
|
| 145 |
+
]
|
| 146 |
+
|
| 147 |
+
model = AutoModelForCausalLM.from_pretrained(model_id, device_map="auto", torch_dtype=torch.bfloat16, trust_remote_code=True)
|
| 148 |
+
inputs = tokenizer.apply_chat_template(chat, tokenize=True, add_generation_prompt=True, return_tensors="pt").to(model.device)
|
| 149 |
+
|
| 150 |
+
import time
|
| 151 |
+
start = time.time()
|
| 152 |
+
outputs = model.generate(inputs, max_new_tokens=8192)
|
| 153 |
+
print(tokenizer.batch_decode(outputs))
|
| 154 |
+
print(time.time() - start)
|
| 155 |
+
````
|
| 156 |
+
|
| 157 |
+
## 6. License
|
| 158 |
+
The use of DeepSeek-Prover-V2 models is subject to [the Model License](LICENSE-MODEL).
|
| 159 |
+
|
| 160 |
+
## 7. Contact
|
| 161 |
+
|
| 162 |
+
If you have any questions, please raise an issue or contact us at [[email protected]](mailto:service@deepseek.com).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|