ついに実現！証明自動化（Proof Automation）が実用レベルに

ついに「証明自動化（Proof Automation）」が手に入る時代が来ました。開発の効率化と信頼性の向上を同時に叶えるこの技術、エンジニアにとって注目すべき転換点となりそうです。

このトピックへのメタコメントとして、プロジェクトで定理証明器を使うことの意味について、いまだに混乱があることに気づいたよ。先日、最近AIに傾倒しているらしい仮想通貨VCのParadigmのツイートを読んだんだ。彼らのLPの誰かが、Ethereumの仮想マシンをLean 4で形式化してみたらしい。ツイートには、APIトークンで15万ドル相当のコストがかかり（「かかっただろう」という話。まあ、彼らは無料で使えるんだろうけど）、LLMの推論に1週間もかかったと書いてあった。気になってそのコードを見てみたんだけど、定理の記述がかなり薄い。それに、個人的にLean 4を使う最大の動機であるBatteriesやMathlibも使われていなかった。つまり、自分としては誰かが圏論や代数構造を正しく構築してくれるなら、その上に自分が取り組んでいるおもちゃのようなコードとの対応関係を証明する義務を負うのは構わないというスタンスなんだ。そういう意味での「証明探索」にLLMを使うのはSMTソルバーを使うのと同じ感覚でアリだ。ただ、LLMはライブラリを使うように強制しないとダメだね。そうしないと、3時間の証明義務を果たすよりも、3分の推論タスクでさっさとオーバーフィットさせて結論をでっち上げる方を優先しちゃうから。それに、LLM（自分はClaudeを使ってる）を説得して「これは学術的な演習なんだ」とか「私がやらなきゃいけないんだ」と言い聞かせないといけないのが本当にうんざりする。そうしないと、LLMは自分からやりたくない理由をでっち上げ始めるからね。今話しているのは、自分が「過去の研究との等価性」を見つけることに興味があるという前提での話だ。LLMが生成するLeanコードの多くは、XがLean 4プログラムに変換できるかどうかを知りたいだけ、という感じのものが多い。それはそれでポジティブなことだけどね。でも、もし洗練された型や定理に興味がないなら、なんでHaskellじゃダメなの？要するに、良い問いを立てられなければ、それがこれらの言語で如実に露呈するってことだよ。これはLLMが助けてくれる部分じゃない。自分で証明の義務を課さなければ、LLMがわざわざ自分のために骨を折って証明を考えてくれるなんてことは絶対にないから。

LLMと定理証明器を組み合わせることで、形式手法がソフトウェア開発において実用的なレベルまでコストダウンできるという根本的な主張には同意するよ。かつてはコストが最大の問題だったからね。ただ、アライメントの問題は依然としてある。人間の監督なしでは、元の仕様や意図からどんどんズレていく可能性があるから。自分の経験から言うと、Hoare論理や分離論理（コントラクト）のようなものが一番うまくいく。これらは理解しやすく、分解もしやすいからね。最低限のHaskellのサブセットにLiquidHaskellを少し加えるだけでも、実用的な視点で見ればかなり強力だよ。

現在のLLMは、証明無関係性（proof irrelevance）と組み合わせることで、非常に強力な証明自動化の形になる可能性がある。自動化が進めば、証明エンジニアリングにそれほど頭を悩ませる必要もなくなるかもしれない。型チェッカーを暴走させない工夫は必要だけど、自分が試した限りではLLMでもそれは防げる。LLMによって依存型システムが飛躍的に実用的になるかもしれない。

Roqのようなインタラクティブな証明システムを使っていると、軸を間違えて切り分けたり、証明しやすい形で問題を定義できなかったりして、自分で泥沼にはまることがよくあった。結局、数学と同じで、簡単に証明にたどり着くには問題を適切な切り口で捉えることが本当に大事なんだ。

みんな、その意思決定がいかに重要かを過小評価していると思う。LLMが特定の証明戦略をこなせるかどうかだけでなく、いかに問題を提起するかといった点も重要だからね。

LLMが役に立たないと言っているわけじゃない。ただ、「証明エンジニアリングが不要になる」というよりは、「ツールを正しく使えば証明エンジニアリングが楽になる」という方が正しいと思う。結局、これらのツールは適切な基盤があってこそ真価を発揮するものだからね。

AWSがAArch64のセマンティクスとシミュレータであるLNSymを作ったのはクールだね。これを使って、ある関数の最適化されたアセンブリ実装とLean側の対応物の等価性を証明し、実行時にはアセンブリコードを使うという方法も考えられるんじゃないか？そうすれば、LLMに最適化を任せても機能的なバグが混入することはない。検証済みアセンブリは暗号実装ではよくある手法だけど、これでもっと安価に実現できるようになるかもしれないね。

CompCertをワンショットでやるのは難しいだろうけど、よく考えて計画を練れば、少しは簡単になるかもしれないね。

これは本当に面白いし、未来はこうなるという意見に同意するよ。最後の2段落の「余談：検証済みアセンブリ」については少し驚いた。僕の理解では、その未来はすでに到来しているからだ。Googleのaglの同僚たちが、Fiat CryptoとCryptOptの研究（https://arxiv.org/pdf/2211.10665 ）をベースにして、検証済みアセンブリで自動合成（あるいはミューテーション）された暗号ルーチンをすでにデプロイしているはずだよ。どちらの研究にもAndres Erbsenが関わっていて、彼は教授職に就く前の期間をGoogleで過ごしているはずだ。