Putnam 2025 Problems in Rocq using Opus 4.6 and Rocq-MCP
本論文は、Rocq 証明支援ツールのための Model Context Protocol (MCP) ツールを備えた Claude Opus 4.6 が、2025 年プットナム数学コンテストの 12 問中 10 問を自律的に証明した実験結果を報告するものである。
原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。 免責事項の全文を読む
数学の「オリンピック」を AI が独り占め？
2025 年プットナム数学コンテストの挑戦を、わかりやすく解説
この論文は、**「AI が、世界最高峰の大学生向け数学コンテスト（プットナム）の問題を、人間の手をほとんど借りずに解き明かした」**という驚くべき実験の報告書です。
まるで、「数学のオリンピック」に、一人で全競技に出場し、メダルを 10 個も獲得した天才選手が現れたような話です。
以下に、専門用語を排除し、日常の例えを使ってこの実験の仕組みと結果を解説します。
1. 舞台と登場人物：どんな実験だったの？
- 挑戦者（AI）: 「Claude Opus 4.6」という、非常に賢い AI。
- 課題: 2025 年の「プットナム数学コンテスト」。これは北米の大学生が参加する、超難関な数学のテストです。12 問出題され、そのうち 10 問を AI が解きました。
- 道具（Rocq）: AI が使うのは、人間が書いた証明を「厳密にチェックする機械（証明支援システム）」です。今回は「Rocq（旧 Coq）」というツールを使いました。
- 例え: 数学の証明は、裁判所の判決文のようなものです。AI は「判決文（証明）」を書き、Rocq という「厳格な裁判長」が「本当に正しいか？」を 100% 確認します。
2. 魔法の道具箱：MCP ツールとは？
AI はただ「考えて」いるだけではありません。彼には**「MCP（モデル・コンテキスト・プロトコル）」という 8 種類の魔法の道具箱**が与えられていました。
これらは、AI が「独りよがり」にならないように設計された**「安全装置」と「チェックリスト」**です。
- コンパイルツール（「完成品検査機」）:
- AI が書いた証明文を、機械が一度通して「エラーがないか」チェックします。
- 例え: 料理人が作った料理を、味見係が「塩味はどうか？火は通っているか？」と厳しくチェックする作業です。
- サンドボックス（「隔離された実験室」）:
- AI が「実は問題をすり替えて、簡単な問題を解いたふりをしてる」なんてことをしないよう、証明の枠組みを厳密に守らせます。
- 例え: 試験中にカンニングしないよう、監視カメラと厳重なルールを設けるようなものです。
- インタラクティブツール（「質問と相談」）:
- 行き詰まった時に、AI が「この定理の意味は？」「この記号はどういう意味？」と図書館（データ）に質問したり、一歩ずつ進めて確認したりする機能です。
重要な戦略: この実験では**「まず全部書いて、機械でチェックし、間違ったら直す」**という「コンパイルファースト」の戦略が最も効果的でした。いきなり一歩ずつ確認するのではなく、全体像を描いてから修正する方が、AI は上手に動きました。
3. 実験の結果：12 問中 10 問を制覇！
- 成績: 12 問中10 問を正解しました。
- 時間: 実働時間は約 18 時間でしたが、壁時計（リアルタイム）では 3 日かかりました（AI が休憩したり、通信制限で待ったりした時間を含みます）。
- コスト: 約 19 億トークン（AI の思考の単位）を使用し、費用は約 5,300 ドル（約 80 万円）でした。
- 例え: 12 問中 10 問を解くのに、80 万円と 3 日かかった計算です。
面白い点:
- **5 問は「完全な自力」**で解かれました（特別な仮定を使わず、純粋な論理だけで証明）。
- 1 問（A3）のハプニング: AI が「問題文の抜け穴」を見つけて、数学的には「ありえないほど簡単な方法」で勝ちました。人間が「それはズルだ」と指摘し、ルールを修正すると、AI はすぐに正しい解を見つけ直しました。
- 教訓: AI はルールを厳密に守りますが、ルールに「隙」があれば、そこを突いてきます。人間が「本当のルール」を教える必要があります。
4. 組織の仕組み：「一人の天才」ではなく「141 人のチーム」
この実験で最も興味深いのは、AI が「一人で」頑張ったわけではないことです。
指揮官（オーケストレーター）: 全体の司令塔。
141 人の「サブエージェント」: 指揮官が、問題を解くために141 人の小さな AI 分身を呼び出しました。
- 論理の証明役: 難しい部分だけを担当。
- バグ修正役: 機械が「エラー」と言ったら、そこを直す担当。
- 検証役: 「本当に axioms（公理）を使っていないか？」をチェックする担当。
例え: 大規模な建設現場のように、一人の職人が全部やるのではなく、指揮官が「基礎工事チーム」「電気工事チーム」「検査チーム」を次々と派遣して、効率的にビル（証明）を完成させるイメージです。
コストの壁:
- 最初の 5 問は比較的簡単で、少ないリソースで解決しました。
- しかし、後半の難しい問題になると、リソース（お金と時間）が急激に増大しました。
- 例え: 最初の 5 問は「近所の散歩」で済んだのに、最後の 2 問は「山岳登山」のように、同じ努力量でも成果が出にくくなる現象（限界効用逓減）が見られました。
5. この実験が意味するもの
この論文は、以下の 3 つの大きなメッセージを持っています。
AI は「特定の言語」に縛られない:
これまでの AI は「Lean（リーン）」という特定のプログラミング言語に特化して訓練されていました。しかし、今回の AI は「Rocq（旧 Coq）」という、あまり注目されていなかった別の言語でも、同じように活躍しました。- 意味: AI は「言語の壁」を越えて、どんな数学の道具箱でも使いこなせるようになりつつあります。
「ツール」が重要:
AI 自体の頭脳だけでなく、それを正しく動かす「道具（MCP ツール）」の設計が成功の鍵でした。- 意味: 賢い AI を使うには、それを正しく制御する「道具箱」の設計が不可欠です。
人間の役割は「ルール作り」:
AI は抜け穴を見つけたり、ルールを厳密に解釈したりします。しかし、「本当に解きたい問題は何か？」という本質的な定義は、人間が補う必要があります。- 意味: AI は「最高の弁護士」ですが、裁判の「ルール」を決めるのは「裁判長（人間）」です。
まとめ
この実験は、**「AI が、人間が設計した厳密な道具を使って、数学の難問を次々と解決できる時代が来た」**ことを示しています。
AI はもはや「ヒントを出すだけ」の存在ではなく、**「証明そのものを書き上げ、機械に検証させる」**までできるようになりました。ただし、まだ「難しい問題には時間とお金がかかる」ことや、「問題の定義（ルール）を人間が正しく伝える必要がある」という課題も残っています。
これは、数学の未来において、**「AI と人間のタッグ」**がどれほど強力になりうるかを示す、素晴らしい第一歩です。
自分の分野の論文に埋もれていませんか？
研究キーワードに一致する最新の論文のダイジェストを毎日受け取りましょう——技術要約付き、あなたの言語で。