AI・テクノロジー

自然言語だけでIMO金メダル——NVIDIA「Nemotron」オープン・レシピの全貌を読み解く

docker agent

• 37 min read
Share

形式証明なしで金メダル——この論文が示したこと

大規模言語モデルによる数学オリンピック挑戦の歴史は、2026年9月9日に公開された論文「An Open Recipe for IMO Gold: Training Nemotron for Olympiad Mathematics」で新しい段階に入った。著者ら（NVIDIA）は、モデル「Nemotron 3 Ultra」を事後学習し、生成・検証・洗練を繰り返す推論パイプラインを組むことで、IMO 2026（国際数学オリンピック）で42点満点中30点を獲得したと報告する。金メダル閾値は29点であり、わずか1点だけ上回った水準——満点ではない点は正確に押さえておきたい。

何が意外か。このシステムは、Leanなどの形式証明器（formal prover）を一切使っていない。証明支援系に記号列として証明を書き下すのではなく、数学者が論文に書くのと同じ自然言語・数式混じりの文章で解答を書く。外部ツールもインターネット接続もなく、問題文（LaTeX）をそのまま読み、解答文を生成して提出する。利点は、記号化が難しい組み合わせ論や整数論といったアイデア勝負の問題にも適用できること。代償は「正しさの自動保証」がないことだ。

さらに重要なのは、これが研究者の自慢話で終わっていない点である。事後学習済みチェックポイント2種（SFTとRL）、訓練データ、訓練・推論コード、提出した6件の解答、そして新作200問のベンチマーク「Nemotron-IMO-Bench」までが公開されている。読者が同じ手順を追試できる「再現可能なレシピ」として提示されているのが、この論文の立ち位置を決めている。

パイプライン全体の骨格は次のように整理できる。

flowchart LR
    A[問題文 LaTeX] --> B[生成 3チェックポイント×8プロンプト]
    B --> C[検証パネル 16判定の全員一致]
    C -->|全員が1なら受理| D[証明プール]
    C -->|不一致| E[洗練 批評付きで再生成]
    E --> D
    D --> F[最終選抜 48判定の平均点]
    F --> G[人間の審査員へ提出]

前半の「生成→検証→洗練」のループが探索ステージ、後半の最終選抜が選抜ステージにあたる。候補を出すことと、出す候補を選ぶことを別の仕組みに分ける——この役割分担が、自然言語だけでも金メダル水準に届いた成果の土台になっている。

IMOとAIのこれまで——なぜ「自然言語」が転換点なのか

IMO（International Mathematical Olympiad、国際数学オリンピック）は、高校生年代の数学競技における世界選手権である。1問7点×6問＝42点満点で、2日間に分けて各4.5時間、合計9時間をかけて6問を解く。出題範囲は代数・組み合わせ・幾何・整数論に大別され、要求されるのは知識の量ではなく、自力で発想を組み立てる力だ。金メダルは「○点以上」と固定されておらず、その年の成績分布に応じて閾値が動く。2026年は29点、システムが獲得したのは30点だった。

AIがこの問題に挑む方法は、大きく2つの系譜に分かれる。

系譜 代表的な取り組み 証明の表現 正しさの担保 強みと限界
① 形式証明・神経記号 AlphaGeometry（2024, Nature）、AlphaProof＋AlphaGeometry 2（IMO 2024で金メダルラインまで1点）、DeepSeek-Prover-V2、Goedel-Prover-V2、Seed-Prover Leanなどの証明支援系の記号列 カーネルが機械的に検証（自動保証あり） 検証が確実でデータ生成にも使えるが、形式化のコストが高く、着想が本質の分野に弱い
② 自然言語 Gemini Deep Think、OpenAIの実験モデル（IMO 2025で金メダル水準）、Huang & Yang（2025）、DeepSeekMath-V2、Aletheia 数学者が論文に書くのと同じ文章＋数式 LLMによる検証（自動保証なし） あらゆる分野に適用でき人間が読めるが、誤りを機械が確定できない

系譜①の出発点は、神経言語モデルで記号エンジンを誘導する「神経記号的手法」である。AlphaGeometry（2024, Nature）は幾何の問題に特化し、補助線の候補を言語モデルが提案、厳密な推論は記号エンジンが担う構成で高い成績を出した。その後継であるAlphaProofとAlphaGeometry 2は2024年のIMOで金メダルラインまであと1点に迫っている。並行して、Lean（証明支援系の一つ）向けの自動証明器が相次いで登場した。DeepSeek-Prover-V2やGoedel-Prover-V2、Seed-Proverなどがそれで、高校数学レベルの形式定理を集めたminiF2Fや、大学数学の定理を含むPutnamBenchの記録を塗り替えてきた。ここでの鍵は、正しさをカーネル（証明検査器）が機械的に判定できる点にある。信頼できる検証があるからこそ、大量の訓練データを自動生成できる。

一方、系譜②は「形式化せずに解く」路線である。2025年のIMOで、Gemini Deep ThinkとOpenAIの実験モデルが、自然言語のまま金メダル水準に到達した。この出来事は論点を大きく変えた。問われていたのは「証明を生成できるか」から「生成した候補をどう検証し、どれを最終解答として選ぶか」へ移ったのである。その中間に位置する研究も蓄積されている。モデル非依存の検証＋洗練パイプラインでIMO 2025の6問中5問を正解した研究（Huang & Yang, 2025）、生成器・検証器・メタ検証器を訓練し検証の計算量をスケールさせたDeepSeekMath-V2、そして研究レベルの数学へ踏み出したAletheiaなどだ。共通するのは、生成するモデルとは別に「評価するモデル」を置くという設計である。

timeline
    title AIによる数学オリンピック挑戦の流れ
    2024 : AlphaGeometryがNatureに掲載される
         : AlphaProof＋AlphaGeometry 2がIMO 2024で金メダルラインまで1点
    2025 : 形式証明（Lean）系の自動証明器がminiF2F・PutnamBenchを更新
         : IMO 2025でGemini Deep ThinkとOpenAI実験モデルが自然言語のまま金メダル水準
         : 検証＋洗練パイプラインやDeepSeekMath-V2が「評価の設計」を前面に出す
    2026 : IMO 2026でオープンモデルが30/42点、金メダル閾値29点を超える

