PaperlayerView exact revision on arXiv

Source-linked AI summary

An Open Recipe for IMO Gold: Training Nemotron for Olympiad Mathematics

Ivan Moshkov, Stephen Ge, George Armstrong, Wei Du, Sadegh Mahdavi, Igor Gitman

arXiv:2609.10712v1cs.AI

TL;DR

The paper asks how post-training and test-time inference design can improve natural-language proofs for hard olympiad mathematics. It trains specialist Nemotron checkpoints and combines generation, verification, refinement, and high-compute selection in an open pipeline. The system scored 30 out of 42 points at IMO 2026, reaching the gold-medal threshold, while releasing models, data, code, proofs, and a 200-problem benchmark.

  • Problem

    The paper studies how model post-training and test-time inference choices affect natural-language proof generation for hard olympiad mathematics.

  • Method

    The system combines three Nemotron checkpoints for candidate generation, verification-guided refinement, and separate high-compute final selection without formal or external tools.

  • Results

    30 out of 42 points at IMO 2026 reached the gold-medal threshold.

  • Takeaways & Limitations

    The reported gains came from complementary checkpoints, verification-guided refinement, and substantial compute for final evaluation rather than scaling proof generation alone.

  • Takeaways & Limitations

    Model-based evaluations overestimated the official result by two points because both credited proofs on Problems 3 and 6 that official graders scored at one point.

Abstract

from arXiv · show

We study how model post-training and test-time inference design affect natural-language proof generation for hard olympiad mathematics. Starting from Nemotron 3 Ultra, we train two specialist checkpoints using supervised fine-tuning and reinforcement learning, and evaluate checkpoint choice, verification, and refinement. Based on these findings, we present an open-model test-time-compute pipeline. The system operates entirely in natural language, with no formal prover, external tools, or internet access. Three Nemotron 3 Ultra checkpoints - the general-availability model and two post-trained specialists - power an iterative search that generates, verifies, and refines candidate proofs; a separate high-compute stage then selects each final submission. The system scored 30 out of 42 points at IMO 2026, reaching the gold-medal threshold. We release the two post-trained checkpoints as well as the training data, the training and inference code, the submitted solutions, and Nemotron-IMO-Bench, a new benchmark of 200 novel olympiad-level problems.

1. Introduction

The paper studies how post-training and test-time inference choices affect natural-language proof generation for hard olympiad problems. It presents an open, reproducible Nemotron-based system and benchmark for this setting.

  • The work empirically studies checkpoint performance, verification, and multi-model inference for natural-language olympiad proof generation.
  • The system combines specialized proof-generation checkpoints with verification and high-compute inference while using no formal prover, external tools, or internet access.
  • The authors release post-trained checkpoints, training data, training and inference code, and submitted solutions to support reproducibility.
  • Nemotron-IMO-Bench contains 200 novel olympiad-level problems alongside the 30-problem development set.
  • The report includes compute-hour and generated-token accounting for the competition run.

2. Release Artifacts

The release provides the trained models, datasets, code, submitted proofs, and a 200-problem olympiad benchmark. These artifacts are distributed through named Hugging Face collections and public NeMo repositories.

  • Two post-trained checkpoints, Nemotron-3-Ultra-SFT and Nemotron-3-Ultra-RL, are released under the base model’s OpenMDW-1.1 license.
  • The SFT corpus and RL problem set are released under CC BY 4.0.
  • Nemotron-IMO-Bench provides 200 novel olympiad-level problems under CC BY 4.0.
  • The inference pipeline, development-set assembly script, and submitted IMO 2026 proofs are available in NeMo-Skills.
  • The RL training recipe is available in NeMo-RL, while the SFT stage follows the Nemotron-3-Ultra-GA training pipeline.

3. Related Work

Prior IMO systems progressed from neuro-symbolic and formal methods to natural-language proving at gold-medal level. Related work emphasizes verification, refinement, and scaled inference across mathematics and other reasoning domains.

  • AlphaProof and AlphaGeometry 2 combined to score one point below the human gold-medal cutoff at IMO 2024.
  • Gemini Deep Think and an experimental OpenAI model reached gold-medal level at IMO 2025 with natural-language systems.
  • The 2025 results highlighted verification and final-solution selection as important components of natural-language proving.
  • Model-agnostic verification-and-refinement pipelines and post-trained reasoning harnesses also achieved strong olympiad results without relying exclusively on formal proving.
  • DeepSeekMath-V2 and Aletheia scale iterative generation, verification, and revision compute from olympiad problems toward research-level mathematics.

4. Models and Training

