AI、Lean、そして形式検証の未来：Lean開発者Leo de Moura氏との対談
要約
AIが形式検証をより身近にし、ソフトウェア工学と数学に革命をもたらす可能性について、Lean開発者のLeo de Moura氏が語る。AI生成コードの信頼性確保には機械チェック可能な証明が不可欠であり、Leanのようなツールがその役割を担う。本記事では、AIと形式検証の進化が、エンジニアや研究者のスキル、キャリア、そして科学全般に与える影響について掘り下げている。
全文翻訳
AIがコードを書くとき、その動作を誰が証明するのか？
Leo de Moura氏：形式的証明、AIエージェント、そして「私を信じて」コードの終焉について。
Ben Lorica氏は、AWSのVP兼主任科学者であり、Leanの作成者であるLeo de Moura氏と対談した。Leanはプログラミング言語であり、定理証明支援系でもある。彼らは、AIが形式検証をいかにアクセスしやすくし、ソフトウェアエンジニアリングを変革する可能性を秘めているかについて議論した。仕様と機械チェック可能な証明の重要性、AI生成コードや自律エージェントを信頼することの意味、そして検証されたソフトウェアスタックのビジョンについて語られた。この会話では、AIと形式検証が数学をどのように再構築しているか、それがエンジニアや研究者のスキルやキャリアに何を意味するか、そして次に同様のブレークスルーがどこから現れる可能性があるかについても探求された。
インタビューのハイライト – ビデオ版の主要セクション：
関連記事：
- この会話のビデオ版がYouTubeチャンネルで公開されています。
- AIは数学研究をどう変えているか
- Evalsをパスしても安全とは限らない
- AIエージェントが静かに破る8つのセキュリティ上の仮定
- 実際の作業を行うエージェントのための9つの実践的なルール
- Zhou Yu → なぜあなたのAIエージェントは出荷準備ができていないのか（そしていつ準備ができるかを知る方法）
- Helen Gu → AIエージェントの隠れた失敗モード
- Evan Marshall → コード生成がスピードアップするにつれて、出力のテストは誰がするのか？
私たちの活動をニュースレターの購読でサポートしてください📩
トランスクリプト
以下は、編集・校正済みのトランスクリプトです。
Ben Lorica。さて、今日は特別なゲストをお迎えしています。AWSの自動推論グループのVP兼主任科学者であるLeo de Moura氏です。さらに重要なのは、lean-lang.orgにあるLeanの作成者であることです。Leanはプログラミング言語であり、定理証明支援系でもあります。また、Lean Focused Research Organizationの主任アーキテクトでもあります。それでは、長々とした紹介はこのくらいにして、Leoさん、ポッドキャストへようこそ。
Leo de Moura。ありがとうございます、ありがとうございます。ここに来られてとても嬉しいです。
Ben Lorica。さて、この会話の全体的なテーマは、生成が容易になった時代にいるということです。必ずしも安価ではありませんが、Claude Codeの利用者はそう証言するでしょうが、容易であるということです。そして、主要な課題の一つが検証です。Leanは通常、そのための標準的なツールとして認識されています。実際、今後1年間でAI分野の多くの人々が形式検証というトピックについてLeanの名前を口にするようになるでしょう。そこで、Leoさん、基本から始めましょう。コードレビュー、QA、テストに慣れているリスナーのために、形式検証とは何を意味するのでしょうか？
Leo de Moura。はい、Leanはプログラミング言語であり、証明支援系でもあります。コードを書くことができますが、そのコードが持つべき性質を記述することもできます。数学における未解決の命題を記述し、これらの主張に対する証明を提供することもできます。しかし、その証明は非公式なものではありません。証明はLean言語で書かれ、さらに重要なのは、機械によってチェックされることです。
Leanは大きなコードベースですが、Leanで証明された結果を信頼するには、カーネルのみを信頼すればよいのです。証明がチェックされるのはそこです。他のプログラミング言語と同様に、LSPサーバー、IntelliSense、コードジェネレーター、オートコンプリートなど、すべてのツールがLeanで利用可能ですが、証明チェックのステップには重要ではありません。
そして、チェッカーは一つではありません。Leanでは、証明を操作したり変換したりできるデータとして見ることができます。証明をエクスポートして、異なるチェッカーでチェックすることもできます。これらのチェッカーのいくつかは現在検証済みです。検証済みのチェッカーが2つあります。3つ目がもうすぐ登場します。
しかし、機械でチェック可能な証明を持つこの能力は、信頼のボトルネックを解消するのに役立ちます。これは人間間の信頼だけでなく、人間とAI間の信頼のボトルネックも解消します。
例えば、コードの一部を合成したいとします。特定の性質を持つコードを実装したいとします。過去には、ソフトウェアを実装し、これらの性質が満たされていることを確認するためのテストインフラストラクチャを追加したかもしれません。プロパティベースのテストは最近非常に人気がありますね。そして、テストフレームワークを書きました。
テストフレームワークはバグを見つけるのに非常に役立ちますが、バグがないことを証明するのには役立ちません。
Ben Lorica。別のチームがテストを実施することさえありますね。
Leo de Moura。はい、はい。今、形式検証を使えば、性質から始めることができます。例えば、性質を書き留めて、AIにこれらの性質を満たすコードを実装するように依頼し、「証明してみせろ」と言うことができます。コードを実装し、機械チェックされるLean証明を書くことになります。そしてAIは現在、それを完全に実行できます。
例えば、私の同僚であり友人でもあるKim Morrisonは、zlibをLeanに移植するという実験を行いました。これは圧縮ライブラリです。そして今、彼女は「データを圧縮してから解凍すると、元のデータに戻る」という性質を持っています。損失はありません。データは破損していません。これは重要な性質です。
Ben Lorica。圧縮レベルに関わらず。
Leo de Moura。その通りです、その通りです、その通りです。定理はまさにそれを述べています。定理のパラメータの一つです。
Ben Lorica。それで、Leoさん、リスナーのために、彼女はこの圧縮ツールをLeanを使って書いたのですね。
Leo de Moura。はい。
Ben Lorica。そしてLeanが形式検証ツールとして機能したのですね。では、開発者である私が同じことをして、Rustで書くことにした場合、Leanはそれでも助けてくれますか？
Leo de Moura。はい、はい、2つの方法で助けてくれます。最初の方法はAeneasを使うことです。AeneasはLeanを使ってRustコードを検証できるツールです。
Aeneasは、例えばMicrosoftのSymCryptチームによって使用されています。SymCryptはMicrosoftの暗号ライブラリです。彼らはAeneasとLeanを使って暗号ライブラリを検証しています。
したがって、Aeneasから始めることができます。もう一つの可能性は、AIにLeanでコードのモデルを構築するように依頼することです。AIはあなたのコードを読み取ります、どんな言語であっても—
Ben Lorica。どんな言語であっても。
Leo de Moura。はい、どんな言語であっても。もし去年に誰かが私にこれを言っていたら、私はそれがSFだと言ったでしょう。
Ben Lorica。そしてこれは、少なくとも数学においては、自動形式化と呼ばれるものですね。
Leo de Moura。はい。
Ben Lorica。そうですね。数学では、リスナーのために、数学の論文があるかもしれません。それは論文であり、言葉、数学記号、定理、補題などで構成されています。そして、Leoさんが指摘するように、1年前までは存在しなかった自動形式化が、今や現実のものとなっています。
Leo de Moura。はい、はい。
Ben Lorica。そして、Leoさん、このステップは、Leanの皆さんは関与していませんね。これは、フロンティアモデルがこれを実行できるようになったから起こったことですね。
Leo de Moura。まさに、まさに。Lean側で私たちにとって何が変わるかというと、スケーラビリティです。つまり、今AIは—例えば、人間がLeanのために構築した数学ライブラリはMathlibと呼ばれています。それは250万行あります。
Ben Lorica。信じられない！リスナーのために想像してみてください—これは現実ではありませんが—ほとんどすべての数学の書籍や論文が、自動形式化を使って私たちが説明した方法でLeanに翻訳されたと想像してみてください。つまり、それらすべてにアクセスできるようになるということです。
Leo de Moura。はい。しかし、これらの速度を見てください。現在公開されているLeanの証明の中には、5000万行のものがあります。Mathlibは人間によって書かれ、ゼロから250万行になるのに10年かかりました。そして今、AIが証明を書いている人々が—5000万行の証明を書いています。Anthropic AIによって書かれたフェルマーの最終定理の証明は1300万行です。
Ben Lorica。しかし、Leoさんが指摘するように、ソフトウェアの場合、あらゆるプログラミング言語で同等のことが起こっていますね。
Leo de Moura。はい。
Ben Lorica。フロンティアモデルは、あなたが書いたプログラムを、どんなプログラミング言語であっても、Leanに翻訳できるようになりました。
Leo de Moura。はい。
Ben Lorica。そして、検証のためのLeanインフラストラクチャが手に入ったわけですね。
Leo de Moura。まさに。しかし、一つ覚えておくべき重要なことがあります。プログラムのモデルをLeanで作成する場合、AIを使用すると、常にこの疑問が生じます。「このモデルはあなたのコードに忠実か？」
現在、差分テストを使用している人もいますね。Leanモデルとプログラムを実行し、それらが同じものを計算するかどうかを確認します。不一致を見つけるためです。そして人々はバグを見つけています。たとえ—
Ben Lorica。つまり、あなたはまだこれに責任があるということですね。
Leo de Moura。はい、まさに。そして、私はそれが段階的に起こっているのを見ています。例えば、数週間前、Claude Codeの主要開発者であるBorisは、Claudeに「Leanを使ってClaude Codeのバグをチェックしてくれ」と頼んだビデオを投稿しました。
そしてClaudeはモデルを作成し始め、バグを見つけ、性質を証明しようとしますが、性質を証明できないことに気づき、バグを見つけ、PRを提出し、Borisはそれをマージします。はい、これらは実際のバグでした。そしてBorisは「Leanのことは何も知らない」と言いました。
Ben Lorica。はい、はい。
Leo de Moura。しかし、これはバグ発見のためです。これは比較的うまくいきます。しかし、次のステップ、つまり「はい、バグはありません」と言うためには、モデルを見て、「はい、これは私のコードの正確なモデルであり、それらを同期させて維持したい」と言う必要があります。
おそらくAIを使用するでしょう。性質を証明します。Rustでコードを書いている場合は、Aeneasを使用して、それがコードの忠実なモデルであるかどうかを証明できます。
しかし、今後数ヶ月から数年で、人々は仕様、モデル、ソフトウェアに持たせたい性質に、はるかに多くの時間を費やすようになると予想しています。
Ben Lorica。はい、実際、この現象は数学でも起こっています。最近では、Navier-Stokes方程式の証明でもそうでしたね。つまり、問題の実際のステートメントを翻訳する自動形式化のステップは、それほど忠実ではなかったのかもしれません。あるいは何であれ。
しかし、結局のところ、彼らは結果を証明したのです。ただ、人間がそれをキャッチして微妙な調整を行う必要があっただけですね。
Leo de Moura。はい。はい。いいえ、これはNavier-Stokesにとって重要な点です。なぜなら、それは非常に重要な結果だからです。OpenAIがモデルを指示する前に、私たちはNavier-Stokes問題の人間がキュレーションしたステートメントを持っていました。問題のステートメントはすでに専門家によってキュレーションされていました。問題のステートメントが正しく形式化されていたかどうかについて、疑いの余地はありませんでした。
結果についてはある論争があります。なぜなら、OpenAIは自然言語で書かれた非公式な証明と、Leanで書かれた形式的な証明を提示したからです。非公式な証明と形式的な証明の間には、証明に不一致がありました。
Ben Lorica。それは、4次または5次の微分を仮定しているかどうかというレベルだと思います。
Leo de Moura。はい、はい、はい。正しい。
Ben Lorica。それは数学者にとっては重要ですが、微妙な違いがどれほどあったかは想像できるでしょう。さて、Borisですが—しかし、お渡しします—
Leo de Moura。一つ、リスナーに伝えるべき重要なツールがあります。Verso Blueprintというツールです。
Verso Blueprintは、自然言語とLeanを組み合わせたLeanの結果を提示したい場合に使用するツールです。Verso Blueprintを使用できます。それはほとんどリテララルプログラミングのようなものです。自然言語、LaTeX、Leanを組み合わせ、両方のプレゼンテーションを整列させることができます。
AIがVerso Blueprintを使用していれば、この不一致は起こらなかったと確信しています。これはツールの改善の問題です。
人々が持つもう一つの誤解は、Leanの証明は静的なオブジェクトだと考えていることです。そうではありません。コードをリファクタリングするように、証明をリファクタリングできます。単純化できます。例えば、Anthropicによるフェルマーの最終定理の証明のために、グループがあります。すでに証明を半分に削減したグループがあります。
Ben Lorica。ちなみに、これは人間が書いた証明にも当てはまりますね。
Leo de Moura。はい、はい、はい。しかし、ここでは機械チェックが得られますね。つまり、証明を変更していますが、Leanは「はい、これは真の証明です」と言い続けています。
操作できます。AIに証明のナビゲーションを手伝うように依頼できます。Lean Blueprintを使って、証明を非公式なプレゼンテーションと整列させることができます。これらすべてが可能です。
つまり、ソーシャルメディアで人々が見落としていることの一つだと思います。これらの形式証明は静的なオブジェクトではありません。操作、単純化、調査、質問、対話ができるオブジェクトです。
Ben Lorica。では、現時点で明確になっているはずですが、この一点を明確にしたいと思います。しかし、私たちが話していることになじみのない聴衆に、この点を理解してもらいたいのです。それは、形式検証と通常のQAおよびテストの違いです。
なぜ私は—つまり、AIがすべてのテストを生成してくれるのに、形式検証に手間をかける必要があるのでしょうか？そして、AIを使って多数のテストケース、エッジケースを生成しているので、カバレッジは最大化されています。Leoさん、検証は不要ですよね？
Leo de Moura。はい、テストはバグの存在を示すのに役立ちますが、その不在を示すのには役立ちません。
AIを使って多くのテストケースを生成したとしても、あなたのソフトウェアの脆弱性を見つけるために使用されるAIほど賢くないかもしれません。
これらの技術は互いに競合するものではないと思います。補完し合います。例えば、多くの人が犯す間違いは、おそらくバグのあるものを証明しようとすることです。まあ、どれだけ多くのリソースを投入しても、どれだけ多くのトークンを消費しても、真実ではないものを証明することはできません。
したがって、テストは常に良い出発点です。信頼度と理解度を高め、それから証明します。
今、あなたはあらゆる入力に対して証明しています。試したテストに対してのみ機能したと証明しているわけではありません。しかし、あらゆる可能な入力に対して、あなたのプログラムが機能することを証明しています。つまり、一部ではなく、すべてに対してです。
Ben Lorica。そして正直なところ、ソフトウェアエンジニアリングは、航空宇宙工学などの他の工学分野に遅れをとっていると思います。これらの分野では、結果がより深刻であるため、検証に関して、より厳格な規律があったのではないでしょうか。
Leo de Moura。素晴らしい点です。
Ben Lorica。素晴らしい点です。
Leo de Moura。素晴らしい点です。
Ben Lorica。私は、コードを書く人が増え、コードを書くことが容易になったというだけのケースだと思います。そして、検証がそのImageNetの瞬間を迎えたというだけです。
Leoさん、あなたがたはLeanを長年開発しており、Leanは長年堅牢でした。したがって、主な移行は本当にこの自動形式化、フロンティアモデルがLeanを書く能力です。
Leo de Moura。はい、そしてそれはあなたの以前のコメントにもつながります。あなたは、はい、一部の産業では、人々は過去に形式検証を使用してきたと指摘しました。しかし、それはなぜ人気がなかったのでしょうか、もしそれがそれほど良いのであれば？それは、手作業で証明するには時間がかかりすぎるからです。
そしてAIはコード検証のコストを劇的に削減し、他の利点も提供します。
形式証明を取得した後、AIに「コードを変更して最適化したいが、それが正しいことを証明し続けなければならない」と尋ねることができます。
証明がガードレールのようなものです。今、AIはあなたが正確にどのように機能するかを理解していないかもしれないワイルドな最適化を試すことができますが、証明は「はい、まだ同じものを計算しています」と言っています。それははるかに効率的ですが、まだ同じものを計算しています。
Ben Lorica。したがって、私たちが議論してきたことから判断すると、ソフトウェアエンジニアリングの専門職は、コードを書くことに焦点を当てるのではなく、おそらく検証にさえ焦点を当てることになるでしょう。なぜなら、検証も半自動化できるからです。
それは本当に要件ですね。つまり、あなたが望むものを記述することです。
したがって、2つのバケットがあると思います。要件ギャップがあります。つまり、あなたが望むものと、あなたが書き留めることができるものとの間に違いはありますか？そして、いわゆるモデルギャップ、つまり、テストの条件は本番環境を代表していますか？
つまり、言い換えれば、あなたのテストシナリオは、ある意味で理想化されすぎているのかもしれません。
そして明らかに、あなたは以前にそれをほのめかしました：ある程度、Leoさんとチーム、Leanカーネルを信頼する必要があります。つまり、Leanが人気になり、それに依存するようになると—依存するとは、Leanがあなたのコードを検証しただけでなく、あなたのコードが依存していたすべてのライブラリも検証したことを意味します。
したがって、それらは3つのものだと思います。要件、モデル、そしてLeanカーネルです。
Leo de Moura。まあ、私たちは複数持っています。私たちを信頼する必要はありません。他のチームによって実装されたカーネルがあります。この部分は、うまく対処していると思います。
カーネルアリーナさえあり、カーネルを集めています。それらは互いに競合して、どちらが最も速いかを見ています。もし何か間違ったことをしたら、バグがあったら、ペナルティが科され、誰もが見ることができます。
arena.lean-lang.orgと呼ばれています。すべてを見ることができます。つまり、そしてそれらはすべて—
Ben Lorica。オープンソースですか。
Leo de Moura。そうだと思います。私は pretty sure です。つまり、すべてを使っているわけではありません。主要なものを使っています。私が使っているものはすべてオープンソースです。つまり—
Ben Lorica。それらは—それらであるためにLeanで書かれる必要がありますか？
Leo de Moura。いいえ。
Ben Lorica。いいえ？
Leo de Moura。それらのいくつかはRustで実装されています。C#で実装されたものがあります。Haskellで実装されたものもあります。
信じられないかもしれませんが、TeXで実装されたものがあります。TeXは、コンピュータサイエンスや数学などの論文を組版するための言語ですが、TeXは本格的なプログラミング言語であり、私の同僚であるKim Morrisonは、TeXでカーネルを実装しました。これは、多くの異なるプログラミング言語で実装できることを示すためです。
ああ、例えばCOBOLで実装されたものや、Fortranで実装されたものもあります。
Ben Lorica。そうすると、ソフトウェアエンジニアの教育とトレーニングは変わりますね。
Leo de Moura。まあ、形式仕様を書くこと、性質を書くことに、はるかに多くの焦点が当てられるようになると思います。要件は不可欠です。
多くの場合、ソフトウェアが正確に何をすべきかさえ分かりません。
Ben Lorica。そして、Leoさん、これらのアプリケーションのいくつかは複雑ですよね？データベース、分散システムなどとやり取りします。
Leo de Moura。はい、はい。
Ben Lorica。そして、そう。では、どのように正確に—要件を固定することはできないのでしょうか、あるいはそれがあなたを区別するものなのでしょうか。
過去には、スーパースタープログラマーはスーパーコーダーでした。おそらく将来は、「OK、これらは複雑です。Kafkaを使います。Sparkを使います」と言える人々になるでしょう。そうでしょう。
Leo de Moura。はい、はい。しかし、モデルには不正確さがあるでしょう。時には人々が自分が何を望んでいるのか正確に知らないからです。
しかし、違いを見てください。以前は、人々はドキュメントを書いていました。データベースを設計する前に、設計、アーキテクチャを自然言語で説明するドキュメントを持っていました。一部の人々はWord文書を使って仕様を書いていました。
Ben Lorica。通常、何らかのアーキテクチャ図がありますね。
Leo de Moura。はい、まさに、まさに。しかし、その後どうなるか？今、これらの非公式なドキュメントがあります。実際のインプリメンテーションがこれらのドキュメントと一致しているかどうかを確認する方法がありません。人間がコードベースを調べて、両方を同期させて維持する必要があります。
それは面倒です。つまり、ドキュメントを変更すると、インプリメンテーションがまだ一致しているか確認する必要があります。私たち全員が、コードに同期していないコメントがあることを知っています。
しかし、すべてが形式的であれば、ドキュメント、設計がインプリメンテーションと一致しているかどうかを確認するツールが得られるでしょう。これは前進ですね。
確かに、不正確なドキュメントがあるでしょう。顧客はXを望んでいます。仕様はXプライムです。しかし、あなたは磨き続け、洗練し続けるでしょう。これが現在の真実です。
Ben Lorica。そして、それが現実世界とやり取りするにつれて、あなたは戻って—
Leo de Moura。まさに、そして洗練します。しかし、今あなたのコードには、コードが新しいモデルと一致していると言うツールがあります。それを洗練し、改善します。それは一致します。
例えば、「ああ、コードは検証された」と言う人もいます。多くの注意点があります。何かを検証するとはどういうことですか？書いた性質は、本当に望んでいる性質ですか？
つまり、あなたは性質を磨き続け、より正確にするプロセスにいるでしょう。一部のソフトウェアには—脅威モデルをモデル化するでしょう。システムを攻撃しようとする人々のために、脅威モデルを持つでしょう。
Ben Lorica。したがって、これらの説明、これらの要件ドキュメント、これらのPRDは、ソース管理システムで追跡するものになるということですね。なぜなら、基本的に、多くの点で、Leoさん、あなたは知っています、あなたがもっと学ぶにつれて、あなたは常に各バージョンを検証しています。
しかし、それは各バージョンで、AIにゼロから書かせることになるでしょう。前のコードを保存する必要はなぜあるのでしょうか？
Leo de Moura。はい、はい、そうです。
Ben Lorica。王冠の宝石はこれになり、最終的にはまだ人間によって所有および維持されることになりますね。
Leo de Moura。まさに、まさに。
Ben Lorica。はい、はい、はい、はい。そしてLeanのようなツールですね。
Leo de Moura。はい。
Ben Lorica。しかし、それはほぼCSカリキュラム全体を刷新する必要があるということですか？
Leo de Moura。いいえ、—
Ben Lorica。完全に、しかし—
Leo de Moura。完全にではありません。しかし、適応するでしょう。形式検証が必須科目でさえなかった多くの大学を見てきました。つまり、それは、これまで産業界では使用されてこなかった好奇心のようなものです。
形式検証への焦点は増えると思いますが、低レベルを学ぶことは依然として価値があると思います。つまり、常に低レベルのアセンブリコードを学ぶ人、低レベルの言語を学ぶ人、コードを書いてそれをチェックする方法を学ぶ人がいるでしょう。彼らは非常に低レベルでシステムを設計するのを支援するでしょう。
これは続くだろう。しかし、あなたは正しい、それは確かに変わるでしょう。
Ben Lorica。しかし、この世界では、Leoさん、あなたはコーディングに習熟していなくても、非常に生産的で需要の高いエンジニアになることができますね。
Leo de Moura。はい、これは起こるでしょう。まあ、ある意味では、あなたは書いています—それがまだコーディングだとしましょう。形式モデルを書くこと、証明を行うことはコーディングです。あなたは単に抽象化のより高いレベルで作業しているだけです。
Ben Lorica。はい、はい、はい、はい。ところで、あなたがこのフレーズを書いたと思いますが、私はそれが大好きです。もしあなたがこのフレーズを書いたのであれば、説明していただけますか？それは「検証済みスタック」です。
Leo de Moura。はい。
Ben Lorica。検証済みスタックとはどういう意味ですか？
Leo de Moura。ああ、検証済みスタックは、重要なソフトウェアスタックに関するものです。つまり、バグがあってもそれほど懸念されないコードの一部があります。例えば、ビデオゲームです。それはソフトウェアの一部です。バグがあっても、ユーザーにとっては迷惑ですが、そこにバグがあっても世界的な危機はありません。
重要なソフトウェアスタックは、オペレーティングシステム、コンパイラ、通信レイヤー、TCP/IPです。これがソフトウェアスタックという意味です。
そして、これらのすべてのコンポーネントのモデル、仕様があれば素晴らしいでしょう。専門家がそれらを書き、議論し、そして私たちは適切に検証を開始し、これらの仕様、コード、実際のコードがこれらの仕様と一致していることを確認します。
これは、将来投資する価値がある方向だと思います。
Ben Lorica。つまり、興味深いことに、Leoさん、あなたが大企業のCTOだと想像してみてください。そして、私がベンダーとしてあなたのところに来て、「Leoさん、私たちのソフトウェアを信頼してください。なぜなら私たちは形式的に検証されているからです」と言ったとします。
Leo de Moura。はい。
Ben Lorica。では、私があなたを騙していないことを確認するために、私に尋ねるべき重要な質問は何ですか？
Leo de Moura。仕様を見せてください。あなたの仕様、性質、検証したものを教えてください。
誰かが私の性質が単に真実であることを形式的に検証できます。それは基本的に性質がないと言っているようなものです。あなたは何も主張していません。
「私のコードは形式的に検証されている」という主張に注意すべきであるというあなたの指摘は絶対に正しいと思います。ただし、どの性質が検証されたかを正確に説明せずに。検証した仕様は何ですか？これが質問の種類です。
Ben Lorica。どの証明チェッカーカーネルを使用しましたか？
Leo de Moura。まさに。それも重要です。どのツールか？もう一つ重要なのは、信頼できるコードベースです。
信頼できるコードベースが大きいツールがあります。LeanやRocq、Isabelleのような他の証明支援系では、信頼できるコードベースを非常に小さく保つことに重点を置いています。
Ben Lorica。はい、はい、はい。そして明らかに、あなたのソフトウェアが同様の環境、つまり現実的な環境で実行されたことを私に納得させることができる限り—
Leo de Moura。はい。
Ben Lorica。おそらく、それは検証の主張の背後にある肉付けを加えるでしょう。
Leo de Moura。はい。
Ben Lorica。はい、はい。そして、ソフトウェアは静的なものとして扱いますが、今やエージェントと呼ばれるソフトウェアがありますね。そして今、私たちは長期間実行されるエージェントの世界に入っています。
Leo de Moura。はい。
Ben Lorica。では、エージェントの世界で検証とは何を意味するのでしょうか？
Leo de Moura。はい、素晴らしい質問です。まず、これらのエージェントにガードレールを設けることです。信頼できるサンドボックスがあれば素晴らしいでしょう。
つまり、過去数週間、多くの人々がエージェントがサンドボックスから脱出していると主張しているのを見てきました。
したがって、検証済みソフトウェアスタックの一部はサンドボックスです。信頼できるサンドボックス、良い仕様、そしてインプリメンテーションがこれらの仕様を満たしているという証明が必要です。
また、エージェントの動作に関するポリシーを記述できるようにしたいと考えており、これらのポリシーを強制するコードが形式的に検証されていることを確認したいと考えています。
エージェントができること、できないことに関するポリシーを記述するのにすべての時間を費やしたと想像してみてください。そして、ポリシーを強制するコードにバグがあったらどうなるでしょうか。
Ben Lorica。しかし、別のエージェントが形式検証を行っていたらどうなるでしょうか？つまり、信頼の層があるわけですね。
Leo de Moura。はい、はい。人々が検討している可能性の一つは、エージェントがLeanカーネルの欠陥、またはLeanカーネルが実行されているランタイムの欠陥を悪用できるかどうかということです。
これらは妥当な質問であり、だからこそ複数のカーネルがあるのです。なぜなら、エージェントが欠陥を見つけたとしても、それは証明していないことを証明したと信じ込ませようとするでしょう。そして、その証明書、その証明は、さまざまな—で実装された複数のカーネルによって受け入れられる必要があります。
Ben Lorica。独立して、はい。
Leo de Moura。まさに。これは深刻です。つまり、これらのエージェントは脆弱性を見つけるのが非常に得意です。
Ben Lorica。では、あなたが議論したこと、特にエージェントのための検証を使用している人々と交流したことはありますか？
Leo de Moura。はい。AWSでは、AgentCore、Dogwoodがあります。それらはすべて現在Leanを使用しています。
外部では、例えば、Leanを使ってClaude Codeのバグを見つける例を挙げました。そのようなプロジェクトはますます増えるでしょう。なぜなら、形式検証やLeanのようなツールの主な問題の一つは、急峻な学習曲線だったからです。
Leanを学び、これらのモデルを書く必要がありました。始めるにはあまりにも多くの労力がかかります。しかし、AIを使えば、開始コストを削減できます。
Borisが投稿したビデオのように、すぐに価値が見られます。彼はClaudeにLeanを使ってClaude Codeを検証するように頼んだだけで、すぐに価値を得ました。
そして今、それは価値があるのです。すぐに価値が得られると、テクノロジーを学ぶことにさらに時間を投資するようになると思います。
それから、「ああ、おそらく私のコードに関する形式的な性質を書きたい。ああ、おそらくLeanコードの読み方を学ぶべきだ。書くことはしたくないが、読めるようになりたい。AIエージェントが作成したモデルが正確かどうかを判断できるようになりたい。そして、エージェントとモデルの正確性について議論したい」と言うでしょう。
Ben Lorica。では、長期間実行されるエージェント、つまり、数日間、探索、研究、互いに調整を行う可能性のあるエージェントについてですね。要件を固定することが明らかに課題の一つであると議論しました。
Leo de Moura。はい。
Ben Lorica。つまり、人間がすべての方向を探索するようなものの場合、そのようなものの要件をどのように固定できるのでしょうか？
無限のリソースを持ち、世界中を旅でき、何でもできる人間を想像してみてください。
Leo de Moura。はい、はい。それは大きな課題ですが、AIは開始を助けることができます。最初のモデルを書くことができます。
そして、「ああ、このように形式化するのか」と言うでしょう。エージェントシステムは複雑なシステムです。複数のコンポーネントが互いにやり取りしています。そこにはプロトコル、これらの異なるコンポーネント間の通信プロトコルがあり、これらのプロトコルが正確で、正確であることを確認したいのです。
AIエージェントは、形式モデルの開始を助けてくれます。それはほとんど最初のドラフトを提供してくれるようなもので、そこから反復し続けることができます。
Ben Lorica。したがって、私たちが現在議論しているすべてのことのゼロ地点は、コーディングと数学のようですね。
Leo de Moura。はい。
Ben Lorica。そして数学、過去数週間で、フィールズ賞受賞者が泣いています。つまり、分野全体が大きく混乱しています。
Leo de Moura。はい。
Ben Lorica。そうですね。私の博士号は数学です。以前はその分野にいましたが、あまり得意ではありませんでした。まあ、無限の計算リソースがあれば、今ならできるかもしれません。
しかし、そうですね。その場合、LeanとMathlibの組み合わせが、コーディングよりも数学をさらにスイートスポットにしているように思えます。間違っていますか？
Leo de Moura。いいえ、いいえ、いいえ。Mathlibが提供するものは—Mathlibは、強い数学的背景を持つ数学者によって構築されました。そのため、そこでの定義は正確であることがわかっています。
Ben Lorica。しかし、それは何年も前に始まったはずです。だから彼らは、私たちは炭鉱で地道に働いており、誰も私たちのやっていることを評価していないという先見の明を持っていたはずです。しかし、スケーリングすれば—
Leo de Moura。はい。彼らが始めたとき、AIがこれほど良くなるとは誰も予想していなかったと思います。
しかし、彼らの考えでは、数学コミュニティにとって一つの勝利は、Leanが大きな数で作業するのに役立つことを認識したときでした。
Ben Lorica。はい。
Leo de Moura。例えば、2024年に、Terence Taoはプロジェクトを小さな部分に分割するプロジェクトを持っていました。彼は建築家のようなものでした。
Ben Lorica。はい、はい、はい。そして、彼が個人的にすべてを検証する、すべてを検証する、つまり—
Leo de Moura。AIエージェントの代わりに、彼は多くの人間を雇って、彼が会ったことのない多くの人々—彼のために穴を埋めさせました。彼は自分で証明をチェックする必要はありません。それは、人間が彼の大きな設計の穴を埋めているようなものです。
そして人々は、「すごい、これは素晴らしい」と言いました。彼がアマチュアと協力するとは思ってもみなかったと私に言っていたのを覚えています。彼はプロフェッショナルとしか協力しません。
Ben Lorica。はい、これは戻ります。これは、あなたが非常に早い段階で言ったことに戻ります。それは信頼です。
Leo de Moura。はい。
Ben Lorica。つまり、多くの意味で、数学、ほとんどの科学は信頼に基づいていますね。
つまり、私は数学者です。定理を証明しています。過去の多くの、多くの他の定理を引用しています。おそらく50年前のものです。個人的には証明の方法を知りません。それらが正しいと信じているだけです。
Leo de Moura。まさに。
Ben Lorica。そして、これが彼らがMathlibで行ったことです。
Leo de Moura。まさに、まさに。しかし、当時、Terryが講演していて、「まあ、いつかAIエージェントがループに入るだろう。彼らはこれらの穴を埋めるだろう」と言っていたのを覚えています。
しかし、誰もそれがこれほど早く、瞬時に起こるとは想像していなかったと思います。
Ben Lorica。はい、はい、はい、はい。
Leo de Moura。数ヶ月前、誰もこれを信じなかったでしょう。6ヶ月前、Lean開発者、Lean Mathlibメンテナーの誰かに、「ああ、これほど有能なAIができるだろう」と言ったら、彼らは信じなかったでしょう。
Ben Lorica。しかし今、自動形式化のおかげで、AIが数学をLeanに翻訳する能力のおかげで、これは続くだろうと思います。これはLeoさんに質問を投げかけます：なぜ理論物理学ではこれができないのですか？
Leo de Moura。まあ、LeanにはPhyslibというライブラリがあり、そこで物理学をマニュアルで形式化しています。
まあ、今では彼らもおそらくAIに切り替えたと信じています。誰もがAIに移行していると思います。つまり、Lean開発者でさえ、私たちは今AIを使って実装しています。
それは面白かったのは、それが「ああ、AIはバグを見つけてバグを分離するのに本当に優れている。ああ、AIはライブラリを修正するのに本当に優れている。ああ、AIはコードを書いている。ああ、すごい、それは私たちよりもコードを書いている」というように始まったからです。
Ben Lorica。では、数学ほど混乱する物理学のタイムスケールはどうなりますか？理論物理学。
Leo de Moura。彼らは最初の勝利を収めました。つまり、数ヶ月前、彼らは重要な物理学論文のバグを、結果を形式化しようとして見つけました。
ここでの課題は、物理学では、現実世界のモデルを作成しているということです。私たちのモデルは常に不正確です。それらはモデルです、つまり、現実世界のモデルです。
Ben Lorica。まあ、それらは理論的に始まりますね。例えば、弦理論は実験的に証明されたことはありません。
Leo de Moura。はい。
Ben Lorica。したがって、実験がまだ行われていない理論物理学の分野にいる可能性もありますが、それでも進歩して論文を発表できます。そして、それらの人々はすぐに混乱する可能性がありますね。
Leo de Moura。はい、はい。彼らは今、Leanを使って非常に正確な数学モデルを書くことができます。はい、これは完全に可能です。
Ben Lorica。そして、Navier-Stokes以来、そしてOpenAIがさらに多くの結果を発表して以来、個人的に数学者の友人から「Leoさん、私たちの分野に何をしたのですか？」と聞いたことはありますか？
Leo de Moura。いいえ、多くの複雑な感情があります。一部の人々は非常に興奮しています。つまり、「想像を超えた問題に取り組むことができる」ということです。
心配している人もいます。つまり、学生、「私の将来はどうなるのか？」ということです。
つまり、ソフトウェア開発と同様に、開発者はいるでしょう。仕事は異なりますが、彼らはいるでしょう。数学も同様です。
はい、つまり、大きな混乱です。怒っている人もいれば、興奮している人もいれば、恐れている人もいます。しかし、これは良い変化になることを願っています。
Ben Lorica。だから、私の心の中の質問—私はこのことについて考えてきました—それは、過去に、ソフトウェアエンジニアリングを脇に置いて、数学では、あなたは最高の数学者が誰であるかを知っていましたね。
つまり、彼らと話し始めると、彼らはあなたよりもはるかに多くのことを知っています。つまり、彼らはより速いです。彼らはあなたよりもはるかに多くのことを知っています。彼らはあなたよりも難しい定理を証明できます。
それは、IQが—どうすることもできないようなものです。つまり、だから私はその分野を離れたのです。
しかし今、それは変わりますか？それは将来、フィールズ賞を獲得する人を変更しますか？
だから、おそらくそれは賢い人ですが、異常に賢いわけではなく、より多くのコンピューティングにアクセスできる人です。わかりません。
それで、あなたは考えましたか—ソフトウェアでは、同じだと思いますね？もし私があなたよりも多くのコンピューティングにアクセスできれば、より多くのことを成し遂げることができるかもしれません。間違いなくあなたよりも多くのことを成し遂げるでしょう。
Leo de Moura。はい、まさに、まさに。はい、あなたが言ったことはすべて真実だと思います。
つまり、私にとって、私のスーパーパワーの一つは苦痛に耐える能力でした。つまり、ソフトウェア開発は苦痛です。
Ben Lorica。はい、はい、はい、はい。定理を証明することも苦痛です。
Leo de Moura。はい。はい。
Leo de Moura。AIはこの苦痛を取り除きましたが、はい、私のスーパーパワーは失われました。私のスーパーパワーは、過去ほど有用ではありません。
しかし、私たちはより速く動くことができるでしょう。つまり、より多くのことを達成できるでしょう。それは良いことだと思います。
つまり、あなたは、異なるスキルセットを持つ人が将来より価値があるかもしれない、あるいは—より有用であると言うのではなく—テクノロジーをより良く活用できるかもしれないと言ったのは正しいです。
トークンへのアクセスに関する問題があるでしょう。しかし、科学では常にそれを見ます。例えば、ジェイムズ・ウェッブ宇宙望遠鏡です。
Speaker 1。はい。
Leo de Moura。あなたは—提案を書く必要があります。望遠鏡へのアクセス権を得ます。それはキューに入ります。
将来も同じことが数学でも起こると信じています。つまり、莫大な費用がかかる大規模なプロジェクトがあります。しかし、提案を書くでしょう。おそらく資金提供されるでしょう。非常に強力なモデルへのアクセス権を得るでしょう。
Ben Lorica。モデルがより効率的になり、チェスのように—
Leo de Moura。はい。
Ben Lorica。つまり、チェスでは、私はこれに追いついていません。Leoさん、ラップトップで実行できるチェスプログラムとクラスターで実行されるチェスプログラムの違いはありますか？それは私に—わかりません。
Leo de Moura。私はチェスプレイヤーではありませんが、私の認識では、コンピューターで実行されるものはすでに非常に優れています。
つまり、そしてあなたが正しいことを願っています。コンピューターで実行できるモデルも手に入るでしょう。しかし、ここでは賭け金が非常に高いので、常にスーパーコンピューターがあるだろうと信じています。
ジェイムズ・ウェッブ宇宙望遠鏡のようなものです。非常に優れた望遠鏡を購入できます—
Ben Lorica。はい。
Leo de Moura。そして家に置くことができますが、ジェイムズ・ウェッブははるかに優れていますが、はるかに高価です。
Ben Lorica。つまり、将来を見据えると、これらの学術会議のいずれかに参加する場合、数学では、かつて人気があったのは最も賢い男、フィールズ賞受賞者でした。今ではクラスターを持っている男です。
まあ、誰もがクラスターを持っている男と話したがっていると思います。
Leo de Moura。まあ、おそらくこの男はアイデアを持っている男でさえありません。つまり、ジェイムズ・ウェッブ宇宙望遠鏡を管理する委員会があるかもしれませんが、科学者は常に提案を提出し、アクセス権を得ています。
つまり、将来も同じことが起こると思います。
Ben Lorica。それで、コーディングから始まり、明らかに数学へと進みました。物理学についても推測しました。
では、他にどのような分野で、あまり注目されていませんが、Mathlibと同等のもの、あるいはそれに類するものが起こっているのを見ていますか？
Leo de Moura。多くの人々が金融に興味を持っているのを見ています。金融には多くのアルゴリズムがあります。つまり、人々はこの分野に興味を持っています。
Ben Lorica。しかし、アルゴリズムは—数学では証明があります。理論物理学では証明があります。しかし—
Leo de Moura。金融には多くの数学があります。
Ben Lorica。はい、はい、知っています。
Leo de Moura。形式検証をこの分野に適用することに興奮している人々を見てきました。より正確なモデルを使用しています。
Ben Lorica。しかし、そこでの課題は、彼らはオープンに仕事をしていないということですね。つまり、彼らは秘密主義です。
Leo de Moura。はい、はい、はい。
Ben Lorica。では、Mathlibのようなものをどのように思いつくのですか？
Leo de Moura。はい、はい。私は、取引アルゴリズムにオープンな人々がいると思います。おそらく彼らはすべての秘密を保持したいでしょう。
しかし、金融には数学的背景があり、人々はそれを形式化して公開したいと考えています。
しかし、あなたは正しいです。秘密のソースを保持する人々もいるでしょう。
Ben Lorica。それで、金融。他に何がありますか？
Leo de Moura。化学、生物学でもライブラリを構築しようとしている人々がいると思います。つまり、どんな分野でも。
Ben Lorica。そして、あなたが挙げた各分野での相対的な進捗はどうですか？つまり、どれくらい進んでいますか？
Leo de Moura。ああ、それらはすべて—Mathlibが圧倒的に先行していると思います。なぜなら、数学は正確だからです。
次に物理学ライブラリがあり、次にMathlibに追いつこうとしているコンピュータサイエンスライブラリがあります。
次に、金融、化学の新しい取り組みがあります。
しかし、各分野の論文を見ると、それらの論文の正確さ、厳密さがわかります。これらの論文の数学は、形式ライブラリを作成するのがどれほど難しいかを示唆してくれるでしょう。
Ben Lorica。はい、なぜなら理論化学と計算化学があるからです。
Leo de Moura。はい。
Ben Lorica。しかし、Leoさん、自動形式化のおかげで、この方向に進むと決めたコミュニティは、より速くそこに到達するのではないでしょうか？なぜなら、Mathlibの人々は長年秘密裏に苦労していましたが、自動形式化が起こると、ブームが起こったからです。
Leo de Moura。まさに。はい。
Ben Lorica。では、科学以外の分野で、これが起こる可能性があると思いますか？
例えば、いくつか例を挙げますが、うまくいかないと思います。
会計。一般に認められた会計原則があります。税法があります。税法とGAAPは、多くの意味で私の定理です。
Leo de Moura。はい。
Ben Lorica。しかし、問題はこうです。会計士数人にこのことについて話しました。問題は、ここに資金があります。これをここに置くべきですか、それともここに置くべきですか、というようなことです。つまり、それは主観的です。
Leo de Moura。はい、はい、はい。法律の形式化を試みている人々を見てきました。
Ben Lorica。ああ、そうですね、はい。私も誰かにこのことについて話しました。しかし、法律の問題は、私たちが互いに訴訟を起こしている理由は、意見が異なるからです。
Leo de Moura。はい、まさに。しかし、法律には部分があります。かつてインターンだった人がいました。彼は弁護士です。彼は今弁護士です。
つまり、例えば、民事訴訟手続きは非常に、非常に—
Ben Lorica。形式的です。それはほとんど—
Leo de Moura。プログラムのようなものです。
Ben Lorica。ああ、本当に？
Leo de Moura。はい、はい。法律には形式化できる部分があります。
Ben Lorica。なるほど。はい、はい、はい。そして、Leoさん、ありがとうございました。
Leo de Moura。ありがとうございます。どうもありがとうございました。どうもありがとうございました。