なぜ自然言語が転換点なのか。形式証明は「正しさを機械が保証できる」代わりに、記号化そのものが研究課題になる。補助線や不変量の着想が本質である組み合わせ論・整数論の問題では、正しい証明を先に知らないと形式化が進まないという循環に陥りやすい。自然言語なら、問題文（LaTeX）を読み、数学者が書くのと同じ文章で解答を書き、そのまま提出できる。適用範囲は一気に広がる。ただしその代償として、正しさの自動保証は失われる。

このトレードオフが、以降の設計を決める。自然言語で書く以上、性能を左右するのはモデルの生成力だけではなく、「どの候補を信じるか」を決める検証と選抜の仕組みになる。オープンモデルで金メダル水準に届くための残された課題は、まさにそこに集約されていく。

土台となるモデル：Nemotron 3 Ultraとは何か

このレシピの土台は、NVIDIAが公開している大規模言語モデル「Nemotron 3 Ultra」である。まず押さえておきたいのは規模の表記だ。総パラメータ550B（5500億）・1トークンあたりの活性パラメータ55B（550億）のMoE（Mixture-of-Experts）モデルであり、「550B-A55B」と書かれる。MoEとは、モデル内部に多数の「エキスパート」と呼ばれる部分ネットワークを並べておき、入力トークンごとにごく一部だけを選んで計算させる設計である。巨大な知識容量を持ちながら、1回の推論で動かす計算量は数十B級のモデル並みに抑えられる。数学の問題文のように長く複雑な入力を扱う場面では、この「容量と計算量の分離」が効く。

アーキテクチャ上の特徴も、長い証明を扱ううえで無視できない。Attention（系列内の全トークンを参照する仕組み）と、状態空間モデル系のMamba（系列を一定のメモリ量で走査する方式）を組み合わせたHybrid Mamba-Attentionにより、長文コンテキストの計算コストを抑える。エキスパートの選択を圧縮された潜在空間で行うLatentMoE、投機的デコード（小さな処理で複数トークンを先読みして検証する高速化手法）のためのMTP層、思考に割く計算量を制御する推論予算（reasoning budget）、そしてNVFP4（4ビット精度の数値形式）での事前学習も備える。対応コンテキスト長は最大100万トークンに達する。

flowchart TD
    A[Nemotron 3 Ultra 550B-A55B] --> B[Hybrid Mamba-Attention]
    A --> C[LatentMoE エキスパート選択]
    A --> D[MTP層 投機的デコード]
    A --> E[推論予算制御]
    A --> F[NVFP4 事前学習]
    G[公開チェックポイント] --> H[事前学習済み]
    G --> I[事後学習済み]
    G --> J[量子化済み]

オープン性も、この論文の前提条件である。事前学習済み・事後学習済み・量子化済みのチェックポイントと訓練データが公開されており、読者が同じ出発点に立てる。本論文のシステムは、そのうち3つのチェックポイントを使い分ける。

チェックポイント 訓練 位置づけ
Nemotron-3-Ultra-GA なし 一般公開版。無改変のまま利用し、主に多様性の源として使う
Nemotron-3-Ultra-SFT 教師あり微調整 証明スペシャリスト。第1ラウンドの精度が最も高い
Nemotron-3-Ultra-RL 強化学習 証明スペシャリスト。総合スコアが最も高い

重要なのは、この3つが単なる性能違いのバリエーションではなく、生成（解答候補を出す）・検証（正誤を判定しフィードバックを書く）・洗練（フィードバックを踏まえて修正する）という3つの役割に割り当てられている点だ。1つのモデルにすべてを任せるのではなく、事後学習の仕方を変えた複数のモデルに別々の仕事を負わせる。この役割分担が、以降に続く訓練と推論パイプラインの設計思想の核になる。なお公開リポジトリ上ではパラメータ数が561Bと表記される場合があるが、論文本体の表記は550B-A55Bである。

訓練① 教師あり微調整（SFT）——40万件の証明データをどう作ったか

教師あり微調整（SFT、Supervised Fine-Tuning）とは、あらかじめ用意した模範解答の組を使ってモデルの重みを追加学習させる手法である。この論文がSFTに求めたのは、単に「正解を書く」能力ではない。証明を書くことと、証明を検証することの両方を同時に学ばせる点が特徴だ。数学オリンピックの証明には一意の正解手順がなく、穴のない論理を組み立てる力と、他人の論理の穴を指摘する力は表裏の関係にある。そこで事後の強化学習で使う検証器の役割まで、この段階で作り込んでおく。

何を学習させたのか

訓練データの出発点は、数学系の公開問題コーパス Nemotron-Math-Proofs-v1 のうち、コミュニティ型の問題投稿サイト由来のサブセットである。ここから、事前に解かせて正答率を測り 「難しい」と判定された15,879問を厳選した。易しい問題を大量に入れても学習信号にならないため、意図的に難問へ寄せている。

これらの問題に対し、生成モデルとしてDeepSeek-V4-Proの最大推論モードを使い、最大40万トークンの証明を生成させた。それでも完全に解けたと判定されなかった問題は、最大3ラウンドの洗練にかける。洗練では先行試行と検証器からのフィードバックを条件として与え、こちらは最大35万トークンを許す設定だ。

検証・メタ検証という発想

このデータ生成の要は、正解・不正解の二値ではなく、検証器に3値の採点をさせた点にある。

スコア 意味 扱い
1 完全に正しい 検証トレースとして全件保持
0.5 概ね正しいが細部の欠落や軽微な誤りがある 検証トレースとして全件保持
0 致命的な誤り、または重大な欠落 決定論的にサブサンプリング