The system uses general-availability, supervised-fine-tuned, and reinforcement-learned Nemotron checkpoints for generation, verification, and refinement. Training combines long-context proof data, synthetic refinement and verification trajectories, and asynchronous RL, with RL producing rapid reward and evaluation improvements.

  • 4.1. Models: Three Nemotron-3-Ultra checkpoints serve as pipeline workers: the unchanged GA model plus SFT and RL specialists.
  • 4.1. Models: The checkpoints support three roles: proposing candidate proofs, judging correctness with feedback, and revising candidates.
  • 4.2.1. Supervised Fine-Tuning: The SFT model is trained on proof-focused data with a maximum sequence length of 425,984 tokens using per-token cross-entropy loss.
  • 4.2.1. Supervised Fine-Tuning: Synthetic data generation uses multiple proof attempts, up to three refinement rounds, and verifier or meta-verifier trajectories to supervise construction and evaluation.
  • 4.2.2. Reinforcement Learning: The RL specialist starts from the GA checkpoint and trains on 9,597 selected proof problems with an asynchronous NeMo-RL framework.
  • 4.2.2. Reinforcement Learning: Figure 1 reports rapid improvements in both RL training reward and evaluation-set performance as judged by GPT-5.5.

5. Submitted Pipeline

The submitted system combines multi-checkpoint proof generation, verification-guided refinement, and high-budget finalist selection in an iterative natural-language pipeline. At IMO 2026, it scored 30/42, above the 29-point gold cutoff, while model-based verification overestimated two official results.

  • 5.1. High-Compute Search: The high-compute search uses three Nemotron-3-Ultra checkpoints to generate, verify, critique, and iteratively refine candidate proofs stored in per-problem pools.Search ends after an accepted proof or a fixed round budget, with up to three finalists or the pool’s highest-ranked proof.
  • 5.1. High-Compute Search: Search-time verification assigns correctness scores and actionable critiques, while checkpoint-level early stopping preserves generation from remaining checkpoints after one finds an accepted proof.The process runs independently for each problem for at most eight rounds.
  • 5.2. Final Candidate Selection: The final-selection stage evaluates every finalist with 48 independent IMO-style judgments and submits the highest mean score, breaking ties by shorter proof text.The final prompt targets integer scores from 0 to 7 according to established solution milestones.
  • 5.3. IMO 2026 Results: 30/42 points exceeded the 29-point gold cutoff at IMO 2026, with full credit on Problems 1, 2, 4, and 5 and one point each on Problems 3 and 6.All submitted proofs were graded by official IMO graders.
  • 5.3. IMO 2026 Results: The internal and independent model scores tracked closely, but both estimated roughly 32 points at the cutoff versus the official 30 because Problems 3 and 6 exposed a shared verification blind spot.The discrepancy was attributed to model-based evaluations crediting proofs that official graders awarded only one point.
  • 5.3. IMO 2026 Results: After the cutoff, an additional search found a Problem 6 solution graded 4/7 by independent human mathematicians, raising the unofficial total to 33 points.The post-cutoff search required 610M additional tokens and 890 GPU-hours; the regrade was not an official IMO result.

6. Experimental Setup

The experimental setup uses a 30-problem development set drawn from a new 200-problem benchmark and recent competitions, with single-checkpoint ablations scored by an independent model jury. It defines fixed search, verification, refinement, and jury procedures for comparing pipeline choices.

  • 6.1. Evaluation Dataset: The development set contains 30 problems: 20 from the 200-problem Nemotron-IMO-Bench and 10 from recent competitions.The benchmark problems were newly written and unpublished, so they were absent from evaluated models’ training data.
  • 6.1. Evaluation Dataset: Nemotron-IMO-Bench comprises 200 novel olympiad-level problems, and the authors release it under the CC BY 4.0 license.A script assembles the 30-problem development set from the released benchmark and public competition sources.
  • 6.1. Evaluation Dataset: The development set spans 3 easy, 7 medium, 10 hard, and 10 unsolved problems across algebra, combinatorics, geometry, and number theory.Difficulty is defined by first-round or later-round acceptance behavior, or by the absence of any accepted proof.
  • 6.2. Single-Model Search: Single-model baselines sample 128 initial attempts, verify each proof with up to 64 judgments, and accept only proofs whose remaining judgments all assign score 1.Later rounds generate 128 refinement attempts from 32 prompts based on the global top-32 proof pool, for at most eight rounds.
  • 6.3. Proof Scoring: An independent jury of GPT-5.5, Gemini 3.1 Pro, and Claude Opus 4.8 scores proofs from 0 to 7 using the same IMO-style prompt as final selection.The evaluation is reference-free and uses a reconciliation procedure based on MathArena’s jury protocol.
  • 6.3. Proof Scoring: A problem is counted as solved when the independent jury gives its selected proof full credit, while per-round cumulative scores assign zero to problems without internally accepted proofs.After the final round, unsolved problems use the highest-ranked proof in their final pool.

