DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning

TL;DR

DeepSeekMath-V2 is a natural-language theorem-proving model built on DeepSeek-V3.2-Exp-Base, trained via an iterative generator/verifier co-evolution loop using GRPO. The core bet is that final-answer rewards (the standard reasoning-RL recipe that has saturated AIME/HMMT) are an unreliable proxy for proof correctness, and that an LLM verifier — gated by a meta-verifier that scores whether the verifier’s identified issues are real — can serve as a reward model for training a proof generator to self-verify. With scaled test-time compute (parallel proof candidates + parallel verification analyses + iterative refinement), the model reaches IMO 2025 gold (5/6), CMO 2024 gold, and 118/120 on Putnam 2024 — exceeding the highest human Putnam score of 90.

Key claims

Final-answer-based RL rewards are inapplicable to theorem proving and unreliable as a proxy for reasoning correctness — models trained this way exhibit high false-positive rates when asked to verify proofs [§1].
A proof verifier can be trained via GRPO against 3-level expert scores (0 / 0.5 / 1) using a format reward × proximity reward; without further constraint this verifier reward-hacks by predicting correct scores while hallucinating non-existent issues in flawed proofs [§2.1.1, §2.1.2].
Meta-verification — a second model scoring whether the verifier’s identified issues are real and justify the proof score — closes the hallucination loophole; incorporating meta-verifier feedback multiplicatively into the verifier reward (R_format · R_score · R_meta) raises issue-analysis quality from 0.85 → 0.96 with no loss in score-prediction accuracy [§2.1.2, Eq. 3].
A generator trained to emit (proof, self-analysis) pairs with the verifier scoring the proof (R_Y = s) and the meta-verifier scoring the self-analysis (R_Z = R_score · R_meta) learns to identify and resolve issues before finalizing — with reward weights α=0.76, β=0.24 [§2.2.2, Eq. 5-6].
Test-time sequential refinement with self-verification monotonically improves proof quality on IMO Shortlist 2024 from pass@1 ≈ 0.15 → 0.27 and best@32 ≈ 0.26 → 0.42 as max iterations grow from 1 → 8 [Fig. 2].
High-compute search with 64 candidate proofs × 64 verifications × up to 16 refinement iterations achieves gold on IMO 2025 (5/6 solved, P6 missed), gold on CMO 2024 (4 fully solved + partial credit on P6), and 118/120 on Putnam 2024 — surpassing the highest human score of 90 [§3.3.3, Table 1].
On IMO-ProofBench, the high-compute system scores 99.0% on the basic set (vs Gemini Deep Think IMO-Gold’s 89.0%) and 61.9% on the advanced set (vs Gemini Deep Think IMO-Gold’s 65.7%) [Fig. 3].
The generator–verifier loop is self-reinforcing: scaling verification samples surfaces issues that need fixing in the proof generator, while meta-verification at scale (n verifier analyses × m meta-checks per analysis) automates the labeling pipeline so that in the last two training iterations no human annotation was needed [§2.3].
On CNML-level problems across algebra, geometry, number theory, combinatorics, and inequality, DeepSeekMath-V2 outperforms both GPT-5-Thinking-High and Gemini 2.5-Pro at one-shot proof generation when scored by the trained verifier [Fig. 1].

Method

The pipeline alternates two GRPO training stages, then iterates. Verifier training (§2.1): given problem X, proof Y, the verifier π_φ(·|X,Y,I_v) emits a structured response summarizing identified issues and a boxed score in {0, 0.5, 1}, supervised against 17,503 AoPS olympiad problems with expert-scored proofs. Format reward enforces the structured output; score reward is 1 − |s’ − s|. Meta-verifier training: a second model π_η scores verifier responses on a separate expert-annotated dataset using the same reward structure; the trained meta-verifier is then folded into verifier RL as a multiplicative R_meta term, suppressing hallucinated issues.

