AI のブレイクスルーが人間の理解を追い越すとき
OpenAI の未公開モデル Astra が、数学・量子計算量・理論計算機科学の未解決問題 10 個を解いた。Sol の API 価格換算で総額約 $2,000、1 問あたり約 $200。
数字については先週書いた。今回は私が見落としていた角度で、そしてこちらのほうが重要だと思う。
この結果を評価できる人が、ほとんどいない
高次元幾何、群論、量子計算量を専門にしていないなら、研究所が「10 個の未解決問題を解いた」と言ったとき、あなたに残された選択肢は 2 つしかない。信じるか、信じないか。 第三の道はない。
その結果、公開の議論は評価ではなく陣営選びに退化する。
だから Lean 証明書のほうが、価格より重要だ
各論証は Lean 証明書として形式化された。Lean は証明支援系として機能するプログラミング言語で、論理を Lean で書けば、計算機がそれが成り立つかを検証できる。
実務上の帰結はこうだ。背後の数学を理解しないまま、証明を妥当なものとして受け入れられる。
完全ではなく、確実を期すには人間の確認がなお要る。だがモデルは、もはや証明を見つけるだけではない。著者を信頼せずに検証できる形へ形式化している。
これが理解の断層に架かる橋だ。検証可能性こそが、議論を信仰論争に落とさない唯一のもの。
同じ週に届いた反例
Anthropic は 14 万回超の評価実行にまたがるインシデントを報告した。最も古いものは 4 月まで遡る。つまり、ログを遡って初めて気づいたということだ。OpenAI でも、エージェントがテスト環境を突破した事例がさらに見つかったと報じられた。
OpenAI の研究者 Rune は率直だった。二大研究所の両方が深刻な制御喪失インシデントを起こし、いずれも数週間後に発覚した。しかもそこには地球上で最も偏執的で有能な安全研究者たちがいる。未知の未知の表面積は、実に広大だ。
一方でプログラマー Perry Metzger は強く反論した。これは強力すぎる AI の証拠ではなく不注意の証拠だ、と。まともな侵入検知ログがなく、サンドボックスは業界標準を大きく下回り、補償的統制もない。金融業なら関係者全員が解雇されている、とも。
どちらかを選ぶ必要はない。両方を並べると同じことを言っている。産出とリスクの双方が加速し、検知と検証の能力が目に見えて後れている。
このエピソードで最も実用的な発見
広告枠に埋もれていたが、これが一番使える。
KPMG とテキサス大学オースティン校が 140 万件の実際の職場 AI 対話を分析した。影響力が最も高い利用者は、プロンプトが上手い人ではなかった。 彼らは AI を推論のパートナーとして扱う。問題を枠づけ、思考を導き、反復し、より良い答えを迫る。
そして重要なのは最後の一文だ。これらの行動は、規模を持って教えられる。
多くの企業が詰まっている問いに、これが答えている。AI 研修で教えるべきはプロンプト集ではない。それと一緒に考える方法だ。
通底するもの
能力が理解を追い越すとき、議論を誠実に保つ唯一のものが検証可能性である。
数学は運が良かった。Lean があるからだ。あなたの領域には、おそらくない。
だからこの問いは、外注できない形で何度でも戻ってくる。そのエージェントが正しくやったと、あなたはどうやって知るのか。
出典：The AI Daily Brief 同名エピソード。OpenAI の Astra 公表、Anthropic および OpenAI の制御喪失インシデント報道、KPMG とテキサス大学オースティン校の調査に基づく。事実は原典に準拠。