7. Experiments

Experiments show that post-trained checkpoints and complementary ensemble search improve proof-search performance, while verifier unanimity trades recall for precision and elaborate routing does not improve final aggregate results.

  • 7.1. Single-Checkpoint Pipeline Performance: Both post-trained checkpoints outperform Nemotron-3-Ultra-GA, with SFT strongest initially and RL achieving the best overall single-checkpoint result.The final row evaluates the end-to-end result over all 30 development problems using fallback finalists when necessary.
  • 7.2. Checkpoint Verification Performance: Relaxing unanimity from 16/16 to 14/16 raises false accepts from about 1% to 17%, while adding GA judgments removes only correct proofs.RL and SFT catch each other’s errors, reducing SFT’s false-accept rate from 4.5% to 1.1%.
  • 7.3. Full Ensemble Pipeline: The ensemble reaches its final accepted-only score within three rounds and outperforms every single-checkpoint pipeline.When fallback finalists are included, it finishes eight points ahead of Nemotron-3-Ultra-RL.
  • 7.3. Full Ensemble Pipeline: Spending the same token budget on SFT attempts helps more than doubling RL attempts because SFT reaches problems that RL does not.In the combined pool, five accepted problems are unique to SFT, whereas doubling RL recovers only one of those five.
  • 7.3. Full Ensemble Pipeline: Alternative selection, refinement, and triage strategies changed early search behavior but none improved final aggregate performance.Aggressive triage could discard candidates that later led to correct proofs.

8. Conclusion

The paper presents an open natural-language IMO pipeline that combines multi-checkpoint generation, verification-guided refinement, and high-compute selection. It scored 30 out of 42 points at IMO 2026, reached the gold-medal threshold, and releases the system artifacts and a 200-problem benchmark.

  • The pipeline scored 30 out of 42 points at IMO 2026 and reached the gold-medal threshold without a formal prover, external tools, or internet access.
  • Its practical lesson is that proof-generation scaling alone is insufficient; gains came from complementary checkpoints, verification-guided refinement, and substantial final-evaluation compute.More elaborate routing and refinement changed early behavior without improving final coverage.
  • The authors release checkpoints, training and inference code, submitted proofs, resource accounting, and Nemotron-IMO-Bench with 200 novel olympiad-level problems.

A. Approaches That Did Not Improve the Final System

Several alternative proof-selection and refinement strategies were tested, but none improved the final aggregate result under the experiments’ distinct baselines, pools, and budgets.

  • Alternative selection and refinement variants sometimes improved early progress or solved different problems, but none improved final aggregate performance.
  • These experiments are not comparable across variants or with Section 7 because each used its own baseline run, problem pool, and search budget.Within each experiment, variants shared the same frozen round-1 pool, checkpoint, and budgets.

A.1. Cross-Proof Context and Zero-First Ranking

Cross-proof context and zero-first ranking changed the timing of accepted proofs but did not improve the final result, so the pipeline retained independent contexts and mean-score ranking.

  • A.1. Cross-Proof Context and Zero-First Ranking: The comparison used the same frozen round-1 pool of 51 problems and the same Nemotron-3-Ultra-GA checkpoint for 10 refinement rounds.
  • A.1. Cross-Proof Context and Zero-First Ranking: Neither cross-proof context nor zero-first ranking improved the final result: both variants finished with 44 accepted problems, matching the baseline or falling below it.Cross-proof context reached 42 accepted problems versus 44 for the baseline; zero-first matched 44 by round 9.
  • A.1. Cross-Proof Context and Zero-First Ranking: Cross-proof context made faster early progress but finished with 42 accepted problems, compared with 44 for baseline independent refinement.
  • A.1. Cross-Proof Context and Zero-First Ranking: Zero-first ranking also accelerated early progress but matched the baseline at 44 accepted problems by round 9.It prioritized candidates with fewer zero-valued verifier judgments, using mean score second and self-evaluation as a tie-breaker.

A.2. Refinement from Diverse Proofs

