「バグのないソフトウェア」の実現を目指してAnthropicが「AIを用いて数学的にバグがないことを証明する」という手法を開発

AIの高性能化によって、さまざまなソフトウェアのバグが大量に発見されており、PHPの緊急アップデートのように大きな影響を及ぼす事例も現れています。そんな中、AI企業のAnthropicが「ソフトウェアにバグがないことを形式的検証で証明する」という手法に取り組んでいることを明らかにしました。

LLMs are making formal software verification feasible at a much larger scale \ Anthropic
https://www.anthropic.com/research/formal-verification

「形式的検証」はソフトウェアのコードを数学的手法で表現してバグがないことを証明する手法です。形式的検証というアイデア自体は新しいものではありませんが、実際の証明作業には多くの労力を費やす必要があるため「飛行機に搭載される航空電子機器コード」といった致命的な影響を及ぼすシステムでのみ採用されてきました。

Anthropicは研究組織のTheoremと協力し、Claudeを用いて形式的検証を実施する手法を開発し、123個のオープンソースライブラリを対象に形式的検証を実施。証明中に見つかったバグをClaudeで修正し続けた結果、「プログラムがRISC-VアーキテクチャのCPUとLinuxを搭載したマシン上で、メモリ使用可能量を固定した状態でシングルスレッドの静的バイナリとして実行される」という条件においてバグによるクラッシュが発生しないことを数学的に証明できたそうです。

形式的検証の実行には1億トークン以上を費やすため、コスト面での課題が存在します。しかし、Anthropicは「モデルの性能向上に伴って処理トークン数は減少する」「異なるソフトウェアでも同様の証明過程を踏む場合があり、証明内容を再利用することで処理トークン数を削減できる」といった理由からコスト問題は徐々に緩和されると推測しています。以下のグラフは36件形式的検証を実施した際のトークン使用量の推移を示しており、Claude Opus 5.5がClaude Opus 5と比べて少ないトークン数で成果を上げていることが分かります。