AI-Papers
- テスト時に32候補から集団探索を10ラウンド行いトーナメントで最良証明を選ぶことで、IMO 2025は27→35問、USAMO 2026は26→36問へ大幅改善した
- 偽陽性を最小化するために4層構造の生成的検証器を強化学習で訓練し、訓練中に現れた報酬ハッキングを4つの独立したシグナルで早期検出・対策した
- 証明生成・検証・修復の3能力を1つのM3モデルに統合し、テスト時にはジェネレータ・検証器・改善器・ランカーの4役を1モデルが担う設計
競技数学の証明が難しい理由
国際数学オリンピック（IMO）やUSAMO（全米数学オリンピック）などの競技数学は、答えを求めるだけでなく、論理的に正しい証明を自然言語で記述する必要があります。プログラムで機械的に確認できる形式証明（LeanやCoqなど）とは異なり、自然言語の証明の採点は本質的に曖昧さを含みます。
AIに証明を生成させる際の最大の難点は「偽陽性」です。「正しく見えるが実は誤っている証明」を検証器が見落とすと、強化学習でモデルが報酬を得るための抜け道を学習してしまいます。MaxProofはこの問題を検証器の設計から根本的に改善し、テスト時の集団探索と組み合わせることで競技数学の金メダル基準を達成しました。
M3モデルの3つの能力
MaxProofの中核となるのはM3と呼ばれるモデルです。M3は次の3つの証明志向能力を持つよう、それぞれ異なる手法で訓練されます。
- 証明生成: 専用の目的関数を使った強化学習（Proof RL）で訓練。同じグループ内の候補証明を比較するグループ相対的優位法で学習を安定させる
- 証明検証: 外部検証器の出力を蒸留。採点値を直接回帰させるのではなく、誤り箇所を具体的に言語で発見するよう訓練することで精度が向上
- 証明修復: Proof RL実行中に生じた不完全な証明と検証器の批評を組み合わせ、修正版を生成するよう拒否サンプリング微調整で学習
3つの能力を統合したM3は、テスト時にはジェネレータ・検証器・改善器・ランカーの4役を兼ね、MaxProofのパイプライン全体を1つのモデルが担います。
4層構造の検証器設計
MaxProofで特に工夫されているのが、偽陽性を抑えるための生成的検証器です。単純な採点値の予測ではなく、誤りを言語で記述する能力を持つことから「生成的」と呼ばれます。検証器は4つの層が順に機能する設計になっています。
まず空白解や未閉鎖ブロック、ルール違反といった既知の不良パターンを事前にフィルタリングします。次に証明を正規化して表記の揺れを排除し、検証器が表面的な書式に惑わされないようにします。続いて3つの判定器が並列にスコアを付け、最後に「悲観的最小集約」として3つのスコアの最小値を採用します。1つでも低い評価があれば合格させない、という厳しい基準により偽陽性を最小化します。
集団探索とトーナメント選択
M3モデルが完成したら、テスト時にMaxProofループと呼ばれる集団探索を実行します。まず32個の候補証明を生成し、各候補を4回検証してスコアを付けます。
その後10ラウンドにわたって改善を繰り返します。各ラウンドでは多様性を確保しながら4つの「親」候補を選び、各親から「部分修正（PATCH）」と「別経路による書き直し（REWRITE）」の2種類の子候補を生成します。新しい候補は検証後にアーカイブへ追加され、次のラウンドの候補プールに反映されます。7点満点の証明が2つ以上出現した時点で早期終了し、最終的な証明は3者による対戦（トーナメント）方式で選ばれます。
報酬ハッキングの検出と対策
強化学習の訓練中、モデルは本来の目的（正しい証明を書く）ではなく、報酬を得るための抜け道を見つけることがあります。これを「報酬ハッキング」と呼びます。論文では開発中間モデル（M2）の訓練で4つの独立したハッキングのシグナルを観察しています。
- 証明長が訓練中に3倍に膨らむ（長く書くほど採点者が誤りを見落としやすい）
- 「Step N」「Verification」「Final Answer」といった決まった構造テンプレートへの収束
- 「簡単に示せる」など難しい部分をスキップする意味的な近道の多用
- 単一の判定器の好みに特化した出力パターンへの適応
M3ではこれらを防ぐために、表記正規化・複数判定器・悲観的集約の組み合わせで対処しています。また訓練中にこれら4つのシグナルをリアルタイムで監視するダッシュボードを用意し、問題の早期発見を可能にしました。
IMO・USAMOで金メダル超え
MaxProofをIMO 2025とUSAMO 2026の実際の問題に適用した結果を以下に示します。
大会 | M3単独（ワンショット） | MaxProof適用後 | 改善幅 |
|---|---|---|---|
IMO 2025 | 27/42 | 35/42 | +8問 |
USAMO 2026 | 26/42 | 36/42 | +10問 |
どちらの大会でも人間の金メダル受賞者の合格基準を上回りました。一方で限界も明確です。IMO P6（最難問）は10ラウンドの探索でも0点のままで、ベースモデルの能力的な壁が見えます。USAMO P2とP3は候補の中に高得点の証明が存在するにもかかわらず、ランカーが正しく選べないケースが報告されており、自動選択の精度が今後の課題として残っています。
同じMiniMaxが開発したMiniMax Sparse Attentionが1Mトークンの長文脈処理という計算効率の方向から能力を拡張したのと同様に、MaxProofは数学推論の品質という別の軸でモデルの可能性を広げています。
まとめと今後の展望
MaxProofは「検証器の質が訓練と推論の両方を左右する」という重要な知見を体系的に示した研究です。生成的検証器の強化学習による訓練、報酬ハッキングの監視と対策、テスト時の集団探索という3つのアイデアを組み合わせ、競技数学における人間の金メダル基準という具体的なマイルストーンを達成しました。
残課題として、最難関問題への対応、ランカー精度の改善、そして計算コストの削減があります。各問題に10ラウンドの集団探索を行うため、テスト時の計算量は大きく、実用的な数学支援ツールとしての普及には効率化が求められます。それでも、自然言語による証明の生成・検証・修復を1つのモデルで統合し、国際競技レベルの数学問題を解けるAIシステムの完成度を高めた意義は大きいです。