さらにメタ検証器を置く。これは「自己評価や検証器の判定がどれだけ信頼できるか」を評価する役割であり、検証の検証という二段構えの構造になっている。証明の成否を一度判定して終わりにせず、その判定自体の確からしさまで訓練対象に含めることで、後の強化学習で「検証器の評価を報酬にする」という設計の土台が整う。

データ品質の管理も明示されている。不完全な出力、壊れた出力、長さ上限で切れた生成はすべて除去する。同時に、スコア0のトレースばかりが集まると訓練分布が誤りの例に偏るため、0.5と1は全件を残し、0は決定論的に間引いた。結果として得られたコーパスは15,818問・414,890例である。

種類 例数
証明生成 58,543
洗練 67,971
検証 236,360
メタ検証 52,016
合計 414,890 
flowchart LR
    A[問題を厳選<br/>15,879問] --> B[証明を生成<br/>最大40万トークン]
    B --> C{完全に解けたか}
    C -- いいえ --> D[洗練<br/>最大3ラウンド・35万トークン]
    D --> C
    C -- はい --> E[検証トレース<br/>1/0.5/0の採点]
    E --> F[メタ検証トレース]
    F --> G[品質フィルタ<br/>破損・切れを除去<br/>0は間引き]
    G --> H[訓練コーパス<br/>15,818問・414,890例]

訓練の規模と設定

SFTは長文コンテキストを前提に組まれている。最大系列長425,984トークンという設定は、1件の問題と証明の組が数十万トークンに達しうることを意味する。数式と自然言語が混在する長い証明を、文書全体として一貫して扱う必要があるためだ。損失はトークン単位の交差エントロピーで、精度はBF16を使う。

計算資源はGB200を512基。並列化はテンソル並列8・コンテキスト並列32・エキスパート並列64という構成で、グローバルバッチ64、オプティマイザステップは約1,600回である。最適化はAdamW（β1=0.9、β2=0.95、weight decay 0.1、勾配クリップ1.0）。学習率は最初の約1%のサンプルでウォームアップして1.5e-5をピークとし、以降はコサイン減衰で2e-6まで下げる。40万トークン級の系列をMoEモデルで回すため、MoE層の選択的再計算と細粒度の活性化オフロードを併用し、メモリと計算をやりくりしている。

学習をどこで止めるかも、勘ではなく評価で決めている。IMO-ProofBenchと近年の競技問題から抽出した133問で各チェックポイントを評価し、採用されたのはステップ1,300だった。ここで作られたSFTモデルは、次の強化学習の出発点であると同時に、推論パイプラインでは「検証」と「洗練」の主要な担い手として、また第1ラウンドの精度が最も高い生成器として使われることになる。

訓練② 強化学習（RL）——検証器を報酬にして証明力を伸ばす

強化学習（RL、Reinforcement Learning）は、モデルが生成した出力に対して与えられた報酬を手がかりに、その出力を出しやすく／出しにくくする方向へ重みを更新する手法である。教師あり微調整（SFT）が「模範解答を真似る」訓練だとすれば、RLは「良かった出力を自分で見つけて伸ばす」訓練だ。この論文のRLが面白いのは、報酬の対象が正解の最終回答ではなく、証明の厳密さである点にある。答えの数値が合っていても論法に穴があれば評価されない。

訓練に使う問題の絞り込み

RLの効き目は問題の難易度に強く依存する。易しすぎて毎回正解できる問題では勾配が立たず、難しすぎて一度も正解できない問題では比較の基準が作れない。そこでベースモデルであるNemotron 3 Ultra自身に4回解かせ、「4回中1〜3回は解ける」問題だけを残した。条件を満たしたのは9,597問である。この中間難易度フィルタが、後の急速な報酬上昇の前提になっている。

報酬設計——検証器の判定をそのまま報酬にする

報酬の骨格はDeepSeekMath-V2の設計にほぼ準拠している。ただし1点だけ変更し、自己分析報酬を外した（α=1、β=0）。報酬の主役は検証器が付ける厳密さのスコアであり、モデル自身の「自信」や自己申告の評価は使わない。自分で自分を採点する経路を切ることで、甘い自己評価に最適化してしまう抜け道をふさいでいる。

効率化の仕組み

証明は数千〜数万トークンに及ぶ長い系列であり、素朴な同期型のRLでは生成待ちで計算資源が遊ぶ。そこで非同期RLを組む。PipeLineRLに近い方式で、生成と訓練を並行させ、完了した系列から順に訓練バッチへ流し込む。生成が終わったものから使うため、バッチ全体の完了を待つ必要がない。

系列の長さに由来する学習の不安定さには、次の3点で対処する。

  • 動的サンプリング（DAPO由来）：全軌道の報酬が同じでアドバンテージが0になるサンプルを除き、実効バッチが痩せるのを防ぐ。
  • クリッピング付き重要度サンプリング：生成側と訓練側のモデルのずれを補正しつつ、外れ値の影響を抑える。長い系列では更新回数が増えて分布がずれやすいため、ここが効く。
  • エントロピー制御：エントロピーが0.4を超えたら、正例に含まれる低確率トークンをマスクする。出力の多様性が崩れて崩壊するのを防ぐ狙いだ。
flowchart LR
    A[問題プール<br/>9,597問] --> B[生成ノード<br/>128ノード]
    B --> C[軌道<br/>128プロンプト×16軌道=2,048]
    C --> D[審判ノード<br/>16ノード<br/>軌道ごとに報酬を計算]
    D --> E[訓練バッチへ<br/>完了順に投入]
    E --> F[方策を更新<br/>訓練ノード128]
    F -->|重みを随時反映| B

訓練の規模と設定

項目 設定
バッチ 128プロンプト × 16軌道 = 2,048軌道
最適化 AdamW（β1=β2=0.9）、学習率3e-6、weight decayなし
軌道の最大寿命 4オプティマイザステップ（古いデータは捨てる）
計算資源 訓練128ノード＋推論128ノード＋審判16ノード（各4基のGB200）
同時in-flightプロンプト 最大160
最大系列長 131,072トークン

