Source-linked AI summary
DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning
Zhihong Shao, Yuxiang Luo, Chengda Lu, Z. Z. Ren, Jiewen Hu, Tian Ye, Zhibin Gou, Shirong Ma, Xiaokang Zhang
TL;DR
Final-answer rewards do not guarantee valid mathematical reasoning and do not apply cleanly to theorem proving. DeepSeekMath-V2 addresses this by training faithful verifiers, using them to optimize proof generation and self-verification, and scaling verification to create harder training data. With scaled test-time compute, it achieved gold-level scores in IMO 2025 and CMO 2024 and scored 118/120 on Putnam 2024.
Problem
Final-answer rewards do not guarantee correct reasoning and are inapplicable to theorem proving, where rigorous derivation is required.
Method
The paper trains a faithful proof verifier, uses it to optimize generators through self-verification, and scales verification to label harder proofs for further training.
Results
DeepSeekMath-V2 achieved gold-level scores in IMO 2025 and CMO 2024 and scored 118/120 on Putnam 2024.
Takeaways & Limitations
The results demonstrate that LLMs can develop meaningful self-evaluation abilities for mathematical proofs and strong competition-mathematics performance.
Takeaways & Limitations
The verifier can receive full reward for correct scores while hallucinating nonexistent issues, undermining trustworthiness.
Abstract
from arXiv · showhide
Large language models have made significant progress in mathematical reasoning, which serves as an important testbed for AI and could impact scientific research if further advanced. By scaling reasoning with reinforcement learning that rewards correct final answers, LLMs have improved from poor performance to saturating quantitative reasoning competitions like AIME and HMMT in one year. However, this approach faces fundamental limitations. Pursuing higher final answer accuracy doesn't address a key issue: correct answers don't guarantee correct reasoning. Moreover, many mathematical tasks like theorem proving require rigorous step-by-step derivation rather than numerical answers, making final answer rewards inapplicable. To push the limits of deep reasoning, we believe it is necessary to verify the comprehensiveness and rigor of mathematical reasoning. Self-verification is particularly important for scaling test-time compute, especially for open problems without known solutions. Towards self-verifiable mathematical reasoning, we investigate how to train an accurate and faithful LLM-based verifier for theorem proving. We then train a proof generator using the verifier as the reward model, and incentivize the generator to identify and resolve as many issues as possible in their own proofs before finalizing them. To maintain the generation-verification gap as the generator becomes stronger, we propose to scale verification compute to automatically label new hard-to-verify proofs, creating training data to further improve the verifier. Our resulting model, DeepSeekMath-V2, demonstrates strong theorem-proving capabilities, achieving gold-level scores on IMO 2025 and CMO 2024 and a near-perfect 118/120 on Putnam 2024 with scaled test-time compute.
1. Introduction
Final-answer rewards can improve quantitative competition performance but do not ensure logically valid reasoning or apply to theorem proving. The paper therefore develops self-verification for proof generation, culminating in strong competition results.
- Motivation: Final-answer rewards can produce correct answers despite flawed logic and cannot directly evaluate theorem proofs requiring rigorous derivations.These limitations make answer matching an unreliable proxy for reasoning correctness and inapplicable when no numerical final answer is required.
- Motivation: Models trained with final-answer rewards frequently generate invalid proofs and falsely judge flawed proofs as valid.The paper identifies high false-positive rates in proof verification, including acceptance of proofs with obvious logical flaws.
- Approach: Self-verification uses issue identification and verification effort to improve proof generation without requiring reference solutions.The proposed cycle feeds verification feedback into generation, labels difficult proofs, and improves the verifier itself.
- Results: DeepSeekMath-V2 assesses and iteratively improves its own proofs, achieving gold-level performance at IMO 2025 and CMO 2024.The model is optimized for natural-language theorem proving and demonstrates self-verifiable mathematical reasoning.
2. Method
The method trains a verifier to analyze proof issues and assign rubric-based scores, then strengthens its faithfulness through meta-verification. Reinforcement learning uses structured rewards and expert-labeled data to support this verification pipeline.
- Verifier training: The verifier produces an issue summary followed by a proof score of 1, 0.5, or 0 based on rigor, minor errors, or fatal flaws.Score 1 denotes complete and rigorous proofs, 0.5 sound logic with minor errors or omissions, and 0 fundamentally flawed proofs.
- Verifier training: The initial dataset contains problems, candidate proofs, and expert-aligned scores in {0, 0.5, 1}.Problems were crawled from proof-oriented AoPS contests, totaling 17,503 problems, and candidate proofs were iteratively refined before sampling.
- Verifier training: Verifier reinforcement learning combines format reward with score reward based on proximity between predicted and annotated proof scores.The objective requires both an issue summary and a proof score in the prescribed response format.
- Meta-verification: The initial verifier objective lacks direct supervision for identified issues, allowing correct scores alongside hallucinated problems.This creates a trustworthiness vulnerability when flawed proofs receive reward for score accuracy alone.
- Meta-verification: Meta-verification evaluates whether identified issues exist and logically justify the predicted proof score.A dedicated meta-verifier is trained from expert assessments and its feedback improves the faithfulness of issue identification.
Meta-Verifier Training Process
The paper trains a meta-verifier to assess the quality of verifier analyses, then incorporates that feedback into verifier and proof-generator training. Self-verification is trained by rewarding both proof quality and accurate recognition of proof rigor.
- Meta-Verifier Training Process: Experts score verifier analyses, and a meta-verifier learns to judge whether those analyses are accurate and justified.The meta-verifier analyzes identified issues and assigns a quality score to each verifier response.
- Meta-Verifier Training Process: Meta-verification feedback is integrated into the verifier’s reward function through a quality score produced by the meta-verifier.The enhanced verifier is trained on both verification and meta-verification datasets.
- Meta-Verifier Training Process: 0.96 average analysis quality, up from 0.85, was achieved while maintaining the same proof-score prediction accuracy.The improvement was measured on a validation split of the verification dataset using meta-verifier evaluation.
- Self-Verification Training: Iterative verification and refinement improve challenging proofs, but one-shot self-analysis can still claim correctness when an external verifier detects flaws.The generator can refine proofs from external feedback but does not initially evaluate its own work with the verifier’s rigor.
- Self-Verification Training: The proof generator is trained to produce a proof followed by a self-analysis using the verifier’s proof and meta-verification scores as rewards.The self-analysis follows the verifier’s format and rubrics, while a format reward checks that both outputs conform to the specified structure.
- Self-Verification Training: The reward structure favors faithful error acknowledgment and resolving as many proof issues as possible before finalizing the response.Correct proofs and accurate recognition of their rigor receive the highest rewards.
2.3. Synergy Between Proof Verification and Generation
The proof verifier and generator improve one another through a feedback cycle: stronger generators produce harder proofs, which provide training data for improving the verifier. Automated multi-sample verification and meta-verification replace manual annotation in later training iterations.
- Synergy Between Proof Verification and Generation: The verifier improves the proof generator, whose increasingly challenging proofs expose cases that can enhance the verifier.Proofs that defeat a single verification attempt become valuable training data for verifier improvement.
- Automated Labeling: Multiple verifier analyses increase the chance of detecting real issues in flawed proofs.This scaling strategy is used to surface potential issues for human review and later automation.
- Automated Labeling: Meta-verification validates verifier-identified issues and is more sample-efficient than finding proof issues from scratch.The process reviews proposed issues rather than requiring a fresh analysis of the entire proof.
- Automated Labeling: For each proof, the automated pipeline generates n independent analyses, validates issue reports with m meta-assessments, and labels the proof using the lowest score supported by at least k valid analyses.Proofs with no legitimate issues across all attempts receive score 1.
- Automated Labeling: In the last two training iterations, fully automated labeling replaced human annotation, with quality checks showing good agreement with expert judgments.The replacement applied to the final two iterations of verifier training.
3. Experiments
The experiments evaluate DeepSeekMath-V2 across theorem-proving benchmarks, testing one-shot generation, sequential self-refinement, and high-compute search. Expert assessments show strong competition performance, while the hardest IMO-level problems remain challenging.
- One-Shot Generation: DeepSeekMath-V2 consistently outperforms GPT-5-Thinking-High and Gemini 2.5-Pro across all five CNML-level problem categories.The categories are algebra, geometry, number theory, combinatorics, and inequality.
- Sequential Refinement with Self-Verification: Sequential self-verification improves Pass@1 as the maximum number of refinement attempts increases.The process generates a proof, analyzes it, and repeatedly prompts the generator to address identified issues until a perfect self-score or the attempt limit.
- Sequential Refinement with Self-Verification: Best@32 receives substantially higher verification scores than the average thread proof, indicating accurate self-selection of stronger proofs.Best@32 selects the highest-scoring proof per problem from 32 independent refinement threads.
- High-Compute Search: Expert evaluation awarded gold-level performance on IMO 2025 and CMO 2024, plus 118/120 on Putnam 2024.The model solved 5 of 6 IMO problems, 4 CMO problems plus partial credit on another, and 11 of 12 Putnam problems completely.
- High-Compute Search: The model outperforms DeepMind’s DeepThink on the basic IMO-ProofBench set and remains competitive on the advanced set.The authors also report that the hardest IMO-level problems remain challenging.
- High-Compute Search: Fully solved problems pass all 64 verification attempts, while unsolved problems typically have their genuine issues identified by the generator.The high-compute procedure scales verification and generation to address subtle proof issues and explore diverse strategies.
4. Related Work
Related work contrasts final-answer-based mathematical reasoning with theorem proving, where rigorous derivations are required, and discusses formal proof assistants as reliable but costly alternatives. The paper positions self-verification as a route combining informal mathematical reasoning with stronger reliability.
- Final-Answer Reasoning and Theorem Proving: Final-answer evaluation supports rapid progress on quantitative benchmarks such as AIME and HMMT but does not apply naturally to theorem proving.Theorem proving often requires rigorous step-by-step derivations without numerical answers.
- Formal Verification: Lean and Isabelle provide reliable proof verification by requiring formal proofs that are checked after compilation.Formal proof search systems can achieve strong results but may require substantial effort and formalization.
- Formal Verification: The paper aims to combine informal mathematical insights with formal guarantees to advance reliable mathematical reasoning systems.This frames self-verifiable reasoning as complementary to formal proof-assistant approaches.
5. Conclusion
The conclusion presents DeepSeekMath-V2 as a model that generates and verifies mathematical proofs through iterative self-evaluation and refinement. Its competition results support meaningful self-evaluation for complex reasoning, while the authors acknowledge that substantial challenges remain.
- Conclusion: DeepSeekMath-V2 generates and verifies mathematical proofs by training models to identify and resolve issues in their own reasoning.This moves beyond rewards based only on final answers.
- Conclusion: The training process alternates between improving verification and using verification to enhance generation, creating a cycle between the two capabilities.The verifier and generator are progressively improved together.
- Conclusion: The technical contributions include faithful proof verification, meta-verification, self-verification-guided generation, and scaled verification compute for automatic labeling.The automatic labeling process targets increasingly hard-to-verify proofs without human annotation.
- Conclusion: DeepSeekMath-V2 achieved gold-medal scores in IMO 2025 and CMO 2024 and a near-perfect Putnam 2024 score.The conclusion presents these results as evidence of strong competition-mathematics performance.
- Conclusion: The authors conclude that LLMs can develop meaningful self-evaluation abilities for complex reasoning tasks, while significant challenges remain.They frame the work as contributing to self-verifiable AI systems for research-level mathematics.
A. Prompt Templates
The prompt templates define how a meta-verifier assesses a verifier’s proof evaluation rather than solving the underlying problem. They separate restatement, defect, expression, and score analysis, then map the assessment to a 0, 0.5, or 1 quality rating.
- A.3. Meta-Verification Prompt: The meta-verification prompt evaluates a solution evaluation against a problem and solution, rather than directly solving the problem.Its output analyzes the evaluation and assigns a quality score.
- A.3. Meta-Verification Prompt: The evaluation checks step restatement, defect validity, expression accuracy, and score consistency.These aspects compare the evaluator’s claims with the original solution and the prescribed scoring rules.
- A.3. Meta-Verification Prompt: Defect analysis asks whether each reported defect exists and whether the evaluation analyzed it accurately.Positive claims about the solution are outside the stated defect-analysis scope.
- A.3. Meta-Verification Prompt: Expression analysis identifies inaccuracies in the evaluation, including typos, calculation errors, and inaccurate restatements.If an incorrect step is identified, downstream conclusions may be described as not rigorously demonstrated rather than automatically wrong.
- A.3. Meta-Verification Prompt: An evaluation receives score 0 when all reported defects are unreasonable and 0.5 when only some are reasonable.These rules apply when at least one unreasonable defect is found.
- A.3. Meta-Verification Prompt: When no defects are reported or all are reasonable, expression and score analysis determine whether the evaluation receives 0.5 or 1.A score of 1 requires no expression error and no scoring error under the evaluation rules.
- A.3. Meta-Verification Prompt: The required output contains an analysis followed by a numerical rating in boxed form using only 0, 0.5, or 1.The template specifies the analysis and rating fields explicitly.
- A.3. Meta-Verification Prompt: A referenced result does not justify a perfect solution score unless the solution also provides a valid proof of the referenced argument.The prompt’s underlying solution rubric scores complete, rigorous proofs as 1, generally correct proofs with minor issues as 0.5, and fundamentally flawed proofs as 0.
A.1. Proof Generation Prompt
The proof-generation prompt requires a detailed solution followed by self-evaluation, with iterative effort to identify and resolve issues before finalizing. It prioritizes faithful reporting of unresolved errors over falsely claiming correctness.
- The prompt requires a detailed, rigorous solution, including proof of any requested answer.
- The generator should locate and fix as many issues as possible before finalizing, while faithfully presenting unresolved problems.
- The generator must present its solution under a Solution section and its assessment under a Self Evaluation section.
- Self-evaluation must explain key steps, assess their correctness, and describe the causes and impacts of errors.
- The final self-evaluation assigns only 0, 0.5, or 1 after careful re-examination of the solution.
A.2. Proof Verification Prompt
The proof-verification prompt asks the model to assess a solution’s quality through detailed reasoning about its steps and then assign a rubric-based score. The rubric distinguishes complete proofs, mostly sound proofs with minor issues, and fundamentally flawed solutions.
- The verifier must evaluate whether a solution fully addresses the problem and provides a rigorous proof when an answer is requested.
- A score of 1 denotes a completely correct solution with all steps properly and clearly demonstrated.
- A score of 0.5 denotes generally correct reasoning with omitted details or minor errors.
- A score of 0 denotes failure to address the problem, fatal errors, or severe omissions.
- The evaluation must analyze key or doubtful steps, explain correctness or errors, and state each error’s impact on the solution.
A.4. Proof Refinement Prompt
The proof-refinement prompt supplies candidate solutions and their evaluations, asking the generator to produce a better solution by addressing reported issues or reusing promising ideas. The response must retain the prescribed solution and self-evaluation format.
- The refinement prompt provides candidate solutions together with correctness evaluations as inputs for improvement.
- The generator should fix issues identified in evaluations, reuse promising ideas, or combine both strategies.
- The final response must follow the earlier format, including Solution and Self Evaluation sections.