iwashi / Yoshimasa Iwase(@iwashi86):定理証明支援系が本当に広まる（使われるようになる）かもしれないな〜・LeanやRocqのような依存型言語は、プログラムの複雑な仕様を型システムで厳密に保証できる・ただ、その型の正しさを証明するのには、実装の10倍以上の時間がかかることもある・結果として、これまではごく一部でしか使われないニッチな存在だった・ソルバー等で自動化する試みもあったが、予測不能で扱うのは非常に困難・そこにLLMが登場し、状況が変わりつつある・LLMを活用することで、極めて強力な証明の自動化が可能に・筆者は実験として、Zstandardの展開処理をLeanで実装した・ZstandardのFSEエンコーダには、複雑な状態遷移などの前提条件がある・普通の言語ではコメントで済ませるしかない暗黙の仕様を、LLMに証明させてみた・結果として、いくつかのLLMはわずか20分程度でこれらの証明を自動で完了させた・大規模なシステムでどこまでスケールするかはまだ未知数である・しかし、証明の自動化によって、日々の開発に依存型言語を導入する道が開けたように感じている

iwashi / Yoshimasa Iwase

@iwashi86

NTTドコモビジネスでEM(育休中)。その他、早稲田大で非常勤講師、#fukabori#.fmの中の人、書籍翻訳者。 AI、マネジメント、Dev、PdM、Agile、HRに関する個人メモをポストしています。発言は個人の見解であり、所属する組織の公式見解ではありません。 Amazonアソシエイト・プログラム参加者。

Joined May 2009

694 Following 20.4K Followers

iwashi / Yoshimasa Iwase@iwashi86

2026.07.28 07:00

定理証明支援系が本当に広まる（使われるようになる）かもしれないな〜・LeanやRocqのような依存型言語は、プログラムの複雑な仕様を型システムで厳密に保証できる・ただ、その型の正しさを証明するのには、実装の10倍以上の時間がかかることもある・結果として、これまではごく一部でしか使われないニッチな存在だった・ソルバー等で自動化する試みもあったが、予測不能で扱うのは非常に困難・そこにLLMが登場し、状況が変わりつつある・LLMを活用することで、極めて強力な証明の自動化が可能に・筆者は実験として、Zstandardの展開処理をLeanで実装した・ZstandardのFSEエンコーダには、複雑な状態遷移などの前提条件がある・普通の言語ではコメントで済ませるしかない暗黙の仕様を、LLMに証明させてみた・結果として、いくつかのLLMはわずか20分程度でこれらの証明を自動で完了させた・大規模なシステムでどこまでスケールするかはまだ未知数である・しかし、証明の自動化によって、日々の開発に依存型言語を導入する道が開けたように感じている

230

Forward to community