LLMにより大規模なソフトウェア形式検証が実現可能に

AnthropicとTheoremの研究チームは、大規模言語モデル「Claude」を用いて、123のオープンソースライブラリ(239のエントリポイント)を対象に、RISC-Vアセンブリコードレベルでセキュリティ特性の大規模な形式検証を世界で初めて実施した。チームはファズテストを仕様へと変換し、64MB未満のあらゆる入力においてクラッシュやメモリ安全性エラーが発生しないことを証明する約1億8000万行のRocq証明コードを自律的に生成させた。この証明の過程でClaudeは長年見逃されていた複数のバグを発見・修正したほか、Linuxカーネル内のzlib実装の検証やRust製Pythonインタプリタの等価性検証も成功させており、モデルの向上や証明の再利用により検証コストが削減され、実用的なソフトウェア開発への統合が進むとしている。