軌道の寿命を4ステップに切るのは、古い方策で生成した系列をいつまでも使い続けると、オンポリシー性が崩れて学習が不安定になるためだ。SFTの最大系列長が425,984トークンだったのに対しRLは131,072トークンと短いのは、RLでは同じ長さの系列を何度も生成し直す必要があり、計算の重心が「長さ」より「本数」に移るからである。

評価と、RLが効く理由

進捗の測定には、IMO-ProofBenchや2025年のIMO・Putnam、近年の各国代表選抜などから抽出した133問を使い、判定はGPT-5.5の高推論設定に任せる。RLを始めると報酬と評価スコアが急速に伸びる。

なぜこれが効くのかを平易に言えば、証明を生成するモデル自身に、自分の証明の穴を見つけて直す能力を内面化させているからだ。検証器の評価を報酬にすることで、「もっともらしいが誤った論法」を書く方向へ進む力が削られ、厳密な論証を書く方向へ重みが寄る。SFTが模範解答から学んだ「正しい証明の型」に対して、RLは検証という外部の目を通じて「自分のどこが危ないか」を学ぶ第二段階として位置づけられる。

推論パイプライン① 高計算量探索——生成→検証→洗練のループ

ここからは、事後学習を終えたモデルをどう動かして1問の解答を作るか、という推論時の設計に入ります。この章で扱うのはパイプラインの第1段階にあたる高計算量探索です。鍵となるのは「テスト時計算（test-time compute）」という考え方で、これはモデルの重みを変えずに、推論時にどれだけ計算を投じるかで性能を引き上げる手法を指します。NVIDIAが採ったのは、1つの解答をじっくり練る方式ではなく、多数の候補を生成し、厳しく検証し、落ちたものを批評付きで洗練する——という反復ループでした。

全体像——1問ごとに独立した最大8ラウンド

探索は問題ごとに完全に独立して走ります。ある問題の探索が別の問題に影響することはありません。各問題について最大8ラウンドのループを回し、生成された証明は検証スコアとフィードバック文と一緒に「証明プール」へ蓄積します。次のラウンドはゼロから作るのではなく、このプールから有望な候補を選び直して洗練する。生成したものを捨てずに貯め続ける点が、単純な再試行との違いです。

flowchart TB
    A[第1ラウンド<br/>3チェックポイント×16試行×8プロンプト<br/>=384件の証明候補] --> P[証明プール<br/>スコアとフィードバックを保持]
    P --> V[検証パネル<br/>RL 8判定 + SFT 8判定 = 16判定]
    V -->|16件すべてが1| ACC[受理<br/>そのチェックポイントは停止]
    V -->|1件でも0 / 0.5| R[洗練<br/>上位16件 + 最大8件の批評文]
    R --> RN[3チェックポイント × 各4サンプル<br/>=192件/ラウンド]
    RN --> P
    ACC --> F[最終候補<br/>1問あたり最大3件]

第1ラウンド——384件をどう作るか

最初のラウンドでは、3つのチェックポイント（GA・RL・SFT）それぞれに16回の試行をさせ、さらに8種類の相補的な生成プロンプトを掛け合わせます。3 × 16 × 8 = 384件の証明候補が一気に生まれる計算です。

この8種類のプロンプトは、同じ問題に対して異なる攻め方をさせるために意図的に散らしてあります。標準的な解答に加え、「補題を先に立てる」「複数の解法ルートを比較する」「反例で自分の議論を壊しにいく」「形式化しやすい書き方を優先する」「論理の穴に強い構成を選ぶ」「不変量や極値を軸にする」「自分の戦略を監査する」といった具合です。数学の証明は同じ結論でも到達経路が何通りもあり、1つの書き方に収束させると行き詰まったときに抜け出せなくなります。戦略の多様性を最初に確保しておくのが、この段階の狙いです。

検証——16件すべてが「1」のときだけ受理

生成した候補は、RLとSFTの2つの検証用チェックポイントが判定します。それぞれ8件ずつ、合わせて16件の独立した判定です。判定は3値で、1は完全に正しい、0.5は概ね正しいが軽微な誤りや欠落がある、0は致命的な誤りを意味します。

受理の条件は極端に厳しく、16件すべてが1を出したときのみです。1件でも0や0.5が混じれば受理しません。判定が途中で切れて解析できないものは無効として扱われます。

ここで重要な但し書きがあります。この「受理」はあくまで内部の検証基準を通過したという意味であり、公式採点で正しいことが保証されたわけではありません。検証器にも見えない限界があり、後の章で見るように、受理された証明の中にも実際には誤りが残っていました。厳格な条件は誤りを減らしますが、ゼロにはしない——これがこの論文自身のデータが示した教訓です。

洗練——批評文を添えて書き直させる

受理されなかった場合、探索は止まりません。グローバルプールの上位16件の証明を選び、それぞれに最大8件の検証批評文を添えて洗練用のプロンプトを組み立てます。要するに「この議論のここが弱い」という具体的な指摘を渡した上で書き直させるわけです。

これを3つのチェックポイントに送り、各4件サンプルするので、1ラウンドあたり192件の洗練試行が生まれます。洗練の結果も同じプールに戻され、次のラウンドでまた16件の検証にかけられます。生成と検証と洗練がリング状につながり、ラウンドを追うごとに候補の質が上がっていく構造です。

早期停止と最終候補

全ラウンドを必ず回すわけではありません。あるチェックポイントが受理済みの証明を出したら、そのチェックポイントからのサンプリングだけを停止し、残りのチェックポイントはそのラウンドの終わりまで走り続けます。1つ受理が出た時点で全部を止めてしまうと、他のモデルが持つ別解を捨てることになるためです。

この設計の結果、1問あたり最大3件の「最終候補」が残ります（3チェックポイントぶん）。次章で扱う第2段階では、この3件の中から提出する1件を選び出す作業を行うことになります。

