commit 1ebf42fa4cc3ec52dd3db8fcaa4818d92d84017d Author: ModelHub XC Date: Sat Jul 25 03:52:07 2026 +0800 初始化项目，由ModelHub XC社区提供模型 Model: unsloth/DeepSeek-Prover-V2-7B-GGUF Source: Original Platform diff --git a/.gitattributes b/.gitattributes new file mode 100644 index 0000000..defb483 --- /dev/null +++ b/.gitattributes @@ -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 diff --git a/DeepSeek-Prover-V2-7B-BF16.gguf b/DeepSeek-Prover-V2-7B-BF16.gguf new file mode 100644 index 0000000..31a78dc --- /dev/null +++ b/DeepSeek-Prover-V2-7B-BF16.gguf @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:6b9c5a9cb8e728df642bb8c5120790b7a0db4ce11468280c7159e33fafc89d66 +size 13825221632 diff --git a/DeepSeek-Prover-V2-7B-IQ4_NL.gguf b/DeepSeek-Prover-V2-7B-IQ4_NL.gguf new file mode 100644 index 0000000..6a26f83 --- /dev/null +++ b/DeepSeek-Prover-V2-7B-IQ4_NL.gguf @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:1e5f5a4cd48025b8eea07ce7c6a91cf2bdc0c91da0719ede9d9a590325d6919b +size 4000064768 diff --git a/DeepSeek-Prover-V2-7B-IQ4_XS.gguf b/DeepSeek-Prover-V2-7B-IQ4_XS.gguf new file mode 100644 index 0000000..8e8c51c --- /dev/null +++ b/DeepSeek-Prover-V2-7B-IQ4_XS.gguf @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:d60e6fd00bb5125decd87693a0b2de820224df780cbd749e884919f2d1d99831 +size 3810338048 diff --git a/DeepSeek-Prover-V2-7B-Q2_K.gguf b/DeepSeek-Prover-V2-7B-Q2_K.gguf new file mode 100644 index 0000000..90d32cd --- /dev/null +++ b/DeepSeek-Prover-V2-7B-Q2_K.gguf @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:a80fe8013d6181c0d6704dd74aab6eeef9dffe8575a56fd1b668ead563981c49 +size 2718426368 diff --git a/DeepSeek-Prover-V2-7B-Q2_K_L.gguf b/DeepSeek-Prover-V2-7B-Q2_K_L.gguf new file mode 100644 index 0000000..c6c1ca4 --- /dev/null +++ b/DeepSeek-Prover-V2-7B-Q2_K_L.gguf @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:a14e5d652caa927cb6e28a8270718598ff5c79c910e8df567c372deb4adf67bd +size 2816730368 diff --git a/DeepSeek-Prover-V2-7B-Q3_K_M.gguf b/DeepSeek-Prover-V2-7B-Q3_K_M.gguf new file mode 100644 index 0000000..f90fe2e --- /dev/null +++ b/DeepSeek-Prover-V2-7B-Q3_K_M.gguf @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:49733c054611440a056cf9e291bdb8568ae28221139e805186e93f728d875fd8 +size 3461195008 diff --git a/DeepSeek-Prover-V2-7B-Q3_K_S.gguf b/DeepSeek-Prover-V2-7B-Q3_K_S.gguf new file mode 100644 index 0000000..ee39f5a --- /dev/null +++ b/DeepSeek-Prover-V2-7B-Q3_K_S.gguf @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:111d81d8d1cffbf606ee27f6489d5cbb4361290093828e5c8d701d11e0d61820 +size 3138020608 diff --git a/DeepSeek-Prover-V2-7B-Q4_0.gguf b/DeepSeek-Prover-V2-7B-Q4_0.gguf new file mode 100644 index 0000000..0a625fb --- /dev/null +++ b/DeepSeek-Prover-V2-7B-Q4_0.gguf @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:8063da1b1dc298e78fb74d859bfb315c1ce580f242ed7a9ab2bb4a82529a36b7 +size 4008518912 diff --git a/DeepSeek-Prover-V2-7B-Q4_1.gguf b/DeepSeek-Prover-V2-7B-Q4_1.gguf new file mode 100644 index 0000000..7020a33 --- /dev/null +++ b/DeepSeek-Prover-V2-7B-Q4_1.gguf @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:ed0d00d6312b42566dfc24b4ddda189ad9b4c1c5084eb47fb159ff53b7461dfe +size 4405732608 diff --git a/DeepSeek-Prover-V2-7B-Q4_K_M.gguf b/DeepSeek-Prover-V2-7B-Q4_K_M.gguf new file mode 100644 index 0000000..43c2581 --- /dev/null +++ b/DeepSeek-Prover-V2-7B-Q4_K_M.gguf @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:1f6039c37ea4197436b3f4fa707afbb83a285c9173a60583e5df063ba432b2d9 +size 4223362304 diff --git a/DeepSeek-Prover-V2-7B-Q4_K_S.gguf b/DeepSeek-Prover-V2-7B-Q4_K_S.gguf new file mode 100644 index 0000000..d6063ee --- /dev/null +++ b/DeepSeek-Prover-V2-7B-Q4_K_S.gguf @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:81ec540911829beb501fd98c0af4f23e74be89a756c00c0ac46bb8199d782d51 +size 4025361664 diff --git a/DeepSeek-Prover-V2-7B-Q5_K_M.gguf b/DeepSeek-Prover-V2-7B-Q5_K_M.gguf new file mode 100644 index 0000000..8fdeca5 --- /dev/null +++ b/DeepSeek-Prover-V2-7B-Q5_K_M.gguf @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:c343f2021a3edb27b04426cdf577057bd4ee7049af8d908e3b91eb836517191b +size 4926432512 diff --git a/DeepSeek-Prover-V2-7B-Q5_K_S.gguf b/DeepSeek-Prover-V2-7B-Q5_K_S.gguf new file mode 100644 index 0000000..363a5c2 --- /dev/null +++ b/DeepSeek-Prover-V2-7B-Q5_K_S.gguf @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:f2ff5c715e6a72e76190e968c4f2dee74a5a76f12337f1b1f9bad88856d14afb +size 4811400448 diff --git a/DeepSeek-Prover-V2-7B-Q6_K.gguf b/DeepSeek-Prover-V2-7B-Q6_K.gguf new file mode 100644 index 0000000..3c16665 --- /dev/null +++ b/DeepSeek-Prover-V2-7B-Q6_K.gguf @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:201d0c7e72d6f57130ce62b08362946a80e40e86a9d4bfe96275457e47906435 +size 5673444608 diff --git a/DeepSeek-Prover-V2-7B-Q8_0.gguf b/DeepSeek-Prover-V2-7B-Q8_0.gguf new file mode 100644 index 0000000..b91148c --- /dev/null +++ b/DeepSeek-Prover-V2-7B-Q8_0.gguf @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:ca590b42a4e55ae58af480d3d06ae02766b5708ac3587f860a096ce58e438e91 +size 7346988288 diff --git a/DeepSeek-Prover-V2-7B-UD-IQ1_M.gguf b/DeepSeek-Prover-V2-7B-UD-IQ1_M.gguf new file mode 100644 index 0000000..681176b --- /dev/null +++ b/DeepSeek-Prover-V2-7B-UD-IQ1_M.gguf @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:b5077f9d6fd4564a8330d78700fef6e90d3445880b7bfbb02a4626ed2ea9e40d +size 1957799168 diff --git a/DeepSeek-Prover-V2-7B-UD-IQ1_S.gguf b/DeepSeek-Prover-V2-7B-UD-IQ1_S.gguf new file mode 100644 index 0000000..44bd4fd --- /dev/null +++ b/DeepSeek-Prover-V2-7B-UD-IQ1_S.gguf @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:e8a5c0742cbe66c12e20828e8b9050331a2f18612aadf45abc758d66f3f1c3f9 +size 1863591168 diff --git a/DeepSeek-Prover-V2-7B-UD-IQ2_M.gguf b/DeepSeek-Prover-V2-7B-UD-IQ2_M.gguf new file mode 100644 index 0000000..bf1f97e --- /dev/null +++ b/DeepSeek-Prover-V2-7B-UD-IQ2_M.gguf @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:1ad1b7204eb7b0de60d30b97032a4cdc0b1b9b8afd837873fb1918d8bcb03c42 +size 2598233344 diff --git a/DeepSeek-Prover-V2-7B-UD-IQ2_XXS.gguf b/DeepSeek-Prover-V2-7B-UD-IQ2_XXS.gguf new file mode 100644 index 0000000..20dae90 --- /dev/null +++ b/DeepSeek-Prover-V2-7B-UD-IQ2_XXS.gguf @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:d69fd75cdeb5f37def318f559d88970e1ef649915689514f25beab8feb0b7cfd +size 2154571008 diff --git a/DeepSeek-Prover-V2-7B-UD-IQ3_XXS.gguf b/DeepSeek-Prover-V2-7B-UD-IQ3_XXS.gguf new file mode 100644 index 0000000..bfd5e6d --- /dev/null +++ b/DeepSeek-Prover-V2-7B-UD-IQ3_XXS.gguf @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:f5dfe8fa40bdbbc682fe1ee44139f7b49a6189ccc53ffde7000ee6aa782d2c7c +size 2801042688 diff --git a/DeepSeek-Prover-V2-7B-UD-Q2_K_XL.gguf b/DeepSeek-Prover-V2-7B-UD-Q2_K_XL.gguf new file mode 100644 index 0000000..24fb524 --- /dev/null +++ b/DeepSeek-Prover-V2-7B-UD-Q2_K_XL.gguf @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:7d304e44a6ace9593a3fc9ca7e93460e5b74083228f3d47c774b2414c30a93e8 +size 2895660288 diff --git a/DeepSeek-Prover-V2-7B-UD-Q3_K_XL.gguf b/DeepSeek-Prover-V2-7B-UD-Q3_K_XL.gguf new file mode 100644 index 0000000..8643dcc --- /dev/null +++ b/DeepSeek-Prover-V2-7B-UD-Q3_K_XL.gguf @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:690726fbf274103feb4f34df13d15f690f4a64c6bc4191e2e3d7bf8b711bdc58 +size 3665765632 diff --git a/DeepSeek-Prover-V2-7B-UD-Q4_K_XL.gguf b/DeepSeek-Prover-V2-7B-UD-Q4_K_XL.gguf new file mode 100644 index 0000000..0427e8d --- /dev/null +++ b/DeepSeek-Prover-V2-7B-UD-Q4_K_XL.gguf @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:15789a118482618b624986406de212db1811d392f5d8f789baed803524b46bd3 +size 4344358144 diff --git a/DeepSeek-Prover-V2-7B-UD-Q5_K_XL.gguf b/DeepSeek-Prover-V2-7B-UD-Q5_K_XL.gguf new file mode 100644 index 0000000..12fd300 --- /dev/null +++ b/DeepSeek-Prover-V2-7B-UD-Q5_K_XL.gguf @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:fde60d5263c76f095c1c194470367e6d2f54aca5ad4407ee02a65b0028cc8b8d +size 4965639424 diff --git a/DeepSeek-Prover-V2-7B-UD-Q6_K_XL.gguf b/DeepSeek-Prover-V2-7B-UD-Q6_K_XL.gguf new file mode 100644 index 0000000..3388f24 --- /dev/null +++ b/DeepSeek-Prover-V2-7B-UD-Q6_K_XL.gguf @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:db614efc83dc9ad075696770297ff082285679079ab54b8c983a50bc60717d37 +size 6460695808 diff --git a/DeepSeek-Prover-V2-7B-UD-Q8_K_XL.gguf b/DeepSeek-Prover-V2-7B-UD-Q8_K_XL.gguf new file mode 100644 index 0000000..b8d5ee8 --- /dev/null +++ b/DeepSeek-Prover-V2-7B-UD-Q8_K_XL.gguf @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:f0bf4b23aa0b169189217aa949c3337d2869136592b7ebc88385811b1be9e6a3 +size 8924767488 diff --git a/README.md b/README.md new file mode 100644 index 0000000..7b1a35f --- /dev/null +++ b/README.md @@ -0,0 +1,211 @@ +--- +tags: +- unsloth +- unsloth +base_model: +- deepseek-ai/DeepSeek-Prover-V2-7B +--- +
+

