AnthropicはパートナーのTheoremと共同で、AIモデル「Claude」を使い、既存のソフトウェアコードが正しく動くことを数学的に証明する取り組みを行いました。対象はGoogleのセキュリティプロジェクト「OSS-Fuzz」に含まれる123のオープンソースライブラリです。数週間で約1億8000万行の証明用コードが生成され、従来のテストでは見逃されていた数百件のバグも見つかったとされています。
「テストに通った」と「正しいと証明された」の距離
ソフトウェアの品質確認といえば、多くの人が思い浮かべるのはテストでしょう。用意した入力を与えて、想定どおりの結果が返ってくるかを確かめる作業です。ただ、テストで確認できるのは「試した範囲」だけ。試していない状況でどう動くかまでは教えてくれません。
そこで登場するのが形式検証です。プログラムの振る舞いを数学の問題として扱い、定めた条件の範囲では必ず正しく動くことを証明します。理屈としては強力ですが、手間が桁違いでした。小規模なOSカーネル「seL4」の検証だけで、専門家チームが延べ20人年を費やしたとされています。旅客機の制御ソフトのような極端なケースに使い道が限られてきたのも、無理のない話です。
今回、AnthropicのFrontier Red TeamはTheoremと組み、この証明作業をClaudeに任せました。新しいコードを書かせたのではありません。すでにあるソフトウェアを対象に、クラッシュを調べるテストを数学的な問題へ置き換え、コンパイル後の機械語まで解析して、大量の証明を組み立てさせたのです。
証明の「採点役」は別のプログラム
AIが自分で書いた証明を自分で「合格」と言っても、説得力はありません。この点で興味深いのが採点の仕組みです。生成された証明は、Rocqという独立した検証プログラムが自動でチェックします。Anthropicによれば、このプロセスに人間のレビュアーはほとんど必要ないといいます。
研究チームはこれを「完全自律」の証明生成と呼んでいます。ただし、証明に使うツールや形式的な土台はTheoremの人間が作ったものです。AIが全部をゼロから生み出したというより、人間が整えた土俵の上で、AIが膨大な量の証明を一気に書き上げた、と捉えるほうが実態に近いでしょう。
証明の途中で見つかった数百のバグ
証明を進める過程で、Claudeは数百件のバグに行き当たり、自分で修正することも許されていました。研究者によれば、その多くは極端に大きな入力ファイルや、特定の順序でのメモリアクセスなど、ごく限られた条件でしか表に出ないものです。通常のテストをすり抜けても不思議ではありません。
具体例も挙がっています。広く使われているPDFリーダーの検証では、そのソフトで通常1年かけて報告されるのと同じ数のセキュリティバグが、1週間で見つかりました。別のアプリケーションでは、10年以上気づかれていなかった論理エラーも発見されたといいます。
もうひとつ見逃せないのが、証明が最後まで完成しなかった場合の扱いです。Anthropicは、証明に失敗しても、その試行の途中で実際のバグが浮かび上がると説明しています。証明は「合格証」を出すためだけの作業ではなく、バグを掘り出す探査機のような役割も果たすわけです。通常のテストと置き換えるより、足りない部分を補う関係に見えます。
「形式検証済み」の射程を読み違えない
とはいえ、「形式検証済み」を「不具合ゼロ」と読み替えるのは危険です。Anthropic自身も、証明が成り立つのは厳しい条件の内側に限られると認めています。想定されているのは特定のプロセッサー構成、単一スレッドで動くプログラム、64MB未満の入力です。現実のライブラリは、さまざまなハードウェアや設定で動いています。
コストも軽くはありません。個々の証明に使われるトークン量は数億に達するケースがあるとされています。プロジェクト全体の費用は公表されていません。一方で、小規模な追加実験では証明が再利用できることが示され、新しいモデルほど効率が上がる傾向も見えています。Opus 5.5は、証明の半分を解くのに必要なトークンが、Opus 5より約40%少ないとされています。
問いは「プログラムを書けるか」から変わる
AIがコードを書き、その正しさを条件付きで保証できるなら、問いの立て方が変わります。「AIはプログラミングできるか」ではなく、「AIは自分が書いたコードの安全性を証明できるか」。AI生成コードの信頼性に不安を感じる開発現場にとって、この転換は小さくありません。AIが自分でコードを検証できれば、人間のレビュー負担も減り、検証だけでなく開発工程全体のコスト削減につながる可能性があります。
Anthropicは、AIによる形式検証が近い将来、通常のテストと同じくらい当たり前の手段になると見込んでいます。Theoremのロードマップには、glibc、OpenSSL、cURLといった重要インフラ級のソフトウェアが対象として含まれています。
ここで大事になるのは、証明の「中身」ではなく「前提」を読む目でしょう。どんな環境で、どんな入力を想定した証明なのか。AIに検査まで任せる時代には、その前提を確認する人間側のリテラシーこそが、安全性の最後の砦になりそうです。
コメント