Update README.md
Browse files
README.md
CHANGED
@@ -7,36 +7,44 @@
|
|
7 |
</div>
|
8 |
<hr>
|
9 |
<div align="center" style="line-height: 1;">
|
10 |
-
<a href="https://www.deepseek.com/"
|
11 |
-
|
12 |
-
|
13 |
-
<
|
14 |
-
|
15 |
-
|
16 |
-
<a href="https://
|
17 |
-
|
18 |
-
|
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 |
-
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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
|
|
|
7 |
</div>
|
8 |
<hr>
|
9 |
<div align="center" style="line-height: 1;">
|
10 |
+
<a href="https://www.deepseek.com/" target="_blank" style="margin: 2px;">
|
11 |
+
<img alt="Homepage" src="https://github.com/deepseek-ai/DeepSeek-V2/blob/main/figures/badge.svg?raw=true" style="display: inline-block; vertical-align: middle;"/>
|
12 |
+
</a>
|
13 |
+
<a href="https://chat.deepseek.com/" target="_blank" style="margin: 2px;">
|
14 |
+
<img alt="Chat" src="https://img.shields.io/badge/🤖%20Chat-DeepSeek%20V3-536af5?color=536af5&logoColor=white" style="display: inline-block; vertical-align: middle;"/>
|
15 |
+
</a>
|
16 |
+
<a href="https://huggingface.co/deepseek-ai" target="_blank" style="margin: 2px;">
|
17 |
+
<img alt="Hugging Face" src="https://img.shields.io/badge/%F0%9F%A4%97%20Hugging%20Face-DeepSeek%20AI-ffc107?color=ffc107&logoColor=white" style="display: inline-block; vertical-align: middle;"/>
|
18 |
+
</a>
|
|
|
|
|
|
|
19 |
</div>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
20 |
|
21 |
+
<div align="center" style="line-height: 1;">
|
22 |
+
<a href="https://discord.gg/Tc7c45Zzu5" target="_blank" style="margin: 2px;">
|
23 |
+
<img alt="Discord" src="https://img.shields.io/badge/Discord-DeepSeek%20AI-7289da?logo=discord&logoColor=white&color=7289da" style="display: inline-block; vertical-align: middle;"/>
|
24 |
+
</a>
|
25 |
+
<a href="https://github.com/deepseek-ai/DeepSeek-V2/blob/main/figures/qr.jpeg?raw=true" target="_blank" style="margin: 2px;">
|
26 |
+
<img alt="Wechat" src="https://img.shields.io/badge/WeChat-DeepSeek%20AI-brightgreen?logo=wechat&logoColor=white" style="display: inline-block; vertical-align: middle;"/>
|
27 |
+
</a>
|
28 |
+
<a href="https://twitter.com/deepseek_ai" target="_blank" style="margin: 2px;">
|
29 |
+
<img alt="Twitter Follow" src="https://img.shields.io/badge/Twitter-deepseek_ai-white?logo=x&logoColor=white" style="display: inline-block; vertical-align: middle;"/>
|
30 |
+
</a>
|
31 |
+
</div>
|
32 |
+
|
33 |
+
<div align="center" style="line-height: 1;">
|
34 |
+
<a href="https://github.com/deepseek-ai/DeepSeek-V3/blob/main/LICENSE-CODE" style="margin: 2px;">
|
35 |
+
<img alt="Code License" src="https://img.shields.io/badge/Code_License-MIT-f5de53?&color=f5de53" style="display: inline-block; vertical-align: middle;"/>
|
36 |
+
</a>
|
37 |
+
<a href="https://github.com/deepseek-ai/DeepSeek-V3/blob/main/LICENSE-MODEL" style="margin: 2px;">
|
38 |
+
<img alt="Model License" src="https://img.shields.io/badge/Model_License-Model_Agreement-f5de53?&color=f5de53" style="display: inline-block; vertical-align: middle;"/>
|
39 |
+
</a>
|
40 |
+
</div>
|
41 |
|
42 |
## 1. Introduction
|
43 |
|
44 |
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.
|
45 |
|
46 |
<p align="center">
|
47 |
+
<img width="100%" src="https://github.com/deepseek-ai/DeepSeek-Prover-V2/blob/main/figures/performance.png">
|
48 |
</p>
|
49 |
|
50 |
## 2. Model Summary
|