DeepSeek-Prover-V1

<!-- markdownlint-disable first-line-h1 -->
<!-- markdownlint-disable html -->
<!-- markdownlint-disable no-duplicate-header -->

<div align="center">
<img src="https://github.com/deepseek-ai/DeepSeek-V2/blob/main/figures/logo.svg?raw=true" width="60%" alt="DeepSeek-V2" />
</div>
<hr>
<div align="center" style="line-height: 1;">
<a href="https://www.deepseek.com/" target="_blank" style="margin: 2px;">
<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;"/>
</a>
<a href="https://chat.deepseek.com/" target="_blank" style="margin: 2px;">
<img alt="Chat" src="https://img.shields.io/badge/🤖%20Chat-DeepSeek%20V2-536af5?color=536af5&logoColor=white" style="display: inline-block; vertical-align: middle;"/>
</a>
<a href="https://huggingface.co/deepseek-ai" target="_blank" style="margin: 2px;">
<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;"/>
</a>
</div>

<div align="center" style="line-height: 1;">
<a href="https://discord.gg/Tc7c45Zzu5" target="_blank" style="margin: 2px;">
<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;"/>
</a>
<a href="https://github.com/deepseek-ai/DeepSeek-V2/blob/main/figures/qr.jpeg?raw=true" target="_blank" style="margin: 2px;">
<img alt="Wechat" src="https://img.shields.io/badge/WeChat-DeepSeek%20AI-brightgreen?logo=wechat&logoColor=white" style="display: inline-block; vertical-align: middle;"/>
</a>
<a href="https://twitter.com/deepseek_ai" target="_blank" style="margin: 2px;">
<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;"/>
</a>
</div>
<div align="center" style="line-height: 1;">
<a href="https://github.com/deepseek-ai/DeepSeek-V2/blob/main/LICENSE-CODE" style="margin: 2px;">
<img alt="Code License" src="https://img.shields.io/badge/Code_License-MIT-f5de53?&color=f5de53" style="display: inline-block; vertical-align: middle;"/>
</a>
<a href="https://github.com/deepseek-ai/DeepSeek-V2/blob/main/LICENSE-MODEL" style="margin: 2px;">
<img alt="Model License" src="https://img.shields.io/badge/Model_License-Model_Agreement-f5de53?&color=f5de53" style="display: inline-block; vertical-align: middle;"/>
</a>
</div>
<p align="center">
<a href="#2-evaluation-results">Evaluation Results</a> |
<a href="#3-model-&amp;-dataset-downloads">Model & Dataset Downloads</a> |
<a href="#4-license">License</a> |
<a href="#5-contact">Contact</a>
</p>

<p align="center">
<a href="https://arxiv.org/abs/2405.14333"><b>Paper Link</b>👁️</a>
</p>

# DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data

## 1. Introduction

Proof assistants like Lean have revolutionized mathematical proof verification, ensuring high accuracy and reliability. Although large language models (LLMs) show promise in mathematical reasoning, their advancement in formal theorem proving is hindered by a lack of training data. To address this issue, we introduce an approach to generate extensive Lean 4 proof data derived from high-school and undergraduate-level mathematical competition problems. This approach involves translating natural language problems into formal statements, filtering out low-quality statements, and generating proofs to create synthetic data. After fine-tuning the DeepSeekMath 7B model on this synthetic dataset, which comprises 8 million formal statements with proofs, our model achieved whole-proof generation accuracies of 46.3% with 64 samples and 52% cumulatively on the Lean 4 miniF2F test, surpassing the baseline GPT-4 at 23.0% with 64 samples and a tree search reinforcement learning method at 41.0%. Additionally, our model successfully proved 5 out of 148 problems in the Lean 4 Formalized International Mathematical Olympiad (FIMO) benchmark, while GPT-4 failed to prove any. These results demonstrate the potential of leveraging large-scale synthetic data to enhance theorem-proving capabilities in LLMs. Both the synthetic dataset and the model will be made available to facilitate further research in this promising field.

## 2. Evaluation Results

<div align="center">

| | miniF2F-test |
|--------|------------------|
| **ReProver** | 26.5% |
| **GPT-f** | 36.6% |
| **Hypertree Proof Search** | 41.0% |
| **DeepSeek-Prover-V1** | 50.0% |

</div>

## 3. Model & Dataset Downloads

We release the DeepSeek-Prover-V1 along with the synthetic dataset to the public.

<div align="center">

