概要
https://alperenkeles.com/posts/test-dont-verify/
詳細内容
## 検証だけでなくテストも：AI時代の形式手法とソフトウェア品質の現実解
https://alperenkeles.com/posts/test-dont-verify/
**Original Title**: Test, don't (just) verify
AIによって主流化しつつある形式検証の可能性を認めつつ、依然としてランダムテストや「検証ガイド付き開発（VGD）」が不可欠である理由を論理的に解説する。
**Content Type**: 💭 Opinion & Commentary
**Language**: en
**Scores**: Signal:5/5 | Depth:5/5 | Unique:4/5 | Practical:3/5 | Anti-Hype:4/5
**Main Journal**: 84/100 | **Annex Potential**: 83/100 | **Overall**: 84/100
**Topics**: [[形式検証, ソフトウェアテスト, AIアシストプログラミング, Lean, 信頼された計算基盤(TCB)]]
AIが数学のオリンピックや複雑なアルゴリズムの問題を解き明かす中、形式検証（Formal Verification）はかつてない注目を浴びている。著者は、著名な研究者たちが期待を寄せるこの分野が、LLMの登場によって「仕様の記述」と「証明の工学」という二つの根本的な障壁を解消しつつあると述べる。AIは、曖昧な言葉による説明をLeanなどの定理証明器が理解できる形式へと「自動定式化」し、人間には困難な証明の探索を肩代わりしてくれるからだ。しかし、著者はこの「AIによる検証の自動化」という理想に対し、エンジニアが直視すべき冷徹な現実を提示している。
最大の懸念は、検証の基盤となる「信頼された計算基盤（TCB）」にある。自動定式化された仕様そのものが開発者の意図と一致しているかどうかを機械的に検証する術はなく、ここが単一障害点（アキレス腱）となるリスクがある。また、証明を容易にするための抽象的なデータ構造（ペアノ数など）は、実世界のハードウェア（キャッシュラインや投機的実行）がもたらす複雑なパフォーマンス特性をモデル化できていない。検証済みのコードであっても、実行環境でのパフォーマンスや、未検証部分との接点でバグが生じるリスクは常に残るのだ。
ここで著者が提唱するのが、「検証ガイド付き開発（VGD）」と「ランダムテスト」の再評価である。検証は「バグの不在」を証明できるが、テストは「バグの存在（反証）」を極めて低コストで見つけ出す。特にVGDは、形式検証された低速だが正しい参照実装と、高速だが複雑な本番実装をランダムな入力で比較検証（ディファレンシャルテスト）する手法であり、検証の「正しさ」と実用的な「速度」を両立させる現実的な解となる。
エンジニアにとっての重要な教訓は、AI時代においても「検証」を魔法の杖として盲信するのではなく、テストによる迅速なフィードバックループを組み合わせることだ。仕様が形式化される未来において、テストは検証を補完し、不完全なモデルが陥る罠から開発者を救い出す不可欠なツールであり続ける。著者は、検証とテストの相乗効果こそが、バグを異常事態として追放できる未来のソフトウェア工学の鍵であると結論づけている。