QED-Nanoは「小さいのに強い」をどこまで証明したのか

2026年4月7日2時44分（JST）にarXivへ公開された「QED-Nano: Teaching a Tiny Model to Prove Hard Theorems」は、4Bという小型の公開モデルを、数学オリンピック級の長い証明生成に特化して鍛えた研究だ。重要なのは、論文だけでなく、モデル本体、学習用データセット、評価コード、訓練パイプラインまで公開している点である。巨大な非公開システムが数学で注目を集める流れの中で、「再現できる公開系でもここまで来られるのか」を正面から問う仕事になっている。 (arxiv.org)

この研究の背景には、数学AIの評価軸が「最終解が合っているか」から「証明そのものがどれだけ厳密か」へ移ってきた事情がある。Google DeepMindは2025年のIMOで、自然言語のまま5問を満点で解き、35/42点の金メダル水準を達成したと報告している。一方で、同社が公開したIMO-Benchは、400問の短答式だけでなく、60問のIMO-ProofBenchと1,000件の採点データを含み、証明文の質そのものを測る基盤を整えた。QED-Nanoは、まさにこの「証明を書けるか」が問われる時代に出てきたモデルだ。 (deepmind.google)

QED-Nanoの立ち位置を理解するうえで大切なのは、これがLeanのような形式証明系ではなく、自然言語で証明を書くモデルだということだ。公式のHugging Face上でも、Lean 4の証明生成やPythonなどのツール利用を目的に学習していないと明言されている。これは、Lean 4上でカーネル検証可能な証明を狙うDeepSeek-Prover-V2のような系統とは別の方向性であり、厳密な自動検証よりも、人間が読む数学的議論の構成力を伸ばす設計だといえる。両者は「数学推論」では近いが、目指す出力の形式はかなり違う。 (huggingface.co)

学習パイプラインの第1段階は、Qwen3-4B-Thinking-2507を土台にした教師あり微調整（SFT）である。教師にはDeepSeek-Math-V2が使われ、4,300の一意な問題を含むFineProofs-SFTで、思考過程とLaTeX形式の証明を蒸留している。このデータセットは全体で7,777サンプルを持ち、Gemini-3-Proによる0〜7点の採点、Qwen3-4Bベースのdifficulty/reward推定、競技種別メタデータまで含む。しかもIMO-ProofBenchやProofBenchとの重複は除かれており、単に答えを覚え込ませたのではなく、証明の書き方そのものを学ばせる設計が見える。 (huggingface.co)

第2段階では、5,227問から成るFineProofs-RLを使い、ルーブリックに基づく0〜7点の報酬で強化学習を行う。問題はAoPS由来が3,794問、オリンピック由来が1,433問で、図や画像が必要な問題は除外されている。ここで効いているのが、論文の中核である“reasoning cache”だ。著者らはこれを、長い証明を要約と再精緻化の反復に分解し、長い推論をそのまま一息に生成するのではなく、短い学習ステップを積み重ねて扱えるようにする仕組みとして説明している。難しい問題をそのまま押し切るのではなく、長距離走を区間ごとに走らせる発想に近い。 (arxiv.org)

結果はかなり興味深い。QED-NanoはIMO-ProofBenchで40.0、ProofBenchで44.9、IMO-AnswerBenchで67.5を記録した。ベースのQwen3-4B-Thinking-2507はそれぞれ20.4、19.5、55.8なので、特に証明生成では大幅な改善だ。IMO-ProofBenchではQwen3-235B-A22B-Thinking-2507の34.1を上回り、Nomos-1の40.3やGPT-OSS-120Bの43.1にもかなり近い。一方で、モデルカード冒頭にはGPT-OSS-120Bに「匹敵」とあるものの、詳細表の数値を見る限り、正確には“到達”というより“肉薄”と表現するのが妥当だろう。さらに、1問あたり100万トークン超まで推論を伸ばすエージェント版ではIMO-ProofBenchが54.0まで上がり、同じ足場をベースモデルに載せてもほぼ伸びないことから、単にテスト時計算を増やしただけではなく、追加学習がその計算を活かせるようにしたことが分かる。 (huggingface.co)

再現性とコストの話も、この研究の読みどころだ。公開GitHubにはデータ生成、SFT、RL、評価の一式がそろっている。SFT段階は8基のH100で5時間、RL段階は8xH100のノードを生成7・訓練4・採点1で使い、4日間、計9,216 H100時間を要した。コミュニティ欄でLewis Tunstallは、H100を1時間3ドルと仮定したラフな見積もりとして、QED-Nanoを端から端まで作る費用は約2.8万ドルだと述べている。もちろん個人には軽い額ではないが、4Bの公開モデルで、しかも重み・データ・コード込みでここまで開示された例としては、たしかに「研究可能なコスト帯」に引き寄せた意義がある。 (github.com)

ただし限界もはっきりしている。QED-Nanoは定理証明専用のドメイン特化モデルで、一般アシスタントとしては使わないよう明記されている。データも英語・テキスト中心で、図形問題は除外され、採点にはGemini-3-Proやgpt-oss-20bの自動評価が入るため、人間評価と完全に一致するわけでもない。また、Leanや外部ツールと結びついていない以上、出力の正しさは最終的に人間や別の検証器が確認する必要がある。その意味でQED-Nanoは「形式検証の代替」ではなく、「公開小型モデルでも長い数学的議論をかなり書ける」ことを示した一歩と見るのがよい。今後の本命は、DeepMindが示唆するように、自然言語の柔軟さと形式検証の堅牢さをどう接続するかにあるだろう。QED-Nanoは、その接続点に向かうための、かなり実務的で再現可能な足場を置いた。 (huggingface.co)

主な出典は、QED-Nano論文、Hugging Faceのモデルカード／データセットカード、公開GitHubリポジトリ、IMO-BenchおよびGoogle DeepMindの公式資料である。 (arxiv.org)