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

0. Introduction

Paper link

Inference code

Pipeline documentation

Olympiad mathematics에서 strong model 하나를 오래 sampling하면 충분할까. 이 paper의 답은 model checkpoint, prompt, verifier, refinement, final judge를 역할별로 분리해야 한다는 쪽에 가깝다.

NVIDIA team은 Nemotron 3 Ultra에서 두 specialist checkpoint를 만든다.

• Supervised fine-tuning specialist
• Reinforcement learning specialist

그리고 general-availability checkpoint까지 포함한 three-model ensemble을 사용한다. Round 1에서 서로 다른 8 prompts and 3 checkpoints가 diverse proof를 만들고, SFT and RL verifier가 strict unanimity rule로 candidate를 검증한다. Accepted proof가 없으면 high-scoring proof를 critique와 함께 다시 refine한다. 마지막에는 GA, SFT, RL 모두가 IMO-style 0 to 7 score로 finalist를 평가한다.

System은 formal prover, external mathematical tool, internet 없이 natural-language proof만 사용한다. IMO 2026에서 30 out of 42 points를 받아 gold-medal threshold 29를 넘겼다.

한 줄 요약: 이 paper는 Nemotron 3 Ultra의 GA, SFT, RL checkpoints를 complementary proof generators and judges로 사용하고, strict multi-model verification, iterative critique refinement, high-compute final selection을 결합해 natural-language proof system으로 IMO 2026 gold threshold를 달성한 open training and test-time-compute recipe를 제시한다.

이 논문을 지금 볼 가치가 있는 이유는 다음과 같음.

• Olympiad proof performance를 single model score가 아니라 post-training plus inference system design으로 분석한다.
• SFT and RL checkpoint가 서로 다른 역할과 error pattern을 가진다는 evidence를 제공한다.
• Generation, verification, refinement, final judging의 exact prompts and counts를 공개한다.
• Checkpoint, data, training code, inference code, submitted proofs, 200-problem benchmark를 함께 release한다.
• Model-based verifier가 unanimity에도 틀릴 수 있다는 failure까지 공개해 natural-language proof verification의 한계를 보여준다.

1. Problem Setting

1-1. Olympiad proof generation은 final answer RLVR와 다르다

AIME-style short answer는 exact answer verifier를 사용할 수 있다. IMO proof는 reasoning chain 전체가 valid해야 하며, 작은 logical gap 하나가 score를 크게 낮출 수 있다.

Proof candidate $p$의 true quality를 다음처럼 생각할 수 있다.

\[Q(p) = \operatorname{Correctness}(p) + \operatorname{Completeness}(p) + \operatorname{Clarity}(p)\]

하지만 natural-language judge가 관찰하는 score $\hat Q(p)$는 imperfect하다.

• Hidden logical gap을 놓칠 수 있다.
• Elegant but unusual proof를 reject할 수 있다.
• Multiple judges가 같은 model family bias를 공유할 수 있다.
• Long proof에서 local inconsistency를 놓칠 수 있다.

따라서 generation quality뿐 아니라 verifier precision이 system ceiling을 결정한다.

1-2. Single checkpoint의 한계

GA, SFT, RL checkpoint는 same backbone에서 출발하지만 behavior가 다르다.

• GA는 broad prior and general instruction behavior를 유지한다.
• SFT는 curated proof style and structure를 강하게 학습한다.
• RL은 verifier reward에서 높은 score를 얻는 exploration and correction behavior를 강화한다.

한 checkpoint를 더 많이 sampling하면 그 model의 mode and blind spot도 반복된다. Checkpoint diversity는 sample count와 다른 exploration axis다.

1-3. Generate-then-rank의 한계

Round 1 proof만 만들고 final judge로 하나를 고르면 다음 opportunity를 놓친다.

• Verifier critique로 local gap을 수정한다.
• Strong partial proof를 다른 checkpoint가 재작성한다.
• Different prompt style의 insight를 합친다.
• Verification disagreement를 search signal로 사용한다.

Paper는 generation, verification, refinement를 iterative search로 묶는다.

1-4. Formal verification이 없는 system의 risk

이 system은 natural language only라는 장점이 있다. Formalization cost와 Lean toolchain 없이 open model proof search를 실행할 수 있다.

반면 accepted proof는 mathematical guarantee가 아니다. Verifier panel이 unanimously score 1을 주어도 correlated error가 남을 수 있다. 실제 paper도 invalid proof 하나가 모든 checkpoint verifier를 통과한 case를 보고한다.

2. Core Idea

2-1. Three complementary checkpoints

Base architecture는 Nemotron 3 Ultra 550B-A55B다. Total 550B parameters 중 55B가 active한 MoE checkpoint에서 다음 세 model을 사용한다.

1. GA
   • General-availability checkpoint
2. SFT
   • Supervised proof specialist
