AIがコードを書く時代、Leanの生みの親が語る「証明」の重要性
AI, Lean, and the Future of Formal Verification, with Lean Creator Leo de Moura
Leanの生みの親でありAWSのDistinguished ScientistであるLeo de Moura氏が、AIが生成したコードをどう信頼するかという問題を論じる。仕様を先に書き、AIにコードと機械検証可能なLeanの証明を書かせる手法が現実になりつつある。Mathlibが10年かけて250万行に達した一方、AIは5000万行の証明を書いており、Fermatの最終定理の証明は1300万行に及ぶ。
Leanで証明された結果を信頼するには、カーネルだけを信頼すればよい。
HNでの議論
32- wbeckler
最強の組み合わせはLean 4/TLA+/などにAIと決定論的ジェネレータを加えたものだと思う。大規模システムでは、形式手法の表明を人間が理解できるサイズまで圧縮する必要がある。これは、表明がモデルとそれに付随するコードジェネレータの正確性を確認するものである場合に可能だ。ジェネレータは生成されたコードの証明を生成でき、人間はジェネレータが正しい大規模な表明を証明可能に生成することを確認するだけでよい。
これが、形式手法が大規模システムに対してAIを制約できる方法だ。
私たちはOpen Markets Initiativeでこれを実践しており、オープンソースの電子取引プロトコルコードが正確であることを保証する数百万行のLean 4、TLA+、Rocqを生成している。予想外だったが、Lean証明器はいくつかの誤ったステップを特定した。
- chamomeal
プロパティベーステストについて皆はどう思う？いくつかプロパティベーステストを設定してみたが、ほとんど形式検証のように感じる。
同じものではないと分かっているが、PBTは私がチェックしようと思わなかったようなとんでもないバグをあらゆる種類で捕まえられる。ステートフルなもの、サービス間のものなど。PBTに対する唯一の不満は、いつも面倒なセットアップだが、LLMがそれを解決する。
最近PBTに関する議論はあまり見かけないが、LLM時代には多大なコストパフォーマンスが得られる。
- PandaRider
> ... しかし、今後数か月から数年のうちに、人々は仕様、モデル、ソフトウェアに持たせたいプロパティにはるかに重点を置くようになると予想している。
形式検証のためのモデリングを学ぶためのリソースを誰か知っている？(Leanでなくてもよい)
- fspeech
現在、mathlibの基礎理論は、形式証明は高コストであるという仮定の下で構築されている。概念はできるだけ多くの証明を共有するために断片化されている。LLMがあれば、その仮定はもはや正しくない。概念と証明は可能な限り人間の思考に合うように構築されるべきであり、証明はLLMによって理論間で移植できる。Leanは翻訳が正しいことを保証するだろう。
- westurner
動画で説明されているように、Leanと例えばRustの結果を比較する例はある？
Leanに記号的な誤差項があり、それをサンプリングしてモンテカルロ解析と比較できると思う？しかし、すでにサンプリングベースの解析があったからこそ、これをすべてLean 4で（二重スリット実験とGrC(2,4)を使った重力）やらなければならなかった。
Leanと1つ以上のRust TLA+実装を組み合わせるには何が必要か？エージェントはこれをどう計画し実装するのか、利点と欠点は何か？
「Isabelle/HOL、Lean、HOL4、Agdaの比較：4つの定理証明器の物語」（2026年）だがRocqはない？