推論パイプライン② 最終選抜——別目的の審判団を用意する

ここまでで見てきた「高計算量探索」は、1問について複数のチェックポイントが大量の証明候補を生み、厳密な検証と批評文付きの洗練を繰り返す仕組みだ。その結果、1問あたり最大3件の「最終候補」が残る。しかし、実際の競技で提出できる解答は1問につき1つだけである。この章で扱うのは、その「最後の1つをどう選ぶか」という問題だ。

結論から先に言うと、NVIDIAはここで探索中の検証器とは別の、目的の異なる審判団を用意した。これが本論文の推論パイプライン第2段階にあたる。実装は単純に見えるが、この「検証」と「選抜」の切り分けこそ、汎用的なシステム設計の知恵として読める部分だ。

なぜ検証と選抜を分けるのか

探索ループの中で動いていた検証器は、実は「提出する証明を決める」ために作られたものではない。その役割は、証明が受理条件を満たすかどうかを判定し、満たさなければ洗練のためのヒント（改善点の批評文）を返すことだ。つまり検証器の出力は、次のラウンドに渡すフィードバックの材料であって、最終的な序列ではない。

一方、最終選抜に求められるのは「限られた予算の中で、どの候補を提出すべきか」というランク付けの仕事だ。探索の途中で「この証明を受理して探索を止めてよいか」を判断するのと、探索が終わって「この中で一番まともな解答はどれか」を判断するのとでは、問いの性質が異なる。同じチェックポイントを使っていても、プロンプトの作り方と評価の形式を変えて別のタスクとして設計したのが、この段階のポイントである。

IMO採点を模した「参照なし」の審判プロンプト

最終選抜の評価は、IMOの公式採点方式に近づける形で設計されている。

具体的には、審判役のモデルに対し、参照解答（模範解答）を一切与えずに、ある証明が完全解に至るために必要なマイルストーンを列挙させ、その到達度に応じて0〜7の整数点を付けさせる。この「マイルストーン列挙＋0〜7の絶対評価」という手続きは、数学評価プラットフォーム MathArena（Dekoninck et al., 2026）の審査手法を、参照解答を持たない設定（reference-free）に翻案したものだ。

探索時の検証が「1（完全に正しい）／0.5（概ね正しいが軽微な誤り）／0（致命的な誤り）」という3値の判定だったのに対し、こちらは0から7までの細かい絶対評価である。単に「通ったか通らないか」を超えて、複数候補を序列化できるのが狙いだ。ここで参照解答を与えないのは、模範解に依存すると「模範解と文面が似ているか」に評価が引きずられ、あるいは模範解自体が漏れてしまえば公正な比較ができないためである。あくまで解答の論理的な完成度だけを見て点をつけるようになっている。

審判団の構成——1候補につき48判定

この審判を、1件の最終候補に対して大量に実施する。構成は次の通りだ。

  • 3つのチェックポイント（GA・RL・SFT）それぞれが1候補につき16回判定
  • 合計で 3チェックポイント × 16判定 ＝ 48判定

各判定は独立して行われる。候補ごとにこの48個の0〜7点を集めて平均点を出し、その平均点で候補をランキングする。平均点が同点だった場合は、短い証明を優先する。情報量が同等なら、冗長でない簡潔な解答の方を提出するという、実際の採点文化にも通じる発想だ。

ここに、複数モデルへの分散という前章と同じ思想が顔を出す。1つのモデルが偏った評価をしても、他が相殺する。探索段階で「RLとSFTの一致」を要求したのと同じく、最終選抜でも単一モデルの判断に委ねない作りになっているのである。

なぜこの分離が「再利用できる設計パターン」なのか

検証と選抜を分けるこの設計は、数学に限った工夫ではない。むしろ、長文の生成物の品質をAIで担保したい場面では、そのまま移植できる一般的なパターンである。

たとえばコードレビューでは、開発中は「この実装のどこを直せばよいか」という改善指示が欲しい一方、リリース前は「候補の中でどれを選ぶか」という判定が欲しい。法務文書や設計レビューでも、ドラフト段階では欠陥を指摘する批評が、承認段階では複数案の序列化が必要になる。どちらも形式的には「AIに評価させる」ことだが、求める出力の粒度も判断の厳しさも異なる。

この論文が示しているのは、その二つの段階を同じモデルで済ませつつプロンプトと評価形式で分ける、という実践的な解だ。探索フェーズでは「ヒントを返す3値判定」、選抜フェーズでは「ランクをつける0〜7の絶対評価」。同じ検証器の部品を、役割に合わせて二度使いする感覚は、テスト時計算を設計する際の具体例として参考になる。

IMO 2026の結果——30/42点、金メダル閾値越え

問題別の得点と探索ラウンド

IMO 2026（国際数学オリンピック）で、このシステムは42点満点中30点を獲得し、金メダル閾値の29点を1点上回った。採点はIMO公式の採点者によって行われている。内訳は第1問・第2問・第4問・第5問が満点の7点、第3問・第6問が各1点だった。内部パイプラインで「受理」に到達したラウンドは、P1・P3・P4・P5が第1ラウンド、P2・P6が第2ラウンドである。ただし「受理」はあくまで内部検証基準を満たしたという意味で、公式採点の正しさを保証するものではない。

際立つのは速さだ。満点を取った4問は競技開始から76分以内に最終選抜パネルを通過し、残りの2問も100分以内に到達した。その後の4.5時間の競技時間中、探索を続けてもスコアはほとんど伸びなかった。これは「長時間かけて解を磨き上げた」のではなく、「最初のラウンドから十分に質の高い候補が得られていた」ことを示している。

かかった計算資源

提出された6件の証明が見つかるまでの消費は約7億700万トークン、1,464 GPU時間（GB200）だった。走り終えたラウンドまで含めた競技中の総消費は約23億1,000万トークン、約4,800 GPU時間に達する。

