ReasoningPaperAdvanced2024~14 min theory

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

A proof assistant can check a proof exactly, so the bottleneck is not verification but data. Generate eight million synthetic Lean proofs and the model can prove competition theorems.

arXiv:2405.14333

Where this sits

DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language ModelsDeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic DataDeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search

Formal proving had the same problem as everything else in late 2023: strong checkers, almost no training data. The paper attacks that gap with synthesis, and the model starts from the same DeepSeekMath 7B checkpoint that the founding era used for math.

Turns informal competition problems into a scalable Lean 4 training set instead of relying on the small human-written corpora of the time.
Trains a 7B prover that reaches 46.3% pass@64 on miniF2F-test, versus 23.0% for GPT-4-turbo and 41.0% for Hypertree Proof Search.
Uses iterative self-training: each round's verified proofs are folded back into the dataset, so the model and its data improve together.
Proves 5 of 148 problems from FIMO while the GPT-4 baseline proves none, evidence that formal provers can handle harder olympiad-level statements.

What it is

DeepSeek-Prover is the paper that opened the formal-mathematics line at DeepSeek. It takes high-school and undergraduate competition problems, translates them into Lean 4 statements, filters bad ones out, asks a model to write proofs, keeps only proofs the Lean kernel accepts, and retrains on that growing pile. The result is a 7B model whose whole-proof generation accuracy on the miniF2F-test benchmark more than doubles the GPT-4 baseline.

1Theory from first principles

What formal verification buys you

In a proof assistant like Lean, a proof is a program and the kernel is the checker. You state a theorem in a precise language, write a sequence of tactics, and the kernel either accepts the whole proof or points at the first step it cannot justify. There is no partial credit and no learned judge: the signal is exact, mechanical, and free once the hardware is running. That is why formal proving is such an attractive target for RL later on, because the environment itself hands out ground truth. The price is that the model must learn Lean syntax and the library of already-proved lemmas, which is why data, not compute, is the bottleneck at this stage.

The synthesis pipeline

The paper builds data in four stages. First, natural-language problems (from competition archives and math competition sets) are autoformalized: a model writes a Lean 4 statement for each one. Second, low-quality statements are filtered out, because a malformed or trivial statement is worse than no data. Third, a prover model generates proof attempts for the surviving statements. Fourth, every attempt is checked by the Lean kernel; only proofs that compile are kept as training targets. The loop repeats, and each iteration uses the improved model to generate the next round, which the paper calls iterative enhancement.

Synthetic Lean data pipeline: natural-language problems, autoformalization to Lean 4 statements, filtering, proof generation, kernel verification, and a retraining loop that feeds verified proofs back in.

Whole-proof generation and its failure mode

This model writes an entire proof in one pass: the prompt is the theorem statement, the completion is the full tactic script. That is cheap to run (one round trip to the model, one call to the verifier) and it is what makes the pass@64 numbers comparable to text generation. The catch is compounding error: because the model never sees intermediate tactic states while writing, one wrong move early poisons everything after it. Fixing that limitation is exactly the job of Prover-V1.5.

pass@k

pass@k = 1 - C(n - c, k) / C(n, k)

With n sampled proofs of which c are correct, C(n - c, k) / C(n, k) is the probability that a random draw of k samples contains no correct proof, so one minus that is the chance at least one of the k samples is valid. It answers the practical question: how many attempts do I need before the prover succeeds? The paper reports both pass@64 and much larger budgets, and accuracy keeps rising as k grows (30.0% greedy, 46.3% at 64, 50.0% at 65536).

Iteration and data scoring

The paper ablates two choices that matter. First, the autoformalized statements are graded by quality before proofs are generated, and training only on the proofs for the higher-scoring classes beats training on everything (42.6% versus 38.1% on miniF2F-test at pass@128 in the reported ablation). Second, repeating the synthesis loop with the improved model beats a single round, because the model that generates round two data is stronger than the one that generated round one. Both findings are the same lesson in different clothes: in a verifier-rich domain, data quality and data quantity can be manufactured on purpose.

Where this approach breaks down

A Lean proof certifies that the formal statement is provable, not that the formal statement matches the intended English problem. Autoformalization can silently weaken or strengthen a theorem, so verified proofs are only as meaningful as the statements they prove. The benchmark numbers are also on miniF2F, which is small (244 test problems) and high-school level; FIMO stays hard. Treat this paper as a proof of concept that synthesis works, with the harder questions (fidelity, scale, general math) left open.

2Inside the paper

Problem the paper sets out to solve

Formal theorem proving with LLMs is starved of data. Human-written Lean corpora like mathlib are large but not structured as competition problem solutions, and the community's benchmarks are tiny. The paper asks whether a model can bootstrap its own training data in Lean 4.

Key idea to look for while reading

