LLMで証明自動化、依存型言語が実用段階へ
原題: We have proof automation now
なぜ重要か
LLMが形式証明の自動化を実現すれば、ソフトウェアの正確性を数学的に保証する依存型言語が組み込みやセキュリティ分野で広く採用される転換点となりうる。
Adam Langley氏（imperialviolet.org）が2026年7月26日、LLMを活用した定理証明の自動化により依存型プログラミング言語Leanが実用的になったと報告した。同氏はLeanでZstandard展開器を実装し、従来は人手で数日かかっていた形式証明をLLMが大幅に効率化できることを実証した。
Adam Langley氏は、依存型言語（CoqやLeanなど）が持つ「任意の不変条件を型システムでエンコード・強制できる」という強みを長年評価してきた一方、その実用化を阻む最大の障壁が「証明作業のコスト」だったと述べている。
seL4プロジェクトの事後分析として知られる古典的な報告では、熟練エンジニアでも設計・実装の約10倍の時間を証明に費やし、Cコードの20倍以上の証明コードが生まれたとされる。この圧倒的なオーバーヘッドが依存型言語をニッチな存在にとどめてきた。
SMTソルバーを用いたF*などの自動化手法も試みられてきたが、複雑な条件ではソルバーが数時間実行し続けるケースがあり、熟練者でもソルバーを「機嫌よくさせる」ための経験則に頼らざるを得ない状況だったという。
同氏が注目するのは「証明の内容は原則として無関係で、その存在だけが重要」という証明無関連性の原則だ。これにより、LLMが証明の中身を自動生成できれば、開発者は正しいステートメントの記述に集中できる。実際にLeanでZstandard展開器を実装した限定的なテストでは、LLMが型チェッカーをクラッシュさせるような複雑な証明を回避しつつ、証明を自動生成できることを確認した。
なお、Coqが名称を「Rocq」に変更したことにも言及している。証明エンジニアリング（コード変更後の証明再調整コストを下げる構造化）の必要性は残るものの、LLMによる自動化が依存型システムを劇的に実用的にする可能性があると同氏は結論づけている。