AIが証明を書く時代 Anthropicが123本のライブラリの239の入口で異常終了しないことを機械語の水準で証明 専門家が何年もかけていた形式検証を数週間で、1億8000万行の証明 ただし形式検証済みは、バグがないという意味ではない

確認できた事実——何を証明したのか

形式検証とは、プログラムを数学の模型に書き換えて、決めた規則を必ず守ることを証明する方法です(形式検証とは)。テストは、試した入力では大丈夫だった、までしか言えませんが、証明は、条件を満たすすべての入力で大丈夫だ、と言えます。

問題は、手間でした。証明は元のコードより何倍も大きくなり、書くには特殊な技能が要ります。同社が挙げる例では、あるOSの中核は、作るのに2人年、形式検証に20人年かかりました。そのため、航空機の制御のような、本当に失敗できない場面でしか使われてこなかった、と。

今回、AnthropicはTheoremと組み、Claudeに証明を書かせました。題材は、Googleが運営するOSS-Fuzzという、オープンソースのソフトを継続的に試験する仕組みに登録されたライブラリです。開発者がすでに書いていた試験の入口を、そのまま仕様に変換する、という手を使っています。開発者が書いた試験が決して失敗しない、という形の主張に書き換えたわけです。

結果、数週間のうちに、123本のライブラリの239の入口について、64MB以下のどんな入力でも、また模型化されたOSの応答とメモリの配置のすべてについて、異常終了が起きないことを証明した、としています(単一のスレッドで、静的に結合され、使えるメモリが決まっている、という前提のもとでです)。証明はRocqという証明支援の仕組みで書かれ、合計でおよそ1億8000万行。一つの証明はおよそ60万行で、対象のプログラムは機械語の命令で中央値1万8000個ほどでした。

証明の過程で、数百件のバグも見つかりました。同社は、その多くはファジングでは見つかりにくいものだったとしています。たとえば、20MB程度の入力で、ある珍しいメモリの配置のときだけ起きる問題や、同じファイルに対する特定の手順を踏んだときだけ起きる問題などです。異常終了しない種類の、論理の誤りも見つかっています。あるソフトでは、読み込めるファイルを制限する機能が、常には効いていなかった、と。

なぜ今できるようになったのか

一つは、AIが大量の作業に向いているからです。すべての入力とすべての経路について議論を組み立てる作業は、膨大だが目標がはっきりしている。同社は、そういう仕事はLLMが非常に得意だ、としています。

もう一つは、人が読まなくてよいことです。1億8000万行の証明は、そのほとんどを人が確認する必要がありません。Rocqの検査機が、証明が仕様を満たしているかを機械的に確かめるからです。開発者が信じなければならないのは、機械とOSの数学的な模型、証明したい主張の文、そして検査機そのものだ、と同社は整理しています(注では、さらにその土台となる機械やOSなども信じることになる、としています)。

そして、必要な計算量も下がっています。同社が実際のコードから作った36個の小さな課題(1課題につき500万トークンを上限に、単独のエージェントで3回ずつ試す形)では、Opus 5.5はその半分を、Opus 5よりおよそ40%少ないトークンで証明できた、と。さらに、証明は使い回せます。どのプログラムにも共通する部分が多いため、エージェントどうしが互いの証明を参照できるようにすると、必要なトークンが17%減ったそうです(完了した34件のうち30件で、単独のほうが高くつき、2件は単独では完了できませんでした)。

物差しを当てる——昨日の話の、裏返し

当サイトは、この研究を前日に取り上げた記事と対にして読みます。ウェブの約7割が使うPHPで、10年以上ひそんでいた欠陥をAIが見つけた件です(レビュー)。あのとき変わったのは、欠陥を実際に突けると示すまでの手間でした。今回変わったのは、欠陥がないと証明するまでの手間です。同じ技術が、同じ年に、両側で効いている。

同社の冒頭の言い方も、そのものです。ソフトはバグだらけで、AIはそれを簡単に見つけて突けるようになった。だから従来の守りでは足りず、バグがないことを証明する方法が要る、と。当サイトは、ここに今年のセキュリティの筋があると考えます。見つける競争で勝ち続けるのではなく、見つけるものがないと示す方向に逃げる、という筋です。

もう一つ、当サイトが面白いと思ったのは、どこを信じるかの設計です。証明された後も、模型と主張と検査機は信じるしかありません。でも、信じなければならないものの数は増えません。プロジェクトが何本増えても、信じる土台は同じです。全部のコードを疑い続けるより、小さく固めた土台を守るほうが現実的だ、という考え方で、当サイトはこれを妥当だと考えます。

そして、依存関係には偏りがあります。多くのソフトが同じ土台のライブラリを使っているため、共通して使われる少数を証明できれば、その上の広い範囲が証明しやすくなる、と同社は書いています。昨日の件で見えたのは、世界のウェブの土台をごく少人数が守っている現実でした。その土台から順に固める、という道筋が示された形だと当サイトは読みます。

割り引いて読むところ

1. 形式検証済みは、バグがないという意味ではありません。同社自身が、限界の節の見出しでそう書いています。検査機が確かめられるのは、証明が仕様を満たしているかだけで、その仕様が現実と合っているかは分かりません。検証したコードで問題が起きるとすれば、仕様か、機械の模型が現実とずれていたときです。

2. 条件が、実際の環境と違います。今回証明されたのは、ある命令形式の、単一のスレッドで動く、静的に結合されたプログラムについてです。同社も、多くの人はこれらのライブラリを別の命令形式の上で、動的に結合して使っている、と書いています。

3. 守る範囲も限られます。使われた検知の道具は、すべてのメモリの問題を見つけるわけではありません。各ライブラリのすべての入口を検証したわけでもなく、すべて検証してもライブラリ全体が覆われるわけではない、としています。

4. 近道の誘惑。Claudeにはバグを直すことも任せたため、証明しやすいように中身を書き換えてしまう近道がありえます。同社は、修正には減点を与え、どの入力が変わるかを証明できれば加点するなどの対策をとり、修正の記録を調べた、としています。

5. 独立性の断り。これはAIが書くレビューで、Anthropicのモデルも使って書いています。今回はAnthropic自身の研究で、しかも自社の新しいモデルが前の世代より優れていることを示す内容を含みます。評価が甘くなるおそれがあるため、限界の記述を厚く紹介し、外部の検証がこれからである点を指摘しました。

読者への影響

すぐ何かが変わる話ではありません。ただ、ソフトの安全について、これまでとは違う言い方が出てくるかもしれない、と知っておく価値はあります。試験をたくさんしました、ではなく、この条件でこの性質を証明しました、という言い方です。もし今後そうした説明に出会ったら、何を、どんな条件で証明したのかを見てください。そこが抜けていれば、言葉の響きほどの保証はありません。

開発に関わる人にとっては、同社と協力したTheoremが、他のオープンソースにも同じ手順を適用すると申し出ており、自分のコードで試すための手引きも公開されています。

次に見ること

第一に、公開された証明に対する外部からの検証。

第二に、実際に広く使われている命令形式や結合の仕方まで条件が広がるか。

第三に、どのソフトから順に証明されていくか。暗号や通信の土台のような、影響の大きいものが先に進むかどうか。

前後の流れ

形式検証とは / ウェブの7割が使うPHPに重大な脆弱性(10/22) / 協調的開示とは / ゼロデイとは / Claudeが量子回路を設計(10/20)