問題 得点 受理R 提出までのトークン 提出までのGPU時間
P1 7 R1 5.57M 11.7
P2 7 R2 227M 479.3
P3 1 R1 106M 240.9
P4 7 R1 20.4M 42.9
P5 7 R1 36.4M 76.7
P6 1 R2 312M 612.9
合計 30 – 707M 1,464.4

表を見ると偏りは明らかだ。P1はわずか5.57Mトークン・11.7 GPU時間で満点を取ったのに対し、P6は312Mトークン・612.9 GPU時間を投じて1点にとどまる。難問に計算が集中する構造がそのまま得点効率の非対称性になっている。

競技終了後も探索を走らせた「継続実行」では、8時間25分・第8ラウンドでP6の新しい解答を発見した。追加で6億1,000万トークン・890 GPU時間を消費し、独立の人間数学者パネルが4/7点と採点している（公式採点方式を使わない非公式の再採点であり、合計は33点相当の参考値である）。

検証器の「見えない限界」——2点のずれが示すもの

競技終了時、内部検証器も、事後の独立モデル審判団（GPT-5.5・Gemini 3.1 Pro・Claude Opus 4.8）も、そろって約32点と推定した。公式結果の30点を2点上回る数字である。ずれはP3とP6に集中しており、どちらのモデル評価も、公式採点では1点だった証明に高い点を与えていた。報告ではこれを単なるノイズではなく「モデル検証に共通する盲点」と論じている。

ここが重要な示唆だ。スコアが伸びることと、検証が信頼できることは別問題である。AIの審判をそのまま最終判定に使う危うさを、このシステム自身のデータが示している。高い得点を挙げても、その答え合わせが同じ方向に誤る可能性は残る——この2点のずれは、自動採点や自動検証を設計するうえで見落とせない警告になっている。

何が効いて、何が効かなかったのか（アブレーション）

チェックポイントの役割分担——「同じモデルを増やす」より「別のモデルに振る」

アブレーション（ある構成要素を外して効果を測る比較実験）は、開発セットで行われた。新作20問と近年の競技問題10問を合わせた30問で、難易度は易3・中7・難10・未解決10、分野は代数6・組み合わせ8・幾何8・整数論8に配分されている。この30問に対し、8ラウンドの探索とフォールバック（8ラウンドで受理に至らなかった場合にプール最上位の証明を最終候補にする措置）を通した累積の独立審判スコアを比較すると、次のようになった。

構成 累積審判スコア 受理問題数
アンサンブル（GA+RL+SFT） 188 25
RL単独 180 23
SFT単独 165 21
GA単独（無改変） 162 23

事後学習を行った2つのチェックポイントは、無改変のGAを上回った。ただし性格は異なる。SFTは第1ラウンドの時点で最も強く、RLは最終的な総合で最も強い。第1ラウンドで得られる候補の初期品質と、洗練を重ねたあとの伸びは、同じ事後学習でも別の方向に効いている。

総合スコア以上に重要なのが、役割の相補性である。RLに128回、SFTに128回の試行を割り当てた構成で受理できた18問の内訳は、両方が受理した6問、RLのみが7問、SFTのみが5問だった。ここでRLの試行を128から256へ倍増しても、SFTのみが取れていた5問のうち救えるのは1問だけである。

プール 第1ラウンド試行 受理問題数 全30問の得点
RL 128 128 13 135
RL 256 256 14 139
SFT 128 128 11 127
RL 128 + SFT 64 192 15 159
RL 128 + SFT 128 256 18 159
RL 128 + GA 128 256 13 140

同じ計算予算を使うなら、同じモデルを増やすより、訓練の異なる別のモデルへ振り分けたほうが網羅率が上がる。GAについては、第1ラウンドでRLやSFTが取れない問題を新たに受理することはできなかった。それでも後のラウンドで洗練の多様性の源として働くため、全ラウンドで使われている。

検証パネルの設計——偽受理と偽却下はコストが非対称

採用された検証パネルは「RLとSFTが各8件、計16判定がすべて完全に正しい（1）と判定したときのみ受理」という極端に厳しいルールである。この厳しさの根拠は、受理済み25件とスコアで層化した非受理275件、計300件の証明を独立審判の7点判定を正解基準として監査した結果にある。ここでいう偽受理は誤った証明を通してしまうこと、偽却下は正しい証明を弾いてしまうことを指す。

パネル規則 偽受理率 偽却下率
GA 8/8一致 31.6% 22.8%
RL 8/8一致 12.4% 64.2%
SFT 8/8一致 4.5% 69.1%
GA+SFT 16/16一致 3.4% 75.6%
RL+SFT 16/16一致（採用） 1.1% 81.3%
GA+RL+SFT 24/24一致 1.1% 82.9%
RL+SFT 14/16一致 17.0% 59.4%
RL+SFT 12/16一致 25.4% 30.9%

単一チェックポイントでは、GAは甘く（偽受理31.6%）、SFTとRLは厳しい。複数モデルの全員一致にすると偽受理は1%台まで落ちるが、その代償として偽却下が8割を超える。なぜこれほど偏ったトレードオフを受け入れられるのか。探索を止める検証器では、二つの誤りの重さが等しくないからだ。

flowchart LR
  subgraph FA["偽受理：誤りを見逃す"]
    A1["誤った証明で探索を打ち切る"] --> A2["以降のラウンドが走らない<br/>新候補が生まれない"]
  end
  subgraph FR["偽却下：正解を弾く"]
    B1["候補はプール上位に残る"] --> B2["批評文付きの洗練対象になる"] --> B3["フォールバック提出の資格も保つ<br/>損失は遅延のみ"]
  end

偽却下された証明は捨てられず、上位候補として洗練され続け、何も受理されなかった場合の最終候補にもなる。だから厳しく弾いても損失は時間に留まる。一方、偽受理はその問題の探索そのものを誤りで終わらせる。閾値を14/16に緩めると偽受理率は約1%から17%へ跳ね上がり、「救える正解1件につき誤り1件を通す」取引になった。