| **Model & Dataset** | **Download** |
| :-----------------------------: | :----------------------------------------------------------: |
| DeepSeek-Prover-V1 | [🤗 HuggingFace](https://huggingface.co/deepseek-ai/DeepSeek-Prover-V1) |
| Synthetic Dataset | [🤗 HuggingFace](https://huggingface.co/datasets/deepseek-ai/DeepSeek-Prover-V1) |

</div>

## 4. License
This code repository is licensed under the MIT License. The use of DeepSeek-Prover models is subject to the Model License. DeepSeek-Prover supports commercial use.

See the [LICENSE-CODE](LICENSE-CODE) and [LICENSE-MODEL](LICENSE-MODEL) for more details.

## 5. Contact

If you have any questions, please raise an issue or contact us at [[e-mail]](mailto:[e-mail]).

<div align="center">
<img src="https://github.com/deepseek-ai/DeepSeek-V2/blob/main/figures/logo.svg?raw=true" width="60%" alt="DeepSeek-V2" />
</div>
<hr>
<div align="center" style="line-height: 1;">
<a href="https://www.deepseek.com/" target="_blank" style="margin: 2px;">
<img alt="主页" src="https://github.com/deepseek-ai/DeepSeek-V2/blob/main/figures/badge.svg?raw=true" style="display: inline-block; vertical-align: middle;"/>
</a>
<a href="https://chat.deepseek.com/" target="_blank" style="margin: 2px;">
<img alt="对话" src="https://img.shields.io/badge/🤖%20Chat-DeepSeek%20V2-536af5?color=536af5&logoColor=white" style="display: inline-block; vertical-align: middle;"/>
</a>
<a href="https://huggingface.co/deepseek-ai" target="_blank" style="margin: 2px;">
<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;"/>
</a>
</div>

<div align="center" style="line-height: 1;">
<a href="https://discord.gg/Tc7c45Zzu5" target="_blank" style="margin: 2px;">
<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;"/>
</a>
<a href="https://github.com/deepseek-ai/DeepSeek-V2/blob/main/figures/qr.jpeg?raw=true" target="_blank" style="margin: 2px;">
<img alt="微信" src="https://img.shields.io/badge/WeChat-DeepSeek%20AI-brightgreen?logo=wechat&logoColor=white" style="display: inline-block; vertical-align: middle;"/>
</a>
<a href="https://twitter.com/deepseek_ai" target="_blank" style="margin: 2px;">
<img alt="推特关注" src="https://img.shields.io/badge/Twitter-deepseek_ai-white?logo=x&logoColor=white" style="display: inline-block; vertical-align: middle;"/>
</a>
</div>
<div align="center" style="line-height: 1;">
<a href="https://github.com/deepseek-ai/DeepSeek-V2/blob/main/LICENSE-CODE" style="margin: 2px;">
<img alt="代码许可" src="https://img.shields.io/badge/Code_License-MIT-f5de53?&color=f5de53" style="display: inline-block; vertical-align: middle;"/>
</a>
<a href="https://github.com/deepseek-ai/DeepSeek-V2/blob/main/LICENSE-MODEL" style="margin: 2px;">
<img alt="模型许可" src="https://img.shields.io/badge/Model_License-Model_Agreement-f5de53?&color=f5de53" style="display: inline-block; vertical-align: middle;"/>
</a>
</div>
<p align="center">
<a href="#2-evaluation-results">评估结果</a> |
<a href="#3-model-&amp;-dataset-downloads">模型与数据集下载</a> |
<a href="#4-license">许可协议</a> |
<a href="#5-contact">联系方式</a>
</p>

<p align="center">
<a href="https://arxiv.org/abs/2405.14333"><b>论文链接</b>👁️</a>
</p>

# DeepSeek-Prover：借助大规模合成数据提升大语言模型的定理证明能力

## 1. 引言
Lean这类证明助手革新了数学证明验证工作，保障了极高的准确性与可靠性。尽管大语言模型（Large Language Model, LLM）在数学推理领域展现出应用潜力，但在形式化定理证明方向的发展却受限于训练数据的匮乏。为解决这一问题，我们提出一种生成大规模Lean 4证明数据的方案，该数据源自高中及本科阶段的数学竞赛题目。该方案涵盖将自然语言问题转换为形式化语句、过滤低质量语句以及生成证明以构建合成数据集三个环节。我们在包含800万条带证明的形式化语句的合成数据集上对DeepSeekMath 7B模型进行微调后，该模型在Lean 4的miniF2F测试集上实现了64样本下46.3%的完整证明生成准确率，累计准确率达52%，超越了基线模型GPT-4（64样本下23.0%）与树搜索强化学习方法（41.0%）。此外，我们的模型在Lean 4形式化国际数学奥林匹克（Formalized International Mathematical Olympiad, FIMO）基准的148道题目中成功证明了5道，而GPT-4未能证明任何一道。上述结果证实了借助大规模合成数据提升大语言模型定理证明能力的可行性。本研究生成的合成数据集与模型均将公开，以推动该新兴领域的后续研究。

## 2. 评估结果
<div align="center">

| | miniF2F测试集 |
|--------|------------------|
| **ReProver** | 26.5% |
| **GPT-f** | 36.6% |
| **Hypertree Proof Search** | 41.0% |
| **DeepSeek-Prover-V1** | 50.0% |

</div>

## 3. 模型与数据集下载
我们面向公众开源发布DeepSeek-Prover-V1模型及其配套合成数据集。

<div align="center">

| **模型与数据集** | **下载链接** |
| :-----------------------------: | :----------------------------------------------------------: |
| DeepSeek-Prover-V1 | [🤗 Hugging Face](https://huggingface.co/deepseek-ai/DeepSeek-Prover-V1) |
| 合成数据集 | [🤗 Hugging Face](https://huggingface.co/datasets/deepseek-ai/DeepSeek-Prover-V1) |

</div>

## 4. 许可协议
本代码仓库遵循MIT开源许可协议。DeepSeek-Prover系列模型的使用需遵循模型许可协议。DeepSeek-Prover支持商业使用。
详细条款请参阅[LICENSE-CODE](LICENSE-CODE)与[LICENSE-MODEL](LICENSE-MODEL)文件。

## 5. 联系方式
若您有任何疑问，请提交Issue或发送邮件至[[e-mail]](mailto:[e-mail]).