unsloth/DeepSeek-Prover-V2-7B-GGUF
1
0
Fork 0
Code Issues Pull Requests Actions Projects Releases Wiki Activity

初始化项目，由ModelHub XC社区提供模型

Browse Source 
Model: unsloth/DeepSeek-Prover-V2-7B-GGUF
Source: Original Platform
This commit is contained in:
ModelHub XC
2026-07-25 03:52:07 +08:00
commit 1ebf42fa4c
31 changed files with 401 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

72
.gitattributes vendored Normal file
View File

@@ -0,0 +1,72 @@
*.7z filter=lfs diff=lfs merge=lfs -text
*.arrow filter=lfs diff=lfs merge=lfs -text
*.bin filter=lfs diff=lfs merge=lfs -text
*.bin.* filter=lfs diff=lfs merge=lfs -text
*.bz2 filter=lfs diff=lfs merge=lfs -text
*.ftz filter=lfs diff=lfs merge=lfs -text
*.gz filter=lfs diff=lfs merge=lfs -text
*.h5 filter=lfs diff=lfs merge=lfs -text
*.joblib filter=lfs diff=lfs merge=lfs -text
*.lfs.* filter=lfs diff=lfs merge=lfs -text
*.model filter=lfs diff=lfs merge=lfs -text
*.msgpack filter=lfs diff=lfs merge=lfs -text
*.onnx filter=lfs diff=lfs merge=lfs -text
*.ot filter=lfs diff=lfs merge=lfs -text
*.parquet filter=lfs diff=lfs merge=lfs -text
*.pb filter=lfs diff=lfs merge=lfs -text
*.pt filter=lfs diff=lfs merge=lfs -text
*.pth filter=lfs diff=lfs merge=lfs -text
*.rar filter=lfs diff=lfs merge=lfs -text
saved_model/**/* filter=lfs diff=lfs merge=lfs -text
*.tar.* filter=lfs diff=lfs merge=lfs -text
*.tflite filter=lfs diff=lfs merge=lfs -text
*.tgz filter=lfs diff=lfs merge=lfs -text
*.xz filter=lfs diff=lfs merge=lfs -text
*.zip filter=lfs diff=lfs merge=lfs -text
*.zstandard filter=lfs diff=lfs merge=lfs -text
*.tfevents* filter=lfs diff=lfs merge=lfs -text
*.db* filter=lfs diff=lfs merge=lfs -text
*.ark* filter=lfs diff=lfs merge=lfs -text
**/*ckpt*data* filter=lfs diff=lfs merge=lfs -text
**/*ckpt*.meta filter=lfs diff=lfs merge=lfs -text
**/*ckpt*.index filter=lfs diff=lfs merge=lfs -text
*.safetensors filter=lfs diff=lfs merge=lfs -text
*.ckpt filter=lfs diff=lfs merge=lfs -text
*.gguf* filter=lfs diff=lfs merge=lfs -text
*.ggml filter=lfs diff=lfs merge=lfs -text
*.llamafile* filter=lfs diff=lfs merge=lfs -text
*.pt2 filter=lfs diff=lfs merge=lfs -text
*.mlmodel filter=lfs diff=lfs merge=lfs -text
*.npy filter=lfs diff=lfs merge=lfs -text
*.npz filter=lfs diff=lfs merge=lfs -text
*.pickle filter=lfs diff=lfs merge=lfs -text
*.pkl filter=lfs diff=lfs merge=lfs -text
*.tar filter=lfs diff=lfs merge=lfs -text
*.wasm filter=lfs diff=lfs merge=lfs -text
*.zst filter=lfs diff=lfs merge=lfs -text
*tfevents* filter=lfs diff=lfs merge=lfs -text
DeepSeek-Prover-V2-7B-BF16.gguf filter=lfs diff=lfs merge=lfs -text
DeepSeek-Prover-V2-7B-IQ4_NL.gguf filter=lfs diff=lfs merge=lfs -text
DeepSeek-Prover-V2-7B-IQ4_XS.gguf filter=lfs diff=lfs merge=lfs -text
DeepSeek-Prover-V2-7B-Q2_K.gguf filter=lfs diff=lfs merge=lfs -text
DeepSeek-Prover-V2-7B-Q2_K_L.gguf filter=lfs diff=lfs merge=lfs -text
DeepSeek-Prover-V2-7B-Q3_K_M.gguf filter=lfs diff=lfs merge=lfs -text
DeepSeek-Prover-V2-7B-Q3_K_S.gguf filter=lfs diff=lfs merge=lfs -text
DeepSeek-Prover-V2-7B-Q4_1.gguf filter=lfs diff=lfs merge=lfs -text
DeepSeek-Prover-V2-7B-Q4_K_M.gguf filter=lfs diff=lfs merge=lfs -text
DeepSeek-Prover-V2-7B-Q4_K_S.gguf filter=lfs diff=lfs merge=lfs -text
DeepSeek-Prover-V2-7B-Q5_K_M.gguf filter=lfs diff=lfs merge=lfs -text
DeepSeek-Prover-V2-7B-Q5_K_S.gguf filter=lfs diff=lfs merge=lfs -text
DeepSeek-Prover-V2-7B-Q6_K.gguf filter=lfs diff=lfs merge=lfs -text
DeepSeek-Prover-V2-7B-Q8_0.gguf filter=lfs diff=lfs merge=lfs -text
DeepSeek-Prover-V2-7B-UD-IQ1_M.gguf filter=lfs diff=lfs merge=lfs -text
DeepSeek-Prover-V2-7B-UD-IQ1_S.gguf filter=lfs diff=lfs merge=lfs -text
DeepSeek-Prover-V2-7B-UD-IQ2_M.gguf filter=lfs diff=lfs merge=lfs -text
DeepSeek-Prover-V2-7B-UD-IQ2_XXS.gguf filter=lfs diff=lfs merge=lfs -text
DeepSeek-Prover-V2-7B-UD-IQ3_XXS.gguf filter=lfs diff=lfs merge=lfs -text
DeepSeek-Prover-V2-7B-UD-Q2_K_XL.gguf filter=lfs diff=lfs merge=lfs -text
DeepSeek-Prover-V2-7B-UD-Q3_K_XL.gguf filter=lfs diff=lfs merge=lfs -text
DeepSeek-Prover-V2-7B-UD-Q4_K_XL.gguf filter=lfs diff=lfs merge=lfs -text
DeepSeek-Prover-V2-7B-UD-Q5_K_XL.gguf filter=lfs diff=lfs merge=lfs -text
DeepSeek-Prover-V2-7B-UD-Q6_K_XL.gguf filter=lfs diff=lfs merge=lfs -text
DeepSeek-Prover-V2-7B-UD-Q8_K_XL.gguf filter=lfs diff=lfs merge=lfs -text

3
DeepSeek-Prover-V2-7B-BF16.gguf Normal file
View File

@@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:6b9c5a9cb8e728df642bb8c5120790b7a0db4ce11468280c7159e33fafc89d66
size 13825221632

3
DeepSeek-Prover-V2-7B-IQ4_NL.gguf Normal file
View File

@@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:1e5f5a4cd48025b8eea07ce7c6a91cf2bdc0c91da0719ede9d9a590325d6919b
size 4000064768

3
DeepSeek-Prover-V2-7B-IQ4_XS.gguf Normal file
View File

@@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:d60e6fd00bb5125decd87693a0b2de820224df780cbd749e884919f2d1d99831
size 3810338048

3
DeepSeek-Prover-V2-7B-Q2_K.gguf Normal file
View File

@@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:a80fe8013d6181c0d6704dd74aab6eeef9dffe8575a56fd1b668ead563981c49
size 2718426368

3
DeepSeek-Prover-V2-7B-Q2_K_L.gguf Normal file
View File

@@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:a14e5d652caa927cb6e28a8270718598ff5c79c910e8df567c372deb4adf67bd
size 2816730368

3
DeepSeek-Prover-V2-7B-Q3_K_M.gguf Normal file
View File

@@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:49733c054611440a056cf9e291bdb8568ae28221139e805186e93f728d875fd8
size 3461195008

3
DeepSeek-Prover-V2-7B-Q3_K_S.gguf Normal file
View File

@@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:111d81d8d1cffbf606ee27f6489d5cbb4361290093828e5c8d701d11e0d61820
size 3138020608

3
DeepSeek-Prover-V2-7B-Q4_0.gguf Normal file
View File

@@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:8063da1b1dc298e78fb74d859bfb315c1ce580f242ed7a9ab2bb4a82529a36b7
size 4008518912

3
DeepSeek-Prover-V2-7B-Q4_1.gguf Normal file
View File

@@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:ed0d00d6312b42566dfc24b4ddda189ad9b4c1c5084eb47fb159ff53b7461dfe
size 4405732608

3
DeepSeek-Prover-V2-7B-Q4_K_M.gguf Normal file
View File

@@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:1f6039c37ea4197436b3f4fa707afbb83a285c9173a60583e5df063ba432b2d9
size 4223362304

3
DeepSeek-Prover-V2-7B-Q4_K_S.gguf Normal file
View File

@@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:81ec540911829beb501fd98c0af4f23e74be89a756c00c0ac46bb8199d782d51
size 4025361664

3
DeepSeek-Prover-V2-7B-Q5_K_M.gguf Normal file
View File

@@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:c343f2021a3edb27b04426cdf577057bd4ee7049af8d908e3b91eb836517191b
size 4926432512

3
DeepSeek-Prover-V2-7B-Q5_K_S.gguf Normal file
View File

@@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:f2ff5c715e6a72e76190e968c4f2dee74a5a76f12337f1b1f9bad88856d14afb
size 4811400448

3
DeepSeek-Prover-V2-7B-Q6_K.gguf Normal file
View File

@@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:201d0c7e72d6f57130ce62b08362946a80e40e86a9d4bfe96275457e47906435
size 5673444608

3
DeepSeek-Prover-V2-7B-Q8_0.gguf Normal file
View File

@@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:ca590b42a4e55ae58af480d3d06ae02766b5708ac3587f860a096ce58e438e91
size 7346988288

3
DeepSeek-Prover-V2-7B-UD-IQ1_M.gguf Normal file
View File

@@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:b5077f9d6fd4564a8330d78700fef6e90d3445880b7bfbb02a4626ed2ea9e40d
size 1957799168

3
DeepSeek-Prover-V2-7B-UD-IQ1_S.gguf Normal file
View File

@@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:e8a5c0742cbe66c12e20828e8b9050331a2f18612aadf45abc758d66f3f1c3f9
size 1863591168

3
DeepSeek-Prover-V2-7B-UD-IQ2_M.gguf Normal file
View File

@@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:1ad1b7204eb7b0de60d30b97032a4cdc0b1b9b8afd837873fb1918d8bcb03c42
size 2598233344

3
DeepSeek-Prover-V2-7B-UD-IQ2_XXS.gguf Normal file
View File

@@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:d69fd75cdeb5f37def318f559d88970e1ef649915689514f25beab8feb0b7cfd
size 2154571008

3
DeepSeek-Prover-V2-7B-UD-IQ3_XXS.gguf Normal file
View File

@@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:f5dfe8fa40bdbbc682fe1ee44139f7b49a6189ccc53ffde7000ee6aa782d2c7c
size 2801042688

3
DeepSeek-Prover-V2-7B-UD-Q2_K_XL.gguf Normal file
View File

@@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:7d304e44a6ace9593a3fc9ca7e93460e5b74083228f3d47c774b2414c30a93e8
size 2895660288

3
DeepSeek-Prover-V2-7B-UD-Q3_K_XL.gguf Normal file
View File

@@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:690726fbf274103feb4f34df13d15f690f4a64c6bc4191e2e3d7bf8b711bdc58
size 3665765632

3
DeepSeek-Prover-V2-7B-UD-Q4_K_XL.gguf Normal file
View File

@@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:15789a118482618b624986406de212db1811d392f5d8f789baed803524b46bd3
size 4344358144

3
DeepSeek-Prover-V2-7B-UD-Q5_K_XL.gguf Normal file
View File

@@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:fde60d5263c76f095c1c194470367e6d2f54aca5ad4407ee02a65b0028cc8b8d
size 4965639424

3
DeepSeek-Prover-V2-7B-UD-Q6_K_XL.gguf Normal file
View File

@@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:db614efc83dc9ad075696770297ff082285679079ab54b8c983a50bc60717d37
size 6460695808

3
DeepSeek-Prover-V2-7B-UD-Q8_K_XL.gguf Normal file
View File

@@ -0,0 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:f0bf4b23aa0b169189217aa949c3337d2869136592b7ebc88385811b1be9e6a3
size 8924767488

211
README.md Normal file
View File

@@ -0,0 +1,211 @@
---
tags:
- unsloth
- unsloth
base_model:
- deepseek-ai/DeepSeek-Prover-V2-7B
---
<div>
<p style="margin-top: 0;margin-bottom: 0;">
<em><a href="https://docs.unsloth.ai/basics/unsloth-dynamic-v2.0-gguf">Unsloth Dynamic 2.0</a> achieves superior accuracy & outperforms other leading quants.</em>
</p>
<div style="display: flex; gap: 5px; align-items: center; ">
<a href="https://github.com/unslothai/unsloth/">
<img src="https://github.com/unslothai/unsloth/raw/main/images/unsloth%20new%20logo.png" width="133">
</a>
<a href="https://discord.gg/unsloth">
<img src="https://github.com/unslothai/unsloth/raw/main/images/Discord%20button.png" width="173">
</a>
<a href="https://docs.unsloth.ai/basics/qwen3-how-to-run-and-fine-tune">
<img src="https://raw.githubusercontent.com/unslothai/unsloth/refs/heads/main/images/documentation%20green%20button.png" width="143">
</a>
</div>
</div>
<div>
<p style="margin-top: 0;margin-bottom: 0;">
<em><a href="https://docs.unsloth.ai/basics/unsloth-dynamic-v2.0-gguf">Unsloth Dynamic 2.0</a> achieves superior accuracy & outperforms other leading quants.</em>
</p>
<div style="display: flex; gap: 5px; align-items: center; ">
<a href="https://github.com/unslothai/unsloth/">
<img src="https://github.com/unslothai/unsloth/raw/main/images/unsloth%20new%20logo.png" width="133">
</a>
<a href="https://discord.gg/unsloth">
<img src="https://github.com/unslothai/unsloth/raw/main/images/Discord%20button.png" width="173">
</a>
<a href="https://docs.unsloth.ai/basics/qwen3-how-to-run-and-fine-tune">
<img src="https://raw.githubusercontent.com/unslothai/unsloth/refs/heads/main/images/documentation%20green%20button.png" width="143">
</a>
</div>
</div>
<!-- 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-V3" />
</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%20V3-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-V3/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-V3/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>
## 1. Introduction
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.
<p align="center">
<img width="100%" src="https://github.com/deepseek-ai/DeepSeek-Prover-V2/blob/main/figures/performance.png?raw=true">
</p>
## 2. Model Summary
---
**Synthesize Cold-Start Reasoning Data through Recursive Proof Search**
- 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.
- 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.
---
**Reinforcement Learning with Synthetic Cold-Start Data**
- 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.
- 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.
- 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).
---
## 3. ProverBench: Formalization of AIME and Textbook Problems
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.
<div align="center">
| Area | Count |
| :---------------------: | :-------: |
| AIME 24&25 | 15 |
| Number Theory | 40 |
| Elementary Algebra | 30 |
| Linear Algebra | 50 |
| Abstract Algebra | 40 |
| Calculus | 90 |
| Real Analysis | 30 |
| Complex Analysis | 10 |
| Functional Analysis | 10 |
| Probability | 10 |
| Total | 325 |
</div>
## 4. Model & Dataset Downloads
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.
<div align="center">
| **Model** | **Download** |
| :-----------------------------: | :----------------------------------------------------------: |
| 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">
| **Dataset** | **Download** |
| :-----------------------------: | :----------------------------------------------------------: |
| DeepSeek-ProverBench | [🤗 HuggingFace](https://huggingface.co/datasets/deepseek-ai/DeepSeek-ProverBench) |
</div>
## 5. Quick Start
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).
The following is a basic example of generating a proof for a problem from the miniF2F dataset:
````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)
````
## 6. License
The use of DeepSeek-Prover-V2 models is subject to [the Model License](LICENSE-MODEL).
## 7. Contact
If you have any questions, please raise an issue or contact us at [service@deepseek.com](mailto:service@deepseek.com).

39
config.json Normal file
View File

@@ -0,0 +1,39 @@
{
"architectures": [
"LlamaForCausalLM"
],
"attention_bias": false,
"attention_dropout": 0.0,
"bos_token_id": 100000,
"eos_token_id": 100001,
"head_dim": 128,
"hidden_act": "silu",
"hidden_size": 4096,
"initializer_range": 0.02,
"intermediate_size": 11008,
"max_position_embeddings": 32768,
"mlp_bias": false,
"model_type": "llama",
"num_attention_heads": 32,
"num_hidden_layers": 30,
"num_key_value_heads": 32,
"pad_token_id": 100008,
"pretraining_tp": 1,
"rms_norm_eps": 1e-06,
"rope_scaling": {
"beta_fast": 32,
"beta_slow": 1,
"factor": 16,
"mscale": true,
"original_max_position_embeddings": 4096,
"rope_type": "yarn",
"type": "yarn"
},
"rope_theta": 10000,
"tie_word_embeddings": false,
"torch_dtype": "bfloat16",
"transformers_version": "4.52.3",
"unsloth_fixed": true,
"use_cache": true,
"vocab_size": 102400
}

1
configuration.json Normal file
View File

@@ -0,0 +1 @@
{"framework": "pytorch", "task": "others", "allow_remote": true}

BIN
imatrix_unsloth.dat Normal file
View File

Binary file not shown.