DOCSEARCHbyAlgolia
Submit Docs

DeepSeek-Prover-V2 Documentation

repository·main·Indexed 23 days ago

https://github.com/deepseek-ai/deepseek-prover-v2

An open-source large language model specialized for formal mathematical reasoning using the Lean 4 theorem prover. It utilizes reinforcement learning and a recursive theorem proving pipeline to decompose complex problems. Available in 7B and 671B parameter sizes, the model generates proof plans and formal Lean 4 code. Includes information on the ProverBench benchmark dataset containing 325 formalized mathematical problems.

Tokens
1.1K
Snippets
1
Records
3
Agent score
29%

What's inside DeepSeek-Prover-V2

  1. Overview of ProverBench benchmark

    main

    ProverBench is a benchmark dataset containing 325 formalized mathematical problems designed to evaluate performance across high-school competition and undergraduate-level mathematics.

    Composition:

    • AIME 24&25: 15 problems (Number Theory and Algebra)
    • Total Breakdown:
      • Calculus: 90
      • Linear Algebra: 50
      • Abstract Algebra: 40
      • Number Theory: 40
      • Elementary Algebra: 30
      • Real Analysis: 30
      • Abstract Algebra: 40
      • Probability: 10
      • Complex Analysis: 10
      • Functional Analysis: 10
      • Other areas include Linear Algebra and Real Analysis.

  2. Download DeepSeek-Prover-V2 models and ProverBench dataset

    main

    DeepSeek-Prover-V2 is available in two parameter sizes. The 671B model is built on DeepSeek-V3-Base, while the 7B model is built on DeepSeek-Prover-V1.5-Base and supports up to 32K context length. The ProverBench dataset is also available on Hugging Face.

    Models:

    Datasets:

  3. Quick Start: Generate Lean 4 proofs with DeepSeek-Prover-V2

    main

    You can use the transformers library to perform inference with DeepSeek-Prover-V2 models. The model is designed to take a Lean 4 formal statement and a specific prompt instruction, then generate a detailed proof plan followed by the formal Lean 4 code.

    Note that DeepSeek-Prover-V2-671B shares the same architecture as DeepSeek-V3. For full architectural details, refer to the DeepSeek-V3 documentation on Hugging Face.

    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.-/\ntheorem 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)