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

AI summary

Overview

• Research area: AI for mathematical reasoning — natural-language proof generation for olympiad mathematics, combining LLM post-training (supervised fine-tuning and reinforcement learning) with large-scale test-time compute.
• Technical level: Advanced. The high-level story is accessible, but the paper reports RL algorithm internals, parallelism configurations, and verifier operating-point statistics.
• Scope: A single paper reporting how checkpoint choice, verification design, and test-time search affect natural-language proof generation, culminating in a system that scored 30/42 at IMO 2026 and an open release of checkpoints, data, code, and a new benchmark.

What This Paper Is About

The paper asks how model post-training and inference-time design affect a model's ability to write natural-language proofs for hard olympiad problems. Starting from the Nemotron 3 Ultra (Nemotron-3-Ultra 550B-A55B) base model, the authors train two specialist checkpoints and build a generate-verify-refine pipeline that uses no formal prover, external tools, or internet access. The goal is both a competitive result at IMO 2026 and a reproducible, openly released recipe for others to build on.

Key Contributions

1. An empirical study of post-training and test-time inference choices, covering single-checkpoint performance, checkpoint verification operating points, and the full multi-checkpoint ensemble.
2. Two open post-trained checkpoints — Nemotron-3-Ultra-SFT (supervised fine-tuning) and Nemotron-3-Ultra-RL (reinforcement learning) — released alongside the training data, training and inference code, and the proofs submitted to IMO 2026.
3. Nemotron-IMO-Bench, a benchmark of 200 novel olympiad-level problems created with Professor Titu Andreescu, plus the 30-problem development set used in the report.
4. Resource accounting for the competition run, including compute hours and generated-token counts per problem and in total.

Main Findings

• Gold-medal result at IMO 2026: The system scored 30 out of 42 points, above the gold-medal cutoff of 29, with all submitted proofs graded by official IMO graders. It received full credit on Problems 1, 2, 4, and 5, and one point each on Problems 3 and 6.
• Fast convergence under contest conditions: All six submitted proofs were found within approximately 707M generated tokens and 1,464 GPU-hours. The four full-credit proofs passed the final-selection panel within the first 76 minutes; the remaining two within 100 minutes. Completing rounds already in flight brought the full run to approximately 2.31B tokens and 4,800 GPU-hours (the table reports 4,784.6 GPU-hours).
• Post-training helps, RL helps most: Both post-trained checkpoints beat Nemotron-3-Ultra-GA on the development set. Nemotron-3-Ultra-SFT leads in round 1 (70 vs 47 for RL and 34 for GA), while Nemotron-3-Ultra-RL achieves the best overall single-checkpoint result (180 with fallback, versus 165 for SFT and 162 for GA).
• The ensemble dominates: With fallback scoring, the ensemble reaches 188 on the 30-problem development set, eight points ahead of Nemotron-3-Ultra-RL, and reaches its accepted-only score of 167 within three rounds.
• Verification selectivity matters more than accuracy: On a 300-proof audit set, Nemotron-3-Ultra-GA (8/8 rule) falsely accepts 31.6% of jury-incorrect proofs, RL 12.4%, and SFT 4.5%. The submitted RL+SFT unanimous 16/16 panel reaches a 1.1% false-accept rate at an 81.3% false-reject rate. Relaxing to 14/16 raises false accepts to 17.0%; relaxing to 12/16 raises them to 25.4%.
• Permissive checkpoints add nothing to the panel: Adding GA's eight judgments to the RL+SFT panel changes the false-accept rate from 1.1% to 1.1% and raises false rejects to 82.9%, removing only two proofs, both correct.
• A shared blind spot in model-based verification: At the contest cutoff, both the search-time verifier and the independent model jury assigned roughly 32 points, two above the official 30. The discrepancy is entirely attributable to Problems 3 and 6, where model-based evaluation credited proofs that received one point from official graders.
• Complementary checkpoints beat more attempts from one: Doubling RL's round-1 attempts from 128 to 256 adds one accepted problem and a few jury points (92 vs 87 accepted-only), while spending comparable tokens on 64 SFT attempts yields 98. Of the 18 problems accepted by the combined RL 128 + SFT 128 pool, six are accepted by both, seven only by RL, and five only by SFT; doubling RL recovers just one of those five.
• Continued search beyond the cutoff: In round 8, after 8 h 25 m of total search time, Problem 6 produced a new solution requiring an additional 610M tokens and 890 GPU-hours. An independent human panel awarded it 4/7 (unofficial, without official marking schemes), which would raise the total to 33 points.
• Elaborate alternatives did not help: Cross-proof context finished with 42 accepted problems versus 44 for baseline, zero-first ranking matched the baseline's 44 by round 9, and diverse-proof refinement accepted 22 of 47 problems for both methods, with 21 shared successes.

Methodology in Plain English

The authors start from a large general-availability model, Nemotron-3-Ultra-GA, and produce two specialists from it.

For the SFT specialist, they assemble a proof-focused corpus from 15,879 challenging problems drawn from the AoPS subset of Nemotron-Math-Proofs-v1. Using DeepSeek-V4-Pro in Max inference mode, they generate multiple initial proof attempts per problem and run up to three refinement rounds on problems not fully solved, conditioning each round on earlier attempts and verifier feedback. They also generate verifier and meta-verifier traces that score proofs in {0, 0.5, 1}. After filtering out incomplete, malformed, or length-capped generations, the corpus contains 414,890 examples over 15,818 unique problems: 58,543 proof-generation traces, 67,971 refinement traces, 236,360 verification traces, and 52,016 meta-verification traces. Training uses a maximum sequence length of 425,984 tokens in BF16, on 512 GB200 GPUs, with a global batch size of 64 and roughly 1.6K optimizer steps. The released checkpoint is the one at step 1300, selected on 133 proof-based problems from IMO-ProofBench and recent competitions.

