決めていたのは検証器だった — AI が数学で突き抜け、音楽で止まった理由

前の記事の宿題

AI は音楽の何を変えたのかで、「2026 年時点で『長年の謎が AI で解けた』と言える単独の大発見はまだ無い」と書いた。書いたあとで気になった。

では、他の業界ではどうなのか。

調べたら、ある。しかも極端にある。そして面白かったのは、その差が分野の知的な難しさと相関していないことだった。

数学では、実際に落ちている

2026 年 5 月、DeepMind の AlphaProof Nexus が、試行した 353 問の Erdős 問題のうち 9 問を自律的に解いた。うち 2 問は 56 年間未解決だったもので、1 問あたりの推論コストは数百ドル。

2025 年 10 月以降で見ると、AI は Erdős の未解決問題をおよそ 100 問片づけている。OpenAI のモデルが 80 年もの幾何学予想を倒し、23 歳が 60 年来の問題をチャットボットへの一度のプロンプトで決着させた例まである。AxiomProver は 2026 年の Putnam の全 12 問を自律的に解き、うち 8 問は公式の制限時間内に収めた。

数学は難しい。にもかかわらず、AI の成果が最も派手に出ている分野が数学だ。

静かに本番に入ったもの

• 気象 — ECMWF が AIFS を 2025 年 2 月に運用化、7 月に確率版。NOAA が 2026 年 1 月に追随。物理シミュレーションを機械学習が本番で置き換えた初の大規模例で、計算コストが桁で違う
• 材料 — DeepMind の GNoME が約 220 万の候補構造を予測し、約 38 万を安定と判定。Nature 論文の時点で外部の研究室が 736 個を実際に合成済み
• 核融合 — プリンストンがミリ秒単位でプラズマを制御する AI を実証。人間の操作者より遥かに速い
• 自動運転 — Waymo が米 4 都市で週 15 万回以上。Baidu の Apollo Go は中国 10 都市超で累計 1000 万回超
• 創薬 — 2026 年 7 月時点で 63 社の 117 の治療資産が臨床試験に入っている。ただし Phase 2 完了は 8 で、完全に AI 設計された薬の FDA 承認はまだゼロ

気象がいちばん地味で、いちばん広く使われている。毎日の天気予報の裏側が入れ替わったのに、ほとんど話題になっていない。

ところが、会社では

• Gartner（2026 年 4 月）— AI プロジェクトで ROI を完全達成できたのは 28%、20% は完全に失敗
• RAND — 80% 以上が本番運用に到達せず失敗。最大の原因はデータ品質
• BCG — 導入企業の 74% が PoC 成功後にスケールできていない
• 106 件の調査研究のメタ分析 — 人間と AI の組み合わせは、平均でパフォーマンスが低下する

最後のひとつが効く。使っている実感はあるのに、測ると下がっている。

並べて見えたもの

数学は難しい。企業の業務は、少なくとも数学よりは易しい。それでも結果は逆になっている。難しさでは説明がつかない。

並べ直して見えたのは、成果が出た分野に共通する 3 条件だった。

1. 検証器がある — 出力が正しいかを、機械的・客観的に判定できる
2. 構造化された大量データがある
3. 律速が探索の回数だった — 人間の手で試せる数がボトルネックだった

中でも決定的なのは 1 つ目だ。

分野	検証器	判定にかかる時間
数学	Lean 等の証明支援系	秒〜分
プラズマ制御	装置が安定するか	ミリ秒
気象	翌日の実際の大気	1 日
材料	実際に合成できるか	週〜月
創薬	臨床試験	年
音楽（生成・演奏評価）	無い	—
経営判断・教育	無い（あっても遅く、交絡が多い）	—

Lean が秒で判定するから数学は独壇場になり、臨床試験が年単位だから創薬は「速くなった」止まりになる。進度を決めているのは、AI の賢さではなく検証器の速さと安さだ。

誤答のコストがゼロになる

なぜ検証器がこれほど効くのか。理由は 3 つあると思う。

1. 誤答のコストがゼロになる。 Lean が通した証明は正しい。AI が 999 個の誤りと 1 個の正解を出しても、捨てるだけで済む。だから生成の精度が低くても総当たりが成立する。

検証器が無い領域では、誤りを選別するコストを人間が払うことになる。AI の出力が増えるほど、人間の負担が増える。 106 件のメタ分析で平均が下がったのは、たぶんこれだ。

2. 自己改善のループが閉じる。 検証器の判定をそのまま学習信号にできるので、人手のラベル付けなしに能力が上がる。AlphaProof も、プラズマ制御も、囲碁・将棋も、全部この形をしている。

3. 主張の真偽が交渉の対象にならない。 音楽の生成 AI と企業導入で起きているのは、まさにこれが成立していない状態だ。「良い曲か」「効果があったか」が判定できないので、議論は法廷と社内政治に移る。

音楽が、そのまま実例だった

この枠組みで前の記事を読み直すと、話がきれいに閉じる。

音源分離と自動採譜には検証器があった。分離結果は元のステムと比べられる。採譜結果は Disklavier の MIDI と比べられる。だから実用水準まで届いた。

生成と演奏評価には検証器が無い。「良い曲」「良い演奏」を判定する機械が存在しない。だから技術の話にならず、権利の帰属の話になった。

同じ分野の中で、検証器のある側だけが動いた。 音楽は、自分の主張の一番良い実例だった。

検証器には 4 つの型がある

型	例	特徴
形式検証	Lean、型検査、モデル検査	速く安く確実。適用範囲は狭い
物理実験	合成、臨床試験、走行試験	確実だが遅く高価
自然の答え合わせ	翌日の天気、市場価格	速く安いが、待つしかない
参照実装との差分	元のステム、既存処理系の出力	参照の質が上限を決める

音源分離と自動採譜は 4 番目にあたる。参照が存在したことが、音楽の分解側だけが動いた理由だった。

これは手元の話でもある

自作言語を作っていると、この話は他人事ではない。ゲートが緑かどうかで進退を決めているので、検証器の質がそのまま開発の質になる。

ただし 15 本のゲートが全部緑で、どれも訊いていなかった問いで書いたとおり、検証器は「あるかないか」だけでは足りない。何を訊いているかも同じだけ効く。全部緑でも、誰も訊いていない問いは残る。

分野の話に戻すと、これは「検証器を作れないか」という問いになる。自律実験室は、遅く高価だった物理実験の検証器をロボティクスで速く安くしようとする試みだ。CMU の Materials Innovation Cloud Lab のような環境が立ち上がっている。

逆に言えば、検証器を設計できない領域では当面この構図が続く。芸術、教育、経営判断、対人ケアがそこに入る。

結局のところ

AI が革新を起こしたのは「知的な分野」ではなく、答え合わせができる分野だった。数学が最も派手に成果を出しているのは、数学が難しいからではなく、証明が機械で検証できるからだ。

だから判断に迷ったときの問いは 1 つでいい。

この作業の出力が正しいかどうかを、人が判断せずに確かめる方法はあるか。

あるなら、AI を投入する価値は高い。無いなら、AI は速度ではなく「案の量」を増やす道具として使い、選別のコストを誰が払うのかを先に決めておく。

ピアノに話を戻すと、自分の演奏を MIDI で録って楽譜とアライメントを取るのは、検証器を自分で作る行為にあたる。そこまでは機械が手伝える。その先の「音楽的に良いか」には、まだ誰も検証器を持っていない。