この設計にも限界はある。受理された25件のうち23件は審判7点だったが、1件は量化子の形式的な不備で6点、もう1件は0点だった。0点の証明は列置換の対称性に関する誤った議論を含み、明示的な反例が存在する。それでも全チェックポイントが満点を付け、24判定の一致ルールでも捉えられなかった。厳格な全員一致は偽受理を1%まで下げるが、ゼロにはできない。

効かなかった工夫——凝ったルーティングと安易な足切り

探索中の検証は「改善のヒントを返す3値判定」、最終選抜は「0〜7の絶対評価」と目的が異なる。その洗練側を速くしようとした試みは、いずれも最終的な網羅率を改善しなかった。問題レベルの教訓を統合して洗練に渡す方法（cross-proof context）は途中の進行は速いが、最終的に42問でベースラインの44問に届かない。0判定の少なさを優先するランキング（zero-first ranking）は第9ラウンドでベースラインと並ぶだけ。複数の多様な証明から洗練する方法も、受理できる問題数を増やさなかった。

最も示唆的なのはトリアージの失敗である。3判定だけである程度候補を絞れば、ルーティング段階の判定コストを95.3%削減できる。ところが固定プールを使った再生実験では、後により良い正解へ育つ第1ラウンドの祖先を44%のケースで捨ててしまった。捨てられた系譜の最終証明のうち13/14は、人間のレビューで完全に正しいと判定されている。コスト削減のための足切りが、育つはずだった正解を殺す。この結果を受けて、トリアージは本番構成から外された。

オープンリリースの中身——何が再現できるのか

公開されたものの一覧

IMO 2026の30点という結果は、そのままブラックボックスとして提示されたわけではない。事後学習済みのチェックポイント、訓練データ、ベンチマーク、推論パイプラインのコード、そして提出した解答と計算資源の会計までが、まとめて公開されている。基礎になっているのは550B総パラメータ・55B活性のMoEモデル（Nemotron 3 Ultra）で、その無改変版（GA）と、SFT・RLの2つの専門版が探索・検証・洗練を分担する構成だ。

種別 名称 ライセンス／内容
チェックポイント Nemotron-3-Labs-Ultra-Math-SFT ベースモデルのOpenMDW-1.1。教師あり微調整済み
チェックポイント Nemotron-3-Labs-Ultra-Math-RL ベースモデルのOpenMDW-1.1。強化学習済み
訓練データ Nemotron-Math-Proofs-v3-SFT CC BY 4.0。証明生成・洗練・検証・メタ検証の4種のトレース
訓練データ Nemotron-Math-Proofs-v3-RL CC BY 4.0。強化学習用の問題セット
ベンチマーク Nemotron-IMO-Bench CC BY 4.0。新作200問
コード 推論パイプラインのレシピとRL訓練ガイド 探索・検証・洗練のループと30問開発セットの構成方法
記録 提出した6件の証明と計算資源の会計 問題別のトークン消費・GPU時間

モデルとデータでライセンスが分かれている点は実務上重要だ。チェックポイントはベースモデル由来のOpenMDW-1.1、データとベンチマークはCC BY 4.0であり、再利用の条件が同じではない。

再現の難易度はどこで決まるか

最も再現しやすいのは評価まわりである。Nemotron-IMO-Benchは数学教育者・問題作者の協力のもとで作られた新作200問で、未公開の問題を含むため、既存の学習データに答えが混入している懸念が小さい。30問の開発セットも同じ方針で構成され、難易度（易3・中7・難10・未解決10）と分野（代数6・組み合わせ8・幾何8・整数論8）が明示されている。同じ物差しで自分の構成を測れるという意味で、公開物の中で最も価値が高い部分だ。

訓練の再現はより重い。SFTは最大425,984トークンの系列長を512基のGB200で学習し、RLは最大系列長131,072トークンで128訓練ノード・128推論ノード・16審判ノードを動かす。ここを同規模で再現できる組織は限られる。ただし公開されているのは重みとデータだけでなく、生成・検証・洗練のループというアルゴリズムであり、こちらははるかに小さい計算でも部分的な再現が可能である。

注意すべき但し書きも引き継がれる。パイプラインが「受理」とするのは内部検証基準を満たしたという意味で、公式採点の正しさの保証ではない。実際、公式採点との間には2点のずれが残った。

何を再利用できるのか

この公開の中心的な価値は、フロンティアモデルのAPIに依存せず、公開モデルだけでも高難度の推論タスクを組み立てられることを示した点にある。持ち帰れる設計は4つだ。

flowchart TD
  P["問題"] --> G["複数モデルで候補を生成"]
  G --> V["独立した検証<br/>厳格な全員一致"]
  V -->|未受理| R["批評文付きで洗練し<br/>候補プールへ戻す"]
  R --> V
  V -->|受理| S["探索とは別の評価基準で<br/>最終候補をランク付け"]

第一に、候補生成を訓練の異なる複数モデルに振り分けること。同じモデルの試行回数を増やすより網羅率が上がる。第二に、検証を独立した判定の全員一致で行い、誤って通すコストを極小に抑えること。第三に、弾かれた候補を捨てずに批評文付きで洗練し続けること。第四に、探索中の検証と最終選抜で評価基準を分けること——探索は改善のヒントを返す3値判定、最終選抜は0〜7の絶対評価である。

この骨格は数学に固有ではない。正解が一意に定まらない長文タスク、たとえばコードレビュー、法務文書の点検、設計レビューでも同じ構造が使える。検証器を別モデルにする、最終選抜を別プロンプトにする、という分離は、そのまま移植できる設計パターンである。

よくある質問

「自然言語で証明する」とは、どういうことか

形式的な証明支援系（Lean など）に記号列として証明を書き下すのではなく、数学者が論文に書くのと同じ、自然言語と数式が混じった文章として解答を書くことだ。このシステムは形式証明器も外部ツールもインターネット接続も使わず、LaTeX で与えられた問題文を読み、そのまま提出できる解答文を生成する。利点は、記号化が難しい分野（組み合わせ論や整数論のようなアイデア勝負の問題）にも適用できること、欠点は「正しさが自動的に保証されない」ことだ。実際、この論文でも内部検証器の推定と公式採点の間に2点のずれが残った。