Synthetic data generation with kernel verification as the filter, applied iteratively. Section 3 walks through autoformalization, quality filtering, and proof search; Section 4 shows what iteration and proof scoring add. Read the ablations because they are where the paper justifies its design choices rather than just reporting a score.

Evidence the paper musters

An 8-million-statement synthetic dataset with proofs, fine-tuning from DeepSeekMath 7B. Whole-proof generation reaches 46.3% on miniF2F-test at pass@64 and 52.0% cumulatively across iterations, against 23.0% for GPT-4-turbo at the same budget and 41.0% for the Hypertree Proof Search RL baseline. On miniF2F-valid the cumulative number is 60.2%. The model proves 5 of 148 FIMO problems; GPT-4 proves none. Scaling samples from 1 to 65,536 moves miniF2F-test accuracy from 30.0% to 50.0%.

Limits the authors admit

The paper states that the approach targets high-school and undergraduate competition mathematics, and that results depend on the quality of autoformalization. FIMO success is low in absolute terms. There is no RL and no interaction with tactic states yet, so errors compound inside a proof attempt and search is limited to independent samples.

Practitioner takeaway

If you have a verifier, you can manufacture supervision: generate candidates, keep what verifies, retrain, repeat. Score and filter data rather than dumping everything in, and expect each loop to pay off. This recipe reappears in every DeepSeek reasoning paper after it, from Prover-V1.5's RL to R1's rule-based rewards.

3Implementation check

0 of 5 questions answered

1.Why does the paper use the Lean kernel as the filter for synthetic data instead of a learned reward model?
2.In the synthesis pipeline, why filter formal statements before generating proofs for them?
3.A prover achieves 46.3% pass@64 on miniF2F-test. What does that number mean?
4.The ablation 'excellent/good/above-average statements only' beats training on all quality classes. What is the lesson?
5.A generated proof compiles in Lean. What is the strongest thing you can conclude?

4Build it yourself

Proof Search in a Toy Rewrite System

Starter2-3 hours

Encode Peano arithmetic as tuples, give the system two rewrite rules, and write a breadth-first search that discharges random additions. Generation plus a mechanical checker is the paper's data loop in miniature, and prove rate is the metric.

Milestones

Encode numerals as nested tuples and write the two addition rewrite rules.
Implement match so a pattern such as ("+", ("s", "x"), "y") binds x and y to subterms.
Enumerate every one-step rewrite, including rewrites inside subterms rather than only at the root.
Run breadth-first search from a start term to a goal term with a depth cap and return the proof path.
Generate 30 random a + b equalities from a fixed seed and report the fraction proved.
Add a multiplication rule and watch the depth cap start to bind on longer proofs.

Starter code

python · editable

import random
from collections import deque
def numeral(k):
    return ("z",) if k == 0 else ("s", numeral(k - 1))

# Toy Peano-arithmetic rewrite system: patterns and term builders.
RULES = [
    (("+", ("z",), "x"), lambda env: env["x"]),
    (("+", ("s", "x"), "y"), lambda env: ("s", ("+", env["x"], env["y"]))),
]

def match(pattern, term, env):
    # TODO: bind pattern variables ("x", "y") to subterms and return the
    # extended env, or None when the shapes do not line up.
    return None

def rewrites(term):
    out = []
    for pattern, build in RULES:
        env = match(pattern, term, {})
        if env is not None:
            out.append(build(env))
    if isinstance(term, tuple):
        for i, child in enumerate(term):
            for new_child in rewrites(child):
                out.append(term[:i] + (new_child,) + term[i + 1:])
    return out

def prove(start, goal, depth):
    # TODO: breadth-first search over rewrites() up to depth steps; return
    # the list of terms from start to goal, or None if no proof is found.
    return None

def main():
    rng = random.Random(0)
    total, solved = 30, 0
    for _ in range(total):
        a, b = rng.randint(0, 3), rng.randint(0, 3)
        if prove(("+", numeral(a), numeral(b)), numeral(a + b), 20):
            solved += 1
    print("rules:", len(RULES), "theorems:", total)
    print("proved:", solved)
    # EXPECTED: after the TODOs, rules: 2 theorems: 30 / proved: 30; the
    # unfilled starter prints proved: 0.
main()

Runs locally in your browser.

Success criteria

All 30 seeded equalities are proved: the run ends with proved: 30.
Every returned proof replays one rewrite at a time under rewrites() and ends at the goal term.
Deleting a basis rule makes the corresponding equalities unprovable, confirming the search cannot bypass the rules.

Stretch goals

Add multiplication and prove distributivity, a * (b + c) = a * b + a * c, which needs many more steps.
Replace breadth-first search with iterative deepening and report expansions on proofs of length 10 or more.
Estimate pass@k by sampling random rewrite walks and compare with the exhaustive search at equal budgets.

Problems

5Keep going

previousDualPath: Breaking the Storage Bandwidth Bottleneck in Agentic LLM Inference nextDeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search