10月23日、The Decoderが「Anthropic's Claude now writes code and proves it safe automatically」と題した記事を公開した。Claudeを使って123のオープンソースライブラリを形式検証するAnthropicの取り組みを紹介している。10年以上見逃されていたバグの発見、通常1年分のセキュリティバグを1週間で検出——その成果は、形式検証の常識を揺さぶるものだ。
形式検証の「20人年の壁」
ソフトウェアの「形式検証（formal verification）」——プログラムがあらゆる条件下で正しく動作することを数学的に証明する手法——は、長年にわたってコストの壁に阻まれてきた。小規模なOSカーネル「seL4」の検証だけで専門家チームが20人年を要したという事実が、その困難さを端的に示している。実用されてきたのもAirbusの航空機用ソフトウェアのような、命がかかった極限的なケースに限られてきた。
Anthropicとパートナー企業のTheoremは、この証明作業をClaudeに委ねる実験を行った。結果、Claudeはわずか数週間で約1億8000万行の数学的証明コードを生成した。対象はGoogleのセキュリティプロジェクトOSS-Fuzzから取得した123のオープンソースライブラリのテストプログラムだ。
Claudeの証明プロセス：クラッシュテストを数学問題に変換する
Claudeが行ったのは新しいコードを書くことではなく、既存コードの形式検証だ。具体的には以下の流れで動作する。
- クラッシュテスト（fuzzテスト）を数学的な問題に変換する
- コンパイル済みの機械語コードを解析する
- 大量の証明を生成する
- 証明の正しさを独立した検証プログラム「**Rocq**」が自動チェックする
Anthropicはこれを「完全自律的な証明生成」と呼んでいる。ただし、ツールと形式的な基盤はTheoremの人間チームが構築したものだ。
10年間見逃されていたバグを発見
実用上の成果も出ている。証明生成の過程でClaudeは数百件のバグを検出し、自ら修正することも許可された。これらの多くは「特定の大きさの入力ファイル」や「特定のアクセス順序」のような極めて限定的な条件でしか再現しないバグであり、通常のテストでは見落とされやすいものだ。
広く使われているPDFリーダーの検証では、通常1年かけて報告される数のセキュリティバグを1週間で発見した。別のアプリケーションでは、10年以上見逃されていた論理エラーを検出している。完全な証明に失敗した場合でも、その試みの過程で実際のバグが浮かび上がることがあるとAnthropicは述べている。
限界は明確：「形式検証済み」≠「完全に安全」
Anthropicは「形式検証済み」が「エラーゼロ」を意味しないと明言している。証明が成立する条件は厳格で、以下の制約がある。
- 特定のプロセッサアーキテクチャに限定
- シングルスレッドプログラムのみ
- 入力サイズ64MB以下
実際のライブラリは異なるハードウェアや構成で動作するため、証明の適用範囲は限られる。
計算コストも重い。個々の証明が数億トークン規模に達することがあり、プロジェクト全体のコストはAnthropicが公表していない。ただし、小規模な試験では証明の再利用が可能であることが確認されており、モデルの効率も改善している。元記事によれば、より新しいモデルは旧モデルと比べ約40%少ないトークンで半数の証明を解決できることが示されているという。
次のターゲットはglibc、OpenSSL、cURL
Anthropicは、AIを活用した形式検証が近い将来、通常のテストと同じくらい一般的になると予測している。Theoremのロードマップにはすでにglibc、OpenSSL、cURLといったクリティカルなインフラライブラリが対象として挙げられている。
「AIはコードを書けるか？」という問いはすでに過去のものになりつつある。今問われているのは「AIは既存コードの安全性を数学的に証明できるか？」だ。
詳細はAnthropic's Claude now writes code and proves it safe automaticallyを参照していただきたい。