3. RL
   • Reinforcement learning proof specialist

모든 model이 generation, refinement, final judging에 참여할 수 있지만 search-time verifier panel은 SFT and RL을 사용한다.

2-2. Strict verification panel

Candidate proof $p$를 verifier $v$가 여러 seed로 평가한다. Search stage score는 0, 0.5, 1 중 하나다.

Verifier mean은 다음처럼 쓸 수 있다.

\[S_{\mathrm{verify}}(p) = \frac{1}{J} \sum_{j=1}^{J}s_j(p)\]

하지만 acceptance는 mean threshold가 아니다.

\[\operatorname{Accept}(p) = \mathbb{I} \left[ \forall j,\ s_j(p)=1 \right]\]

SFT and RL이 각각 8 judgments를 생성하므로 candidate당 16 judgments가 모두 1이어야 accepted proof가 된다.

이 rule은 false accept를 줄이지만 correlated verifier failure를 없애지는 못한다.

2-3. Iterative generate-verify-refine

Round 1

• 8 generation prompts
• 3 checkpoints
• Prompt당 checkpoint별 16 samples

\[8\times3\times16 = 384\]

Problem당 384 initial proof attempts를 만든다.

Rounds 2 to 8

Accepted proof가 없으면 verifier mean score로 proof pool을 rank한다. Top 16 proofs에 최대 8 critiques를 붙이고, each checkpoint가 proof당 4 refinement samples를 만든다.

\[16\times3\times4 = 192\]

Refinement round당 최대 192 attempts다.

Final selection

One to three checkpoint finalists를 GA, SFT, RL이 각각 16 times IMO-style 0 to 7 prompt로 평가한다.

\[3\times16 = 48\]

Finalist당 최대 48 judgments의 mean score로 submission을 고른다. Tie에서는 shorter proof를 우선한다.

2-4. Per-checkpoint early stop

Checkpoint가 자기 proof 중 accepted candidate를 만들면 그 checkpoint의 remaining generation and verification을 cancel한다. 다른 checkpoint는 independent하게 계속 탐색한다.

이 방식은 easy problem에서 compute를 줄이고, one checkpoint가 빠르게 solution을 찾았을 때 redundant sampling을 막는다.

3. Architecture / Method

3-1. End-to-end pipeline

Stage	Input	Main operation	Output
Generation	Problem plus one of 8 prompts	GA, SFT, RL sampling	Diverse proof candidates
Verification	Distinct proof	SFT and RL, 8 judgments each	Score, critique, acceptance
Pooling	Complete verifier panel	Deduplicate and rank	Proof pool
Refinement	Top proof plus critiques	Three checkpoints rewrite	New proof candidates
Fallback	No accepted proof after round 8	Highest pool score	Sole finalist
Final selection	One to three finalists	Three checkpoints, 0 to 7 grading	Submitted proof

3-2. Candidate parsing and deduplication

Generation response는 ## Solution and ## Self Evaluation section으로 나뉜다.

• Solution이 없거나 truncated response면 candidate로 사용하지 않는다.
• Identical proof text는 merge하고 한 번만 verify한다.
• Every proof는 content hash and provenance를 가진다.

Deduplication은 verifier cost를 줄이지만 semantic-equivalent proof를 text-level duplicate로 잡지는 못한다.

3-3. Critique-balanced refinement

Proof pool record에는 verifier score and critique가 저장된다. Refinement prompt는 최대 8 critiques를 사용한다.

Mixed score가 있을 때 score value별 critique를 균형 있게 고르고, SFT and RL verifier source도 나눈다. 한 유형의 judge feedback이 prompt를 지배하지 않게 한다.

3-4. Final judge

Search verifier는 valid or flawed를 엄격히 분류하지만, final judge는 IMO-style partial credit를 준다.

• 0 to 7 integer score
• Truncated or unparsable score는 fresh seed로 resample
• Up to 3 retry
• Valid judgment mean으로 finalist rank

Search stage와 selection stage의 objective를 분리한 설계다.

3-5. Resumable infrastructure

Public recipe는 every request를 deterministic identity와 JSONL row로 저장한다.

• Run manifest
• Frozen input
• Prompt hash
• Generation and verification logs
• Proof pool
• Final judgments
• Error rows
• Token budget
• Model and seed provenance

Relaunch하면 missing request만 다시 실행한다. Long high-compute experiment에서 resume and auditability가 중요한 engineering contribution이다.

4. Training / Data / Recipe

4-1. SFT specialist

SFT corpus는 약 15,879 hard AoPS proof problems에서 구성된다. Curated solution and synthetic augmentation을 사용해 natural-language proof style을 학습한다.

Reported SFT setting에는 다음 요소가 포함된다.

• BF16 token-level cross-entropy
• Maximum context about 425,984 tokens
• AdamW
• Learning rate warmup and cosine decay
• Gradient clipping
• Selective recomputation and activation offload

