解説
形式的検証とは何か ClaudeがAIコード証明を自動化した仕組み
AIが書いたコードをどこまで信頼してよいか、判断に迷う現場が増えています。Anthropicは、従来は一部の重要インフラにしか使われなかった「証明によってバグがないことを示す」手法を、AIモデルClaudeに任せる取り組みを公開しました。
何が起きたか
Anthropicの研究チーム「Frontier Red Team」は、パートナー企業Theoremと共同で、AIモデルClaudeに既存ソフトウェアの正しさを数学的に証明させる取り組みを実施しました。対象はGoogleのセキュリティ基盤「OSS-Fuzz」に登録された123件のオープンソースライブラリのテストプログラムです。Claudeはわずか数週間で、約1.8億行に及ぶ数学的な証明コードを作成しました。
具体的には、クラッシュテストを数学の問題に変換し、コンパイル後の機械語を解析したうえで、詳細な証明を組み立てる手順を踏みます。生成された証明は独立した検証プログラム「Rocq」が自動でチェックする仕組みで、Anthropicによれば人間のレビューはほとんど必要ありません。研究チームはこの手法を「完全に自律的な証明生成」と呼んでいます。
証明を作成する過程で、Claudeは数百件のバグに遭遇し、自ら修正も行いました。広く使われているPDFリーダーの検証では、通常1年間に報告される件数に匹敵するセキュリティ上の不具合を、わずか1週間で発見した例があります。また別のアプリケーションでは、10年以上見過ごされてきた論理エラーを検出したといいます。
背景・解説
ソフトウェアがあらゆる条件下で誤作動しないことを数学的に証明する手法は「形式的検証」と呼ばれます。通常のテストが限られたケースを個別に確認するのに対し、形式的検証は理論上すべての入力パターンを網羅して正しさを保証します。
ただしこの手法は従来、極めて高コストでした。小規模なOS基盤「seL4」を形式的に検証するだけでも専門家チームが20人年を要したとされ、採用されるのはエアバスの航空機用ソフトウェアのような極めて重要な領域に限られてきました。
Anthropicの取り組みは、この証明作業そのものをClaudeに任せる点が特徴です。人間が証明を一行ずつ組み立てる代わりに、AIが膨大な証明コードを生成し、Rocqという別の検証プログラムが正しさを機械的に確認します。
ただし「形式的に検証済み」は「無欠陥」と同じ意味ではありません。証明が成立するのは、特定のプロセッサアーキテクチャ、シングルスレッドのプログラム、64MB未満の入力という厳しい条件下に限られ、実際のライブラリは異なるハードウェアや構成で動くことが少なくありません。
計算コストも軽くはなく、1件の証明に数億トークンを要するケースがあるといいます。Anthropicはプロジェクト全体の総コストを公表していませんが、新しいモデルOpus 5.5はOpus 5に比べて約4割少ないトークン数で、同じ証明の半分を解けるようになったとしています。
仕事や業務への影響 — AI Topicaの見方
AIが生成したコードの検証コストは、条件を絞り込める業務ほど下がります。例えば、自社の在庫管理システムをシングルスレッドで動かし、取り扱うファイルサイズを常に64MB以下に抑えている中堅物流企業のシステム担当者なら、該当モジュールに限って形式的検証を使い、レビュー時間を減らす判断がしやすくなります。
一方で、複数スレッドで並行処理する業務システムや、サイズの大きいファイルを扱う画像・動画処理の現場では、今回示された条件に当てはまりません。該当しない業務については、従来通りのテストとレビュー体制を維持すべきです。
コスト構造にも目を向ける必要があります。1件の証明に数億トークンを要する以上、検証対象を絞らずに全社のコードへ一律適用するのは費用対効果が合いません。まずは障害時の影響が大きい決済処理や認証まわりのコードから着手するので十分です。
Theoremのロードマップでは、glibcやOpenSSL、cURLといった多くの企業が間接的に依存する基盤ライブラリが検証対象に挙がっています。これらが実際に検証されれば、自社で意識せずに使っているライブラリの安全性が底上げされ、情シス部門が個別に対応する負担は軽くなります。
不確かな点・注意
Anthropicはプロジェクト全体にかかった総コストを公表していません。「完全に自律的な証明生成」とされていますが、証明の土台となるツールや形式的な枠組みはTheoremの技術者が構築したものです。証明が成立する条件も、特定のプロセッサ向け・シングルスレッド・入力64MB未満に限定されており、一般的な業務システムにそのまま当てはまるとは限りません。glibcなど基盤ライブラリへの適用はロードマップ上の計画であり、実施時期や結果は明らかにされていません。