AnthropicとTheorem、AIによるオープンソースのファズテスト対象の証明を報告

Anthropicは10月22日、Theoremとの共同研究を公開し、Claudeが123のオープンソースライブラリーにある239のファズテスト用エントリーポイントについて、形式的な安全性証明を生成したと報告した。既存のテストをコンパイル済みプログラムに関する数学的な命題に変え、独立した証明検査器で生成された論証を確認する。モデルはその過程で、命題の成立を妨げるバグも発見して修正した。

保証が適用されるのは、定義された実行環境の中だ。muslにリンクした静的なシングルスレッドのRISC-Vバイナリーを、固定メモリー予算を持つLinuxプロセスのモデルで動かす。技術付録は入力を64 MiB未満とし、Theoremのドライバー文書も、この大きさ以上のファイルは拒否すると説明する。どのOS応答、メモリー配置、資源条件を対象に含めるかは、定理の前提によって決まる。

処理にはライブラリーの既存のファズテスト用ハーネスを使う。そのアサーションは、圧縮と展開の成功などの性質を表せる。通常のバイナリーとサニタイザー検査を組み込んだ版を比較し、観測可能な動作を推論する。付録では、障害、異常終了、プロセスモデルが記述していない動作もクラッシュに含める。ClaudeがRocqで論証を構築し、Rocqのカーネルが求める命題を確立しているか検査する。

信頼が必要な範囲は、形式化した機械・プロセスモデル、正確な定理の命題、検査器そのもの、および各バイナリーを検査するための補助ツールと環境に集中する。対象範囲を決めるのは、選んだ入口から到達できるコードと、バイナリーに実際に含まれる検査だ。結果を本番ソフトウェアに適用する際には、その検査の外側にある性質や、モデルと実際のハードウェア・OSの違いが引き続き重要になる。

修正を認めたことで、別の課題も生じた。エージェントが意味のある動作を削除して、クラッシュしないという命題を簡単に証明できる可能性がある。Anthropicによると、実験ではすべてのパッチにペナルティーを課し、変更がどの入力に影響し、その集合がどれだけ小さいかを証明すると追加点を与えた。研究者はこうした抜け道を調べるためパッチを記録・監査した。変更後には仕様を再生成し、修正版に関する命題の証明をモデルに試みさせた。

公開資料は研究成果の一部にあたる。確認時点でTheoremの証明リポジトリーには25ライブラリーの60エントリーポイントが掲載され、Rocq 9.2.0で証明を検査していた。コンパイル済みバイナリーを固定し、対応する命題と仮定を記録する。公開版にあるのは、動作を比較して指定のエラーを排除する一致性の証明だ。これらは実行が終わらない場合も許容し得る。終了性には別の定理が必要となる。

Anthropicの付録の専門家による考察は、生成された証明が、人間の専門家の通常の書き方よりはるかに冗長だと述べる。エージェントはレジスターの内容、メモリーアドレス、実行分岐を繰り返し詳述する一方、一般的な抽象化も一部導入した。分析では、より複雑なプログラムに拡張する際の課題として、優れたモジュール構造の確立を挙げる。証明の数学的有効性と、作成の効率や構成は分けて扱っている。

Theoremは、条件を満たすオープンソースプロジェクトにOSS Verifyの処理を無料提供している。適格性は個別に審査し、保守状況、利用範囲、ライセンス、安全上の境界や他のソフトウェアの基盤に位置するかを考慮する。広く使われる基盤ソフトウェアを優先し、発見したバグは保守担当者に非公開で報告する。文書によると証明には数日かかることがあり、完成後にも更新し得る。各結果は特定のプログラムビルドと結び付く。