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

何が起きたのか

AIが高性能になり、多くのソフトウェアでバグが見つかっています。Anthropicは、研究組織のTheoremと協力して、AI「Claude」を使った形式的検証の方法を作りました。形式的検証とは、プログラムを数学の言葉で書き表し、バグがないことを証明する方法です。

主な数字と事実

• 対象は123個のオープンソースライブラリ
• 形式的検証には1億トークン以上を使う（トークンはAIが文章を処理する単位）
• 36件の検証でトークン使用量の推移を調べた
• 証明できたのは、RISC-Vという種類のCPUとLinuxを積んだマシン上で、特定の条件で動かした場合のバグによるクラッシュがないこと

なぜ今まで難しかったのか

形式的検証のアイデア自体は新しくありません。しかし、証明には多くの手間がかかります。そのため、飛行機の制御機器のように、失敗すると大事故になるシステムでしか使われてきませんでした。

なぜ大事なのか

AIでバグが見つかる数が増えると、修正が追いつかなくなります。形式的検証が広く使えるようになれば、ソフトウェアの安全性を大きく高められるかもしれません。ただし、Anthropicも限界を認めています。RISC-V以外のCPUでは、同じ証明が当てはまるとは限りません。実際の使用環境すべてを確かめる必要もあります。

今後の注目点

• コストが下がるかどうか（モデルが良くなると使うトークンが減ると見込まれている）
• 証明の内容を別のソフトウェアで再利用できるかどうか
• Armやx86など他のCPUへ広げられるかどうか
• TheoremがOSSプロジェクト向けに無償提供している手法が、どれだけ使われるか