AIの満点主張は6件、公式採点は2件のみ

満点を主張したAIは6件、公式採点は2件のみだった

7月16日、上海で国際数学オリンピック（IMO）が閉幕しました。666名が参加し、42点満点を獲得した生徒は7名でした。

ところが、その翌週はさらに騒がしくなりました。わずか1週間のあいだに、6つのAIシステムが「自社も42点満点だった」と相次いで発表したからです。ファーウェイ（華為技術）、小紅書（RED）、そして独立したテストから出た4つのモデルに至るまでです。

しかし、この6つのうち、IMO主催者側に実際に答案を提出したのは2件だけでした。残りは公式採点の枠外での結果です。これにはClaudeベースのエージェントが採点したテストや、AxiomProverによるLean 4形式証明が含まれます。公式採点とは検証方式がそもそも異なります。

いまAIの評価に不足しているのは、より難解な問題ではありません。「答案を誰が、どのような条件で、どう採点したのか」を記録として残す手続きです。スコアだけを公表するベンチマークではなく、受験条件と検証手続きを備えた試験が必要だということです。

---

満点の主張は6件、受験条件はまちまちだった

人間の側の成績は極めて明確です。666名中7名が満点。生徒たちは2日間にわたり、計9時間をかけて6問を解きました。同じ日の、同じ時間に、同じ部屋でです。対するAI側は、次のように分かれます。

公式採点ルート：ファーウェイのCeliaと小紅書のdots-note-3.0は、人間の大会が終了したあとに問題を受け取り、規定の時間内に答案を提出して、その答案をIMO主催者側に渡しました。小紅書は「いかなる形態の人間の介入も厳格に禁止した」と明かしています。

独立テストルート：下の表には、研究者が独自に構築したテスト環境の結果と、Axiom Mathが公開したAxiomProverの形式証明の結果がまとめられています。

モデル	初回試行	最終	コスト	所要時間
Claude Fable 5	42/42	42/42	約51ドル	2.5時間
GPT-5.6 Sol (xhigh)	39/42	42/42	約21ドル	3.8時間
Kimi K3	36/42	42/42	約31ドル	17.4時間
AxiomProver	形式証明	42/42	非公開	約25時間

数字だけを見れば確かに驚くべき結果です。Fable 5は1回で解ききり、生徒たちに与えられた9時間の3分の1もかかりませんでした。AxiomProverは毛色が異なり、Lean 4¹という形式証明言語を用い、6問を計7,722行にわたって機械検証可能な証明として組み上げました。問3の1問だけでも4,229行、869分を費やしています。

しかし、この表を見ながら私が終始引っかかっていたのは、成績ではなく条件でした。

自然言語で書かれた解答をAIエージェントが採点した結果と、Lean 4で証明を検証したAxiomProverは区別して見る必要があります。推論努力（effort tier）の設定次第で、同一モデルのスコアが11点も変動しました。そして最も腑に落ちない点がひとつあります。同一のテストにおいて、MetaのMuse SparkとDeepSeek V4 Proが、問3でまったく同じ誤答を出したのです。

人間の試験会場であれば、これは即座に調査の対象となります。同一の誤答が出た理由を追加で確認しなければならないからです。学習データが重複していた可能性もありますが、誤答が同一であるという事実だけで、独立して解いていなかったと結論づけることはできません。しかしベンチマークには、そうした事態に対処する手続きそのものが存在しません。単にどちらも「誤答1問」と記録されて終わりです。

---