Exact data construction and checkpoint selection step은 final paper appendix에서 다시 확인할 필요가 있다.

4-2. RL specialist

RL problem set은 9,597 problems로 구성된다. Base model이 four attempts 중 1 to 3을 풀 수 있는 intermediate difficulty problem을 중심으로 고른다.

이 data choice는 다음 trade-off를 겨냥한다.

• 0 out of 4 solved problem은 reward가 너무 sparse할 수 있다.
• 4 out of 4 solved problem은 improvement signal이 약하다.
• Mixed success problem은 verifier-relative learning signal이 풍부하다.

RL은 asynchronous NeMo-RL stack을 사용하고, dynamic sampling, truncated importance sampling, low-probability token control을 적용한다.

Reward는 proof correctness judge를 기반으로 하지만 natural-language verifier bias를 그대로 포함할 수 있다.

4-3. Checkpoint diversity가 post-training objective diversity다

SFT and RL을 one final checkpoint로 merge하지 않고 ensemble member로 유지한다. 이 선택은 important하다.

• SFT가 strong initial proof format을 제공한다.
• RL이 difficult proof exploration and correction에 강하다.
• GA가 specialist가 잃을 수 있는 broad prior를 보완한다.

Test-time system은 model averaging 대신 behavioral diversity를 search resource로 사용한다.

4-4. Nemotron-IMO-Bench

Paper는 200 novel olympiad-level problems를 release한다.

Development set은 30 problems다.

• 20 novel benchmark problems
• 10 recent public competition problems

Development split은 fast system ablation에 사용된다. Full 200-problem high-compute experiment는 매우 비싸기 때문에 all configurations를 full scale로 비교하지는 않는다.

4-5. Engineering notes

1) Verifier calibration을 task difficulty별로 봐야 한다

Easy proof and frontier proof에서 false accept rate가 다를 수 있다. Score threshold 하나보다 problem-conditioned calibration이 필요하다.

2) Checkpoint diversity를 correlation으로 측정해야 한다

Accepted proof count만 아니라 model별 success overlap, error overlap, verifier disagreement를 보고해야 ensemble value를 설명할 수 있다.

3) Compute ledger를 role별로 분리해야 한다

• Generation tokens
• Verification tokens
• Refinement tokens
• Final judge tokens
• GPU hours
• Cancelled requests

Strict verification은 proof quality를 높이지만 total compute의 큰 부분을 차지할 수 있다.

4) Proof pool provenance를 유지해야 한다

Refined proof가 어느 parent and critiques에서 나왔는지 dependency graph를 저장해야 insight composition and failure propagation을 분석할 수 있다.

5) Formal checker bridge가 유용하다

Natural-language search를 유지하되 final candidate를 Lean formalization agent or symbolic checker로 보내는 hybrid pipeline이 correctness assurance를 높일 수 있다.

5. Evaluation

5-1. IMO 2026 result

System은 official six problems에서 30 out of 42 points를 받았다. Gold-medal threshold는 29 points였다.

• Full score on Problems 1, 2, 4, 5
• Partial score on Problems 3 and 6
• Total 30 points

Paper는 contest cutoff까지 submitted proofs를 찾는 데 약 707M generated tokens and 1,464 GB200 GPU-hours를 사용했다고 보고한다.

Contest 이후 in-flight search를 계속해 additional Problem 6 proof를 찾았지만 official submission에는 포함되지 않았다. Internal verifier acceptance와 official score가 다를 수 있음을 보여주는 사례다.

5-2. Checkpoint comparison

Single checkpoint analysis에서는 역할이 다르게 나타난다.

• SFT는 round-1 generation에서 strong proof를 빠르게 만든다.
• RL은 multi-round search and refinement에서 strongest single-model result를 보인다.
• GA는 final ensemble에서 marginal but complementary contribution을 제공한다.

Best system은 strongest single checkpoint를 더 많이 sampling하는 것보다 multiple checkpoint를 섞는다.

5-3. Ensemble versus deeper sampling

Development experiment에서 RL sample 수를 두 배로 늘리는 것보다 SFT candidate를 추가하는 편이 더 많은 problems를 solve한다.

Reported example은 다음과 같다.

Candidate pool	Internal score
RL 128 samples	135
RL 256 samples	139
RL 128 plus SFT 64	159
RL 128 plus SFT 128	159

같은 checkpoint의 depth보다 behaviorally different checkpoint의 breadth가 더 큰 gain을 만들 수 있음을 보여준다.

5-4. Eight-round ensemble

Nemotron-IMO-Bench에서 paper의 internal verifier 기준 result는 다음 방향을 보인다.