+ Unsloth Dynamic 2.0 achieves superior accuracy & outperforms other leading quants. +

+
+ + + + + + + + + +
+
+ +
+

+ Unsloth Dynamic 2.0 achieves superior accuracy & outperforms other leading quants. +

+
+ + + + + + + + + +
+
+ + + + + +
+ DeepSeek-V3 +
+
+
+ + Homepage + + + Chat + + + Hugging Face + +
+ +
+ + Discord + + + Wechat + + + Twitter Follow + +
+ +
+ + Code License + + + Model License + +
+ +## 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. + +

+ +

+ +## 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. + +
+ +| 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 | + +
+ +## 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. + +
+ +| **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) | + +
+ +
+ +| **Dataset** | **Download** | +| :-----------------------------: | :----------------------------------------------------------: | +| DeepSeek-ProverBench | [🤗 HuggingFace](https://huggingface.co/datasets/deepseek-ai/DeepSeek-ProverBench) | + +
+ +## 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). diff --git a/config.json b/config.json new file mode 100644 index 0000000..3282537 --- /dev/null +++ b/config.json @@ -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 +} diff --git a/configuration.json b/configuration.json new file mode 100644 index 0000000..159097f --- /dev/null +++ b/configuration.json @@ -0,0 +1 @@ +{"framework": "pytorch", "task": "others", "allow_remote": true} \ No newline at end of file diff --git a/imatrix_unsloth.dat b/imatrix_unsloth.dat new file mode 100644 index 0000000..cd6e3f8 Binary files /dev/null and b/imatrix_unsloth.dat differ