形式検証への反論、50年後の再検証
The Case Against Formal Verification, 50 Years Later
AIコーディングの台頭により形式検証への関心が高まる中、1979年の古典的論文「Social Processes and Proofs of Theorems and Programs」の主張を現代の視点から再検証する。著者は形式検証の限界を指摘するが、その後の技術発展により多くの論点が覆されている。本稿では、仕様の曖昧さ、自動検証の可能性、現実システムへの適用性など、6つの論点を最新の動向と照らし合わせて考察する。形式検証は万能ではないが、AIエージェントがコードを書く時代において、その重要性は増している。
「プログラムの検証は失敗する運命にある。それが誰かのプログラムに対する信頼に影響を与えるとは思えない。」
HNでの議論
113- somat
いつも疑問に思うのは、「形式検証が、検証対象のプログラムよりも正しいと言えるのはなぜか」ということだ。注：検証エンジンのバグではなく、プログラム用に作られた仕様についての話だ。
これは大した問題ではないと思う。形式検証は正しさに近づくための非常に有用なツールだとは思うが、説明させてほしい。プログラムが書かれるとき、それは問題を解こうとしている。その問題を正しく解けばバグはなく、間違って解けばそれがバグだ。複雑な問題では、正しく解くことは非常に難しい（不可能に近い）ことがわかっている。形式検証の仕様が、プログラム自体よりも正しいと想定する理由はどこにあるのか？ 両方とも非常に複雑な問題を解こうとしているのだ。
私はこれを実感しようと、sel4のgitの変更履歴を読み、OSのバグ修正と仕様のバグ修正がそれぞれいくつあるかを数えようとした。残念ながら明確な結論は出なかった。なぜなら、ほぼ常に両方を同時に修正しなければならないからだ。OSでバグが見つかれば仕様が悪いことになり、仕様でバグが見つかればOSにバグがある可能性が高い。
- ibarrajo
今年はLeanでたくさんvibe codingをした。
分かったのは、守りたい保証に不可欠な不変条件を決めてしまえば、それは素晴らしいということだ。
自分で形式検証済みのワークフローエンジンを構築したが、簡単だった。しかしそれは主に、CadenceとTemporalの落とし穴と基礎となる柱をすでに知っていたからだ。
また、一般的な知識ではないかもしれないが、LeanからCにコンパイルされるライブラリをエクスポートできる。それを使えば、検証済みで高性能なコードが得られ、他の場所からCバインディングとして簡単に呼び出せる。
Lean自体は一般的に優れたIOスタックを持っていないが、小さなプロジェクトには十分だ。
ライブラリのエクスポートやnative_decide全般には注意点がある。Cにエクスポートすると、ABIはLeanカーネルのスコープ外になる。つまり、コンパイラ自体からバグが入り込む可能性がある。
- mpweiher
「逆の主張は、仕様は実装よりも非形式的な要件に近い（したがって、間違いを見つけやすい）というものだ」
大学で形式検証を学んだとき、私はまったく逆のことを経験した。それが、形式仕様／検証に魅力を感じなかった主な理由だ。
- gr_norm
タイトルは、記事を読んでいなければ少し誤解を招くかもしれない。これは1979年の形式検証を批判した有名な論文への反論だ。記事は結局、その最も強い主張のほとんどに後から反対しているが、いくつかは依然として価値があるように見える。
- jochenm
完全な大規模プログラムの正当性証明には、仕様自体にバグがあるかもしれないという問題が常につきまとうという点には同意する。したがって、統合テストが不要になることはほとんどないだろう。しかし、他の人たちがすでに指摘しているように、その場合でもプログラムの重要な部分の形式検証は有用だ。
付け加えると、「単に」プログラムが未定義動作や実行時エラーを引き起こさないことを証明できるだけでも、大きな価値がある。
Cプログラムにとっては、もちろん特に有用だろう。
しかし、安全なRustでも（私の理解では、まだRustを使ったことはないが）パニックという形の実行時エラーが発生しうる。そして、医療機器がソフトウェアの範囲外読み書きの試みによってパニックで中断され、動作を停止したら、それは本当に楽しいことではない。そのような不正なアクセスが決して発生しないことを静的に証明する方が良い。これはまだ安全なRustの話であり、unsafeコードは考慮していない。同様の議論は、CやC++より安全だと考えられている他のシステムプログラミング言語にも当てはまるだろう。
- _tgxm
Rustで分散アルゴリズムを書いたとしよう。それを検証するために、同じアルゴリズムをTLA+で記述し、その仕様をモデル検査し、私が気にする特性を満たすことを証明するかもしれない。
これで2つの成果物ができる：
TLA+仕様 → 証明済み
Rust実装 → 実行時
しかし、証明が確立するのは次のようなものだ：
TLA_Spec => Safety
実際に必要なのは：
Rust_Program => Safety
これはモデルコードギャップと呼ばれていると思う。これに対処する方法はあるが、簡単に追えるアプローチは見つけていない。
- Almondsetat
誰もが弱い部分は仕様だと知っている。しかし、これは見せかけの議論だ。なぜなら、定義上、実装を保証すれば、露出するのは仕様自体だけだからだ。少なくとも攻撃対象領域を減らしていることになる。
- Animats
Lipton/Perlis/De Milloの論文を何年も見ていなかった。あの議論の時代に私はいた。それが本当に年齢を感じさせる。あの人たちはミューテーション解析を推していた。[1] それはテストスイートのテストだ。プログラムにランダムな変更を加えて、テストスイートがそれを検出するかどうかを見る。ファジングはその概念に関連している。
検証が普及するのに時間がかかりすぎた。ここが私が約50年前にいた場所だ。[2] 問題の一部は、関心のほとんどが形式主義に夢中な人々から来ていたことだ。ほとんどの研究者が使う表記法はひどいものだった。Lipton/Perlis/De Milloの論文で指摘されている通りだ。プログラミング言語に合った表記法が必要だ。
当時、私たちは基本的なアーキテクチャを持っていた。簡単な問題にはSATソルバーを使い、難しい問題にはAI機能を備えた何かを使うというものだ。簡単な問題には、最初のSATソルバーであるOppen-Nelson簡約器があった。難しい問題にはBoyer-Moore証明器があった。それは古き良き古典的AIであり、1970年代後半としては非常に優れていた。SATソルバーは検証条件の90%以上を片付ける。そして、AIソルバーにとって難しく抽象的な問題を生み出す検証表記法が必要だ。例えば、2つのassertを続けて書き、最初のassertから2番目を証明するのが難しい問題にする、といった具合だ。
当時は十分な計算能力がなかった。Boyer-Moore証明器がペアノの公理に似たものから数論を構築するのに、VAX 11/780で約45分かかった。今では約1秒だ。私はBoyer-Moore証明器を移植した […]