2025/12/17 6:14
Prediction: AI will make formal verification go mainstream
RSS: https://news.ycombinator.com/rss
要約▶
Japanese Translation:
記事は、人工知能がソフトウェアが仕様を満たしていることを数学的に証明する「形式検証」を、ニッチな研究活動から日常のエンジニアリング実務へと導くと主張しています。Coq、Isabelle、Lean、F*、Agda などの証明支援ツールはすでに OS カーネル、コンパイラ、暗号スタックなど大規模システムを形式的に検証することを可能にしています。現在では言語モデル型コーディングアシスタントが実装コードとそれに付随する証明スクリプトの両方をドラフトでき、極小の検証済みチェッカーは無効な証明を拒否し、AI エージェントが幻覚（hallucinate）した場合には再試行を強制します。2009 年に公開された seL4 マイクロカーネル（8,700 行の C コードで 20 人年と 20 万行の Isabelle コード）が示すように、従来は労力集約的な検証が行われてきましたが、世界中で数百人程度の専門家しかそのような証明を作成できず、コストはバグ修正費用を上回ることも多いです。著者は AI がこれらのコストを低減するにつれて、より多くのソフトウェアが形式検証され、人間によるレビューではなく AI 生成コードに依存するようになると予測しています。残された最大の障壁は正確な仕様書を書くことです——仕様書作成は証明より容易ですが、それでも専門知識を要します。AI は自然言語での要求を形式的に翻訳する手助けができるかもしれませんが、ニュアンスの損失リスクがあります。広範な採用はバグと脆弱性を削減し、エンジニアリングワークフローを再構築し、仕様書作成に関する新たなスキルを要求しますが、文化的受容こそが主流化への主要障壁となります。
本文
マーティン・クレップマン（Martin Kleppmann）著、2025年12月8日発表
AIがソフトウェア開発に与える影響については多く語られていますが、私がまだ目にしたことのない角度があります。それは「AIが長い間マイナーだった形式的検証を主流のソフトウェア工学へ導入する」という考えです。
Coq、Isabelle、Lean、F*、Agda などの証明支援ツールや証明志向プログラミング言語は長年存在します。これらを使うと、あるコードが満たすべき正式仕様を書き、そのコードが常にその仕様を満たしていることを数学的に証明できます（想定外のエッジケースでも）。こうしたツールはオペレーティングシステムカーネル、C コンパイラ、暗号プロトコルスタックなど、大規模な形式的検証済みソフトウェアを開発する際に使われています。
現在、形式的検証は主に研究プロジェクトで利用されており、産業界のソフトウェアエンジニアが使用するケースは稀です（医療機器や航空機などの高信頼性領域を除く）。その理由は、証明を書くことが非常に難しく（博士号レベルの専門知識が必要）かつ労力が大きいからです。
例えば 2009 年時点で、形式的検証済み seL4 マイクロカーネルは C コードが 8,700 行しかなかったものの、Isabelle のコードで 20 人年と 200,000 行を要しました。実装行一つにつき 23 行の証明が必要だったわけです。このような証明を書ける人は世界に数百名程度しかおらず、証明システムへの深い知識が必須です。
簡単に言えば：ほとんどのシステムではバグによるコストの期待値が、バグを排除するための形式的手法のコストよりも低くなります。バグは負の外部性であり（ソフトウェア開発者がその費用を負担しないことが多い）、たとえ負担したとしても、形式的検証は難しく高価です。
それは最近までの話でした。LLM ベースのコーディングアシスタントは、実装コードだけでなくさまざまな言語での証明スクリプトを書けるようになってきています。専門家がプロセスを導くことは変わりませんが、数年以内に完全自動化が現れる可能性があります。その時点で、形式的検証の経済学は劇的に変わります。
もし形式的検証が格段に安価になれば、私たちはもっと多くのソフトウェアを検証できるようになります。さらに AI が必要とする検証は増えるでしょう：人間が AI 生成コードをレビューする代わりに、AI に「出力が正しいこと」を証明させたいと思います。もしそれが可能なら、私は手作業で書かれたコード（その多くは職人のようなバグを含む）よりも AI が生成したコードを選びます。
LLM で証明スクリプトを書くことは最適な応用の一つだと主張します。もし LLM が幻覚的に間違いを生じても、証明チェッカーが無効な証明を拒否し、AI に再試行させます。証明チェッカー自体は少量の検証済みコードで構成されているため、無効な証明をスルーすることはほぼ不可能です。
それでもソフトウェアが瞬時にバグゼロになるわけではありません。検証が自動化されると、課題は仕様の正確な定義へ移ります――証明された性質が本当にあなたが重要視するものかどうかを保証することです。形式的仕様の読み書きには依然として専門知識と慎重な思考が必要ですが、手書きで証明を書くよりは遥かに簡単で迅速です。これは進歩と言えるでしょう。
さらに、AI エージェントが仕様作成を支援し、形式言語と自然言語の間を翻訳する役割も担えると想像できます。微妙なニュアンスが失われるリスクはありますが、そのリスクは管理可能に思えます。
コードの高レベルで宣言的なプロパティを指定し、AI に実装と証明を自動生成させることができれば、ソフトウェア開発の性質は変わります。私たちは AI が生成したコードを検査する必要がなくなるでしょう――コンパイラが機械語を生成するように。
まとめ
- 形式的検証は劇的に安価になろうとしている。
- AI が生成したコードには形式的検証が必要で、人間のレビューを省くことができる。
- 形式的検証の精度は、LLM の不確実かつ確率的な性質を補完する。
これらを総合すると、形式的検証は近い将来主流になると予測されます。技術面でなく、人々が「形式手法が実務上で実用可能だ」と認識する文化的シフトが制約となるでしょう。
この記事がお役に立ったら、Patreon で私をサポートしてください。新しい記事をお知らせしたい場合は Bluesky や Mastodon をフォローするか、メールアドレスをご入力ください（住所は第三者へ渡さず、スパム送信も行わず、いつでも退会可能です）。