LLMがLeanの証明自動化を実現、依存型が実用的に
Original : We have proof automation now
Pourquoi c'est important
LLMによる形式検証の自動化は、安全クリティカルなソフトウェア開発のコストを大幅に削減しうる。
Adam Langleyは2026年7月26日、LLMを活用してLean言語でZstandard解凍器を実装。依存型言語の最大障壁だった証明コスト問題をLLMの自動化で克服できる可能性を実証し、形式検証の実用化に向けた新たな展望を示した。
Google セキュリティエンジニアのAdam Langley（ImperialVioletブログ著者）は、LLMを用いたLeanの証明自動化を実験し、Zstandard解凍器をLeanで構築した成果を公開した。
依存型言語（CoqやLean）はコードの不変条件を型として形式的に表現できるが、長年の課題は証明コストの高さだった。seL4プロジェクトの報告では、C実装の20倍以上の証明コードが必要で、設計・実装の10倍の時間を証明に費やしたとされる。
従来の自動化手法であるF*（SMTソルバー活用）は単純なケースには有効だが、ソルバーが無限ループに陥る問題があり、利用者が「ソルバーが受け入れる書き方」を神秘的に習得する必要があった。
Langleyは「証明の内容ではなく存在のみが重要」という証明無関係性の原則に着目。LLMはこの性質を活かし、型チェッカーを過負荷にせず証明を自動生成できると指摘。依存型システムが劇的に実用的になる可能性があると述べた。