金メダル水準とは、具体的に何点くらいか

IMO は1問7点×6問の42点満点で、金メダルのカットオフ（閾値）は開催年ごとに変わる。この論文が対象とした IMO 2026 では金メダル閾値が29点で、システムは30点を獲得した。問題別では第1・2・4・5問が満点の7点、第3・6問が各1点である。30点は「金メダルラインを1点上回った」水準であり、満点からはほど遠いという点は正確に押さえておく必要がある。

なぜ同じモデルを何回も走らせるのではなく、別のモデルを混ぜるのか

「同じモデルを増やしても、解けない問題は解けない」という実測があるからだ。第1ラウンドで強化学習（RL）モデルの試行を128回から256回へ倍増しても新たに受理できた問題は1問だけだったが、同等の計算量を教師あり微調整（SFT）モデルの試行に振ると受理数は大きく伸びた。RL 128回＋SFT 128回で受理できた18問の内訳を見ると、両方が取れたのは6問、RLだけが7問、SFTだけが5問である。多様性は試行回数ではなく、訓練の異なるモデルから生まれる——これがこの論文の中心的な実務的知見だ。

検証に16回の一致を要求するのは厳しすぎないか

厳しいからこそ採用されている。探索を止める検証器では、誤った証明を受理してしまう「偽受理」のコストが、正しい証明を弾く「偽却下」よりはるかに大きいためだ。偽却下された証明は上位候補として洗練され続け、何も受理されなかった場合の最終候補にもなれるが、偽受理はそのラウンドで探索を打ち切ってしまう。閾値を16件中14件の一致に緩めると、偽受理率は約1%から17%へ跳ね上がり、「救える正解1件につき誤り1件を通す」取引になった。なおここでいう「受理」は内部検証基準を満たしたという意味で、公式採点の正しさを保証するものではない。

この成果は研究用のデモで、実務には関係ないのか

パイプラインの骨格は特定分野に依存しない。「複数モデルで候補を出す」「独立した検証を厳格な一致条件で行う」「批評文を添えて洗練する」「探索と最終選抜で別の評価基準を使う」という4点は、コード生成、文書レビュー、設計検証など、正解が一意でない長文タスクにそのまま移植できる。実際この論文自身が、検証コストと精度のトレードオフや、安易な足切りが正解を捨てるリスク（3判定だけで候補を絞ると、後により正解へ育つ第1ラウンド祖先を44%のケースで捨ててしまう）まで定量的に示しており、AI システム設計の教材としても読める。

まとめ

この論文が到達した結論は明快である。Leanなどの形式証明器も、外部ツールも、インターネット接続も使わずに、事後学習した複数のチェックポイントによる検証駆動の洗練ループと、最終選抜への十分な計算配分を組み合わせれば、IMO 2026で42点満点中30点——金メダル閾値29点を1点上回る水準——に届く。しかも、その手順はチェックポイント2種、訓練データ、訓練・推論コード、提出した6件の解答、新作200問のベンチマークとして公開されており、誰でも追試できる形になっている。ここで押さえておきたいのは、30点はあくまで内部検証を通過した候補を公式採点者に提出した結果であり、パイプライン内部の「受理」は正しさの保証ではないという点だ。実際、競技終了後にP6へ追加の計算を投じて得た新しい解答の4/7点は、公式採点方式にアクセスしない独立の人間数学者パネルによる非公式な再採点であり、合計33点相当という数字も参考値にとどまる。

何が効いて、何が効かなかったのかは、この論文の実務的な価値がもっとも凝縮された部分である。

区分 内容
効いたもの 相補的な事後学習モデルのアンサンブル（開発セット30問の累積独立審判スコアはアンサンブル188、RL 180、SFT 165、未改変のGA 162）、全員一致の厳格な検証、有望候補を保持する洗練、最終選抜への大きな計算配分
効かなかったもの 凝ったルーティングや複数証明の融合（cross-proof contextは42問でベースライン44問に届かず）、ゼロ判定優先のランキング、攻めの足切り（3判定トリアージは判定コストを95.3%削減する一方、後により正解へ育つ第1ラウンド祖先を44%のケースで捨てた）
残された課題 モデル検証に共通する盲点（内部検証器と独立審判はいずれも約32点と推定し、公式30点とP3・P6で2点ずれた）、検証そのもののコスト、スコアの高さと検証の信頼性は別問題だという構造的な問題

とくに最後の課題は重い。受理された25件のうち23件は審判が7点を付けたが、1件は量化子の形式的な不備で6点、残る1件は列置換の対称性に関する誤った議論を含む0点の証明だった。この0点の証明には、どのチェックポイントも満点を付け、24判定の一致ルールでも捉えられていない。同じ種類のズレがP3とP6に集中して2点分の過大評価を生んだことは、ノイズではなく「モデルによる検証に共通の盲点がある」ことの証拠として提示されている。スコアが伸びるほど、その検証をそのまま最終判定に使う危うさも増す——AI審判を実務の意思決定に組み込む読者にとって、この論文自身のデータが最も有用な警告になっている。

読者への持ち帰りはこう整理できる。難問推論のコストと精度は、「良いモデルを1つ選ぶ」ことでは決まらない。生成・検証・洗練という役割を別々のモデルと計算予算に割り当て、誤りの見逃しと正解の切り捨てのコストが非対称であることを前提に検証の厳しさを設計する。この骨格は数学に依存せず、コードレビュー、法務文書の確認、設計レビューのように正解が一意でない長文タスクへそのまま移植できる。公開されたチェックポイント・データ・コード・ベンチマークは、その設計図を自分の手元で検証するための出発点になる。

参考資料

論文・公式リソース

関連論文

ニュース・背景

関連記事