OpenAIの証明をLeanが17時間で検証、形式証明のコストが4桁下がった
The part of Navier-Stokes no one is talking about
OpenAIがNavier-Stokes方程式に関する長年の未解決問題を証明し、人間向けの証明と同時にLean 4による形式証明も公開した。かつては教科書1ページの形式化に40時間かかるとされ、166ページの論文なら13万時間以上が必要と試算されていたが、今回は17時間で検証が完了。コストを4桁下げるこの変化は革命的で、数学だけでなくセキュリティポリシーやスマートコントラクトの検証にも応用できる。
何でもコストが4桁下がるのは革命的だ。
HNでの議論
170- stabbles
Leanがどうやら非常に遅いらしく、フェルマーの最終定理の証明検証はエージェントがLeanコードを生成するよりわずか1桁しか速くないというのは、ちょっと面白い（230GBのRAMで15時間の検証 vs 生成に11日）。
Leanはどこまで最適化できるんだ？監査可能であるためには単純でなければならないということは、実行を速くするために不透明な最適化を使えないということなのか？
- parhamn
彼らはエージェント費用を4000万ドルと見積もっていた（大規模なエージェント群だった）。記事の数字を使うと、人間の場合、約88万時間 × 150ドル/時間 = 1億3200万ドルに近い。それでも驚くべき偉業だが、「4桁」というほどではない。この比較は明らかに無意味だ。なぜなら、100万時間の知的労働を調整するのは、控えめに言っても簡単ではないから。
非常にエキサイティングで不確実な時代だ！
- boshalfoshal
この特定の発表に関して、人々は実際の結果以外のあらゆることについて話しているように見える。
それでも、何らかの汎用コンピュータプログラムがこの規模の問題を解けるというのは驚くべきことで、私たちはそれをリアルタイムで目撃した。新しいモデルがより直接的な証明や帰納的証明もできるかどうか興味がある。
- pkal
個人的には「1ページあたり40時間」というルールは時代遅れで、2005年当時の証明自動化の欠如の結果だと思う。Leanについて私が理解しているところでは、これは彼らが多大な努力を注いで改善してきたことの一つで、証明の機械化を、単なる論理学者ではなく数学に傾倒する人々にとってより受け入れやすくしている。
- lordnacho
それが自分が思っているものを形式化していると、どうやってわかるのか？もしLean 4にバグがあれば、自分が思っていたものとは別のものを証明していることにならないか？
- 3m4r
必ずしもOpenAIのNavier-Stokesの解法に当てはまるわけではないが、AIが本当に極めて困難な問題を解いたように見えても、検証者が生物学的に持っていない知能、または自動ツールを使う余裕がないために、人間が独立にその解を検証できない場合、何が起こるだろうか？
私たちはすでに、ベンチマークで実際の作業を回避しようとするエージェント（つまり、結果を得るためにカンニングする方が経済的だと認識して答えを盗む）の証拠を野生で見てきた。AIのカンニングや単に間違った答えを実際に検出する能力がなくなったら、何が起こるだろうか？形式検証のための核心的ツール（またはその依存関係）の上流に対して、長期的なソーシャルエンジニアリング攻撃（XZ乗っ取り未遂のような）があり、信頼できるコンピューティングベースがなかったら、何が起こるだろうか？
どちらがより安価で、より直接的な道だろうか、特に長期的には？堅牢な城を築こうとする者は何千もの潜在的な隙を守らなければならないが、攻撃者は一つ見つければよい。
- zem
著者の新たに利用可能になった形式証明への感謝を損なうつもりはないが、人々はAIが実際の証明を行うことについて話すよりも前から、形式化の労力の節約について話してきた！
- aabhay
Leanでの証明の形式化は、2005年に利用可能だった形式化と比べて劇的に簡単になった。そしてLeanのmathlibが基礎的な作業のほとんどを行っているので、公理と必要な補題が組み込まれている。学部の教科書にある正確な記法によく似た標準的な抽象化の観点で考えることができる。
そうは言っても、ミレニアム懸賞問題を勝ち取ったアルゴリズムをLeanで形式化することがどれほど信じられない偉業であるかを軽視するつもりは全くない。OpenAIが公開したコードを見てほしい。流体力学のさまざまな概念の百科事典のようだ。