For the RL specialist, they keep problems from Nemotron-Math-Proofs-v1 that the model solves in one to three of four attempts, as judged by DeepSeek-V3.2-Speciale, giving 9,597 problems. Rewards largely follow DeepSeekMath-V2, with the self-analysis reward removed (alpha = 1, beta = 0). Training uses an asynchronous framework built on NeMo-RL, an algorithm similar to PipeLineRL, dynamic sampling to prevent batch-size shrinkage from zero-advantage samples, truncated importance sampling, and entropy control that masks low-probability tokens in positive samples when entropy exceeds 0.4. Each batch has 128 prompts with 16 trajectories each, for a global batch of 2,048 trajectories, using 128 trainer nodes, 128 inference nodes, and 16 judge nodes of four GB200 GPUs each.

At inference, the submitted system has two stages. The search stage runs up to eight rounds per problem. Round 1 draws 384 attempts — each of the three checkpoints samples 16 attempts from each of eight complementary generation prompts that push different strategies. Verification is reference-free and uses RL and SFT, each producing eight judgments per proof for 16 equally weighted judgments; a proof is accepted only if a full panel of 16 valid judgments is available and all assign a score of 1. If nothing is accepted, the system selects up to 16 top-ranked proofs, builds a refinement prompt per proof with up to eight verifier critiques, sends each prompt to all three checkpoints with four samples each (192 refinement attempts), and verifies the results into the same pool. Early stopping operates at the checkpoint level, so a problem can end with up to three finalists, one per generation checkpoint, or the highest-ranked pooled proof as a sole finalist.

The second stage exists only for ranking. Each finalist is scored by all three checkpoints with an IMO-style judge prompt adapted from Dekoninck et al. (2026) to a reference-free setting, producing an integer score from 0 to 7; 16 judgments per checkpoint give 48 judgments per finalist, and the highest mean wins, with ties broken toward the shorter proof.

For experiments, the authors build a 30-problem development set: 20 problems from Nemotron-IMO-Bench and 10 from recent competitions, spanning 3 easy, 7 medium, 10 hard, and 10 unsolved problems, and covering 6 algebra, 8 combinatorics, 8 geometry, and 8 number-theory problems. Most ablations use single-checkpoint configurations on this set, scored by an independent jury of GPT-5.5, Gemini 3.1 Pro, and Claude Opus 4.8 following MathArena's jury procedure.

Why This Matters

The paper shows that a gold-medal-level olympiad system can be built entirely in natural language, without a formal prover, external tools, or internet access, and that the decisive gains come from complementary post-trained checkpoints, verification-guided refinement that preserves candidates across rounds, and heavy compute on final evaluation rather than from generation volume alone. It also documents a concrete failure mode: at the contest cutoff, both the search-time verifier and an independent model jury over-credited Problems 3 and 6 by about two points relative to official grading, suggesting a shared blind spot in model-based verification rather than noise.

Real-world applications:

• Automated grading and feedback for proof-based coursework, where the paper's verifier and IMO-style judge prompts provide a tested scoring design.
• Scientific and technical writing assistance where arguments must be checked for logical gaps, using the refinement loop that diagnoses and repairs invalid reasoning.
• Benchmark construction for evaluating reasoning systems, following the Nemotron-IMO-Bench model of novel, unpublished problems that avoid training-data contamination.
• High-reliability AI deployment patterns, where the paper's finding that permissive verifiers add little and strict unanimity panels improve precision informs how ensembles of judges should be assembled.

Industry relevance centers on the open release: post-trained checkpoints under the OpenMDW-1.1 license of the base model, training data under CC BY 4.0, and the inference and RL recipes in NeMo-Skills and NeMo-RL. This gives teams a reproducible reference for the system-level trade-offs — verifier thresholds, ensemble composition, and final-selection budgets — that dominate results at high compute.

Future Directions

• Closing the verification blind spot: the paper shows that no unanimity rule over 24 judgments separated the two questionable accepted proofs, so new verification signals are needed beyond repeated judgments of the same checkpoints.
• Improving coverage on the hardest problems: Problem 3 did not improve even in the continued run, and the development set contains 10 unsolved problems, leaving open how to reach them.
• Extending the benchmark and evaluation: the authors note the full 200-problem Nemotron-IMO-Bench was too expensive to run end-to-end with the high-compute pipeline, so cheaper faithful evaluation remains an open problem.
• Determining when elaborate scaffolding pays off: cross-proof context, zero-first ranking, diverse-proof refinement, and triage routing all failed to improve final aggregate performance, raising the question of which refinements could actually add coverage rather than just change early search behavior.

Target Audience

Researchers and engineers working on LLM reasoning, post-training, and inference-time compute for mathematics; benchmark designers interested in uncontaminated olympiad-level evaluation; and practitioners building verification or grading systems where precision of acceptance decisions matters more than raw accuracy. Readers need some familiarity with supervised fine-tuning, reinforcement learning, and test-time search to follow the training and ablation details, though the system-level conclusions are stated plainly enough for a broader technically literate audience.

Authors’ abstract

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.