• SFT and RL specialist가 GA보다 강하다.
• Single round보다 iterative refinement가 좋다.
• Three-checkpoint ensemble plus fallback이 strongest result다.
• Reported best configuration은 200 problems 중 188을 internal pipeline 기준으로 해결한다.

이 score는 official formal correctness가 아니라 model-based verification pipeline outcome이다. Benchmark headline과 mathematical guarantee를 구분해야 한다.

5-5. Verifier precision

Acceptance rule을 16 out of 16에서 14 out of 16으로 완화하면 recall은 늘지만 false accept가 크게 증가한다. Paper는 strict unanimity가 false positive를 줄이는 데 중요하다고 분석한다.

그럼에도 invalid proof 하나가 all checkpoint verifier에게 accepted된다. Multiple samples and multiple checkpoints가 correlated conceptual error를 공유할 수 있기 때문이다.

5-6. Approaches that did not help

Paper는 다음 attempt가 consistent gain을 만들지 못했다고 보고한다.

• Multiple proofs를 한 context에 넣는 cross-proof reasoning
• Alternative final ranking rule
• Multiple parent proof refinement
• Aggressive triage

특히 early triage는 weak-looking candidate 안의 useful insight를 버릴 수 있다. High-compute search에서 candidate pruning은 verifier efficiency and discovery diversity 사이의 trade-off다.

6. Limitations

1. Compute cost가 매우 크다.
   • 550B-A55B model three checkpoints와 repeated verification이 필요하다.
2. Formal proof guarantee가 없다.
   • Natural-language verifier unanimity에도 invalid proof가 통과할 수 있다.
3. Judge correlation이 남는다.
   • GA, SFT, RL은 same base family에서 출발하므로 diverse checkpoint라도 blind spot을 공유할 수 있다.
4. Full benchmark ablation이 제한적이다.
   • High-compute pipeline은 비싸서 many design choices를 200 problems 전체에 반복하기 어렵다.
5. Development set selection bias가 있을 수 있다.
   • Preliminary model difficulty로 split을 구성하면 system tuning과 difficulty distribution이 얽힐 수 있다.
6. Ensemble comparison이 완전히 compute-matched하지 않은 경우가 있다.
   • Sample count, verifier load, refinement opportunity를 함께 맞춰야 diversity gain을 정확히 분리할 수 있다.
7. Natural-language score parser에 의존한다.
   • Boxed score formatting, truncation, retry rule이 acceptance and final ranking에 영향을 준다.
8. Reproduction hardware barrier가 높다.
   • Open artifact가 공개되어도 three 550B checkpoints를 high context로 serving하는 것은 turnkey reproduction이 아니다.

7. My Take

7-1. Why this matters for my work

이 paper의 핵심은 IMO gold headline보다 checkpoint specialization and verifier architecture를 어떻게 test-time search로 묶었는지에 있다.

Reasoning model evaluation에서 pass@K만 늘리는 것은 같은 policy mode를 반복 sampling하는 방식이다. SFT, RL, GA처럼 training history가 다른 checkpoints를 ensemble하면 candidate diversity and error diversity를 더 크게 만들 수 있다.

7-2. Reuse potential

1) Multi-checkpoint reasoning ensemble

Same base model의 SFT, RLVR, instruction-following checkpoints를 generator and verifier 역할로 분리할 수 있다.

2) Proof-like document reasoning

Legal clause reasoning, evidence synthesis, scientific derivation에서 candidate answer를 generate-verify-refine loop로 처리할 수 있다.

3) Strict acceptance plus partial-credit ranking

Search stage에서는 unanimous binary verifier로 false accept를 줄이고, final stage에서는 rubric score로 candidate를 비교하는 two-stage judge를 재사용할 수 있다.

4) Resumable high-compute evaluation

Every request를 deterministic JSONL row로 저장하는 recipe는 large-scale benchmark and agent evaluation에도 유용하다.

5) Formal verification bridge

Natural-language proof search가 diverse candidate를 만들고, final candidate만 formalization and proof checker에 보내는 cascade를 만들 수 있다.

7-3. Follow-up papers

• DeepSeekMath-V2
• AlphaProof
• DeepSeek-Prover
• Goedel-Prover
• Seed-Prover
• LeanDojo
• Process Reward Models for Mathematical Reasoning

8. Summary

• Nemotron IMO system은 GA, SFT, RL three checkpoints를 complementary generator and judge로 사용한다.
• Round 1에서 384 proofs를 만들고, 16 unanimous verifier judgments로 acceptance를 결정한다.
• Accepted proof가 없으면 up to eight rounds의 critique-based refinement를 수행한다.
• IMO 2026에서 30 out of 42 points로 gold threshold를 넘겼고 training data, checkpoints, code, proofs, 200-problem benchmark를 공개한다.
• 가장 큰 한계는 massive compute and correlated natural-language verifier error이며, unanimity도 formal correctness를 보장하지 않는다.