LLMが証明自動化を変える：LeanでZstandardデコーダを書いて分かったこと

We have proof automation now

依存型言語LeanでZstandardデコーダを実装した経験から、LLMによる証明自動化が依存型プログラミングを実用的にする可能性を探る。従来、証明には設計・実装の10倍の時間がかかり、seL4の例ではCコードの20倍以上の証明コードが必要だった。しかし、証明の内容は無関係で存在のみが重要という「証明無関係性」により、LLMが証明を自動生成できる。ZstandardのFSEエントロピー符号化の仕組みも解説する。