An Open Recipe for IMO Gold: Training Nemotron for Olympiad Mathematics
Ivan Moshkov, Stephen Ge, George Armstrong, Wei Du, Sadegh Mahdavi, Igor Gitman
cs.AI
2026-09-10
NVIDIA post-trains two Nemotron 3 Ultra specialists into a generate-verify-refine search with no formal prover, scoring 30/42 at IMO 2026, one above gold.
The IMO has become a public exam for model-written proofs. In 2024 AlphaProof plus AlphaGeometry 2, with formal tools, landed near silver. In 2025 Gemini Deep Think and an experimental OpenAI model reached gold in natural language. What was missing was a reproducible open recipe: how to train the checkpoints, how to set verification, and where to spend test-time compute.
NVIDIA starts from Nemotron 3 Ultra (550B-A55B) and keeps the problem narrow: natural-language proofs only, no Lean, no tools, no internet. The point of the report is to separate post-training from inference orchestration, and to publish enough that someone else can rerun it.
Three checkpoints: stock GA, Ultra-SFT from long-context supervised fine-tuning on GA, and Ultra-RL from RL on GA. The SFT mix has 414,890 traces covering generation, refinement, verification, and meta-verification, with a 425,984-token context, 512 GB200 GPUs, and a pick at step 1300. RL uses 9,597 medium-hard problems that the base model solved in one to three of four attempts. The reward follows DeepSeekMath-V2 with the self-analysis term removed.
The contest system has two stages.
Search: all three checkpoints generate. Round 1 draws 384 attempts (each checkpoint times eight strategy prompts times 16 samples). Verification uses only RL and SFT, eight judgments each. A proof is internally accepted only if all 16 scores equal 1. Otherwise the pool yields up to 16 parents, each with up to eight critiques; every checkpoint samples four refinements, 192 per round, for at most eight rounds.
Final selection: at most one finalist per generation checkpoint. All three checkpoints score each finalist 16 times on an IMO-style 0-7 rubric, 48 judgments in total. Rank by the mean; break ties toward the shorter writeup.
Official score: 30/42, gold cutoff 29. Full credit on P1, P2, P4, and P5; one point each on P3 and P6. The four full-credit proofs cleared final selection within 76 minutes; all six submissions were locked within 100 minutes. Those proofs cost about 707M generated tokens and 1,464 GB200 hours. Finishing in-flight rounds took the run to about 2.31B tokens and 4,800 GPU hours.
Search continued after the cutoff. Round 8 produced a new P6 proof that the internal verifier did not accept. Independent human graders, without official marking schemes, gave it 4/7, which would make 33. That is not an official result. P3 did not improve.
On a 30-problem development set, end-to-end independent-jury totals are GA 162, SFT 165, RL 180, ensemble 188. Doubling round-1 RL from 128 to 256 attempts adds one accepted problem. Spending comparable tokens on 64 SFT attempts raises accepts from 13 to 15. RL 128 plus SFT 128 accepts 18 problems; five of those come from SFT only, and doubling RL recovers one of the five.
A 300-proof verifier audit: the submitted unanimous RL+SFT panel has about 1.1% false accepts and 81% false rejects. Relaxing to 14/16 lifts false accepts to 17%. Of 25 internally accepted proofs, the jury gives 23 a 7, one a 6, and one a 0 (a broken symmetry step). Every checkpoint scored both of the last two a perfect 8/8, so no unanimity rule over this panel catches the error.
This is the most complete open natural-language IMO gold recipe so far: checkpoints, data, training and inference code, submitted proofs, a compute bill, and a 200-problem unpublished benchmark. The transferable findings matter more than the medal. Complementary checkpoints beat doubling samples from one model. The search verifier should be strict, because a false accept stops generation. Final ranking needs a separate high-compute judge; the search-time prompt is the wrong instrument.
The cost is on the table. Gold here is thousands of GPU hours, and model judges overscored P3 and P6 by two points versus official graders.
The authors note a shared blind spot: both the search verifier and the independent model jury credited P3 and P6 proofs that official graders scored 1. One fully wrong proof still passed unanimous internal acceptance. The development set has 30 problems; the full 200-problem bench was never run through the high-compute pipeline. Ensemble and single-checkpoint runs are not compute-matched.
Natural language throughout means there is no formal guarantee of correctness. The recipe reproduces the procedure. Reproducing 30 points still needs a similar pile of GB200s.