検証できる出力が、すでに機能している分野
AIの導入が進まない理由は、モデルの賢さとはほとんど関係がない。企業は、確かめようのない出力を使えない。しかも人手による確認は、出力の量が増えるよりずっと早く限界に達する。アナリストは一段落なら注意深く読める。だが1万段落を読む人間はいない。企業のAI活用の多くは、ここで座礁する。
一部の業種は、この問題を最初から抱えていない。数十年前から、機械による検証を仕事の流れに組み込んできたからだ。もっともわかりやすいのが半導体設計である。形式検証（formal verification。仕様どおりに動くことを、一件ずつのテストではなく数学的な証明によって確かめる手法）のツールは、回路が仕様書の記述どおりに動くことを数学的に証明する。この基盤は、そこに言語モデルを使おうと誰かが考えるよりずっと前から存在していた。
その結果は、こうした企業が実際に出荷している製品に表れている。Cadenceは5月のCOMPUTEXで、自社の設計エージェントを完全な自律動作にまで拡張したと発表した。このエージェントは同社の「Jasperフォーマル検証エンジン」に対して数百回のシミュレーションを走らせ、5週間かかっていた検証のループを1日未満にまで圧縮する。Synopsysも、同じ種類のツールをVC Formalとして販売している。設計を1件ずつテストするのではなく、静的解析（対象を実際に動かさずに解析する手法）によって正しさを証明する製品だ。
これほど速く動けるのは、半導体業界が大胆だからではなく、損得の計算が合うからだ。半導体の設計者は、機械の出した答えを自動で、しかも安く確かめられる。だから、誤った答えを見つけ出す費用はほとんどかからない。
同じ構造は、証明義務（正しさを形式的に示すことがあらかじめ求められている条件）がすでに存在する場所ならどこでも成り立つ。暗号、人命に関わる安全性が要求されるソフトウェア、ハードウェア検証は、いずれもその構造を共有している。この検証の層を握っている企業こそ、AIの出力が増えるほど製品の価値が上がる。人手による確認を破綻させるのは、まさにその量だからだ。
難問の答えを出す費用は、ほぼゼロにまで下がった。そして制約は、その答えが正しいと証明することのほうに移った。