Refining from four diverse proofs changed which problems yielded accepted solutions but did not increase total coverage over single-parent refinement.

  • A.2. Refinement from Diverse Proofs: The experiment compared both methods from the same frozen proof pool on 47 Nemotron-IMO-Bench problems lacking an accepted round-1 proof.
  • A.2. Refinement from Diverse Proofs: Both diverse-proof and single-parent refinement accepted solutions for 22 of 47 problems after one additional refinement round.The methods shared 21 successes, while each uniquely solved one problem.
  • A.2. Refinement from Diverse Proofs: Combining four low-overlap proofs changed problem-level coverage without increasing the total number of accepted problems.The synthesis prompt summarized each proof’s useful and failed steps before requesting one self-contained solution.

A.3. Triage-Based Refinement Routing

Triage routing reduced preliminary verification cost, but its results were not directly comparable in an early run and it discarded many ancestors of correct proofs in a fixed-pool replay.

  • A.3. Triage-Based Refinement Routing: The triage experiment was designed to reduce verification cost by avoiding full-panel ranking for every first-round candidate.
  • A.3. Triage-Based Refinement Routing: Triage reduced routing judgments from 64 to 3 per candidate, a nominal 95.3% reduction, by forwarding only the top 32 candidates.The router obtained three preliminary judgments per candidate before selecting candidates for refinement.
  • A.3. Triage-Based Refinement Routing: An early held-out run accepted proofs for 88.0% of problems with triage versus 94.6% for the standard pipeline, but the runs differed in sampling, prompts, budgets, routing, and acceptance rules.The reported gap therefore cannot be entirely attributed to triage.
  • A.3. Triage-Based Refinement Routing: Triage discarded the eventual standard-pipeline ancestor in 44% of replayed problems, including 13 of 14 cases whose accepted proofs were fully correct.The remaining case involved a problem statement missing assumptions, so the production system did not use triage.

B.3. Proof-Verification Prompt

The IMO-style proof-verification prompt requires a detailed correctness assessment before assigning a discrete score, with explicit treatment of missing justification and unsupported claims.

  • B.3. Proof-Verification Prompt: The prompt assigns scores of 1, 0.5, or 0 according to whether a proof is completely correct, mostly correct with minor issues, or materially incorrect or incomplete.
  • B.3. Proof-Verification Prompt: References receive credit only when the solution also proves the referenced argument, rather than relying on an unsupported citation.
  • B.3. Proof-Verification Prompt: It requires evaluators to analyze key proof steps, explain doubts and errors, and assess each step’s impact on the solution.

B.7. Cross-Proof Context Prompts

The prompts extract reusable lessons from individual proofs, compile cross-proof context, and use it to refine future solutions while preserving diversity and mathematical fidelity. A separate multi-proof workflow analyzes candidates, compares verifier evidence, and synthesizes an improved proof.

  • B.7. Cross-Proof Context Prompts: Cross-proof context extracts attempt-level lessons, compiles problem-level guidance, and supplies that context to later refinement.The workflow preserves promising ideas, gaps, edge cases, unsafe moves, and verifier objections.
  • B.7. Cross-Proof Context Prompts: Attempt analysis records promising directions, reusable components, missing obligations, edge cases, unsafe approaches, and verifier objections.Components are labeled by whether they are proved, partially justified, or merely suggested.
  • B.7. Cross-Proof Context Prompts: The prompts require strict fidelity: unsupported claims remain unproved, disagreements remain visible, and vague advice is replaced by exact mathematical obligations.Previous attempts provide lessons but cannot substitute for proving every claim.
  • B.7. Cross-Proof Context Prompts: Shared lessons list distinct approaches without ranking one route, while compatibility notes describe which local components may support each direction.Future proofs are not required to follow the same strategy.
  • B.7. Cross-Proof Context Prompts: Refinement uses shared lessons selectively, allowing a candidate to continue its direction, borrow a local component, avoid a pitfall, or address an observed edge case.Future solutions must still establish every mathematical claim they use.
  • B.7. Cross-Proof Context Prompts: Candidate refinement uses solution samples and correctness evaluations to repair identified issues, reuse promising ideas, or combine both strategies.Evaluations below score 1 mean the candidate is not treated as complete and correct.
  • B.8. Diverse-Proof Refinement Prompts: Multi-proof refinement compares candidate proofs, verification metadata, verifier feedback, and analyses before synthesizing one improved final solution.It prefers independently supported ideas, repairs gaps when possible, and avoids failed or risky steps unless explicitly fixed.
  • B.8. Diverse-Proof Refinement Prompts: Candidate analysis summarizes each proof’s core idea, successful steps, failed steps, and missing or risky steps without inventing a corrected proof.Conflicting verifier feedback is summarized as disagreement.
Loading 2609.10712v1…