Generator training (§2.2): π_θ emits a proof Y followed by a self-analysis Z in the same rubric as the verifier. The verifier scores Y (giving R_Y), and the meta-verifier scores Z (giving R_meta(Z) = ms). The combined reward R = R_format(Y,Z) · (α·R_Y + β·R_Z) with R_Z = R_score(s’, s) · R_meta(Z) makes faithful self-acknowledgment of errors strictly more rewarding than false claims of correctness. Iteration (§2.3): newly generated proofs become training data; multiple verifier samples plus majority-voted meta-verification automatically label hard new examples, replacing human annotation in the last two iterations. The generator is initialized from the verifier checkpoint at each iteration via rejection fine-tuning that consolidates both capabilities into a single model.

At test time, three compute axes stack: (i) sequential refinement (up to 8 iterations, with the generator re-prompted with its own previous proof + self-analysis); (ii) parallel candidates (64 proofs per problem); (iii) parallel verification (64 verifier analyses per proof, used to score candidates and to surface analyses identifying issues). The pool is updated by selecting the 64 highest-scoring proofs by average verification score, pairing each with 8 analyses (prioritizing those that flag issues), and refining.

Results

IMO 2025: 5/6 solved (P1, P2, P3, P4, P5; P6 missed), 83.3% — gold-medal performance [Table 1].
CMO 2024: 4/6 fully solved (P1, P2, P4, P5) + partial credit on P6, 73.8% — gold-medal performance [Table 1].
Putnam 2024: 11/12 fully solved (A1–B4, B6) + minor errors on B5, 118/120 (98.3%) — exceeds highest human score of 90 [Table 1].
IMO-ProofBench Basic: 99.0% (Heavy); next-best is Gemini Deep Think IMO-Gold at 89.0% [Fig. 3].
IMO-ProofBench Advanced: 61.9% (Heavy); Gemini Deep Think IMO-Gold reaches 65.7% — DeepSeekMath-V2 is competitive but not strictly best on hardest IMO-level problems [Fig. 3].
IMO Shortlist 2024 sequential refinement scaling: pass@1 ≈ 0.15 → 0.27 and best@32 ≈ 0.26 → 0.42 going from 1 → 8 max iterations [Fig. 2].
One-shot generation on CNML-level problems: mean proof scores across algebra (0.60), geometry (0.52), number theory (0.54), combinatorics (0.47), inequality (0.59), outperforming GPT-5-Thinking-High and Gemini 2.5-Pro on every category [Fig. 1].
Verifier-issue-quality jump from incorporating meta-verification: 0.85 → 0.96 on a held-out split of D_v with no loss in score-prediction accuracy [§2.1.2].

Why it’s interesting

This is the cleanest filed example of training a verifier as a generative reward model and then training the generator to be that verifier — a different bet than the Reasoning RL mainstream where rewards are either gold-final-answer (saturating AIME) or external (preference models, perception stacks, tool-call success). The meta-verifier trick is the load-bearing piece that makes the loop work: it closes the reward-hacking loophole where a verifier predicts correct scores while hallucinating issues — a failure mode that’s directly analogous to the LLM-as-judge hallucination problem this team’s VLM-as-Evaluator cousins are also wrestling with. The recipe extends the Inference-Time Scaling taxonomy along an axis the existing concept page doesn’t cover: not parallel agents, not REPL scaffolds, not cache compression, but verifier-guided parallel proof search with sequential self-refinement, where extra compute is spent both on more candidate proofs and on more verification analyses per proof. Will’s “editing chains” intuition lands here — the generator’s self-analysis-then-refine loop is structurally an edit chain over the proof, with the verifier reward shaping each edit toward higher rigor. Also notable: the automated labeling pipeline in the last two iterations (multiple verifier samples + meta-verification majority vote replaces human annotation) is the same “verification gate replaces human labels” thesis that Synthetic Training Data holds for tool-use (Close the Loop: Synthesizing Infinite Tool-Use Data via Multi-Agent Role-Playing) and vision-CoT (Video-Thinker: Sparking "Thinking with Videos" via Reinforcement Learning), now applied at the hardest end of the difficulty spectrum where ground truth is itself uncertain.