Anthropic：Claude が大規模な形式検証を実施したオープンソース・ライブラリ

10月22日、人工知能企業Anthropic傘下のFrontier Red Teamは、大規模言語モデル（LLM）がすでに大規模な形式的証明を自動生成できる能力を有しているとする研究を発表した。同チームはTheoremと共同で、Claudeモデルを基盤として、RISC-Vアセンブリレベルにおいて100以上の実際のオープンソースライブラリについて、セキュリティ特性の形式的検証を実施した——これは、AIシステムがアセンブリレベルで本番環境向けソフトウェアを大規模に形式的に検証した、これまでで初めての事例である。証明構築の過程において、チームは意図せず、長期間見過ごされてきた複数のセキュリティ脆弱性を明らかにした。実験手法としては、GoogleのOSS-Fuzzに既存するコンパイル可能なファズテストケースを形式仕様へ変換し、シングルスレッド静的バイナリ、固定メモリ予算、RISC-V CPUアーキテクチャ、Linux実行環境といった制約条件下で、サイズ64MB以下の任意の入力に対して検証を実行した。