Deepseek Prover V2 671B

🚀 DeepSeek-Prover-V2

DeepSeek-Prover-V2 is an open - source large language model for formal theorem proving in Lean 4. It integrates informal and formal mathematical reasoning, achieving state - of - the - art performance in neural theorem proving.

🚀 Quick Start

You can directly use Huggingface's 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.

💻 Usage Examples

Basic Usage

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)

## ✨ Features
### 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).

## 📚 Documentation
### 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.

| Property | Details |
|----------|---------|
| Area - AIME 24&25 | 15 |
| Area - Number Theory | 40 |
| Area - Elementary Algebra | 30 |
| Area - Linear Algebra | 50 |
| Area - Abstract Algebra | 40 |
| Area - Calculus | 90 |
| Area - Real Analysis | 30 |
| Area - Complex Analysis | 10 |
| Area - Functional Analysis | 10 |
| Area - Probability | 10 |
| Total | 325 |

### 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.

| Property | Details |
|----------|---------|
| Model - DeepSeek - Prover - V2 - 7B | [🤗 HuggingFace](https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-7B) |
| Model - DeepSeek - Prover - V2 - 671B | [🤗 HuggingFace](https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B) |
| Dataset - DeepSeek - ProverBench | [🤗 HuggingFace](https://huggingface.co/datasets/deepseek-ai/DeepSeek-ProverBench) |

## 📄 License
The use of DeepSeek - Prover - V2 models is subject to [the Model License](LICENSE - MODEL).

## 📞 Contact
If you have any questions, please raise an issue or contact us at [service@deepseek.com](mailto:service@deepseek.com).