DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning

ArXiv: 2511.22570

🎯 Pitch

Forget final answers—DeepSeekMath-V2 teaches AI to catch its own mathematical lies by pitting a proof generator against a ruthless verifier that it also trains. This self-critiquing loop allows the model to nearly perfect the notoriously brutal Putnam exam (118/120) without ever seeing the solutions, eclipsing the best human score and suggesting a path toward AI that can reliably check its own reasoning on problems no one has ever solved.

---

1. Executive Summary

This paper introduces a framework for self-verifiable mathematical reasoning, training LLMs to both generate and verify natural-language mathematical proofs through an iterative cycle where a verifier identifies issues in proofs and a generator is incentivized to resolve those issues before finalizing its output. Built on DeepSeek-V3.2-Exp-Base and evaluated on competition theorem-proving benchmarks (IMO 2025, CMO 2024, Putnam 2024, IMO Shortlist 2024, and IMO-ProofBench), the system combines three named mechanisms—proof verification (training an LLM to score proofs on a 0/0.5/1 rubric via RL), meta-verification (a secondary evaluator that assesses whether the verifier's identified issues are real, reducing hallucinated flaws and improving analysis quality from 0.85 to 0.96), and self-verification (prompting the generator to produce a proof alongside a self-analysis, then rewarding faithful error acknowledgment over false correctness claims)—to create a synergistic cycle where scaling verification compute auto-labels increasingly hard-to-verify proofs, which in turn improves the verifier. With scaled test-time compute featuring parallel generation and iterative refinement guided by self-verification, DeepSeekMath-V2 achieves gold-medal scores on IMO 2025 (5 of 6 problems solved) and CMO 2024, and a near-perfect 118/120 on Putnam 2024—surpassing the highest human score of 90—while outperforming GPT-5-Thinking-High and Gemini 2.5-Pro on CNML-level problems across all mathematical categories, establishing that LLM-based self-verification can reliably assess proof correctness at competition levels, though the hardest IMO-level problems remain challenging.

2. Context and Motivation

The Core Problem: Correct Answers Don't Imply Correct Reasoning

The paper addresses a fundamental gap in how frontier LLMs are trained for mathematical reasoning. Over the past year, the dominant paradigm — reinforcement learning with rewards based on whether the model's final answer matches a ground-truth answer — has driven staggering progress on quantitative reasoning benchmarks. Models have gone from poor performance to saturating competitions like AIME and HMMT (Guo et al., 2025). But the paper argues this success masks a critical vulnerability:

"correct answers don't guarantee correct reasoning"

The paper identifies two specific failure modes of final-answer-based rewards (Section 1):

1. The proxy problem: A model can arrive at the correct numerical answer through flawed logic or fortunate errors. The reward signal treats this identically to a genuinely rigorous solution, creating no pressure for the model to develop sound reasoning habits. In practice, this means LLMs trained this way "still frequently produce mathematically invalid or logically inconsistent natural-language proofs."

2. Inapplicability to theorem proving: Many mathematical tasks — including the entirety of formal theorem proving — don't produce numerical answers at all. They require rigorous step-by-step derivation where the "answer" is the proof itself. Final-answer rewards are simply undefined for these problems. This is not a niche concern: it encompasses the entire field of proof-based mathematics, from high-school olympiads to research-level work.

Why This Matters: The Verification Gap and Its Consequences

The paper frames these limitations as symptoms of a deeper structural problem: the generation-verification gap in natural-language theorem proving (Section 1). In quantitative reasoning, verification is trivial — you check whether the final number matches. In theorem proving, verification requires understanding the entire logical structure of a proof, identifying gaps, and judging whether each step follows from previous ones. This is a fundamentally harder cognitive task.

The consequences of this gap are both practical and aspirational:

Practical bottleneck for self-improvement. The paper's central thesis is that "to push the limits of deep reasoning, we believe it is necessary to verify the comprehensiveness and rigor of mathematical reasoning." Without reliable verification, there's no mechanism for an LLM to distinguish good proofs from bad ones during training, and no way for it to iteratively improve its own outputs at test time. The entire RL-for-reasoning pipeline breaks down when the reward signal is unavailable or unreliable.

Scaling test-time compute. The paper explicitly connects verifier quality to test-time compute scaling. When a verifier can reliably identify issues, a model can spend additional inference compute searching for proofs that survive verification — analogous to how process reward models enable search in the quantitative reasoning setting (as discussed in the reference paper). But when the verifier hallucinates issues or misses genuine flaws, scaling compute amplifies noise rather than signal. This is particularly acute for "open problems without known solutions" where no ground-truth reference exists — verification must come from the model itself.

Toward research-level mathematics. The paper's ultimate ambition is not competition performance per se but building systems that could contribute to mathematical research. This requires models that can reason about problems without known answers, evaluate their own conjectures, and reliably distinguish promising approaches from dead ends. All of these capabilities depend on robust self-verification.

Prior Approaches and Their Shortcomings

The paper surveys several lines of work and identifies specific limitations in each:

Final-answer RL for quantitative reasoning (Guo et al., 2025; OpenAI, 2024). This is the approach that saturated AIME and HMMT. Its limitation is straightforward: it doesn't generalize to proof-based tasks. The paper acknowledges this as the state of the art for quantitative reasoning but positions it as fundamentally insufficient for theorem proving. The models produced by this approach "do not naturally develop the ability to verify proof validity — they exhibit high false-positive rates, often claiming incorrect proofs are valid even when they contain obvious logical flaws."

Prompting-based self-verification (Huang and Yang, 2025). Recent work has shown that models like Gemini 2.5 Pro can, to some degree, refine their own solutions by identifying issues and correcting them. The paper acknowledges this as evidence that "a certain level of self-verification capabilities" already exists in frontier models. However, the paper argues that this prompting-based approach is fragile and inconsistent — a theme echoed in the broader literature on LLM self-correction for reasoning (similar to the findings discussed in the reference paper, where prompted self-correction was largely ineffective without purpose-built fine-tuning). The paper's own experiments confirm this: when prompted to both generate and analyze its own proof, the generator "tends to claim correctness even when the external verifier easily identif[ies] flaws" (Section 2.2.2). In other words, the model can refine based on external feedback but fails to evaluate its own work with the same rigor.

Formal proof assistants (Lean, Isabelle) and neural theorem proving (AlphaProof, DeepSeek-Prover-V2, Seed-Prover). Formal verification offers perfect reliability — once a proof compiles in Lean or Isabelle, correctness is guaranteed (de Moura et al., 2015; Paulson, 1994). Systems like AlphaProof (AlphaProof and teams, 2024; Trinh et al., 2024) achieved IMO silver in 2024 using formal proof search, and Seed-Prover (Chen et al., 2025) recently solved 5 of 6 IMO 2025 problems in formal settings. The paper acknowledges these as powerful approaches but identifies two limitations:

1. Computational intensity: Formal proof search requires enormous computation. AlphaProof's IMO 2024 results required "intensive computation" for formal proof search.
2. The natural-to-formal gap: Writing proofs in formal languages is unnatural and laborious. Recent work has used informal reasoning to guide formal proof generation (Jiang et al., 2023; Ren et al., 2025), dramatically improving efficiency. But the paper argues that the informal reasoning components in these systems were "not specifically optimized for theorem proving tasks." The implicit argument is that improving the quality of informal mathematical reasoning — including verification — will directly benefit formal systems by providing better guidance.

The paper positions itself as complementary to formal methods: "We believe advancing natural language theorem proving will significantly benefit formal reasoning. We hope to contribute toward truly reliable mathematical reasoning systems that leverage both informal insights and formal guarantees."

DeepThink IMO-Gold (Luong and Lockhart, 2025). DeepMind's internal system achieved IMO 2025 gold using pure natural-language reasoning. The paper cites this as "an existence proof that LLM-based verification of complex proofs is achievable" — crucial motivation, since it demonstrates the ceiling is high. However, DeepThink is a proprietary system with no public methodology, leaving open questions about how such verification capabilities can be systematically developed.

Proof evaluation benchmarks and studies (Dekoninck et al., 2025; Luong et al., 2025). Recent work has begun systematically studying whether LLMs can evaluate proofs, both with and without reference solutions. The paper cites these as showing "promising results" but positions its own contribution as going beyond evaluation into a complete training methodology that produces both generation and verification capabilities, including the IMO-ProofBench benchmark (Luong et al., 2025) as a key evaluation target.

How This Paper Positions Itself

The paper's positioning involves several interconnected theses that collectively define a research direction rather than a single method:

Thesis 1: Verification can be learned through RL with human-annotated rubrics, not just prompted. The paper rejects the approach of simply prompting existing models to verify proofs (which it shows is unreliable) and instead develops a training pipeline that produces a dedicated verifier model through reinforcement learning on expert-annotated proof scores. This is analogous to how process reward models are trained in the quantitative reasoning setting, but applied to the substantially harder domain of natural-language proof evaluation.

Thesis 2: Meta-verification is necessary for faithful verification. The paper identifies a specific failure mode in training verifiers with score-only supervision: the verifier learns to predict the correct score while hallucinating non-existent issues. This is a form of reward hacking specific to the verification task. The meta-verification mechanism — training a second model to evaluate the verifier's analyses — is presented as the solution, and the paper argues this creates a "sustainable cycle" where improved verification enables improved generation, which produces harder-to-verify proofs, which become training data for further improving the verifier.

Thesis 3: Self-verification should be trained, not assumed. The paper's most distinctive argument is that the generator should be explicitly trained to perform verification on its own outputs, rather than relying on a separate verifier. This is operationalized through the reward function in Equation 5, which combines proof quality and self-assessment accuracy. The goal is to make the generator "explicitly aware of its reward function and enable it to maximize this reward through deliberate reasoning rather than blind trial-and-error" (Section 1). This is a departure from the standard RL-for-reasoning paradigm where the reward model is external and the generator's only job is to produce outputs that score highly.

Thesis 4: Scaling verification compute can automate the labeling bottleneck. The paper acknowledges that the verifier-generator cycle requires labeling new proofs as the generator improves and produces novel solutions. Manual annotation becomes increasingly expensive and eventually infeasible as proofs grow more sophisticated. The paper's automated labeling pipeline — using multiple verification samples and meta-verification to validate identified issues — is presented as a way to close the loop without human intervention. The paper reports that in its final two training iterations, "this fully automated pipeline replaced human annotation entirely" with labels aligning well with expert judgments.

Relationship to the reference paper's framework. The reference paper (on compute-optimal test-time scaling) decomposed test-time methods into modifications to the proposal distribution versus modifications to the verifier. This paper roughly inverts that relationship: instead of scaling test-time compute by optimizing how to use a fixed verifier, it focuses on building a better verifier and training the generator to internalize verification. The test-time compute scaling in Section 3.3.3 (parallel generation + iterative refinement guided by self-verification) is enabled by, rather than being the subject of, the core training methodology. In other words, the reference paper asked "given a verifier, how should we use it?" This paper asks "how do we build a verifier good enough that it's worth using at scale, and how do we make the generator incorporate verification into its own reasoning process?"

3. Technical Approach

3.1 Reader Orientation

This paper builds a training system that produces an LLM capable of both generating rigorous mathematical proofs and verifying their correctness—including its own—through a carefully orchestrated cycle of reinforcement learning where a verifier model is trained to identify logical flaws in proofs, a meta-verifier ensures those identified flaws are real rather than hallucinated, and a proof generator is explicitly incentivized to catch and fix errors in its own reasoning before finalizing its output. The system solves the problem of unreliable self-evaluation in theorem proving: existing LLMs can generate plausible-looking proofs but cannot reliably distinguish correct from incorrect reasoning, making them untrustworthy for tasks without known answers and blocking the feedback loop needed for iterative self-improvement. The shape of the solution is a three-component architecture—verifier, meta-verifier, and self-verifying generator—trained in alternating RL phases so that each component's improvements feed into the next, creating a virtuous cycle where better verification enables better generation, which produces harder-to-verify proofs that become training data for further improving the verifier.

3.2 Big-Picture Architecture (Diagram in Words)

The system has five major components connected by data flows during training and inference:

1. Problem Database (Dₚ) — 17,503 theorem-proving problems crawled from Art of Problem Solving (AoPS) contests, prioritizing math olympiads, team selection tests, and post-2010 problems that explicitly require proofs. This is the raw material from which all training data derives.

2. Proof Verifier (π_φ) — An LLM fine-tuned via RL to take a problem and a candidate proof as input, produce a detailed analysis of identified issues, and output a score in {0, 0.5, 1} according to defined rubrics. Trained on expert-annotated proof-score pairs (D_v), later enhanced with meta-verification feedback. This is the central evaluation engine.

3. Meta-Verifier (π_η) — A secondary LLM trained to evaluate the verifier's analyses rather than proofs directly. Given a problem, a proof, and the verifier's analysis of that proof, it checks whether identified issues actually exist and whether they logically justify the score. Trained on expert-annotated analysis-quality scores (D_mv). Its output feeds back into verifier training as an additional reward term, forcing the verifier to be faithful rather than just score-accurate.

4. Proof Generator (π_θ) — An LLM that produces proofs along with self-analyses. Trained via RL with a composite reward combining proof quality (scored by the verifier), self-assessment accuracy (how well its self-analysis score matches the verifier's score), and meta-verification quality of its self-analysis. The key design choice: it is rewarded for honestly identifying errors in its own work, not just for producing correct proofs.

5. Automated Labeling Pipeline — A test-time procedure that scales verification compute (multiple verifier samples per proof, multiple meta-verifier samples per analysis) to auto-label new proofs with scores of {0, 0.5, 1}. Used in later training iterations when the generator creates proofs too sophisticated for easy human annotation.

Information flow during training (iterative): Problems from Dₚ → Generator π_θ produces proofs → Verifier π_φ scores proofs → Expert annotations create labeled datasets (D_v, D_mv) → RL trains verifier π_φ and meta-verifier π_η → Meta-verifier feedback enhances verifier training → Enhanced verifier scores generator outputs → Generator π_θ is trained via RL against verifier scores plus self-verification rewards → New generator produces harder proofs → Automated labeling pipeline creates new training data → Cycle repeats.

Information flow during inference (scaled test-time compute): Problem → Generator produces 64 proof candidates → Verifier produces 64 analyses per proof → High-scoring proofs selected → Each proof paired with 8 analyses identifying issues → Generator refines each proof-analysis pair → New proofs enter candidate pool → Process iterates up to 16 times or until proofs pass all 64 verification attempts.

3.3 Roadmap for the Deep Dive

• First, the proof verification training pipeline (Section 2.1.1) — how the verifier is trained from cold-start human annotations, the RL objective, the scoring rubric, and the reward structure. This is foundational because all downstream components depend on having a reliable verifier.
• Second, the meta-verification mechanism (Section 2.1.2) — why score-only supervision leads to hallucinated issues, how the meta-verifier is trained, and how its feedback is integrated into verifier training via the composite reward (Equation 3). This addresses the faithfulness problem that would otherwise make the verifier unreliable.
• Third, the proof generator training (Section 2.2.1) — how the verifier serves as a generative reward model for RL-based generator optimization, including the GRPO algorithm and the iterative training schedule.
• Fourth, the self-verification mechanism (Section 2.2.2) — how the generator is prompted to produce both proofs and self-analyses, the composite reward function (Equations 5–6) that incentivizes honest self-assessment, the α/β weighting, and why this creates pressure to identify and resolve issues before finalizing output.
• Fifth, the automated labeling pipeline (Section 2.3) — how scaling verification and meta-verification compute enables automatic labeling of hard-to-verify proofs, the conditions under which a proof receives a score of 1 versus being discarded or routed to humans, and how this closed the training loop in the final iterations.

3.4 Detailed, Sentence-Based Technical Breakdown

This is primarily a systems and training methodology paper whose core idea is that reliable self-verification in theorem proving can be achieved by training a verifier with meta-verification-grounded RL, then training a generator to internalize verification through a composite reward that rewards honest error identification over false correctness claims, with the entire system bootstrapped through an iterative cycle where improved generation creates training data for improved verification.

---

3.4.1 Proof Verification: Training a Verifier with Score-Based RL

The proof verifier is the cornerstone of the entire system—every other component (meta-verification, generator training, self-verification, automated labeling) depends on having a model that can evaluate proof quality with reasonable accuracy. The paper develops this verifier through a multi-stage process: curating cold-start data with expert annotations, then training via reinforcement learning with a reward function that combines format compliance and score prediction accuracy.

Cold-start data curation (D_v). The initial training data is constructed through a three-step process that the paper describes in Section 2.1.1:

1. Problem collection: The authors crawl 17,503 problems from the Art of Problem Solving (AoPS) contest collections, specifically targeting "math olympiads, team selection tests, and post-2010 problems explicitly requiring proofs." This problem set is denoted D_p. The filtering criteria are important: by focusing on problems that explicitly require proofs (rather than numerical answers), the dataset is aligned with the verifier's intended use case. Post-2010 problems are prioritized to ensure relevance to modern competition standards.

2. Proof generation: Candidate proofs are generated using "a variant of DeepSeek-V3.2-Exp-Thinking." The paper notes that this base model "was not optimized for theorem proving and tended to produce concise but error-prone outputs." To compensate, the model is prompted to "iteratively refine its proofs over multiple rounds to improve comprehensiveness and rigor." This is a crucial design choice: the cold-start proofs are deliberately generated by a model that is not specifically good at theorem proving, producing a mix of correct, partially correct, and incorrect proofs that mirrors the distribution the verifier will encounter early in training. Using a stronger model might produce proofs that are too homogeneous (mostly correct), starving the verifier of negative examples.

3. Expert annotation: Mathematical experts score randomly sampled proofs across diverse problem types (algebra, number theory, etc.) according to evaluation rubrics I_v (detailed in Appendix A.2). Each proof receives one of three scores specified in the rubrics:

   • Score 1: "completely correct, with all steps executed properly and clearly demonstrated" — the proof is logically complete and rigorous.
   • Score 0.5: "generally correct, but with some details omitted or minor errors" — the overall logical structure is sound but there are small gaps or imprecisions.
   • Score 0: "does not actually address the required problem, contains fatal errors, or has severe omissions" — the proof is fundamentally flawed.

   Additionally, the rubrics specify that referencing external results (e.g., from papers) is acceptable "IF AND ONLY IF the solution also presents a valid proof of the reference argument(s); otherwise... the solution should be scored according to the criteria above, and definitely not with a score of 1." This prevents the model from claiming correctness by appealing to authority without demonstrating understanding.

The resulting dataset is D_v = {(X_i, Y_i, s_i)}, where X_i is a problem, Y_i is a candidate proof, and s_i ∈ {0, 0.5, 1} is the expert-annotated score.

Base model for verifier training. The verifier is trained starting from "a version of DeepSeek-V3.2-Exp-SFT which was supervised fine-tuned on reasoning data related to mathematics and code." This is a deliberate choice: rather than starting from a raw base model, the verifier inherits mathematical reasoning capabilities from SFT, which provides a stronger initialization for learning to evaluate proofs. The paper does not specify the exact SFT data composition beyond "reasoning data related to mathematics and code."

RL objective for the verifier. The verifier π_φ is trained with reinforcement learning to produce proof analyses. The model takes as input a problem X, a proof Y, and the evaluation rubrics I_v, and outputs a response V' containing both a summary of identified issues and a predicted score s'. The training uses two reward components:

Format reward (R_format): An indicator function—essentially a binary 0/1 check—that enforces the model's output to follow a specific structure. The format requirements are: (1) the response must contain the key phrase "Here is my evaluation of the solution:" and (2) the response must contain a score within \boxed{} following the text "Based on my evaluation, the final overall score should be:". If either condition fails, R_format = 0, zeroing out the total reward regardless of score accuracy. This is a common technique in RL for LLMs to enforce output structure without requiring the reward model to learn formatting preferences.

Score reward (R_score): Rewards proximity between the predicted score s'_i and the expert-annotated score s_i:

$R_{\text{score}}(s'_i, s_i) = 1 - |s'_i - s_i|$

where s'_i is the score predicted by the verifier (extracted from its output) and s_i is the ground-truth expert score.

What it computes: The absolute difference between the predicted and true scores, subtracted from 1. Since scores are in {0, 0.5, 1}, the possible outcomes are: if s'_i = s_i, R_score = 1 (perfect match); if they differ by 0.5 (e.g., predicting 1 when the truth is 0.5, or predicting 0.5 when the truth is 0), R_score = 0.5; if they differ by 1 (predicting 1 when truth is 0, or vice versa), R_score = 0. This is a linear penalty in the absolute error—well-calibrated for a three-point ordinal scale where adjacent mistakes (0 vs. 0.5) are less severe than extreme mistakes (0 vs. 1).

Why this form: A binary correct/incorrect reward would treat all mismatches equally, failing to capture the ordinal structure where 0.5 is "between" 0 and 1. The linear absolute-error penalty naturally encodes this: confusing a partially-correct proof with a correct one (0.5 → 1) is penalized less harshly than confusing a completely wrong proof with a correct one (0 → 1). The paper could have used a squared penalty (1 - (s'_i - s_i)²), but the linear form is simpler and adequate for a three-point scale.

Full RL objective. The verifier is trained to maximize:

$\max_{\pi_\varphi} \mathbb{E}_{(X_i, Y_i, s_i) \sim D_v, (V'_i, s'_i) \sim \pi_\varphi(\cdot|X_i, Y_i)} \left[ R_{\text{format}}(V'_i) \cdot R_{\text{score}}(s'_i, s_i) \right]$

where π_φ(·|X_i, Y_i) is the verifier's distribution over responses given the problem and proof, V'_i is the sampled response, and s'_i is the score extracted from it.

What it computes: For each training example (problem X_i, proof Y_i, true score s_i), the verifier generates a response V'_i containing a predicted score s'_i. The total reward is the product of the format reward and the score reward. Because R_format is binary (0 or 1), the product is zero if the format is wrong (no partial credit for partially correct formatting), and equals R_score if the format is correct. The expectation is over the training dataset D_v and the verifier's own stochastic generation.

Why this form: The multiplicative combination of format and score rewards creates a hard constraint: the model must learn formatting before it can receive any score-based reward. This prevents the model from achieving high rewards through accurate scores in unparseable outputs. It is mathematically equivalent to a constrained optimization where score accuracy is maximized subject to format compliance—a standard technique when the downstream consumer (the generator training pipeline) requires structured outputs.

Training algorithm. The paper uses Group Relative Policy Optimization (GRPO) (Shao et al., 2024) for all RL training in the system. GRPO is a variant of policy gradient methods that normalizes rewards within groups of sampled outputs for the same input, reducing variance and improving stability. The paper does not provide detailed GRPO hyperparameters for the verifier training specifically, but the general approach is consistent across all RL phases described in Section 3.1.

Design choice: score-only supervision. A critical aspect of this training approach is that the verifier receives supervision only on the final score s_i—not on the content of its issue analysis. The expert annotations do not include labels for whether each identified issue is real, whether all real issues are identified, or whether the reasoning in the analysis is sound. This makes annotation cheap (a single score per proof rather than detailed rubrics) but creates a vulnerability: the verifier can achieve perfect R_score by predicting the correct score while hallucinating non-existent issues or providing nonsensical justifications. The paper explicitly identifies this vulnerability and addresses it through meta-verification (Section 2.1.2), discussed in the next subsection.

---

3.4.2 Meta-Verification: Ensuring Faithful Issue Identification

The score-only supervision in Section 2.1.1 creates what the paper identifies as a "critical vulnerability":

"when evaluating flawed proofs (where s_i < 1) during training, the verifier can receive full reward by predicting the correct scores while hallucinating non-existent issues, undermining its trustworthiness."

In other words, the verifier learns that when it sees a proof with score 0, it should output a score of 0 along with some justification. The training signal does not distinguish between a verifier that correctly identifies the actual logical flaw and one that invents a plausible-sounding but non-existent issue. Both receive R_score = 1. This is a form of reward hacking specific to the verification task: the verifier optimizes for score prediction accuracy at the expense of analysis faithfulness.

The meta-verification concept. The solution is to introduce a secondary evaluation process: meta-verification—evaluating the verifier's analysis itself rather than the proof directly. Given a problem X, a proof Y, and the verifier's analysis V (which identifies issues and assigns a score), the meta-verifier assesses:

1. Whether the issues identified in V actually exist in Y (are they real or hallucinated?)
2. Whether the identified issues logically justify the score assigned (does the score follow from the issues, given the evaluation rubrics I_v?)

The meta-verifier uses a separate set of rubrics I_mv (detailed in Appendix A.3), which are substantially more elaborate than the basic verification rubrics because they must define what makes an analysis "reasonable" across multiple dimensions.

Meta-verifier rubric structure (Appendix A.3). The meta-verification rubrics define four analysis dimensions:

• Step Restatement: Checking whether the behaviors of the solution mentioned in the verifier's analysis actually appear in the original proof text. If the verifier claims "the solution assumes X without proof," the meta-verifier checks whether that assumption actually appears.
• Defect Analysis: The core dimension—checking whether errors or defects pointed out by the verifier are genuinely present in the proof. The rubric explicitly states that positive statements about the solution (claims that something is correct) are "not within your evaluation scope." This focuses the meta-verifier on false positives (hallucinated issues) rather than false negatives (missed issues).
• Expression Analysis: Checking for misstatements, typos, calculation errors, or inaccurate restatements in the verifier's analysis itself—separate from whether the underlying defect claim is valid.
• Score Analysis: Checking whether the final score matches the defects found, according to the original scoring rules.

The meta-verifier assigns quality scores m_s ∈ {0, 0.5, 1} to the verifier's analysis V according to these rules:

• Score 0: "If all defects found by the solution evaluation are unreasonable" — every claimed issue is hallucinated. This is the worst case: the verifier is fabricating problems.
• Score 0.5: Two cases: (a) "If some defects found by the solution evaluation are reasonable and some are unreasonable" — mixed quality, or (b) If all defects are reasonable but there are expression errors or the score is wrong. This captures partially-faithful analyses.
• Score 1: If the analysis finds no errors/defects and all defects found are reasonable, AND there are no expression errors AND the score is correct. This is a fully faithful, accurate analysis.

A subtle but important detail in the rubrics: "If the solution evaluation believes that the solution is completely accurate and has not found any errors or defects, then regardless of whether the solution itself is actually accurate, even if there are obvious errors, you should still consider its analysis of errors to be reasonable." This means the meta-verifier does not penalize false negatives (failing to identify real issues)—it only penalizes false positives (claiming issues that don't exist). This is an asymmetric evaluation that prioritizes avoiding hallucinated criticisms over ensuring comprehensive issue detection, which makes sense given the paper's goal of using verification feedback to guide generator training: hallucinated issues would lead the generator to "fix" non-existent problems, potentially introducing real errors.

Meta-verifier training. The meta-verifier π_η is trained through a similar process to the verifier:

1. Obtain initial verifier: Train π_φ following Section 2.1.1 to produce proof analyses.

2. Expert annotation of verifier analyses: Mathematical experts score the quality of verifier responses according to I_mv, creating dataset D_mv = {(X_i, Y_i, V_i, ms_i)}, where V_i is the verifier's analysis of proof Y_i for problem X_i, and ms_i ∈ {0, 0.5, 1} is the expert-annotated quality score.

3. RL training: The meta-verifier π_η(·|X, Y, V, I_mv) is trained to analyze the verifier's proof analysis V. Its output includes a summary of issues found in the analysis itself, followed by a quality score. The RL objective "follows the same structure as the verifier training, with format and score rewards." The format reward enforces that the meta-verifier outputs the expected structure; the score reward uses the same linear penalty 1 - |ms'_i - ms_i| to reward proximity to the expert-annotated quality score.

Integrating meta-verification into verifier training. With the trained meta-verifier π_η, the paper enhances verifier training by adding a third reward term:

$R_V = R_{\text{format}} \cdot R_{\text{score}} \cdot R_{\text{meta}}$

where R_meta is the quality score produced by the meta-verifier π_η when evaluating the verifier's analysis.

What it computes: The total reward for the verifier during enhanced training is the product of three terms: format compliance (0 or 1), score prediction accuracy (0 to 1, from the linear penalty), and meta-verification quality (0 to 1, the meta-verifier's assessment of how faithful the analysis is). Because format is binary, a format violation zeroes out everything. With correct format, the reward is R_score × R_meta. This means the verifier must simultaneously predict accurate scores AND produce faithful analyses—hallucinated issues that lower R_meta will reduce the total reward even if R_score remains high.

Why this form: The multiplicative composition is crucial. An additive combination (R_score + R_meta) would allow the verifier to compensate for unfaithful analysis with highly accurate scores. Multiplication forces both components to be non-zero for the reward to be non-zero, creating a logical AND condition: the verifier only receives high reward when it is BOTH score-accurate AND faithful. This is the same principle as the format × score multiplication, applied one level up in the hierarchy.

Training on both datasets. The enhanced verifier is trained on both the verification dataset D_v (problem-proof-score triples) and the meta-verification dataset D_mv (problem-proof-analysis-quality tuples), using "the same reward mechanism on D_mv as used for training the meta-verifier." This means the verifier learns to perform both tasks: verifying proofs and meta-verifying other verifications. The paper states the resulting model "can perform both proof verification and meta-verification tasks," which is important because during self-verification training (Section 2.2.2), the generator needs to produce both proofs and self-analyses, and during automated labeling (Section 2.3), the system needs to meta-verify verification analyses.

Results of meta-verification. The paper reports a specific quantitative improvement:

"On a validation split of D_v, the average quality score of the verifier's proof analyses—as evaluated by the meta-verifier—improved from 0.85 to 0.96, while maintaining the same accuracy in proof score prediction."

This is a substantial jump: from 0.85 to 0.96 on a 0–1 scale means the verifier goes from having noticeable unfaithfulness issues to being nearly perfectly faithful at identifying real issues. Critically, this improvement comes "while maintaining the same accuracy in proof score prediction"—the meta-verification feedback doesn't degrade the verifier's core scoring capability. This validates the paper's central thesis that faithfulness and accuracy can be jointly optimized through meta-verification.

Design choice: meta-verification as a separate model vs. self-consistency. The paper trains a dedicated meta-verifier rather than using the verifier to check its own outputs (self-consistency) or using ensemble disagreement as a faithfulness signal. A dedicated meta-verifier is more expensive to train (requiring additional expert annotations) but provides a stronger training signal because it is specifically optimized for the meta-evaluation task. Self-consistency approaches (generating multiple verifier analyses and checking agreement) are used later in the automated labeling pipeline (Section 2.3) as a test-time technique, but for training, having a purpose-built meta-verifier provides cleaner gradient signals.

---

3.4.3 Proof Generator Training: RL with Verifier as Reward Model

With a trained verifier π_φ that can assign scores to proofs, the paper uses it as a generative reward model to train the proof generator π_θ. This follows the standard RL-for-reasoning paradigm (Guo et al., 2025) but applied to theorem proving rather than quantitative reasoning.

RL objective for proof generation. The generator π_θ(·|X) is trained to maximize:

$\max_{\pi_\theta} \mathbb{E}_{X_i \sim D_p, Y_i \sim \pi_\theta(\cdot|X_i)} [R_Y]$

where R_Y is the proof score produced by the verifier π_φ(·|X_i, Y_i, I_v).

What it computes: For each problem X_i sampled from the problem database D_p, the generator produces a proof Y_i by sampling from its current policy π_θ(·|X_i). This proof is then scored by the frozen verifier π_φ using the evaluation rubrics I_v, producing a score R_Y ∈ {0, 0.5, 1}. The generator is optimized to maximize the expected score over the problem distribution—essentially, to produce proofs that the verifier rates highly.

Why this form: This is the standard policy gradient setup for RL fine-tuning of LLMs, where the verifier serves as the reward function. The expectation over problems from D_p ensures the generator is optimized for the right distribution (competition math problems requiring proofs). The expectation over Y_i ∼ π_θ(·|X_i) means the generator learns from its own outputs (on-policy), which is important for alignment: the generator must learn to produce good proofs under its own distribution, not just mimic a dataset of good proofs.

Initialization and training schedule (Section 3.1). The paper employs an iterative training schedule described in Section 3.1:

"In each iteration, we first optimized proof verification. The proof generator was then initialized from the verifier checkpoint and optimized for proof generation."

This means the generator is not trained from scratch—it inherits the verifier's capabilities as a starting point. This is a crucial design choice with several implications:

1. Knowledge transfer: The verifier has learned to recognize what makes a proof correct or incorrect. By initializing the generator from the verifier checkpoint, these evaluation capabilities are preserved in the generator, enabling the self-verification behavior that is central to the paper's approach.

2. Warm start: Rather than learning theorem proving from scratch, the generator starts with a model that already understands mathematical reasoning (from the SFT base), proof evaluation (from verifier training), and meta-evaluation (from the joint training on D_v and D_mv). This dramatically reduces the exploration required during generator RL.

3. Iterative improvement: Starting from the second iteration, the verifier is initialized from a checkpoint that "consolidated both verification and generation capabilities from the previous iteration through rejection fine-tuning." This means each iteration's verifier benefits from the previous iteration's generation improvements, and vice versa, creating the synergistic cycle described in Section 2.3.

GRPO training. The paper uses Group Relative Policy Optimization (GRPO) for generator training. GRPO normalizes rewards within groups of outputs sampled for the same input, computing advantages relative to the group mean. This reduces variance compared to standard REINFORCE and provides a natural curriculum: early in training when all outputs score similarly, advantages are small; as the generator improves and produces a mix of good and bad proofs, advantages grow, providing stronger learning signals.

What the generator is NOT trained to do at this stage. In this phase (Section 2.2.1), the generator is trained solely to produce good proofs—it does not yet produce self-analyses or engage in self-verification. The reward R_Y comes entirely from the external verifier. The self-verification capability is added in the next phase (Section 2.2.2) through a modified training procedure.

---

3.4.4 Self-Verification: Training the Generator to Evaluate Its Own Proofs

The paper observes a critical limitation with the generator trained in Section 2.2.1:

"when prompted to both generate and analyze its own proof in one shot, the generator tends to claim correctness even when the external verifier easily identif[ies] flaws. In other words, while the generator can refine proofs based on external feedback, it fails to evaluate its own work with the same rigor as the dedicated verifier."

This is the self-evaluation gap: the generator possesses the capability to produce proofs (learned in Section 2.2.1) and the capability to evaluate proofs (inherited from the verifier initialization), but it does not reliably apply the evaluation capability to its own outputs. When generating and evaluating simultaneously, it defaults to claiming correctness—a form of confirmation bias or self-consistency pressure.

The self-verification training format. To close this gap, the paper trains the generator with a specific output format and reward structure. During training, the generator π_θ is prompted to produce two components in sequence (see Appendix A.1 for the full prompt):

1. ## Solution: The proof itself, following the same standards as before.
2. ## Self Evaluation: A self-analysis of that proof, following the same format and rubrics I_v as the external verifier. This includes a detailed issue analysis and a predicted score s' within \boxed{}.

The prompt is carefully designed to incentivize honest self-assessment. Key excerpts from the generation prompt (Appendix A.1):

"Only when you fail to locate any issues in your solution should you score it with 1."

"If you do notice some issues in your solution but fail to resolve them with your best efforts, it's totally ok to faithfully present the issues in your final response."

"The worst final response would provide a wrong solution but lie that it's correct or claim that it's correct without careful error checking. A better version should faithfully identify errors in the solution. Remember! You CAN'T cheat! If you cheat, we will know, and you will be penalized!"

These prompts create explicit instructional pressure for honest self-evaluation, but the paper found that instructions alone are insufficient—the training reward structure must be designed to reinforce the desired behavior.

Composite reward function for self-verification. The generator's output (proof Y and self-analysis Z) is evaluated using a reward function that combines proof quality and self-assessment fidelity:

$R = R_{\text{format}}(Y, Z) \cdot (\alpha \cdot R_Y + \beta \cdot R_Z)$

where:

• R_format(Y, Z) is a binary indicator (0 or 1) verifying that both the proof and self-analysis follow the specified format (correct markdown headers, required phrases, boxed score).
• R_Y is the proof quality score produced by the external verifier π_φ(·|X, Y, I_v)—this is the same R_Y from Section 2.2.1.
• R_Z is the self-assessment quality score (defined below).
• α = 0.76 and β = 0.24 are weighting coefficients.

What it computes: The total reward is the format check (0 or 1) multiplied by a weighted sum of proof quality (R_Y) and self-assessment quality (R_Z). If the format is wrong, reward is 0 regardless of content. If the format is correct, the reward is a convex combination of how good the proof is (76% weight) and how good the self-assessment is (24% weight). This means producing a correct proof with accurate self-recognition of its correctness is rewarded most; producing a flawed proof but honestly identifying the flaws is rewarded more than producing a flawed proof and claiming it's perfect.

Why this form: The additive combination (rather than multiplicative) means that proof quality and self-assessment quality can partially compensate for each other: a perfect proof with mediocre self-assessment still gets some reward, and a flawed proof with excellent self-assessment also gets some reward. This is different from the verifier's reward structure (where format × score was multiplicative). The additive form here reflects that both objectives matter independently and a failure in one should not zero out the other—the generator should be encouraged to improve both simultaneously, not gate one on the other. The specific α/β split (0.76/0.24) heavily weights proof quality, which makes sense: the ultimate goal is correct proofs, and self-assessment is a means to that end, not an end in itself.

Self-assessment quality R_Z. This is itself a composite:

$R_Z = R_{\text{score}}(s', s) \cdot R_{\text{meta}}(Z)$

where:

• s' is the score the generator predicts for its own proof in the self-analysis Z.
• s is the score the external verifier assigns to the proof Y—this is the "ground truth" for the self-assessment task.
• R_score(s', s) = 1 - |s' - s| is the same linear penalty as in verifier training, rewarding accuracy of self-assessment.
• R_meta(Z) is the meta-verification score of the self-analysis Z, produced by the meta-verifier π_η.

What it computes: The self-assessment quality R_Z is the product of two terms: how accurately the generator scored its own proof (R_score, comparing self-predicted score to external verifier score) and how faithful the self-analysis is (R_meta, checking whether identified issues are real). Both must be non-zero for R_Z to be non-zero. This is a multiplicative gate: the generator cannot get credit for accurate self-assessment if that assessment is unfaithful (e.g., claiming the correct score but for hallucinated reasons), and it cannot get credit for faithful analysis if the score prediction is wrong.

Why this form: This directly parallels the verifier's enhanced training objective (R_V = R_format × R_score × R_meta) from Section 2.1.2. The generator's self-analysis is held to the same standard as the verifier's analyses: it must be both score-accurate and faithful. The key difference is that in the verifier's case, the three terms were multiplied together; here, R_score and R_meta are multiplied within R_Z, and R_Z is then additively combined with R_Y. This reflects the different roles: the verifier's sole job is verification accuracy, so all requirements are non-negotiable (multiplicative); the generator's primary job is proof production, with verification as a secondary capability, so the verification component is additive.

The incentive structure created by this reward. The paper explicitly describes the incentives:

"Faithful acknowledgment of errors is rewarded over false claims of correctness."

• If the generator produces a flawed proof (s = 0 or 0.5) and honestly identifies the flaws (s' = s, faithful analysis), R_score = 1 and R_meta = 1, so R_Z = 1. The total reward is α × (low R_Y) + β × 1, which is modest but non-zero.
• If the generator produces a flawed proof but falsely claims it's correct (s = 0, s' = 1), R_score = 0, so R_Z = 0. The total reward is α × R_Y + β × 0 = α × R_Y, which is lower than the honest case because R_Z drops from 1 to 0.

"The highest rewards come from producing correct proofs and accurately recognizing their rigor."

• If the generator produces a correct proof (s = 1, R_Y = 1) and accurately recognizes it as correct (s' = 1, R_score = 1, R_meta = 1, R_Z = 1), the total reward is α × 1 + β × 1 = α + β = 1.0, which is the maximum possible.

"A good strategy to obtain high rewards for the proof generator is to identify and resolve as many issues as possible before finalizing the response."

• The generator is prompted to think through its proof, identify issues, fix them, and only finalize when no more issues can be found. Since R_Y depends on the final proof quality and R_Z depends on the accuracy and faithfulness of the self-analysis on that final proof, the optimal strategy is to produce the best possible proof AND honestly report its quality. There is no incentive to claim uncorrected flaws don't exist (R_meta would detect this), and no incentive to claim flaws exist in a correct proof (R_score would penalize this).

Why α = 0.76 and β = 0.24. The paper does not explain the origin of these specific values, but their ratio (roughly 3:1) means proof quality is weighted about three times as heavily as self-assessment quality. This is a hyperparameter choice that balances two competing concerns: too much weight on R_Z (β > α) would incentivize the generator to produce flawed proofs just so it can demonstrate honest self-criticism—the "good student who can't solve anything but gives great error analyses" problem. Too little weight on R_Z (β → 0) would reduce to the standard generator training from Section 2.2.1, losing the self-verification incentive entirely. The 3:1 ratio provides a strong primary objective (correct proofs) with a non-trivial secondary objective (honest self-assessment) that shapes behavior without dominating.

Relationship to the verifier's training. At this stage, the generator is effectively performing both roles: proof generation (Section 2.2.1) and proof verification (Section 2.1.1), with the self-analysis acting as the verification output. The external verifier and meta-verifier are used only to compute rewards during training—they do not participate in the generator's forward pass. This is what the paper means by "self-verifiable": at inference time, the model can evaluate its own outputs without calling external verifiers.

The self-verification prompt in detail (Appendix A.1). The full prompt is extensive and includes several design elements worth noting:

• It includes the complete evaluation rubrics I_v inline, so the generator has direct access to the same scoring criteria the verifier uses.
• It explicitly tells the model: "In fact, you already have the ability to rate your solution yourself, so you are expected to reason carefully about how to solve a given problem, evaluate your method according to the instruction, and refine your solution by fixing issues identified until you can make no further progress."
• The output format specification (## Solution followed by ## Self Evaluation) provides structural scaffolding for the dual-output task.
• The self-evaluation section requires: "Here is my evaluation of the solution:" as the starting phrase (mirroring the verifier's format), followed by detailed analysis, then \boxed{score} after "Based on my evaluation, the final overall score should be:".

This prompt structure ensures the generator's self-analysis is directly comparable to the verifier's analysis format, which is important for the meta-verifier (trained on verifier-format analyses) to evaluate it reliably.

---

3.4.5 Synergy and Automated Labeling: Closing the Training Loop

The paper identifies a fundamental challenge in maintaining the verifier-generator cycle: as the generator improves, it produces proofs that are increasingly sophisticated and harder for the current verifier to evaluate accurately. This creates a moving target problem: the verifier trained on earlier, simpler proofs may not generalize to the generator's newer, more sophisticated outputs. To maintain the generation-verification gap, the verifier must be retrained on these new proofs—but obtaining labeled data for them requires human annotation, which becomes "increasingly time-consuming as problems grow harder and errors become more subtle."

AI-assisted annotation as an intermediate step. The paper first attempts to boost annotation efficiency through AI assistance: generating multiple verifier analyses per proof to "surface potential issues for human review." Rather than having experts read proofs from scratch and identify issues, experts review the verifier's identified issues and judge whether they are real—essentially performing meta-verification. This is faster because reviewing is easier than discovering, but still requires human effort.

Two observations enabling full automation. From this AI-assisted process, the paper recognizes two facts that make full automation feasible:

1. Scaling verifier samples increases recall: "Scaling verifier samples increases the probability of catching real issues in flawed proofs." If a proof has a flaw, generating many independent verification analyses makes it increasingly likely that at least one analysis will identify it. This is analogous to best-of-N sampling for generation—more samples increase the chance of finding the signal.

2. Meta-verification is easier and more sample-efficient: "Reviewing the verifier's identified issues is exactly meta-verification, which is easier than identifying issues from scratch. Meta-verification is also more sample-efficient for LLMs to master." This is the key insight: determining whether a claimed issue is real (reading the proof at the cited location and checking the logic) is cognitively simpler than reading an entire proof and finding all issues. LLMs, like humans, find verification easier than generation in many domains.

The automated labeling pipeline. Building on these observations, the paper develops a fully automated process that replaces human annotation:

Step 1: Generate n independent verification analyses. For each proof Y (produced by the current generator), the verifier generates n independent analyses, each containing identified issues and a score. The paper does not specify the exact value of n used, but based on the test-time compute settings (64 verification analyses per proof), n is likely in the range 32–64 to achieve high recall.

Step 2: Meta-verify analyses that report issues. For each analysis V that reports issues (scores 0 or 0.5—i.e., claiming the proof is flawed), the meta-verifier generates m independent assessments to validate whether the identified problems are real. An analysis is "deemed valid if the majority of meta-assessments confirm its findings." The paper does not specify m, but majority voting across multiple meta-assessments provides robustness against individual meta-verifier errors—if 3 of 5 meta-assessments say an issue is real, it's likely real.

Step 3: Assign proof scores based on validated analyses. The labeling logic examines analyses that assign the lowest score to the proof (prioritizing analyses that claim the proof is most flawed):

• If at least k such analyses are deemed valid (their identified issues confirmed by majority meta-verification), the proof is labeled with that lowest score. This means: multiple independent verifier runs found genuine issues that survived meta-verification scrutiny—strong evidence the proof deserves that score.
• If no legitimate issues are identified across all verification attempts (no analyses, or all issue-claiming analyses fail meta-verification), the proof is labeled with score 1 (perfect). This means: after extensive verification effort, no real flaws were found—the proof is presumed correct.
• Otherwise, the proof is discarded or routed to human experts for labeling. This handles ambiguous cases where some analyses find issues but too few are confirmed to reach the threshold k, or where meta-verification results are mixed.

The paper does not specify exact values for n, m, and k, stating only that "in our last two training iterations, this fully automated pipeline replaced human annotation entirely" and that "quality checks confirmed that the automated labels aligned well with expert judgments."

Why this works. The automated pipeline leverages the asymmetry between type I and type II errors in verification. A false positive (claiming an issue that doesn't exist) is caught by meta-verification: if a verifier hallucinates a flaw, the meta-verifier will (on average) identify it as unreasonable during majority voting. A false negative (missing a real issue) is mitigated by scaling n: with enough independent verification attempts, at least one is likely to catch the flaw. The proof only receives score 1 if NO analysis finds a genuine issue—a high bar that requires the proof to survive extensive adversarial scrutiny.

The pipeline's reliance on majority voting across independent samples connects to the broader theme of test-time compute scaling: spending more compute (n verifier samples × m meta-verifier samples per proof) increases the reliability of the automated labels, trading compute for annotation quality. This is analogous to how the reference paper used PRM-guided search to improve answer selection—here, it's used to improve training data quality.

The synergistic cycle in practice. The paper describes this as a "synergistic cycle" (Section 2.3):

1. Verifier → Generator: The verifier provides reward signals for generator RL training (Sections 2.2.1) and evaluation of self-analyses (Section 2.2.2).
2. Generator → Verifier: The improved generator produces new proofs that challenge the verifier's capabilities. These proofs, auto-labeled through the pipeline, become training data D_v for further verifier improvement.
3. Verifier → Generator (next iteration): The improved verifier provides better reward signals, enabling further generator improvement.

The paper states that starting from the second training iteration, "the proof verifier was initialized with a checkpoint that consolidated both verification and generation capabilities from the previous iteration through rejection fine-tuning." Rejection fine-tuning likely means: take the previous iteration's best generator outputs (those with high verifier scores), fine-tune on them, and use that as the base for the next verifier. This transfers generation knowledge into the verifier, helping it stay calibrated to the current generator's output distribution.

Connection to the generation-verification gap. The entire Section 2.3 is motivated by this gap: "the verifier improves the generator, and as the generator improves, it produces new proofs that challenge the verifier's current capabilities." Without the automated labeling pipeline, this gap would widen until the verifier could no longer provide useful training signals. The pipeline ensures the gap is continually closed by feeding the verifier training data at the frontier of its capabilities. This creates a sustainable self-improvement loop where neither component outpaces the other's ability to provide feedback—a necessary condition for unbounded improvement through iterative training.

---

3.4.6 Summary of Design Choices and Their Justifications

• Three-point scoring rubric (0/0.5/1) rather than binary pass/fail: captures the nuance between fundamentally flawed proofs, proofs with minor issues, and fully rigorous proofs. The 0.5 category is crucial for generator training—it provides a gradient between "completely wrong" and "perfect" that guides improvement.
• Score-only supervision with meta-verification correction rather than comprehensive annotation of all issues: reduces annotation cost while using a secondary model (meta-verifier) to ensure faithfulness, achieving the benefits of detailed supervision without the annotation burden.
• Multiplicative reward composition for verifier training (R_format × R_score × R_meta): creates hard AND constraints where all requirements must be met; prevents the model from compensating for unfaithfulness with accurate scores.
• Additive reward composition for generator training (α·R_Y + β·R_Z): allows partial credit when one objective is met but not the other; reflects that proof quality is primary and self-assessment is secondary.
• Generator initialized from verifier checkpoint: transfers evaluation capabilities to the generator, enabling self-verification without separate training; the model already knows how to evaluate proofs before learning to generate them.
• GRPO for all RL training: provides stable, variance-reduced policy gradients suitable for the large action spaces of LLM token generation.
• Automated labeling via scaled verification + meta-verification: replaces human annotation in later iterations by exploiting the observation that meta-verification is easier than verification, and that scaling compute increases issue detection probability.
• Edit-distance-based incorrect-correct pairing for revision training data (Appendix A.4): The refinement prompt in Appendix A.4 includes candidate solutions with evaluations; the generator is asked to "provide a better solution by solving issues mentioned in the evaluation(s), or by re-using promising ideas mentioned in the solution sample(s), or by doing both." This is not the same as the edit-distance pairing from the reference paper, but serves a similar purpose: providing the model with concrete examples of what to fix rather than asking it to identify issues from scratch.
• 128K token limit: The paper mentions that for challenging problems "models often cannot generate comprehensive and rigorous proofs in a single attempt within the 128K token limit." This constraint motivates the sequential refinement approach (Section 3.3.2), where the model iteratively improves over multiple inference calls, each building on the previous output. The 128K context window is the ceiling per generation, but sequential refinement effectively extends the total reasoning budget across multiple calls.

4. Key Insights and Innovations

Innovation 1: Self-Verification as a Learned Capability, Not an Emergent Property

Prior to this work, the dominant assumption—implicit in both the RL-for-reasoning paradigm (Guo et al., 2025) and in prompting-based self-correction approaches (Huang and Yang, 2025)—was that a model trained to generate correct outputs would naturally develop the ability to evaluate its own outputs. The reasoning was seductive: if a model can identify correct reasoning when producing it, surely it can recognize errors when they appear. The paper shows this assumption is false and, more importantly, provides a diagnosis of why it fails and a training methodology to correct it.

The diagnostic finding appears in Section 2.2.2: when prompted to both generate and analyze its own proof in one shot, the generator "tends to claim correctness even when the external verifier easily identify flaws." The model possesses the capability to evaluate proofs—it was initialized from a verifier checkpoint explicitly trained for this task—but it fails to apply that capability to its own outputs. This is not a capability gap; it is a deployment gap. The model defaults to self-consistency, treating its own output as presumptively correct rather than subjecting it to the same scrutiny it would apply to another model's proof.

What makes this finding distinctive is that it reframes self-verification from an architectural question (can LLMs verify?) to a training question (how do we incentivize them to actually do it?). The paper's key conceptual move is to make the generator "explicitly aware of its reward function and enable it to maximize this reward through deliberate reasoning rather than blind trial-and-error" (Section 1). This is operationalized through the composite reward function in Equations 5–6, which creates a situation where "faithful acknowledgment of errors is rewarded over false claims of correctness." The critical insight is that the reward must structurally incentivize self-scrutiny—it cannot be assumed to emerge from generic capability improvements.

This is a fundamental shift, not an incremental refinement. It changes the framing of self-evaluation from something that LLMs might eventually do if they become capable enough, to something that must be explicitly trained into them through careful reward design. The evidence is not a single ablation but the entire architecture of the paper: the verifier is trained first, then the generator is initialized from it (transferring evaluation capability), then self-verification training adds the behavioral incentive to actually use that capability on the generator's own outputs. The 0.76/0.24 weighting in Equation 5 is not an arbitrary hyperparameter—it encodes the judgment that proof quality is primary but self-assessment quality must be non-trivially weighted to shape behavior. Without the β·R_Z term (β = 0), the generator would have no incentive to develop honest self-evaluation, and the self-verification capability would atrophy despite the verifier-initialized starting point.

Innovation 2: Meta-Verification as the Mechanism for Closing the Faithfulness Gap

The paper identifies a specific failure mode in training verifiers with score-only supervision that, to the authors' knowledge, had not been systematically characterized in prior work on LLM-based evaluation: the verifier learns to predict correct scores while hallucinating non-existent issues. This is a form of reward hacking unique to the verification domain. The standard approach in prior work—training a reward model to predict human preferences or correctness labels—assumes that the model's internal reasoning, to the extent it exists, will approximately track the true reasons for the label. The paper shows this assumption breaks down when the label is coarse (a single score) and the reasoning space is rich (all possible flaws in a mathematical proof).

The key diagnostic is in Section 2.1.2: a verifier trained only with the R_format × R_score objective can achieve perfect reward on flawed proofs (score = 0) by outputting the correct score along with fabricated justifications. The training signal does not distinguish between a verifier that identifies the actual logical flaw and one that invents a plausible-sounding but nonexistent gap. This is not merely an accuracy problem—the verifier's score predictions might remain well-calibrated—but a faithfulness problem that makes the verifier's analyses unusable as feedback for generator training. If the generator is told to fix issues that don't exist, it may introduce real errors in the process of addressing phantoms.

Meta-verification is the solution, but what makes it innovative is not the specific mechanism (training a second model) but the diagnosis that faithfulness and accuracy are separable objectives that must be optimized jointly through a specific reward structure. The multiplicative composition R_V = R_format × R_score × R_meta (Equation 3) is not an obvious design choice—it encodes the insight that faithfulness cannot be traded off against accuracy; both must be non-zero for the reward to be non-zero. This is a conceptual advance over prior work on reward model training, which typically treats accuracy (correlation with human labels) as the sole objective.

The evidence is the reported improvement in meta-verifier-assessed quality from 0.85 to 0.96 while maintaining score prediction accuracy (Section 2.1.2). This is a substantial effect: the verifier goes from having noticeable unfaithfulness issues to being nearly perfectly faithful at identifying real flaws, without any degradation in its core scoring capability. The finding that these two objectives can be jointly optimized without tradeoff is significant in itself—it suggests that faithfulness and accuracy draw on overlapping capabilities (understanding the proof's logical structure) rather than competing for model capacity.

This is a fundamental contribution to the methodology of training evaluator models. It establishes that when an evaluator's outputs are used as feedback for training another model (rather than just for final assessment), faithfulness matters independently of accuracy, and meta-evaluation provides a scalable mechanism for enforcing it. The paper's approach to meta-verification—defining a detailed rubric that distinguishes defect analysis from expression analysis, and explicitly excluding false negatives from the evaluation scope—is a careful operationalization of what "faithfulness" means in this context, and it could inform similar work in other domains where evaluator outputs serve as training signals.

Innovation 3: The Automated Labeling Pipeline as a Scalable Alternative to Human Annotation for Proof Verification Data

The paper's third distinctive contribution is the recognition that scaling verification and meta-verification compute can replace human annotation for labeling proof correctness—and that this is not merely a cost-saving measure but a necessary condition for sustaining the verifier-generator improvement cycle. As the generator improves, it produces proofs that are increasingly sophisticated and harder for the current verifier to evaluate. Human annotation becomes a bottleneck not just in cost but in expertise: as problems grow harder, fewer human annotators are qualified to judge proof correctness, and even experts may disagree on subtle logical points.

The key insight enabling automation is the asymmetry between two cognitive tasks: identifying issues in a proof from scratch (verification) is harder than judging whether a claimed issue actually exists (meta-verification). The paper explicitly states this in Section 2.3: "Reviewing the verifier's identified issues is exactly meta-verification, which is easier than identifying issues from scratch. Meta-verification is also more sample-efficient for LLMs to master." This mirrors a well-known phenomenon in human cognition—verification is often easier than generation—but operationalizing it as a two-stage automated pipeline with majority voting across independent samples is a novel contribution to the LLM training literature.

The pipeline's design also encodes a second insight: false positives (hallucinated issues) and false negatives (missed issues) have asymmetric consequences for training data quality, and the pipeline can be tuned to handle them differently. False positives are caught by meta-verification majority voting: if a verifier claims an issue that doesn't exist, multiple independent meta-verifier assessments will (on average) identify it as unreasonable. False negatives are mitigated by scaling n (the number of verification samples per proof): with enough independent attempts, at least one is likely to catch any real flaw. The proof only receives a score of 1 if NO analysis finds a genuine issue—a high bar that requires surviving extensive adversarial scrutiny. This asymmetry exploits the fact that it's safer to mistakenly label a correct proof as flawed (which just provides more negative training examples) than to mistakenly label a flawed proof as correct (which teaches the verifier to accept incorrect reasoning).

The significance of this innovation extends beyond the paper's specific results. It demonstrates that test-time compute scaling—generating many samples and aggregating them through voting or verification—can serve not just to improve inference-time outputs (as in the reference paper and Section 3.3.3) but to generate training data that unlocks further capability improvements. This closes the loop between inference-time and training-time compute in a way that prior work on self-improvement (e.g., STaR, ReST^EM) attempted but struggled with due to reward signal reliability. The paper reports that in the final two training iterations, the automated pipeline "replaced human annotation entirely" with labels that "aligned well with expert judgments," though quantitative alignment metrics are not provided.

This is an incremental advance on the specific mechanism (majority voting across model samples is well-established) but a fundamental advance in the use of that mechanism: repurposing it from answer selection to training data generation in a domain where ground-truth labels are otherwise prohibitively expensive. It establishes that automated labeling can be reliable enough to sustain a self-improvement loop for theorem proving, which opens the door to scaling such loops beyond the point where human annotation remains feasible.

Innovation 4: Reframing Theorem Proving as a Self-Verifiable Task Within the RL-for-Reasoning Paradigm

The paper's most conceptually ambitious contribution is its reframing of theorem proving from a generation problem (produce a correct proof) to a joint generation-and-verification problem (produce a proof and verify that it is correct, with the verification being part of the model's output). This reframes what it means for a model to "solve" a theorem-proving problem: success is not just producing a valid proof, but producing a proof along with a credible self-assessment that confirms its validity.

This reframing matters because it changes the nature of the training signal. In standard RL-for-reasoning with final-answer rewards (Guo et al., 2025), the model receives a scalar reward based on correctness and must discover through exploration what constitutes good reasoning. The reward is sparse and the credit assignment problem is difficult—the model doesn't know which steps in a long chain of reasoning contributed to the correct or incorrect outcome. In the self-verification framework, the model receives a structured reward (Equation 5) that separately evaluates the proof and the self-assessment, with the self-assessment providing dense feedback on whether the model correctly identified issues in its own reasoning. This transforms credit assignment from an implicit optimization problem into an explicit task: the model must not only produce correct reasoning but also articulate why it believes the reasoning is correct (or flawed).

This is a fundamental conceptual shift, not an incremental improvement. It changes the role of the verifier from an external critic (used only at training time to compute rewards) to a capability that the generator must internalize and demonstrate. The paper's architecture—training the verifier first, then initializing the generator from the verifier checkpoint, then training with the composite self-verification reward—operationalizes this reframing as a concrete training pipeline. The generator is not just learning to produce proofs that happen to be correct; it is learning to be a system that can both produce and evaluate proofs, with the evaluation capability being demonstrable in its outputs.

The evidence for this reframing's effectiveness is in the self-verification results (Section 3.3.2, Figure 2): on IMO Shortlist 2024 problems, sequential refinement guided by self-verification improves Pass@1 from 0.15 to 0.27 across 8 iterations, and Best@32 (selecting the best proof per problem based on self-assigned scores) reaches 0.42—substantially higher than the thread average. The fact that self-assigned scores can be used to select the best proof across independent refinement threads demonstrates that the self-verification capability is genuine: the model can reliably distinguish higher-quality from lower-quality proofs among its own outputs, not just produce plausible-sounding self-assessments.

This reframing has implications beyond theorem proving. It suggests a general principle for training LLMs on tasks where ground-truth verification is difficult: rather than attempting to build an external verifier that remains reliable as the generator improves (the approach of the reference paper), train the generator to internalize verification as an explicit, rewarded behavior. This turns the generation-verification gap from a problem to be managed into a capability to be developed. Whether this approach generalizes to domains without the clear logical structure of mathematical proofs (where "issues" are well-defined and meta-verification has objective criteria) remains an open question, but the paper establishes the principle and demonstrates its feasibility in a demanding domain.

5. Experimental Analysis

Evaluation Methodology

• Dataset. The paper uses multiple evaluation benchmarks, all consisting of theorem-proving problems requiring natural-language proofs rather than numerical answers. The primary in-house dataset contains 91 "CNML-level" problems spanning algebra (13), geometry (24), number theory (19), combinatorics (24), and inequality (11), described as "comparable in difficulty to problems from Chinese National High School Mathematics League (CNML)." Competition benchmarks include IMO 2025 (6 problems), CMO 2024 (6 problems), Putnam 2024 (12 problems), ISL 2024 (IMO Shortlist, 31 problems), and IMO-ProofBench (60 problems, developed by the DeepMind team behind DeepThink IMO-Gold, split into a basic set of 30 pre-IMO to IMO-Medium problems and an advanced set of 30 challenging IMO-level problems; Luong et al., 2025). Training data for RL comes from a separate set of 17,503 problems crawled from AoPS contest collections (prioritizing "math olympiads, team selection tests, and post-2010 problems explicitly requiring proofs"), denoted D_p, which is distinct from all evaluation benchmarks.

• Base model(s). All models are built on DeepSeek-V3.2-Exp-Base (DeepSeek-AI, 2025). The verifier is initialized from "a version of DeepSeek-V3.2-Exp-SFT which was supervised fine-tuned on reasoning data related to mathematics and code." The generator is initialized from the verifier checkpoint in the first iteration, and from a consolidated checkpoint (verification + generation capabilities from the previous iteration, combined through rejection fine-tuning) in subsequent iterations. For cold-start proof generation (creating initial training data D_v), the paper uses "a variant of DeepSeek-V3.2-Exp-Thinking" prompted to iteratively refine proofs. The choice of a single model family throughout means all results are specific to the DeepSeek-V3.2 architecture and training recipe.

• Metrics. The primary metrics are proof scores on the {0, 0.5, 1} scale as defined by the evaluation rubrics I_v (Appendix A.2). For one-shot generation on CNML-level problems (Figure 1), correctness is "measured by majority voting across 8 verification analyses produced by our final verifier," with the mean proof score reported per category. For sequential refinement (Figure 2, Section 3.3.2), two metrics are reported: Pass@1 — "the average score of the final proof from each thread" (averaged across 32 independent refinement threads per problem), and Best@32 — "the score of the best proof per problem, selected by self-assigned scores across all threads." For competition results (Table 1, Figure 3), expert human evaluators assess proof correctness following the IMO-ProofBench grading guidelines (Luong et al., 2025), with problems classified as "fully solved" (score 1), receiving "partial credit" (score 0.5, explicitly noted as underlined in Table 1), or unsolved. Points in Table 1 are percentages of maximum possible score.

• Baselines. The paper compares against several frontier models on the CNML-level problems (Figure 1): Gemini 2.5-Pro (DeepMind, 2025) and GPT-5-Thinking-High (OpenAI, 2025). On IMO-ProofBench (Figure 3), results are sourced from Luong et al. (2025) and include: Claude Sonnet 4, DeepSeek R1 (Guo et al., 2025), Qwen3-235B, Grok 4, Gemini 2.5 Pro, Gemini 2.5 Pro with (Huang & Yang, 2025) (a prompting-based self-verification approach), Gemini Deep Think (IMO lite), and Gemini Deep Think (IMO Gold) (Luong and Lockhart, 2025). All baselines except DeepSeekMath-V2 were evaluated by the DeepMind team (Luong et al., 2025); DeepSeekMath-V2's IMO-ProofBench results were evaluated by the paper's own experts "following the grading guidelines." This creates a potential confounding factor: different evaluation teams may apply grading standards differently, though both use the same published rubric.

• Generation budget / compute accounting. The paper uses several distinct compute measures across experiments. For one-shot generation (Figure 1), each model generates 8 proof samples per problem. For sequential refinement (Figure 2), each problem launches "32 independent refinement threads," with each thread performing up to 8 sequential iterations (one initial generation + up to 7 refinements). For high-compute search (Section 3.3.3, Table 1), the system initializes a candidate pool with 64 proof samples, generates 64 verification analyses per proof, selects the 64 highest-scoring proofs per iteration, pairs each with 8 randomly selected analyses, generates one refined proof per pair, and iterates up to 16 times. This represents a massive compute budget: in each iteration, up to 64 × 8 = 512 refined proofs are generated, each requiring a full LLM forward pass, plus 64 × 64 = 4,096 verification analyses in the initial pool. The paper does not report total FLOPs or wall-clock time for these experiments. Critically, the automated labeling pipeline (Section 2.3) incurs additional compute for generating n verification analyses and m meta-verification assessments per proof, but these costs are not quantified or amortized in any reported efficiency metric.

• Cross-validation / statistical protocol. The paper does not report any cross-validation, statistical significance testing, confidence intervals, or error bars for any result. The IMO-ProofBench evaluation (Figure 3) uses expert human evaluation from two different teams (DeepMind's for baselines, the paper's own for DeepSeekMath-V2), but no inter-rater reliability metrics are reported. The automated labeling pipeline's quality is described as "align[ing] well with expert judgments" without quantitative alignment metrics. The CNML-level results (Figure 1) report means without variance. The sequential refinement results (Figure 2) show scores across iterations without confidence intervals. This absence of statistical rigor is a significant limitation: with test sets as small as 6 problems (IMO 2025, CMO 2024), single-problem differences can swing pass@1 or solve rates substantially, and without uncertainty quantification it is impossible to determine whether differences between models or between configurations are statistically reliable.

Main Quantitative Results

4.1 One-Shot Proof Generation on CNML-Level Problems

Figure 1 presents the core comparison of one-shot proof generation capabilities across three models on the 91-problem CNML-level dataset, with proofs scored by the paper's final verifier using majority voting across 8 verification analyses. The headline result is that DeepSeekMath-V2 achieves higher mean proof scores than both GPT-5-Thinking-High and Gemini 2.5-Pro across all five mathematical categories.

Per-category breakdown (Figure 1):

• Algebra: DeepSeekMath-V2 achieves approximately 0.60, compared to GPT-5-Thinking-High at roughly 0.35 and Gemini 2.5-Pro at roughly 0.54.
• Geometry: DeepSeekMath-V2 scores approximately 0.52, versus roughly 0.17 for GPT-5-Thinking-High and 0.15 for Gemini 2.5-Pro. This is the largest absolute gap among all categories.
• Number Theory: DeepSeekMath-V2 achieves approximately 0.54, compared to roughly 0.32 for GPT-5-Thinking-High and 0.36 for Gemini 2.5-Pro.
• Combinatorics: DeepSeekMath-V2 scores approximately 0.47, versus roughly 0.32 for GPT-5-Thinking-High and 0.35 for Gemini 2.5-Pro.
• Inequality: DeepSeekMath-V2 achieves approximately 0.59, compared to roughly 0.45 for GPT-5-Thinking-High and 0.38 for Gemini 2.5-Pro.

The paper does not provide exact numerical values; all figures above are approximate readings from the bar chart in Figure 1. DeepSeekMath-V2's advantage is largest in Geometry (where the baselines perform poorly) and smallest in Inequality (where baselines are stronger, particularly GPT-5-Thinking-High at ~0.45). GPT-5-Thinking-High outperforms Gemini 2.5-Pro in 3 of 5 categories (Algebra, Inequality, Geometry) but lags in Number Theory and Combinatorics.

Important caveat: These scores are produced by the paper's own verifier, not by independent human evaluation. While the verifier was trained to align with expert annotations, this introduces a potential self-assessment bias—the verifier may be calibrated to the paper's model's output style, potentially inflating its scores relative to baselines with different proof-writing conventions. The paper does not report human evaluation on this benchmark to validate the verifier-based scoring.

4.2 Sequential Refinement with Self-Verification on IMO Shortlist 2024

Figure 2 demonstrates the effect of increasing the maximum number of sequential refinement iterations (from 1, meaning no refinement, to 8, meaning initial generation plus up to 7 refinements) on the 31 problems of IMO Shortlist 2024. For each problem, 32 independent refinement threads are launched, and proof correctness is measured by majority voting across 32 verification analyses from the final verifier.

Pass@1 trajectory (Figure 2):

• Iteration 1 (no refinement): Pass@1 ≈ 0.15
• Iteration 2: Pass@1 ≈ 0.18
• Iteration 3: Pass@1 ≈ 0.21
• Iteration 4: Pass@1 ≈ 0.22
• Iteration 5: Pass@1 ≈ 0.24
• Iteration 6: Pass@1 ≈ 0.24 (first plateau)
• Iteration 7: Pass@1 ≈ 0.26
• Iteration 8: Pass@1 ≈ 0.27

The improvement from iteration 1 to 8 is approximately 0.12 in absolute terms (from 0.15 to 0.27), representing an 80% relative improvement over single-shot generation. The trajectory shows diminishing returns: the largest jumps occur in early iterations (0.15 → 0.18 → 0.21), with smaller gains (0.01–0.02 per iteration) in later iterations. The curve flattens between iterations 5 and 6 (both at ~0.24), then resumes slow improvement.

Best@32 trajectory (Figure 2):

• Iteration 1: Best@32 ≈ 0.26
• Iteration 2: Best@32 ≈ 0.29
• Iteration 3: Best@32 ≈ 0.33
• Iteration 4: Best@32 ≈ 0.39
• Iteration 5: Best@32 ≈ 0.39
• Iteration 6: Best@32 ≈ 0.40
• Iteration 7: Best@32 ≈ 0.40
• Iteration 8: Best@32 ≈ 0.42

Best@32 shows more improvement than Pass@1 (0.26 → 0.42, a 62% relative improvement), but also plateaus earlier—performance levels off around iterations 4–5 and shows minimal gains thereafter. The gap between Best@32 and Pass@1 grows from 0.11 at iteration 1 to 0.15 at iteration 8, indicating that as refinement proceeds, there is increasing variance in thread quality, and the best thread per problem pulls further ahead of the average thread.

Key insight from the gap between Pass@1 and Best@32: The fact that Best@32 (selected by self-assigned scores) substantially outperforms Pass@1 (the thread average) demonstrates that the generator's self-assessment is informative—it can reliably distinguish higher-quality from lower-quality proofs among its own outputs. If self-assigned scores were random or uninformative, Best@32 would converge to the maximum of 32 random draws, which would be only modestly higher than the mean. The observed gap (0.27 vs. 0.42 at iteration 8) indicates genuine self-evaluation capability.

Caveat: As with Figure 1, these scores are produced by the paper's own verifier, not by independent human evaluation. The verifier may share biases with the generator (since both derive from the same base model and training pipeline), potentially inflating apparent improvement if the verifier favors the generator's refinement style even when logical quality is unchanged.

4.3 High-Compute Search on Competition Problems

Table 1 reports results from the scaled test-time compute approach (Section 3.3.3) on three premier competitions. The approach maintains a candidate proof pool with 64 proofs, 64 verifications per proof, selecting 64 highest-scoring proofs each iteration, pairing each with 8 randomly selected analyses prioritizing those identifying issues, and iterating up to 16 times or until proofs pass all 64 verifications.

IMO 2025 (6 problems, gold medal threshold: approximately 83% based on historical cutoffs):

• DeepSeekMath-V2 achieved 83.3% of maximum points.
• Problems P1, P2, P3, P4, P5 are marked as "fully solved" (gray in Table 1).
• No problem is listed as receiving partial credit (underlined).
• This implies P6 was not solved (receiving score 0 on that problem).
• The paper states this achieves "gold medal performance," consistent with the 83.3% score.

CMO 2024 (6 problems):

• DeepSeekMath-V2 achieved 73.8% of maximum points.
• Problems P1, P2, P4, P5, P6 are marked as "fully solved" (gray).
• No problem is explicitly listed as receiving partial credit in the table text, though the table header mentions "underlined problems received partial credit." The absence of underlining on any problem suggests either all listed problems were fully solved (with P3 receiving no credit) or the underlining notation is not visible in the printed table format.
• The paper states this achieves "gold medal performance."

Putnam 2024 (12 problems, maximum 120 points):

• DeepSeekMath-V2 achieved 98.3% of maximum points, corresponding to 118/120.
• Problems A1 through B4 (10 problems) and B5, B6 (2 problems) are all listed as "fully solved" (gray) in Table 1, totaling 12 problems marked gray. However, the text states "solved 11 of 12 problems completely and the remaining problem with minor errors." This discrepancy suggests one of the gray-marked problems actually received partial credit—likely one of B5 or B6, where minor errors were present—and the table notation may be imprecise.
• The highest human score on Putnam 2024 was 90 (source: Putnam archive statistics, cited in the paper's introduction footnote). DeepSeekMath-V2's 118/120 substantially exceeds this.

Key qualitative observation: The paper reports that "for problems not fully solved, our generator typically identifies the genuine issues in its proofs, while fully solved problems pass all 64 verification attempts." This is a crucial validation of the verifier's reliability: passing all 64 independent verification attempts is a stringent test (any single verifier instance identifying a real issue would flag the proof as potentially flawed), and the correlation between passing this test and expert-confirmed correctness suggests the verifier has high precision. However, the converse—whether the verifier has high recall (identifying issues in all genuinely flawed proofs)—is not directly tested, since the "not fully solved" category includes only problems where the model acknowledged issues, not problems where the verifier missed flaws that experts later found.

4.4 IMO-ProofBench Comparison

Figure 3 presents expert evaluation results on the IMO-ProofBench benchmark (Luong et al., 2025), comparing DeepSeekMath-V2 against baselines from the original benchmark paper plus Gemini 2.5 Pro with a prompting-based self-verification approach (Huang and Yang, 2025).

Basic set (30 problems, pre-IMO to IMO-Medium difficulty):

• DeepSeekMath-V2 (Heavy): 99.0% (highest among all reported systems)
• Gemini Deep Think (IMO Gold): 89.0%
• Gemini Deep Think (IMO lite): 83.8%
• Gemini 2.5 Pro with (Huang & Yang, 2025): 69.5%
• GPT-5: 59.0%
• Gemini 2.5 Pro: 55.2%
• Grok 4: 46.7%
• Qwen3-235B: 33.3%
• DeepSeek R1: 29.0%
• Claude Sonnet 4: 27.1%

DeepSeekMath-V2 outperforms Gemini Deep Think (IMO Gold) by 10 percentage points on the basic set, and more than doubles the performance of the strongest non-DeepThink baselines.

Advanced set (30 challenging problems, up to IMO-Hard level):

• Gemini Deep Think (IMO Gold): 65.7%
• DeepSeekMath-V2 (Heavy): 61.9%
• Gemini Deep Think (IMO lite): 37.6%
• Gemini 2.5 Pro with (Huang & Yang, 2025): 24.8%
• GPT-5: 20.0%
• Gemini 2.5 Pro: 18.6%
• Grok 4: 17.6%
• Qwen3-235B: 5.2%
• DeepSeek R1: 3.8%
• Claude Sonnet 4: 4.8%

On the advanced set, DeepSeekMath-V2 (61.9%) trails Gemini Deep Think (IMO Gold) (65.7%) by approximately 3.8 percentage points. The paper acknowledges this, stating "the hardest IMO-level problems remain challenging for our model." The gap is relatively small (roughly 1–2 problems out of 30), but the direction is notable: DeepMind's proprietary system, which the paper cites as an "existence proof" for LLM-based verification, maintains an edge on the hardest problems.

The performance cliff between basic and advanced: All models show substantial degradation from basic to advanced, but the magnitude varies. DeepSeekMath-V2 drops from 99.0% to 61.9% (37.1 percentage point decline); Gemini Deep Think (IMO Gold) drops from 89.0% to 65.7% (23.3 percentage point decline); Gemini 2.5 Pro drops from 55.2% to 18.6% (36.6 percentage point decline). The smaller relative decline for Gemini Deep Think (IMO Gold) on harder problems suggests it may have specific architectural or training advantages for difficult IMO-level reasoning that DeepSeekMath-V2 does not fully replicate.

Caveats on Figure 3 comparisons:

• All non-DeepSeek results are sourced from Luong et al. (2025) and were evaluated by the DeepMind team. DeepSeekMath-V2 was evaluated by the paper's own experts "following the grading guidelines." Different evaluation teams may apply grading standards differently—particularly for partial-credit judgments on 0.5-score proofs—which could introduce systematic bias in either direction.
• The "(Heavy)" designation for DeepSeekMath-V2 indicates the high-compute search configuration from Section 3.3.3, not the one-shot or sequential refinement configurations. The compute budgets for other models' results are not specified in the original benchmark paper (some may use single-shot generation, others may use search), making the comparison potentially unequal in terms of inference compute.
• The specific problems in IMO-ProofBench are public (part of the benchmark release), raising the possibility that training data contamination could advantage models trained on similar problems. The paper does not discuss data contamination analysis for these benchmarks.

Ablation Studies and Robustness Checks

The paper contains minimal formal ablation studies. Most design choices are justified through the progressive construction of the system rather than through controlled removal of components and measurement of the impact. The following represent the closest the paper comes to ablations:

Meta-verification impact on verifier faithfulness (Section 2.1.2): The paper reports that meta-verification training improved the verifier's average quality score (as evaluated by the meta-verifier on a validation split of D_v) from 0.85 to 0.96, "while maintaining the same accuracy in proof score prediction." This is the paper's only quantitative ablation-like result: it compares the verifier before and after meta-verification enhancement, using the meta-verifier as an independent evaluator. However, this is not a pure ablation because (a) the meta-verifier is itself a trained model that may share biases with the enhanced verifier (both derive from the same base model and training pipeline), and (b) the improved score could reflect the meta-verifier's preferences rather than genuine faithfulness improvement. An ideal ablation would include human evaluation of verifier faithfulness before and after meta-verification, or evaluation by a completely independent verifier trained without meta-verification influence.

Self-verification contribution to refinement (implicit in Figure 2): The sequential refinement results (Figure 2) implicitly demonstrate the value of self-verification, since the refinement process relies on the generator's self-analysis to identify issues and guide improvement. However, there is no ablation comparing refinement guided by self-verification versus refinement guided by external verification (using the dedicated verifier to identify issues and then prompting the generator to fix them). Without this comparison, it is unclear how much of the improvement in Figure 2 comes from self-verification specifically versus from iterative refinement in general, regardless of the feedback source.

Automated labeling vs. human annotation (Section 2.3): The paper reports that in the final two training iterations, automated labeling "replaced human annotation entirely" and that "quality checks confirmed that the automated labels aligned well with expert judgments." However, no quantitative alignment metrics are provided (e.g., correlation coefficient, exact match rate, confusion matrix). There is no ablation training a verifier using only automated labels versus only human labels to measure the impact on downstream performance. This makes it impossible to assess whether the automated pipeline introduced any systematic labeling errors that might have affected the final model's capabilities.

Choice of n, m, k in automated labeling (Section 2.3): The paper does not specify the values of n (number of verification analyses per proof), m (number of meta-verification assessments per analysis), or k (threshold for accepting a score) used in the automated labeling pipeline. It does not ablate these hyperparameters to show sensitivity. Without this information, the automated labeling procedure is not reproducible, and it is impossible to assess whether the results are robust to these choices or depend on specific, potentially overtuned values.

Sequential refinement depth (Figure 2): The sweep over maximum sequential iterations (1 through 8) in Figure 2 serves as an ablation of refinement depth. The key finding is that performance continues to improve through 8 iterations, but with diminishing returns—the curve flattens and shows signs of plateauing. The paper does not extend the sweep beyond 8 iterations, so it is unknown whether further refinement would produce additional gains or whether performance has genuinely saturated. The 128K token limit is cited as a practical constraint for single-generation proofs, but sequential refinement bypasses this by using multiple inference calls, so the token limit does not explain the choice of stopping at 8 iterations.

Choice of α = 0.76 and β = 0.24 in self-verification reward (Section 2.2.2): The paper states these values without derivation or ablation. No alternative weightings are tested (e.g., α = 0.5, β = 0.5; α = 0.9, β = 0.1). Without an ablation, it is impossible to know whether the 3:1 ratio is near-optimal, whether self-verification behavior is robust to the specific weighting, or whether the generator would develop self-verification capabilities under a wider range of weightings.

Missing ablations that would have strengthened the paper:

• Verifier-only vs. self-verification at inference time: Compare test-time refinement guided by the dedicated verifier's analyses versus the generator's self-analyses. This would isolate the contribution of self-verification from the contribution of iterative refinement.
• Generator initialization ablation: Train a generator from the SFT base without inheriting the verifier checkpoint, to measure how much of the final performance depends on this initialization choice versus the RL training itself.
• Meta-verification removal: Train the full system without the R_meta term in Equation 3 and without the meta-verifier, to measure the impact on verifier faithfulness and downstream generator performance.
• Scaling curves for n and m in automated labeling: Show how label quality varies with the number of verification and meta-verification samples, to determine whether the automated pipeline's reliability comes from the specific hyperparameters chosen or scales predictably with compute.
• Cross-model verifier generalization: Evaluate the paper's verifier on proofs generated by GPT-5 or Gemini 2.5 Pro, and evaluate those models' outputs using their own self-evaluation, to test whether the verifier's calibration is specific to DeepSeekMath-V2's proof distribution.

Critical Assessment

The paper makes three central claims that require experimental validation: (1) that the trained verifier accurately and faithfully evaluates mathematical proofs, (2) that self-verification training enables the generator to honestly assess and iteratively improve its own proofs, and (3) that the combined system achieves state-of-the-art theorem-proving performance on competition benchmarks. The experiments provide evidence for each claim, but with important gaps between what was demonstrated and what was claimed.

Claim 1: The verifier is accurate and faithful. The evidence for accuracy is primarily indirect: the verifier's scores are used throughout the system (Figures 1, 2; automated labeling pipeline), and the final model achieves high human-evaluated scores on competitions (Table 1, Figure 3). However, the verifier's accuracy is never directly benchmarked against human judgments on a held-out test set of proofs with known correctness—the standard evaluation for verifier models (as in, e.g., Lightman et al., 2023 for process reward models). The evidence for faithfulness comes from a single before/after comparison using the meta-verifier (0.85 → 0.96) on a validation split of D_v. This is a narrow evaluation: it measures faithfulness only on the distribution of proofs the verifier was trained on, using an evaluator (the meta-verifier) that shares the same base model and training pipeline. There is no independent human evaluation of verifier faithfulness, no cross-model evaluation, and no analysis of whether the faithfulness improvement generalizes to out-of-distribution proofs (e.g., from other model families or harder problems). The automated labeling pipeline's quality check ("aligned well with expert judgments") is asserted without quantification. The paper's strongest evidence for verifier reliability is the correlation reported in Section 3.3.3: problems fully solved pass all 64 verification attempts, while unsolved problems have the generator identifying genuine issues. This is suggestive but anecdotal—it covers only the competition problems, and selection bias is a concern (problems where the verifier incorrectly passes a flawed proof would not be flagged as unsolved, inflating the apparent correlation).

Claim 2: Self-verification enables honest self-assessment and iterative improvement. Figure 2 is the primary evidence. It shows that Pass@1 improves from 0.15 to 0.27 across 8 refinement iterations, and that Best@32 (selected by self-assigned scores) reaches 0.42—substantially higher than Pass@1. This demonstrates that (a) iterative refinement improves proof quality, and (b) self-assigned scores correlate with proof quality (since Best@32 > Pass@1). However, it does not demonstrate that self-verification is necessary for this improvement, or that the self-assessment is faithful rather than merely correlated with quality through some confound (e.g., longer proofs receive both higher self-scores and higher verifier scores regardless of logical content). The missing ablation—comparing self-verification-guided refinement to external-verifier-guided refinement—is critical here. If external verification produces similar or better improvement, then self-verification is a convenience (avoiding the cost of calling an external verifier at each step) rather than a capability breakthrough. If self-verification produces worse improvement than external verification, then the paper's central thesis—that internalizing verification into the generator is valuable—is weakened. The paper also does not evaluate whether the self-assessment component (the ## Self Evaluation section) contains faithful issue identification or merely produces plausible-sounding analysis that happens to correlate with proof quality. A study showing that the specific issues identified in self-analyses match those identified by the external verifier would strengthen the claim substantially.

Claim 3: State-of-the-art theorem-proving performance. The competition results are genuinely impressive: gold medals on IMO 2025 and CMO 2024, 118/120 on Putnam 2024 exceeding the top human score, and 99.0% on IMO-ProofBench Basic. However, several factors complicate the "state-of-the-art" designation:

• Single-run results on tiny test sets. IMO 2025 has 6 problems, CMO 2024 has 6 problems, Putnam 2024 has 12 problems. A single problem solved or missed can swing the score by 8–17 percentage points. Without multiple evaluation runs or confidence intervals, it is impossible to determine whether DeepSeekMath-V2's performance is reliably above baselines or within the range of stochastic variation. This is particularly acute for the comparison with Gemini Deep Think (IMO Gold), which trails by 10 points on the basic set (99.0% vs. 89.0%) but leads by 3.8 points on the advanced set (65.7% vs. 61.9%). On a 30-problem test, a 3.8-point gap corresponds to roughly 1 problem—well within the range of sampling variability or evaluator disagreement.

• Incomparable compute budgets. The IMO-ProofBench results (Figure 3) compare DeepSeekMath-V2 "(Heavy)"—which uses the full high-compute search pipeline (64 proofs, 64 verifications, up to 16 refinement iterations)—against baselines whose inference compute is not specified. If the baselines used single-shot generation (as many LLM evaluations do), the comparison is not between models but between a compute-intensive search system and single-forward-pass models. The paper would need to report total inference FLOPs or wall-clock time for all systems to make a fair comparison.

• The "Heavy" designation signals a scaling approach, not a model capability. The paper's contribution is a training methodology that produces a model capable of self-verification. But the competition results rely on scaling test-time compute (64 parallel proofs, 64 verifications per proof, 16 refinement iterations). This conflates the model's intrinsic capability with the compute budget allocated at inference time. A fairer comparison would include the baselines at matched compute budgets—e.g., Gemini 2.5 Pro with best-of-64 sampling and majority voting. The paper performs no such FLOPs-matched comparison.

• Cross-evaluator reliability. DeepSeekMath-V2's IMO-ProofBench results were evaluated by the paper's own experts, while all baselines were evaluated by the DeepMind team. The paper states the evaluation followed "the grading guidelines" from Luong et al. (2025), but provides no inter-rater reliability metrics between the two evaluation teams. In mathematical proof grading, judgments about whether a proof is "completely rigorous" (score 1) versus "minor errors or omitted details" (score 0.5) can be subjective, and systematic differences in grading strictness could bias results in either direction.

• The Putnam 2024 result. Scoring 118/120 and exceeding the top human score of 90 is the paper's most striking single result. However, the paper's Table 1 lists all 12 problems as gray (fully solved), while the text states "solved 11 of 12 problems completely and the remaining problem with minor errors." This internal inconsistency raises questions about the precision of the result reporting. Additionally, the Putnam competition is taken under timed, closed-book conditions by human participants, while DeepSeekMath-V2 operates with effectively unlimited time and compute. The comparison to human scores is rhetorically powerful but scientifically limited—it demonstrates that an AI system with massive compute can outperform humans who operate under severe constraints, which is a different claim than demonstrating mathematical reasoning capability per se.

What the experiments demonstrate vs. what they do not:

The experiments convincingly demonstrate that the training pipeline produces a model that can generate proofs scored highly by its own verifier (Figures 1, 2) and by human experts on competition problems (Table 1, Figure 3). The iterative refinement results (Figure 2) show that allowing the model to revisit and improve its proofs produces measurable gains, which is a genuine capability advance over single-shot generation.

What the experiments do not demonstrate—and what would substantially strengthen the paper's claims—includes:

• That the verifier's faithfulness improvement from meta-verification (0.85 → 0.96) translates to better downstream generator performance, rather than being an isolated metric on a validation set.
• That self-verification is causally responsible for the refinement improvements in Figure 2, as opposed to iterative prompting with any feedback (even random or oracle-identified issues) producing similar gains.
• That the automated labeling pipeline produces training data of comparable quality to human annotation, as measured by downstream model performance rather than asserted alignment.
• That the model's self-verification capability generalizes to novel problem types or proof styles outside the AoPS contest distribution.
• That the competition results are robust to stochastic variation (multiple runs) and evaluator subjectivity (multiple independent evaluation teams).
• That the model's theorem-proving advantage persists when baselines are allocated comparable test-time compute budgets.

The paper's central thesis—that self-verifiable mathematical reasoning is a feasible and productive research direction—is supported by the existence proof of a working system. But the specific mechanisms claimed as responsible (meta-verification for faithfulness, composite self-verification reward for honest self-assessment, automated labeling for closing the training loop) are supported primarily by the system's overall performance rather than by controlled experiments isolating each mechanism's contribution. This is typical for large-scale systems papers where comprehensive ablations are prohibitively expensive, but it means the paper's scientific claims about why the system works should be treated as plausible hypotheses supported by overall success, rather than as empirically validated mechanisms.

6. Limitations and Trade-offs

6.1 The Hardest Problems Remain Unsolved — No Path to Unbounded Scaling

The paper's most candid limitation appears in Section 3.3.3:

"the hardest IMO-level problems remain challenging for our model"

This is not merely a statement about current performance — it reflects a structural property of the approach. On IMO-ProofBench Advanced, DeepSeekMath-V2 achieves 61.9% versus Gemini Deep Think (IMO Gold)'s 65.7% (Figure 3). On IMO 2025, one problem (P6) was not solved. On CMO 2024, the model achieved 73.8% with an unsolved problem. These are not marginal gaps — they represent problems where the self-verification cycle fails to produce a correct proof despite scaled compute.

The consequence. The paper's central mechanism — iterative refinement guided by self-verification — depends on the generator being able to identify issues in its own proofs. On the hardest problems, two failure modes are possible: (1) the generator produces a fundamentally wrong approach but cannot identify the fatal flaw (missed issues), or (2) the generator identifies an issue but lacks the capability to resolve it within the refinement budget (unresolvable issues). In either case, scaling compute — more verification samples, more refinement iterations — yields diminishing returns or none at all. Figure 2 shows Pass@1 plateauing between iterations 5 and 8 (0.24 → 0.27), suggesting that even on IMO Shortlist problems (which are easier than IMO-Hard), refinement yields marginal gains after a point. The paper provides no evidence that further scaling would break through this plateau, and the architecture provides no mechanism for the model to acquire fundamentally new mathematical insights during inference — it can only refine what it already knows how to approach.

Evidence in the paper. Figure 2 directly shows diminishing returns from sequential refinement on IMO Shortlist 2024: Pass@1 improves from 0.15 to 0.27 across 8 iterations, but the curve flattens substantially after iteration 4. The gap between Best@32 and Pass@1 (0.42 vs. 0.27 at iteration 8) suggests that some threads get "stuck" at suboptimal proofs while others break through — but even the best threads plateau. Table 1 shows specific unsolved problems on IMO 2025 and CMO 2024. Figure 3 shows a 37.1 percentage-point drop from IMO-ProofBench Basic (99.0%) to Advanced (61.9%). The paper does not analyze why the hardest problems fail — no error taxonomy, no breakdown of failure modes (missed issues vs. unresolvable issues vs. incorrect self-assessment), and no measurement of whether increased compute would help.

Mitigation status. The paper acknowledges this limitation explicitly (Section 3.3.3: "the hardest IMO-level problems remain challenging") and treats it as a direction for future work rather than a solvable problem within the current framework. No mitigation is proposed. The automated labeling pipeline (Section 2.3) could, in principle, generate training data from harder problems that would improve the generator's capability ceiling in subsequent training iterations, but the paper does not demonstrate this — the hardest problems in training would face the same verification bottleneck (if the verifier cannot reliably assess proofs for these problems, automated labels will be noisy).

---

6.2 Verifier Evaluation Is Circular — No Independent Ground Truth for Proof Correctness

The paper's entire methodology depends on the verifier being accurate and faithful, yet nearly all evaluation of the verifier comes from within the same system. The CNML-level results (Figure 1) are scored by "majority voting across 8 verification analyses produced by our final verifier." The sequential refinement results (Figure 2) are similarly scored by the paper's verifier. The automated labeling pipeline (Section 2.3) trusts the verifier plus meta-verifier to assign correct labels. The meta-verifier's quality improvement (0.85 → 0.96) is assessed by the meta-verifier itself on a validation split of D_v — not by independent human evaluation.

The consequence. This creates a potential self-consistency trap: the verifier, meta-verifier, and generator all derive from the same base model (DeepSeek-V3.2-Exp-SFT) and are trained on overlapping data distributions (AoPS contest problems). They may share systematic biases — for instance, all three might accept a particular style of hand-wavy reasoning as rigorous, or all three might miss a subtle logical gap that a human expert would catch. If such shared biases exist, they would propagate through the entire system: the verifier would assign high scores to flawed proofs, the meta-verifier would confirm those high scores, the generator would be rewarded for producing those flawed proofs, and the automated labeling pipeline would label them as correct — all without any external corrective signal.

The paper's competition results (Table 1, Figure 3) provide some external validation through human expert evaluation, but only on a tiny set of problems (24 problems across IMO 2025, CMO 2024, and Putnam 2024; 60 problems on IMO-ProofBench). The bulk of the system's training and evaluation — tens of thousands of proofs — relies entirely on internal verification without human cross-check. The automated labeling pipeline's quality check (Section 2.3: "aligned well with expert judgments") is asserted without quantification, so the magnitude of any alignment gap on training data is unknown.

Evidence in the paper. Figure 1 and Figure 2 explicitly state that scores come from the paper's verifier, not from human evaluation. Section 2.3 states automated labels "aligned well with expert judgments" but provides no quantitative metrics. The meta-verification improvement (0.85 → 0.96) is measured by the meta-verifier, which shares the same training pipeline — this is not an independent evaluation. The paper reports no study where the verifier's scores were compared to human expert scores on a held-out test set of proofs spanning the full difficulty range, which would be the standard validation for a verifier model.

Mitigation status. The paper provides partial mitigation through the competition results, where human experts evaluated the final proofs and confirmed high scores (Table 1, Figure 3). This validates the verifier on the specific proofs that survived high-compute search on competition problems, but does not validate the verifier on the much larger set of proofs used during training, nor on proofs the verifier scored as incorrect (where false negatives — marking a correct proof as flawed — would degrade generator training). The IMO-ProofBench evaluation (Figure 3) used the paper's own experts following published grading guidelines, but no inter-rater reliability metrics with the DeepMind team (who evaluated all baselines) are reported. The paper acknowledges none of these circularity concerns explicitly.

---

6.3 Compute Costs Are Massive, Unquantified, and Not Amortized in Any Claim

The paper's headline results depend on inference-time compute budgets that are extraordinary by any standard, yet the paper reports no total FLOPs, no wall-clock time, no dollar cost, and no amortization of compute spent during training (verifier training, meta-verifier training, generator RL, automated labeling). The high-compute search configuration (Section 3.3.3) illustrates the scale: 64 proof samples, 64 verification analyses per proof (4,096 verifier calls just to initialize the pool), selecting 64 proofs per iteration, pairing each with 8 analyses prioritizing those with identified issues, generating 512 refined proofs per iteration, iterating up to 16 times. A conservative estimate: 64 (initial proofs) + 64×64 (initial verifications) + 16 × 512 (refinement generations) + 16 × 512 × 64 (verifications of refined proofs) ≈ 64 + 4,096 + 8,192 + 524,288 ≈ 536,640 LLM forward passes for a single problem in the worst case (full 16 iterations). Each pass generates up to 128K tokens of output. The paper does not report whether early stopping (when proofs pass all 64 verifications) substantially reduces this budget in practice, and if so, by how much.

The consequence. The paper's claims are fundamentally claims about what is possible with effectively unbounded compute, not about what is practical or cost-effective. For the IMO-ProofBench comparison (Figure 3), DeepSeekMath-V2 is designated "(Heavy)" while the baselines' inference budgets are not specified — some may use single-shot generation. This makes the comparison one of system-plus-compute versus model-alone, which conflates two independent variables. A practitioner deciding whether to adopt this approach needs to know: does the $4\times$–$100\times$ inference compute multiplier (relative to single-shot generation) produce proportional accuracy gains, or would a simpler approach (e.g., best-of-64 sampling with majority voting on a strong baseline model) achieve comparable results at lower cost? The paper provides no FLOPs-matched comparisons that would answer this question.

The automated labeling pipeline (Section 2.3) adds another layer of unaccounted compute: for each training proof, generating n verification analyses and m meta-verification assessments. If n = 64 and m = 5 (reasonable guesses based on the test-time settings), labeling a single proof costs 64 + 64×5 = 384 LLM forward passes. Across thousands of training proofs per iteration, this is a massive training-time compute cost that is neither quantified nor factored into any efficiency analysis.

Evidence in the paper. Section 3.3.3 describes the high-compute search pipeline in sufficient detail to estimate the compute budget (as done above), but reports no total FLOPs, wall-clock time, or cost. Section 2.3 describes the automated labeling pipeline conceptually but does not specify n, m, or k, making cost estimation impossible. Section 3.1 mentions GRPO training but provides no information about the number of training steps, batch sizes, or total RL compute. The paper never states total training compute, total inference compute for any experiment, or any efficiency metric (e.g., FLOPs per correctly solved problem).

Mitigation status. The paper does not acknowledge the scale of its compute usage as a limitation, nor does it discuss efficiency, cost, or practical deployability. The word "compute" appears in the paper only in the context of "scaling test-time compute" and "scaling verification compute" — always as a mechanism, never as a cost. This is a significant gap for a paper that presents its results as a practical advance in mathematical AI. Without cost quantification, the results establish an upper bound on what is achievable (an existence proof) but provide no guidance on the cost-effectiveness frontier — which is precisely the question the reference paper addressed through its FLOPs-matched comparisons and efficiency analyses.

---

6.4 Single Model Family, Single Task Domain — No Evidence of Generalization

All experiments use a single base model family (DeepSeek-V3.2-Exp variants) evaluated exclusively on competition mathematics theorem proving — specifically, problems from AoPS contests (training data) and math olympiads/undergraduate competitions (evaluation). The paper does not evaluate on theorem proving outside competition mathematics (e.g., undergraduate textbook proofs, research-level mathematics, formal verification tasks), on non-proof mathematical reasoning (quantitative problems requiring numerical answers), on non-mathematical reasoning requiring self-verification (code verification, legal reasoning, scientific argumentation), or using any model architecture other than DeepSeek-V3.2.

The consequence. Every design choice in the paper — the three-point rubric, the meta-verification criteria, the AoPS problem distribution, the 128K token context window, the specific α/β weighting — was developed and tuned on a single model family and a single task domain. There is no evidence that the approach transfers to other models or other domains. Several components may be particularly sensitive:

• The verifier's calibration depends on the base model's mathematical reasoning capabilities after SFT. A model with weaker mathematical pretraining might produce verifier scores that are less correlated with actual proof correctness.
• The meta-verifier's reliability depends on the verifier's analysis style and failure modes. A different base model might exhibit different hallucination patterns that the meta-verifier (trained on DeepSeek-V3.2 outputs) cannot detect.
• The self-verification reward weighting (α = 0.76, β = 0.24) was presumably tuned for this specific setup. Different models or domains might require substantially different weightings to achieve the same balance between proof quality and self-assessment honesty.
• The automated labeling pipeline relies on majority voting across verifier and meta-verifier samples. If a different base model has different calibration properties (e.g., higher variance in verification outputs, different precision-recall tradeoffs), the thresholds (n, m, k) would need to be re-tuned.

More fundamentally, the paper does not establish why self-verification works — it demonstrates that it works for this specific setup. Is the key ingredient the verifier initialization for the generator? The composite reward structure? The meta-verification feedback? The specific prompting format? Without cross-model or cross-domain experiments, it is impossible to distinguish the essential components from the incidental ones, and practitioners cannot assess whether the approach will work for their use case without replicating the entire pipeline.

Evidence in the paper. All reported results use DeepSeek-V3.2-Exp variants. All training data comes from AoPS contests. All evaluation benchmarks are competition mathematics (CNML-level, IMO, CMO, Putnam, IMO Shortlist, IMO-ProofBench). The paper does not discuss domain transfer, model transfer, or the sensitivity of results to base model choice. The baselines in Figure 1 and Figure 3 are different model families (Gemini, GPT, Claude, Grok, Qwen, DeepSeek R1), but these comparisons are at the final output level — they do not test whether the paper's training methodology would produce similar improvements if applied to those models.

Mitigation status. The paper does not acknowledge this as a limitation. It makes no claims about generalization, but also does not discuss the scope of applicability or caution readers against assuming transferability. The connection to formal verification systems (discussed in Section 4) suggests the authors view natural-language theorem proving as a stepping stone to broader mathematical AI, but the paper provides no evidence that the self-verification methodology would transfer to formal proof generation or other reasoning domains.

---

6.5 Missing Ablations Leave Causal Mechanisms Unverified

The paper presents a complex multi-component system — verifier training, meta-verification, generator RL, self-verification reward, automated labeling — and demonstrates that the final system performs well. However, it provides almost no controlled experiments isolating the contribution of individual components. The only before/after comparison is the meta-verification improvement (0.85 → 0.96 on verifier analysis quality, Section 2.1.2). Every other design choice — the self-verification reward structure (Equations 5–6), the α/β weighting, the generator initialization from the verifier checkpoint, the automated labeling pipeline replacing human annotation, the sequential refinement approach versus alternative test-time strategies — is evaluated only as part of the complete system.

The consequence. The paper's scientific claims about why the system works are hypotheses supported by overall performance, not empirically validated mechanisms. Several claims are particularly vulnerable:

• Claim: Self-verification training causes honest self-assessment. The evidence is that the trained generator produces self-assigned scores that correlate with verifier scores (Best@32 > Pass@1 in Figure 2). But this correlation could arise from simpler mechanisms — e.g., longer or more elaborate proofs might naturally receive both higher self-scores and higher verifier scores, regardless of whether the self-analysis contains genuine issue identification. Without an ablation comparing the self-verification-trained generator to a generator trained without the R_Z term, the causal role of the self-verification reward is unproven.

• Claim: Meta-verification improves verifier faithfulness. The 0.85 → 0.96 improvement is measured by the meta-verifier itself. This is progress, but an independent evaluator (human experts, or a verifier trained on a completely separate data split without meta-verification influence) would be needed to confirm that the improvement is genuine and not an artifact of the meta-verifier's own biases.

• Claim: Automated labeling enables closing the training loop. The paper reports that automated labels "aligned well with expert judgments" but provides no metrics. Without a comparison of models trained with automated labels versus human labels (or a mixture), the impact of any labeling errors on downstream generator performance is unknown.

• Claim: Sequential refinement with self-verification outperforms alternatives. Figure 2 shows improvement across refinement iterations, but there is no comparison to: (a) refinement guided by the external verifier's analyses instead of self-verification, (b) parallel sampling with best-of-N selection using verifier scores, or (c) a hybrid approach (parallel chains with within-chain refinement, analogous to the reference paper's sequential-to-parallel ratio analysis). Without these comparisons, the efficiency of the specific refinement strategy relative to simpler test-time compute allocation strategies is unknown.

Evidence in the paper. As detailed in Section 5's critical assessment, the paper contains no formal ablation study. The meta-verification before/after is the only isolated component comparison. The paper does not discuss why comprehensive ablations were not performed — plausible reasons include computational cost (each training iteration involves RL on large models) and the interconnected nature of the components (the verifier and generator are co-dependent, making isolated ablations difficult). But without at minimum the key ablations listed above, the paper's mechanistic claims should be treated as plausible but unverified.

Mitigation status. The paper does not acknowledge the absence of ablations as a limitation. It does not suggest future work on isolating component contributions. The lack of ablations is a standard weakness of large-scale systems papers where the computational cost of controlled experiments is prohibitive, but it is a weakness nonetheless — particularly for a paper whose primary contribution is a training methodology rather than a single model. A training methodology paper should ideally demonstrate that each step in the methodology is necessary or at least beneficial, not merely that the final product works.

7. Implications and Future Directions

How This Work Changes the Landscape

This paper shifts the conversation around LLM-based mathematical reasoning from a paradigm where models are optimized to produce correct outputs (final answers, passing proofs) to one where models are optimized to know whether their outputs are correct. This is not merely a new capability—it is a fundamentally different objective that, if widely adopted, changes what it means for a model to "solve" a reasoning problem. Under the final-answer RL paradigm (Guo et al., 2025), success is a correct answer. Under the self-verification paradigm, success is a correct answer plus a credible self-assessment confirming its correctness. The paper demonstrates that this second criterion is not a free byproduct of the first—it must be explicitly trained—and that doing so produces measurable improvements in both generation quality and the model's ability to iteratively refine its own outputs.

The magnitude of this shift is best understood as a reframing with methodological consequences, not a paradigm shift in the Kuhnian sense. The core techniques—RL with verifier rewards, iterative refinement, scaling test-time compute—are well-established. What changes is the training objective: the generator is rewarded not just for proof quality but for the accuracy and faithfulness of its self-evaluation (Equations 5–6). This reframing has three specific consequences for the field:

1. Self-evaluation becomes a first-class training target, not an emergent property to hope for. The paper provides direct evidence that a model can possess evaluation capability (inherited from verifier initialization) but fail to apply it to its own outputs. The fix is not better prompting or more capable base models—it is a reward structure that makes honest self-assessment instrumental to achieving high reward. This finding should discourage future work from assuming that models with strong evaluation capabilities will spontaneously self-evaluate, and instead direct effort toward training methodologies that explicitly incentivize self-scrutiny. The paper's specific mechanism—initializing the generator from the verifier checkpoint plus composite reward—provides a concrete template.

2. The generation-verification gap is reframed from a problem to be managed to a capability to be developed. The reference paper on compute-optimal test-time scaling treated the verifier as a fixed external resource and optimized how to allocate compute against it. This paper treats the verifier as something that can be improved through meta-verification, and then internalized into the generator through self-verification training. The automated labeling pipeline (Section 2.3) goes further: it uses scaled verification compute not just to select answers at inference time but to generate training data that improves the verifier. This closes the loop between inference-time compute and training-time capability in a way that had not been systematically demonstrated for theorem proving. Future work on test-time compute scaling should consider not just how to use a verifier efficiently (the reference paper's question) but how to use scaled verification to improve the verifier itself (this paper's contribution).

3. Human annotation bottlenecks become addressable through scaled automated verification. The paper demonstrates that, at least for competition mathematics, automated labeling via majority voting across verifier and meta-verifier samples can replace human annotation entirely in later training iterations (Section 2.3). This is significant because it changes the scaling economics of self-improvement pipelines. Prior approaches to self-improvement (STaR, ReST^EM) were limited by the reliability of automated reward signals—if the reward model makes errors, those errors are amplified through iterative training. The paper's two-stage pipeline (verification → meta-verification) provides a more robust signal by exploiting the fact that meta-verification is easier than verification, and that scaled compute can compensate for individual model errors through majority voting. This is a transferable pattern for any domain where a secondary evaluation task is cognitively simpler than primary evaluation.

What this work reconciles. The paper resolves a tension between two observations that had coexisted uneasily in the literature: (a) frontier models like Gemini 2.5 Pro show some self-verification capability through prompting (Huang and Yang, 2025), but (b) prompted self-correction for reasoning is often unreliable, with models claiming correctness for flawed outputs (a finding echoed across multiple studies, including Huang et al., 2023 on self-correction in reasoning). This paper's diagnosis is that self-verification capability exists in potentia (the model can evaluate proofs when initialized from a verifier checkpoint) but is not reliably deployed on the model's own outputs without explicit training incentives. This explains both the positive prompting results (the capability is real) and the negative ones (the deployment is fragile). The paper's contribution is showing that the deployment gap can be closed through reward design.

Research directions that become more attractive:

• Training evaluator models with explicit faithfulness objectives, not just accuracy objectives. The paper's meta-verification mechanism (Section 2.1.2) and multiplicative reward composition (Equation 3) provide a template that could apply to any domain where evaluator outputs are used as training signals—code review, legal reasoning, scientific peer review.
• Internalizing evaluation into generators through joint training rather than relying on external verifiers at inference time. The paper shows this is feasible and beneficial for theorem proving; the approach could generalize to other reasoning domains.
• Automated training data generation through scaled verification plus meta-verification. The paper's labeling pipeline (Section 2.3) is domain-specific in its rubric design but generic in its structure (generate multiple evaluations → meta-evaluate → majority vote → label).

Research directions that become less attractive:

• Prompting-only approaches to self-verification. The paper demonstrates that even with careful prompt design (Appendix A.1), the generator "tends to claim correctness even when the external verifier easily identify flaws" (Section 2.2.2) without explicit training. Future work should not assume that better prompts alone will solve the self-evaluation problem.
• Training verifiers with score-only supervision without addressing faithfulness. The paper identifies a specific failure mode—hallucinated issues achieving perfect score prediction reward—and shows it degrades verifier trustworthiness. Future verifier training should incorporate some form of faithfulness constraint, whether through meta-verification or alternative mechanisms.
• Treating theorem proving as a pure generation problem solvable by scaling final-answer-style RL. The paper explicitly argues this approach "does not naturally develop the models' ability to verify proof validity" (Section 1) and provides an alternative. Future work on theorem proving should engage with the verification component as a first-class objective.

---

Follow-Up Research This Work Enables

Scaling laws for verification compute vs. labeling reliability. The paper's automated labeling pipeline (Section 2.3) uses majority voting across n verification analyses and m meta-verification assessments per proof to assign labels, but the paper does not specify how n and m were chosen, nor how label quality varies with these parameters. A systematic study could sweep n (number of verification samples) from 1 to 256 and m (number of meta-verification samples) from 1 to 16 on a fixed set of proofs with ground-truth human labels, measuring precision and recall of the automated labels against human judgments at each budget level. This would produce scaling laws analogous to those in the reference paper—showing how label quality improves with verification compute and where diminishing returns set in—and would establish principled guidelines for choosing n, m, and the acceptance threshold k based on the desired label quality. The key question is whether the marginal value of additional verification samples eventually saturates (analogous to the reference paper's finding that best-of-N plateaus at high budgets) and whether meta-verification samples provide more label-quality improvement per FLOP than verification samples.

Cross-model verifier generalization and bias audit. The paper's verifier is trained on proofs from DeepSeek-V3.2 variants and evaluated primarily on proofs from the same model family. A critical follow-up would evaluate the verifier on proofs generated by diverse model families—GPT-5, Gemini 2.5 Pro, Claude, open-source models—across a range of difficulty levels, with human expert scores as ground truth. The specific hypothesis to test is whether the verifier exhibits an in-family bias: assigning systematically higher scores to DeepSeek-family proofs than to equally-correct proofs from other model families, due to shared stylistic conventions, reasoning patterns, or artifacts from the shared SFT base. A strong study would collect ~500 proofs (100 each from five model families) spanning the {0, 0.5, 1} score distribution, have multiple human experts score each proof, then measure the verifier's deviation from human consensus scores as a function of the proof's source model. If bias exists (e.g., DeepSeek proofs scored 0.1 higher on average than human-equivalent non-DeepSeek proofs), it would qualify the paper's CNML-level results (Figure 1, where the verifier scored all models) and the automated labeling pipeline's reliability for training data that may include non-DeepSeek proofs.

Ablation of self-verification reward components with human evaluation. The paper's composite reward (Equations 5–6) combines proof quality (R_Y), self-assessment accuracy (R_score), and meta-verification faithfulness (R_meta), with weights α = 0.76, β = 0.24. A targeted experiment would train three generator variants with identical initialization, data, and training steps, varying only the reward function: (A) R = R_format × R_Y only (no self-verification incentive—standard generator training), (B) R = R_format × (α·R_Y + β·R_score(s', s)) (adds score accuracy but not faithfulness), and (C) the full reward from Equation 5 (adds both score accuracy and faithfulness). All three variants would be evaluated on a held-out set of ~200 competition problems with both verifier-based scoring and human expert evaluation of proof quality and self-analysis faithfulness. This would answer three specific questions: (1) Does self-verification training improve proof quality (R_Y), or only self-assessment quality (R_Z)? (2) Does adding R_meta (faithfulness) provide benefits beyond adding R_score alone (accuracy)? (3) Do verifier-based scores and human judgments agree on the relative ranking of variants A, B, and C? The paper currently provides no evidence that the self-verification reward causally improves proof quality rather than merely producing better-calibrated self-assessments.

Failure mode taxonomy on the hardest problems. The paper reports that "the hardest IMO-level problems remain challenging" (Section 3.3.3) but provides no analysis of why. A systematic study would take the unsolved problems from IMO 2025 (P6), CMO 2024 (the unsolved problem), IMO Shortlist 2024 (the problems with lowest Best@32 scores), and IMO-ProofBench Advanced (the ~38% of problems not solved), and perform a detailed qualitative analysis of the model's behavior on each. For each problem, record: (a) whether the model's initial proof attempt is in a fundamentally wrong direction (categorization error) or contains a correct high-level approach with a specific logical gap (local error), (b) whether the model's self-analysis identifies the error (if any) and whether that identification is faithful (confirmed by human expert review of the analysis), (c) whether the model attempts to fix the identified error during refinement and, if so, whether the fix succeeds, introduces new errors, or is superficially responsive without addressing the core issue, and (d) whether scaling compute—more refinement iterations, more parallel threads—appears to help or whether performance has saturated. The output would be a taxonomy of failure modes (e.g., "incorrect approach + unrecognized," "incorrect approach + recognized but unfixable," "correct approach + unrecognized gap," "correct approach + recognized gap + fix introduces new error") with frequency counts. This would tell us whether the primary bottleneck for hard problems is the generator's proof-finding capability, the self-verification's issue-detection capability, or the refinement's issue-resolution capability—each suggesting a different research priority.

Self-verification for formal proof generation. The paper positions itself as complementary to formal verification (Section 4): "advancing natural language theorem proving will significantly benefit formal reasoning." A concrete follow-up would replace the natural-language verifier in this paper's pipeline with a formal proof checker (Lean or Isabelle) and train the generator to produce both an informal proof sketch and a formal proof, with the self-verification component checking the informal proof against the formal one. Specifically: the generator outputs a natural-language proof and a Lean translation; the verifier checks the Lean proof (guaranteed correct if it compiles); the meta-verifier checks whether the natural-language proof faithfully represents the formal proof; and the generator's self-verification checks whether its own informal-formal pair is consistent. The training reward would reward (a) the Lean proof compiling, (b) the meta-verifier confirming the informal-formal alignment, and (c) the self-assessment accurately predicting both. This would combine the reliability of formal verification with the interpretability and flexibility of natural-language reasoning, and would test whether the self-verification methodology transfers to a setting where one component of verification is perfectly reliable (the formal checker), removing the circularity concern from the current paper's all-LLM verification pipeline.

Difficulty-conditioned test-time compute allocation for theorem proving. The reference paper demonstrated that the optimal test-time compute strategy depends on problem difficulty, with easy problems benefiting from sequential refinement and hard problems requiring parallel exploration. This paper's high-compute search (Section 3.3.3) uses a fixed strategy: 64 parallel threads, 64 verifications per proof, up to 16 refinement iterations. A follow-up could apply the reference paper's difficulty-estimation framework to theorem proving: estimate problem difficulty using the verifier's average score on initial proof attempts, then dynamically allocate compute between parallel exploration (more independent proof threads) and sequential refinement (more iterations per thread) based on the estimated difficulty. The hypothesis is that easy problems (where the model's initial proofs are close to correct) would benefit from deeper sequential refinement, while hard problems (where initial attempts miss the mark) would benefit from broader parallel exploration of different proof strategies. This would quantify whether the 4× efficiency gains the reference paper achieved through adaptive allocation translate to the substantially more expensive theorem-proving setting, and would connect the two papers' contributions into a unified framework for inference-time optimization.

---

Practical Applications and Downstream Use Cases

Automated contest problem grading and feedback. The paper's verifier, trained to score proofs on a {0, 0.5, 1} scale with detailed issue analysis, could serve as an automated grading assistant for mathematics competitions. On the CNML-level problems (Figure 1), the verifier's scores are used as the primary evaluation metric, and the paper reports that the meta-verification-enhanced verifier achieves a quality score of 0.96 (Section 2.1.2). In a deployment setting, competition organizers could use the verifier to provide initial scores and detailed feedback on student proofs, with human graders reviewing only proofs where the verifier's confidence is low or where meta-verification flags potential issues in the verifier's analysis. The specific benefit is throughput: the verifier can process proofs in parallel at LLM inference speeds (~128K tokens per forward pass), compared to human grading which may take 10–30 minutes per proof for olympiad-level problems. The paper's automated labeling pipeline (Section 2.3) provides the template—multiple verification samples plus meta-verification for quality control—which could be adapted to retain human oversight for high-stakes decisions while automating routine grading.

Training data generation for formal proof systems. Systems like DeepSeek-Prover-V2 (Ren et al., 2025) and Seed-Prover (Chen et al., 2025) use informal reasoning to guide formal proof search, but the informal reasoning components in these systems were "not specifically optimized for theorem proving tasks" (Section 4). DeepSeekMath-V2's self-verifying proof generator could serve as the informal reasoning engine for such systems, producing natural-language proof sketches that a formal proof assistant then attempts to formalize. The benefit is a tighter integration: because DeepSeekMath-V2 is specifically trained for rigorous theorem proving with self-verification, its informal proofs are more likely to contain complete logical reasoning that maps cleanly to formal proof steps, reducing the search space for the formal prover. The paper's IMO 2025 and Putnam 2024 results demonstrate that the model can produce proofs that survive extensive verification scrutiny, which is exactly the property needed for effective informal-to-formal translation. A concrete integration would replace the general-purpose LLM in DeepSeek-Prover-V2's pipeline with DeepSeekMath-V2 and measure the formal proof success rate on IMO-ProofBench problems relative to the current system.

Self-improving mathematical assistants for research mathematicians. The paper's iterative training cycle—verifier improves generator, generator produces harder proofs, automated labeling creates training data for verifier improvement (Section 2.3)—could be adapted to create a mathematical assistant that improves over time through interaction with a human mathematician. In this setting, the mathematician poses problems (conjectures, lemmas, proof sketches) and the model generates proofs or counterexamples. The mathematician provides occasional feedback (confirming or rejecting proofs), which serves the same role as expert annotations in D_v and D_mv. Between human interactions, the model uses its self-verification capability to evaluate and refine its own outputs, and the automated labeling pipeline generates training data from its own successful and unsuccessful attempts. The specific benefit over static models is continuous improvement: as the mathematician works on a specific research area, the model's capabilities in that domain improve through iterative training on domain-specific proofs, without requiring the mathematician to label every intermediate attempt. The paper's results on IMO Shortlist 2024 (Figure 2) demonstrate that iterative self-refinement produces measurable improvements (Pass@1 from 0.15 to 0.27), and the automated labeling pipeline (Section 2.3) shows that training data can be generated without human annotation. The key requirement for this application—not demonstrated in the paper—is that the model's self-verification remains reliable on novel, research-level mathematics where the "correctness" of a proof may be ambiguous even to experts. The paper's competition results (Table 1) establish reliability on problems with known solutions; extension to open problems would require additional safeguards.

---

When to Prefer This Method

The paper does not explicitly articulate a tradeoff against named alternatives with specific decision criteria. It positions self-verifiable mathematical reasoning as a research direction rather than as a method to be chosen over competing approaches in specific circumstances. The paper's relationship to alternative approaches is complementary rather than competitive: it frames formal verification systems as benefiting from improved informal reasoning (Section 4), acknowledges that final-answer RL is sufficient for quantitative reasoning but inapplicable to theorem proving (Section 1), and treats prompting-based self-verification as a baseline that the training methodology improves upon (Section 2.2.2). The paper does not provide the kind of head-to-head comparisons or cost-benefit analyses that would support a conditional decision rule (e.g., "prefer self-verification training over standard RL when X, prefer formal verification when Y"). Producing a "Prefer A when... Prefer B when..." matrix would require imposing a structure on the paper's positioning that the authors did not articulate.