生成AIで形式検証を実用化、&Truthなどが挑戦

生成AIを使い、ソフトウェアが仕様どおり動くかを数学的に確かめる「形式検証」を実用化する動きが広がっています。スタンフォード大学の研究者チュユエ・サン氏らは、Signalの暗号処理の一部を検証し、同氏が関わるスタートアップ&Truth;も事業を始めました。

形式検証では、プログラムが満たすべき条件を厳密に記述し、コードを数式に変換して正しさを確認します。従来は仕様作成に専門知識と時間が必要でしたが、AIで作業を自動化できれば、重大な欠陥を本番投入前に見つけやすくなると期待されています。

記事が紹介したサン氏らの研究では、AIツールが5カ月かけて熟練者3人が行ったエンジニアリング作業を、半日未満、500ドル未満で完了したと報告されました。&Truth;は7000万ドルを調達し、将来的に幅広いプログラミング言語の検証を目指します。HarmonicやAnthropicとTheoremも関連技術を開発しています。

一方、普及には費用、検証人材、導入にかかる時間が課題です。形式検証は設定した前提の範囲を扱うため、利用者の誤操作やハードウェア故障など、すべての不具合を捕捉できるわけではありません。検証済みのコードでも、別のテストで欠陥が見つかった事例があります。

AIが仕様作成まで担う場合、誤った仕様に基づく検証が過信を招く恐れもあります。形式検証は安全性を高める手段の一つですが、広範なテストや人による確認と組み合わせ、対象コードと前提を明確にして使う必要があります。