論文解説: An Open Recipe for IMO Gold — オープンモデルで国際数学オリンピック金メダル水準に届いた「生成・検証・修正」の設計
Nemotron 3 Ultra の3チェックポイントで証明を生成・検証・修正し、IMO 2026 で42点中30点(金メダル水準)に届いたNVIDIAの公開レシピを、推論時計算の設計という観点から1から解説します。
要点
- この論文はNVIDIAの研究者らによる「An Open Recipe for IMO Gold」（arXiv:2609.10712）で、数学オリンピックの自然言語証明を扱う。
- システムは形式証明器・外部ツール・インターネットを使わず、3つのチェックポイントが証明を「生成→検証→修正」する反復探索を回す。
- 別の高計算段階が最終提出を選び、このシステムはIMO 2026で42点中30点を取り、金メダルの基準に達した。
- 検証パネルは全員が満点をつけたときだけ合格とする極端に厳しい基準で、正しい証明も落とすが「遅れるだけ」で済む。
- 土台はNemotron-3-Ultra 550B-A55Bで、GA（一般公開版）、SFT版、RL版の3つのチェックポイントを使い分ける。
An Open Recipe for IMO Gold: Training Nemotron for Olympiad Mathematics
一次資料 — この記事の根拠
論文の発表 2026-09-09→この解説の公開 2026-09-24同月
An Open Recipe for IMO Gold: Training Nemotron for Olympiad MathematicsIvan Moshkov, Stephen Ge, George Armstrong ほか · 2026-09-09 · v1arXiv:2609.10712論文ページ·PDF原文の要旨（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.
この論文は何をしたのか
今回読むのは、NVIDIA の研究者らによる "An Open Recipe for IMO Gold: Training Nemotron for Olympiad Mathematics"（arXiv:2609.10712、2026年9月公開）です。
アブストラクトの要旨はこうです。著者らは、難しい数学オリンピック問題の「自然言語による証明」を書かせるとき、モデルの事後学習と推論時の設計がどう効くかを調べました。Nemotron 3 Ultra を出発点に、教師あり微調整（SFT）と強化学習（RL）で2つの専門チェックポイントを作り、どのチェックポイントを使うか、検証と修正をどう組むかを評価しています。その結果をもとに組んだシステムは、形式証明器・外部ツール・インターネットを一切使わず、すべて自然言語で動きます。元の一般公開版と2つの専門版、計3つのチェックポイントが候補証明を「生成→検証→修正」する反復探索を回し、別の高計算段階が最終提出を選びます。このシステムは IMO 2026 で42点中30点を取り、金メダルの基準に達しました。さらに2つのチェックポイント、学習データ、学習・推論コード、提出した解答、新作200問のベンチマーク Nemotron-IMO-Bench を公開しています。
一言でいえば「大きなモデルを1つ賢くする話」ではなく、「性格の違うモデルを組み合わせ、検証に大量の計算を回すと金メダル水準に届いた」という、推論時計算（test-time compute）の設計報告です。
比喩: 3人の作家と2人の厳しい編集者
推論時計算という言葉が初めての方のために、出版社にたとえます。
- 作家が原稿（証明の候補）を大量に書く。作風の違う作家を3人雇っている
- 編集者が原稿を読み、「完璧」「惜しい」「致命的な穴あり」と採点し、赤ペンでコメントを付ける
- コメント付きで差し戻された原稿を作家が書き直す
- 最後に、残った原稿を別の審査会がもっと時間をかけて読み、1本だけ出版する
ポイントは、作家を増やすことより編集者の厳しさと作風の多様さの方が効いた、という点です。これは論文の結論（§8）そのものです。
直感: なぜ「たくさん書く」だけでは足りないのか
言語モデルに同じ問題を何百回も解かせれば、どこかに正解が混ざることはよくあります。問題はどれが正解か分からないことです。数学の証明は答えの数値が合うかどうかでは判定できないので、誰かが読んで論理の穴を探す必要があります。
この論文の設計は、その「誰か」を複数のモデルで組んだ検証パネルにし、しかも「全員が満点をつけたときだけ合格」という極端に厳しい基準にしました。厳しすぎると正しい証明も落としますが、それは後で説明するように「遅れるだけ」で済む、というのが設計の核心です。
使ったモデルと学習（§4）
土台は Nemotron-3-Ultra 550B-A55B（総パラメータ5500億、1トークンあたり550億が動く混合エキスパート型）です。論文は次の3つを使い分けます（§4.1）。
- GA: 一般公開版そのまま
- SFT版: 証明に特化したデータで教師あり微調整
- RL版: GA から強化学習で証明生成を鍛えたもの
3つは同じ土台から分かれた兄弟ですが、後で見るように「解ける問題」も「採点の甘さ」も違います。この違いこそが、パイプライン全体で使われる資源になります。
コメント
コメントにはログインが必要です