LLMでLeanの証明自動化が実現、Zstd実装で実証
मूल शीर्षक: We have proof automation now
यह क्यों महत्वपूर्ण है
LLMによる証明自動化が実現すれば、依存型言語の実用化が加速し、ソフトウェアの形式検証コストが大幅に削減される可能性がある。
2026年7月26日、暗号エンジニアのAdam Langleyが、依存型言語Leanを使ってZstandard解凍器を実装し、LLMによる証明自動化の実用性を実証した。従来、seL4プロジェクトでは証明コードがCコードの20倍以上に達し、証明作業が設計・実装の約10倍の時間を要していた。
暗号エンジニアのAdam Langleyは、依存型言語Leanを用いてZstandard（Zstd）解凍器を実装し、LLMを活用した証明自動化の可能性を検証した。
依存型言語（CoqやLeanなど）は、型システムで任意の細かい不変条件を形式的に記述・検証できる点が強みだが、証明作業の膨大なコストが実用化の壁となってきた。seL4プロジェクトの事後分析では、証明作業が設計・実装の約10倍の時間を消費し、証明コードの行数がCコードの20倍以上に達したことが報告されている。
F*などのSMTソルバーを用いた自動化の試みも存在するが、複雑なケースではソルバーが長時間稼働し収束しないケースも多く、使いこなすには「ソルバーを満足させる感覚」を培う必要があるとされる。
Langleyは、「証明の内容は原理上無関係であり、その存在のみが重要」という証明無関連性（proof irrelevance）の性質と、LLMの能力を組み合わせることで、証明自動化が飛躍的に実用的になると主張する。自身の限定的なテストでは、LLMが型チェッカーのメモリ爆発を回避しつつ証明を生成できることを確認した。
なお、Coqは名称をRocqに変更している。