ReasoningPaperCore2025~15 min theory

DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning

Correct answers do not prove correct reasoning. Train a faithful verifier, use it as the reward model, and reward the generator for finding and fixing its own proof's flaws before finalizing.

arXiv:2511.22570

Where this sits

DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal DecompositionDeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning

The reasoning era's final paper closes the loop the era opened: R1 showed that verifiable outcomes can drive reasoning, and this paper asks what to do when the outcome is not a number but a proof. It inherits the verified-reward machinery of the prover line and the self-checking behavior observed in R1's traces, and it runs on the V3.2-Exp base from the frontier era.

Trains a generative verifier that scores a proof 0, 0.5, or 1 with an explicit issue analysis, using RL against expert annotations rather than a fixed classifier.
Adds meta-verification: a second model judges whether the issues the verifier claims actually exist and justify the score, raising analysis quality from 0.85 to 0.96 on the validation split.
Uses the verifier as the reward model for a proof generator and trains the generator to self-analyze, with a reward that pays for faithful error acknowledgment, not just for claiming correctness.
Scales verification compute to auto-label proofs that are hard to verify, creating fresh verifier training data without human annotation and keeping the generation-verification gap productive.
Reports gold-medal scores on IMO 2025 and CMO 2024 and 118/120 on Putnam 2024 with scaled test-time compute, against a best human score of 90 on the same Putnam set.

What it is

DeepSeekMath-V2 is the natural-language theorem-proving model built on DeepSeek-V3.2-Exp-Base. Its argument is that outcome rewards have hit their ceiling: they cannot tell a rigorous proof from a lucky one, and they do not exist at all for theorem proving, where there is no final number to check. The paper instead trains an LLM verifier that scores a proof from 0 to 1 with a written analysis, guards it against hallucinated criticisms with a second meta-verifier, and then uses the verifier as the reward model for a proof generator. The generator is trained to write a proof and a self-analysis in one response, and rewarded for honest self-assessment, so the best strategy is to find and fix its own errors before finalizing. With scaled test-time compute the model reaches gold-medal level on IMO 2025 and CMO 2024 and 118/120 on Putnam 2024.

1Theory from first principles

Why final-answer rewards run out

Reinforcement learning on verifiable outcomes worked spectacularly on competition mathematics: check the boxed answer, reward the trace that produced it. But two problems remain. First, a correct answer can come from flawed reasoning, and a model trained only on outcomes learns to get lucky as well as to reason. Second, large parts of mathematics do not end in a number at all: a proof is judged on whether every step follows, which is exactly the kind of judgement that final-answer rewards cannot express. The paper's premise is that progress now depends on verifying reasoning itself, and that a verifier good enough to train against must be built rather than borrowed.

A verifier that writes before it scores

The verifier is a generative reward model: given a problem and a proof, it produces an analysis of the proof's issues and then a score in {0, 0.5, 1}. It is trained with reinforcement learning against expert annotations, with rewards for format and for matching the expert score. That training has a subtle hole: when the proof is flawed, the model can earn full reward by predicting the right score while inventing issues that do not exist. A verifier that hallucinates criticisms is not usable as a reward model, because the generator would be punished for correct steps.

Meta-verification

The fix is a second evaluation layer. A meta-verifier is trained to read the verifier's analysis and judge whether the claimed issues exist and whether they logically justify the score. Verifier training then multiplies its reward by the meta-verifier's quality score, so an analysis that gets the number right for the wrong reasons no longer pays. On a validation split, the average quality of the verifier's analyses rises from 0.85 to 0.96 while score accuracy holds. This is the paper's most transferable idea: any learned judge needs a second judge that checks the first one's reasons, and the check is easier than the original task.

The generator's reward

R = R_format(Y, Z) * (alpha * R_Y + beta * R_Z)
R_Z = R_score(s', s) * R_meta(Z)
alpha = 0.76,  beta = 0.24

Y is the proof and Z is the generator's self-analysis. R_Y is the verifier's score for the proof; s is the verifier's score for the whole proof, s' is the score the generator predicts for its own proof, and R_Z pays for self-assessment that is both accurate (s' close to s) and faithfully argued (meta-verification passes). The format term gates everything, so the model cannot earn reward by dropping the analysis. The weighting makes the proof the main objective while keeping honest self-checking worth a quarter of the reward, which is what creates the incentive to find and fix issues before finalizing.

Generate, verify, revise: the verifier scores the proof and the meta-verifier audits the criticism. Hard-to-verify proofs get extra verification samples and become training data for the next verifier, keeping the gap between generator and verifier productive.

The generation-verification cycle

Verifier and generator improve each other. The verifier trains the generator as a reward model; the improved generator then writes proofs the verifier cannot confidently judge, and those hard cases are exactly the data the verifier needs. Labeling them by hand does not scale, so the paper automates it: for each proof, draw m independent verifier analyses, keep the analyses that report issues (scores 0 or 0.5), and run meta-verification on each. If at least k analyses that assign the lowest score are confirmed by a majority of meta-checks, the proof is labeled with that score; if no legitimate issues survive, it is labeled 1; otherwise it is discarded or sent to a human. RL uses GRPO, and training alternates: improve verification, then initialize the generator from the verifier checkpoint, then consolidate both capabilities into the next verifier through rejection fine-tuning.

Automated labeling of a hard proof

python

def label_proof(analyses, meta_checks, m, k, majority=0.5):
    """analyses: list of (score, issues) from the verifier.
    meta_checks: list of booleans per analysis confirming its issues exist."""
    confirmed = [a for a, ok in zip(analyses, meta_checks)
                 if ok and a.score < 1.0]
    if len(confirmed) >= k:
        # trust the lowest score that enough meta-checks validated
        return min(a.score for a in confirmed)
    if all(a.score == 1.0 for a in analyses):
        return 1.0
    return None   # discard or route to a human annotator

# Scaled verification compute means m and k grow with the proof's difficulty,
# so the labeler spends more samples exactly where the verifier is unsure.

The paper's procedure draws m independent analyses per proof and runs meta-verification on those that report issues; a label is accepted only when enough of them are confirmed.
Returning None is deliberate: uncertain proofs are dropped or escalated rather than given a noisy label that would teach the verifier the wrong thing.
Because the verifier can also write proofs, the same checkpoint family serves both roles, which is what makes the alternating training loop cheap.

Results and the honest limits

With scaled test-time compute the model reaches gold-medal level on IMO 2025 and CMO 2024, and 118 out of 120 on Putnam 2024, above the best human score of 90 on the same paper. Those results depend on the test-time recipe - generate candidates, verify, revise - so the headline is about a system spending compute, not a single greedy decode. The limits are equally important: verification quality is a learned approximation and can still be wrong; the automated labeling keeps humans in the loop for uncertain cases; the domain is competition and undergraduate mathematics, not research mathematics; and the method inherits its base model's weaknesses. The paper's claim is deliberately directional: self-verifiable reasoning looks feasible, and this is an existence proof, not a solved problem.

2Inside the paper

Problem the paper sets out to solve

Outcome-based RL saturates on competition problems without guaranteeing rigorous reasoning, and theorem proving has no final answer to check. The paper asks whether an LLM can learn to verify mathematical proofs well enough to serve as the reward signal for a proof generator.

Key idea to look for while reading

Three mechanisms: verifier training with RL and expert scores, meta-verification as a faithfulness check, and a generator reward that pays for honest self-analysis. Section 2 builds the verifier and the generator, Section 2.3 describes the alternating cycle and automated labeling. Read the reward equations closely; the alpha and beta weights are the incentive design.

Evidence the paper musters

Verifier analysis quality rises from 0.85 to 0.96 under meta-verification on a validation split, at equal proof-score accuracy. The generator reward uses alpha = 0.76 and beta = 0.24. Reported outcomes with scaled test-time compute: gold-medal level on IMO 2025 and CMO 2024, and 118/120 on Putnam 2024, where the best human participant scored 90. The model is built on DeepSeek-V3.2-Exp-Base and evaluated with an accompanying repository.

Limits the authors admit

The verifier remains a learned model with residual failure modes, and the automated labeling deliberately defers uncertain proofs to humans. The evaluation focuses on competition and undergraduate mathematics; research-level problems and open conjectures are explicitly future work. The headline scores come from test-time scaling, so they measure a system with a compute budget rather than a one-shot model.

Practitioner takeaway

When your task lacks a final answer to check, build the verifier first and check the verifier itself. Reward reasons, not just verdicts: a judge that writes its criteria can be audited by a second model, and a generator rewarded for honest self-criticism will fix more of its own errors. Then treat verification as a scalable resource, because spending more samples where the verifier is unsure is what keeps the training signal honest.

3Implementation check

0 of 5 questions answered

1.Why is a correct final answer not a sufficient training signal for theorem proving?
2.What failure mode of the verifier does meta-verification fix?
3.In the generator's reward R = R_format * (0.76 * R_Y + 0.24 * R_Z), what is R_Z?
4.How does the system label hard-to-verify proofs without human annotation?
5.The Putnam result is 118/120, above the best human score of 90. What caveat does the paper itself attach?

4Build it yourself

Self-Verified Proof Generation for Toy Identities

Advanced4-6 hours

Generate candidate rewrite proofs for associativity-style identities, verify every step mechanically, and measure pass@k and the false-accept rate. Verification is sound, so the work is in generation and in measuring what self-checking actually buys.

Milestones

Define terms over plus with integer leaves and three rules: commutativity, left association, right association.
Implement rewrite for a rule applied at a path, returning None when it does not apply.
Implement verify, which replays a proof and rejects at the first illegal step.
Implement generate as a random walk of up to eight legal steps that never looks at the target.
Measure pass@k for k = 1, 4, and 16 over 200 trials on one true identity.
Run the verifier on candidates for a false identity and confirm zero accepts.

Starter code

python · editable

import random
RULES = ("comm", "assoc", "assoc2")

def plus_nodes(term, path=()):
    nodes = []
    if isinstance(term, tuple):
        nodes.append(path)
        for i in (1, 2):
            nodes.extend(plus_nodes(term[i], path + (i,)))
    return nodes

def rewrite(term, rule, path):
    # TODO: apply comm, assoc, or assoc2 at a path; return the rewritten
    # term, or None when the rule does not apply at that position.
    return None

def verify(start, target, proof):
    # TODO: replay the (rule, path) steps from start; every step must apply
    # and the final term must equal target.
    return False

def generate(start, steps, rng):
    # TODO: random walk of up to a fixed number of legal steps from start,
    # without looking at the target; return the list of steps.
    return []

def pass_at_k(start, target, k, rng, steps=8):
    return 1 if any(verify(start, target, generate(start, steps, rng))
                    for _ in range(k)) else 0

def main():
    rng = random.Random(0)
    start = ("+", 1, ("+", 2, 3))
    target = ("+", ("+", 3, 2), 1)
    for k in (1, 4, 16):
        hits = sum(pass_at_k(start, target, k, rng) for _ in range(200))
        print("pass@%d:" % k, round(hits / 200, 3))
    falsestart = ("+", 1, ("+", 2, 3))
    falsetarget = ("+", ("+", 1, 2), 4)
    accepted = sum(verify(falsestart, falsetarget, generate(falsestart, 8, rng))
                   for _ in range(200))
    print("false-claim proofs accepted:", accepted)
    # EXPECTED: after the TODOs, pass@1 about 0.17, pass@4 about 0.48,
    # pass@16 about 0.94, zero false claims; the unfilled starter prints 0.0.
main()

Runs locally in your browser.

Success criteria

pass@k rises monotonically and reaches at least 0.9 at k = 16.
The verifier accepts zero candidates for the false identity across 200 trials.
Every accepted proof replays to the target under an independent replay, and no accepted proof skips a legal rule.

Stretch goals

Add a self-analysis to each candidate and reward correct predictions of its own score, mirroring the paper's alpha/beta split.
Add a meta-verifier that audits the verifier's rejection reasons on a noisy rule set.
Spend extra verification samples on candidates the verifier rejects and report the extra passes found.

Problems

5Keep going

previousDeepSeek-R1-0528 Report nextJanus: Decoupling Visual Encoding for Unified Multimodal Understanding and Generation

Concepts

Problems

Articles

Post-Training: RLHF → DPO → GRPO

Where this sits

What it is

1·Theory from first principles

Why final-answer rewards run out

A verifier that writes before it scores

Meta-verification

The generation-verification cycle

Results and the honest limits

2·Inside the paper

Problem the paper sets out to solve

Key idea to look for while reading

Evidence the paper musters

Limits the authors admit

Practitioner takeaway

3·Implementation check

4·Build it yourself

Milestones

Success criteria

Stretch goals

Problems

5·Keep going

Concepts

Problems

Articles

1Theory from first principles

2Inside the paper

3Implementation check

4Build it yourself

5Keep going