数学的超知能の実現を目指すHarmonicのTudor Akimが、AI数学システムの現状と未来を語る。国際数学オリンピアードで金メダル級の性能を達成したAIシステムは、形式証明言語Leanを活用することで幻覚を排除し、検証可能な数学証明を生成する。探索とパターン認識を組み合わせたハイブリッドシステムは、既に数学者の協働パートナーとして機能しており、将来的には人間の介入なしに複雑な数学問題を解決する可能性を秘めている。数学者の役割は証明の生成から問題の選定と方向性の決定へとシフトし、形式検証による正確性保証が数学研究の新たな標準となる時代が到来しつつある。
AIによる数学的超知能への挑戦
今日のゲストはHarmonicのTudor Akimです。Harmonicはharmonic.funで見つけることができます。タグラインは「私たちは数学的超知能を構築しています」というものです。それでは、Tudorさん、ポッドキャストへようこそ。
お招きいただきありがとうございます。ここに来られて嬉しいです。
さて、ここでの数学というのは、リスナーの皆さんのために申し上げると、算数ではなく本物の数学のことです。実際には2つの領域をカバーすることになります。1つは大まかにコンテスト数学と呼ばれる領域、つまり国際数学オリンピアードのようなものです。そしてもう1つは実際の研究数学で、プロの数学者が自分の分野で進歩を遂げようとしているものです。主に定理の証明ですが、必ずしもそれだけではありません。
数学的超知能とは何か
それでは、数学的超知能についてお聞きします。Tudorさん、数学に全く馴染みのないリスナーのために説明すると、超知能という言葉は通常、何らかの基盤モデルを連想させます。それで、皆さんが構築しているコンポーネントの1つはそれなのでしょうか。実際のシステムについては後で詳しく説明していただきますが、その要素の1つは何らかの形の基盤モデルなのでしょうか。
数学的超知能自体は、それがどのように実装されるかについて何も言及していません。私たちはそれを、地球上のどんな人間の集団よりも高度な数学ができるAIシステム全体として定義しています。そして、私の考えでは、どんな数学的超知能システムにも2つのコンポーネントがあります。それは探索とパターン認識です。
探索は、数学のフロンティアを探求して何が機能し何が機能しないかを確認するために使用するものです。そしてパターン認識は、探索の結果を圧縮するコンポーネントで、次に問題を解こうとするときにその恩恵を受けることができます。
その観点から、私たちはもちろんシステムの一部として大規模言語モデルを使用していますが、もし何かより優れたパターン認識の基本要素が登場すれば、それも喜んで使用します。数学的超知能を特定のモデルアーキテクチャや基盤モデルと呼ばれるものに結びつけているとは考えていません。
コンテスト数学における現在の到達点
この分野を詳しく追っていないリスナーのために、Tudorさん、コンテスト数学、つまり国際数学オリンピアードに関しては、現在いくつかのシステムが大体金メダルレベルにあると言って良いでしょうか。
確かなことは、2025年の国際数学オリンピアードで、いくつかの企業が内部システムで金メダル性能を主張したということです。OpenAIとDeepMindは非形式的推論を使用し、Harmonicは形式的推論を使用しました。ByteDanceもseed proverで少し後に金メダル性能を発表したと思います。
ですから、その時点のスナップショットでは、それができるシステムがいくつかあったと思います。次の国際数学オリンピアードで何が起こるか興味があります。私の見解では、競技後に事後的にテストするのは本当に物事を測る方法ではありません。ですから、次の7月まで、つまりこの来る7月まで判断を保留したいと思います。しかし、大まかに言えば、最近では国際数学オリンピアードで金メダルを取れるだけの能力を持ったシステムがあると思います。
しかし、文脈を説明すると、2、3年前にはこれらのシステムはこの能力には全く近づいていませんでしたよね。
そうですね、2、3年前は基本的な高校数学のコンテストでさえ苦戦していたと思います。しかし、兆候はあったと思います。いつか話すかもしれませんが、高校数学コンテストと形式検証における生命の兆候が、Harmonicの創設につながったと思います。ですから、この3年間で目覚ましい進歩があったと思います。
ハイブリッドシステムのアーキテクチャ
それでは、高いレベルで、人々が落ち着いたと思われるアーキテクチャについて簡単に議論しましょう。私は皆さんのシステムにあまり詳しくありませんが、例えば、DeepMindは少なくとも高いレベルでAlethiaシステムを説明しています。それは皆さんのシステムと似ているように見えるハイブリッドシステムのようです。つまり、神経的直感に何らかの記号的検証を加えたものですね。実装の詳細はシステムごとに異なりますが、これが進むべき方法だというのが多かれ少なかれ一般的な合意なのでしょうか。
合意があるとは言えません。世界は急速に変化していると思います。私がコメントできるのは、国際数学オリンピアードの時点でのHarmonicシステムの状態だけです。それは技術報告書で公表しましたが、ハイブリッドシステムでした。
ですから、非形式的推論ができる一種の曖昧な推論システムがあり、そして形式的推論ができる形式的推論システムがありました。そして、それらの相互作用が問題を解決する探索トレースにつながりました。しかし、人間が解釈可能な推論さえ気にしないようなより高度なシステムを簡単に想像できます。
その時点での合意が何であれ、あるいは現在の合意が何であれ、1年後のシステムがどのようなものになるかを必ずしも示すものではないと思います。
しかし、一般的なAIシステムに精通しているリスナーにとって、数学者のインターフェースは人々が慣れ親しんでいるものと似ていますよね。つまり、彼らはテキストを使ってこれらのシステムと対話します。
はい。
そして、バイブコーディングのような感じで対話するのですよね。
そうですね、私たちはそれを証明執筆と呼んでいます。ええ、証明執筆は非常に適切だと思います。コーディングエージェントと対話しているときは、ほとんどペアプログラミングのような、そういう対話ですよね。
この場合、数学者はシステムとアイデアを練ることができます。そしてシステムは新しいアイデアを提案することさえあるかもしれません。その場合、仮説の数はもはや数学者の想像力や知識に限定されません。
分野を超えた知識の統合
研究数学に馴染みのないリスナーのために説明すると、研究数学はやや専門化されています。ある分野の人々は、文字通り別の分野の論文の冒頭段落すら理解できないかもしれません。
しかし、数学における多くの進歩は、誰かが偶然にも「量子場理論からのアイデアがトポロジーに応用できるかもしれない」というような繋がりを見つけることができたときに起こることがわかっています。
しかし、問題は、実際に幅広く文献をスキャンする人がほんの一握りしかいないということです。ですから、これらのシステムができることは、基本的に他の分野からアイデアをスキャンできるようにすることだと思います。
そうですね、これは分野内でさえ起こっていると思います。2、3ヶ月前に解決されたErdősの問題のいくつかでは、数十年前に人々が発表した論文に非常に似たアイデア、あるいは同じアイデアがあったことがわかりました。これらのアイデアは、AIがそれらを見つけて問題を解決する際に効果的にそれらを参照しなければ、完全に見過ごされていたでしょう。
ですから、数学的発見は挑戦だと思いますし、AIはそれに大いに役立っています。あなたが言及した点に触れたいのですが、現在AIは数学者のペアプログラマーです。これは非常に一時的な設定だと思います。チェスでいわゆるケンタウロスシステムで見たのと同じことだと思います。
チェスのケンタウロスシステムからの教訓
ちょっと待ってください。リスナーのために説明すると、IBMのDeep Blueのブレークスルーがあり、そこでAIシステムが初めて人間を打ち負かしました。そしてしばらくの間、オープン競技での最高のシステムは機械と人間の組み合わせでした。それで今あなたが言っているのは、もはや人間さえ必要ないということですね。
ええ、システムに人間を加えることは、システムのパフォーマンスを損なうだけです。私は、RenaissanceテクノロジーズのBob MercerかPeter Brownのどちらかの面白い引用を覚えています。あるいは彼らのうちの一人が、昔IBMで音声認識に取り組んでいたときのことです。
それは実際、最も初期の実用的な機械学習モデルの1つで、これらの隠れマルコフモデルです。そして彼らには「言語学者を解雇するたびに、私の統計的機械翻訳のパフォーマンスが上がる」というような面白い引用がありました。
近い将来、数学者の役割は重要な問題を定義し、これらの計算システムを正しい方向に向けることになると思います。しかし、AIにアイデアを与えることで最も役立つかどうかはわかりません。なぜなら、AIは仮説を提案し、それらを評価し、優先順位を決め、それらを解決するために独自の計算予算を割り当てることを自分自身で非常に上手くできるようになると思うからです。
しかし、あなたが言ったように、趣味はまだ重要ですよね。何が興味深い問題かという点で。
最終的に、数学は人間の営みであり、人間にとって有用でなければなりません。その一部は、人間によって方向づけられなければならないということを意味します。私たちは数学として、私はここで王様の「私たち」を使っています。私は数学者ではありません。私はコンピュータ科学者ですが、数学コミュニティは自分自身で何を気にかけるか、どの問題が最も重要かを決定しなければなりません。
Riemann予想に割り当てたいのか、量子場理論と他のすべてとの間の同型性を見つけたいのか。そして、そこに人間の理解がまだ必要だと思います。どこに予算を投入するかを選択しなければなりません。
現在の数学者の役割
それは未来を見据えたものですね。少なくとも今のところ、数学者はまだ役割を果たしていますよね。システムと対話します。Poincaré予想やFermat’s Last Theoremなど、あるいは他の多くの同様に難しいかもしれないがあまり知られていない問題を解決するような種類の天才性をまだ見ていません。
そのような創造性をAIがまだ持っているとは思いません。既存の技術を非常に奇妙な方法で組み合わせて結果を得ることには極めて強いと思います。しかし、この種の洞察の閃きと発見される美しい構造については、AIがまだそこにいるとは思いません。
実際、数学者のグループがFirst Proof Challengeと呼ばれるものをまとめたと思います。それは基本的に彼らの分野からの補題の束で、どういうわけかこれらすべてのシステムがまだこれらの問題に取り組むことができません。そして、問題を解決できる稀な機会では、それはどこかで読んだものに過ぎないことがわかります。
その観点から、あなた方にとってまだ多くの構築が残っているので興味深いと思います。
それは公平な質問だと思います。強化学習をスケールし続けることがそのような洞察の閃きにつながるかどうか。答えは、50%以上の確率でイエスだと思いますが、何かを見逃している可能性もあります。
例えば、AIシステムを人間のデータから完全に独立して訓練しなければならないかもしれません。そのような洞察を得るために。物理的直感が鍵で、それを見逃しているかもしれません。わかりません。少なくとも30%の確率で何か違うことが起こらなければならないと思いますが、それがこの分野を刺激的にしているものです。
形式証明言語Leanの役割
コーディングエージェントに馴染みのあるリスナーのために説明すると、コーディングの利点の1つは、明らかにコードをコンパイルまたは実行して、それが動作することを確認できることです。
しかし、数学でも同様のことがある程度可能であることがわかります。なぜなら、LeanやMathlibのような形式定理証明器があるからです。しかし、Tudorさん、これらのシステムが何であるか説明してもらえますか。多くの人々がこれらのシステムを見たことも触れたこともないので。非数学の人々にわかるように説明してください。これらのシステムが正確に何であるか。
もちろんです。正確性の観点からは、プログラミング言語のコンパイラよりもはるかに強力だと言っておきます。Leanの考え方は、C++やPythonのようなプログラミング言語ですが、はるかに高度な型システムを持っており、非常に複雑な論理概念を表現できるということです。
そのような豊かな型システムを持っているため、すべての数学をその中にエンコードできることがわかりました。そして型システムにエンコードされているため、コンパイラは書かれている数学的ステートメントが論理的推論の有効な規則に従っているかどうかを自分自身でチェックできます。
Leanが行わないのは、定理の証明を自動的に見つける言語であるということです。それが行うのは、推論のすべてのステップを1つずつ、コンピュータが幻覚のない方法でチェックできる形で表現させることです。
私たちは実際、Harmonicの初めに形式検証された数学を使用することに決めたのには2つの理由があります。最初の理由は、それが人間にとって有用だと思ったからです。2023年7月に、初めに思考実験がありました。もし10年後にRiemann予想をAIに証明させたら、当時のシステムの様子に基づくと、何らかの人間の言語で10万ページのテキストが返ってくると思いました。
そして、それは捨てた方がいいと感じました。なぜなら、第一に、それはおそらく間違っているし、第二に、たとえ間違っていなくても、それがどのように機能するかを理解できないほどの量のコンテンツだからです。しかし、代わりにLeanで証明を得たと想像してください。
まず第一に、コンパイルされるので正しいことがわかります。しかし、おそらくもっと重要なのは、コードベースのように構造化されていて、定義にジャンプして物事の使い方を理解し、物事がどのように相互作用するかを理解できることです。そして、それは人間にとって非常に強力だと思います。
ですから、AIが行う数学を人間が理解できるようにしたいなら、Leanが使うべき正しい言語だと感じました。
私たちがそれを選んだ2番目の理由は、Leanのコンパイルという気密な報酬シグナルがあれば、人々が以前やっていた方法よりもはるかに効率的に強化学習ができると感じたからです。そして、2023年10月に実質的にゼロから2025年の国際数学オリンピアード金メダル性能に到達することで、それを証明したと思います。
ですから、Leanを気にかける理由はたくさんあると思います。内部的な観点からは、効率性が素晴らしいですが、外部的な観点からは、これが数学の未来であるべきだと思います。人々がもはや正確性について心配する必要がなく、趣味と影響について心配するだけでよい未来です。
そして、Leanの周りにはMathlibと呼ばれる付随するコミュニティがあります。それはあなた方も活用しているものですか。もしそうなら、リスナーにMathlibが何であるか説明してください。
ええ、私たちはMathlibを使っています。私たちはそれに貢献する人々をスポンサーし、エージェントをそれと互換性があるように更新しています。私たちはそれを非常に気にかけています。
Mathlibは世界最大のオープンソース数学リポジトリです。それは本質的に学部および大学院レベルの数学と考えることができます。それらすべての教科書、まあその10%を取って、それを形式化すると想像してください。それが本質的にMathlibです。
Harmonicが出力するすべての証明は、Mathlibに依存する傾向があります。なぜなら、コンテスト数学をやっているか研究数学をやっているかに関わらず、どんな証明でもそれらの基本的な数学概念を使用するからです。
Mathlibの素晴らしい点は、完全にオープンソースで分散化された方法で数十万の定義、数百万行のコードに到達したことです。ですから、それを数学のWikipediaと考えることができますが、すべての編集が正確性についてコンピュータで認証されています。
すべての数学が他のすべての数学と互換性のある方法で実装されているのは素晴らしいことです。ですから、サブフィールド間の同型性を見つけることについて話すとき、Mathlibのようなものがあると実際に簡単になります。なぜなら、すべてが一緒に適合することがわかっているからです。
MathlibとAIシステムの相互作用
これらのシステムは、Tudorさん、Mathlibに入ってシステムを指して、「このより優雅な方法を見つけられますか」と言えるところまで到達しましたか。
ああ、そうです。ええ、ええ。
では、Mathlibも今やこれらのシステムによって改善されているわけですね。
ええ、そして人間には一種の、彼らはAIを担当することになると思うので、人間からもっと見たいことの1つは、単に定義に合意することだと思います。人間が数学の特定の部分の定義に合意すれば、AIに行かせて定理を証明し、他の構造や補題などを構築させることができます。
しかし、人間が構造と定義を作らなければ、あなたが必ずしも望まない方法で多様体の定義を作成するAIを得るかもしれませんし、作成された人間の数学の多くと互換性のない定義を作成するかもしれません。
ですから、AIが貢献するための構造を人間が配置するのは人間次第だと思います。それがMathlibであれ、他の数学研究の取り組みであれ、将来的には。
数学分野による受容度の違い
ええと、見てみましょう。数学の特定の分野で、コミュニティがこれらのツールにより開かれているように見える分野はありますか、それとも個人レベルでのことでステレオタイプ化するのは難しいですか。言い換えれば、私が出身のPDEコミュニティ、偏微分方程式は、数論学者よりもそれに対してより開かれていますか、それとも
みんな開かれていると思います。みんながこれが未来だと見ていると思います。Pat Shafterが運営するDARPAプログラムのキックオフであるExponentiating Mathematicsという小さな会議から戻ってきたばかりです。数学におけるAIツールへの熱意は信じられないものでした。
みんなが推論の未来だと見ていると思います。形式検証された数学に関しては、Mathlibで他よりもよく表現されている数学の特定の部分があると思います。
例えば、代数幾何学の多くの重要な定義は、形式化しようと試みられてさえいません。あるいは試みられていても、Mathlibに入らない孤立したプロジェクトのようなものです。そして、それは代数幾何学で研究してからコンピュータでチェックしたい場合、運が悪いということを意味します。最初に基本をやらなければなりません。
対照的に、数論、グラフ理論のいくつかの分野、そしてPDEでは、はるかに多くの数学が形式化されていると思うので、Aristotleでそこで数学をすることができます。
大学院時代に私を狂わせた1つの分野があります。幾何学的トポロジーと呼ばれるものです。彼らは絵を描いて、ここで手術をしますと言いますが、論文を見ると、方程式はほとんどありません。すべて言葉です。
ええ、それを形式化するのにまだそこまで達していません。
ええ、それがどれほど簡単に形式化できるかはわかりません。
数学者の現在のワークフロー
あなたは未来のビジョンを説明しました。しかし現在に留まりましょう。現在のプロの数学者の現在のワークフローは何ですか。
多くの人が独自のワークフローを開発していると思います。私たちがAristotleの使用を見る方法、それが私が最もよく知っているものですが、数学の質問があって、時々Aristotleに行って質問するだけで、Aristotleが多くの分析を行って形式検証された結果を返します。
ちょっと待ってください。その質問は、「これはまだ未解決ですか」というものでもいいのですか。
ええ、尋ねることはできます。何を教えてくれるかわかりませんが、ええ、絶対に尋ねることができます。しかし素晴らしいことは、AristotleにはWebUIがあります。先週それをローンチしたばかりで、質問をすることができ、それが考えて返事をします。
私たちが人々が多くやっているのを見るもう1つのことは、より明確に定義された論文に近づき、多くのアイデアを埋めていくにつれて、それが正しいことを三重チェックするためだけにAristotleを使い始めることです。
ですから、数学者、経済学者、統計学者であれば、Aristotleを自動形式化モードで使うこともできます。そこではPDFやLaTeXファイルなど、ファイルが何であれアップロードします。
怠惰な視点からのワークフロー
ええ、ええ。それで、それが私が尋ねようとしていたことです。怠惰な視点から、LaTeXやPDFファイルをアップロードするだけでいいのですか。それがそれを読んで、やらなければならないすべてのことをやってくれますか。
ええ、Twitterに行けば、これをいつもやっていてたくさんの人がいます。投稿していますよ。私たちのビジョンは、数年以内にAristotle APIを使って、Riemann予想が書かれた黒板の写真を撮るだけで、コンピュータがそれを解いてツイートするようになることです。
OCRから始めるのですか。
まさにそうです。ええ、ええ、ええ。それは簡潔に述べられていて、すでにMathlibにあります。だからステートメントはすでにあります。
それで質問をして、システムとブレインストーミングをして、ある時点で、「さて、計画があると思います。やってください」とシステムに言うのですね。コーディングエージェントと作業しているときのように。仕様駆動開発ですね。これがやることで、エージェントと対話して、「さて、コードを書いてください」と。
繰り返しになりますが、これはケンタウロスシステムに少しなりすぎていると思います。今は絶対に仕様やスキャフォールドや青写真を与えてそれに従わせることができますが、そのようなことを気にしない未来に急速に進んでいると思います。LaTeXファイルやPDFを渡して、「これまで持っていたアイデアです」とか「ほぼ完成した論文です。これを修正して完成させてください」と言うだけです。
ええ、ええ、ええ。今でもコードと同じことですよね。「コードがあります。満足していません。これができるようにしたいです」と。正しいライブラリを使っているかどうかさえわかりません。それを見つけて、修正してください、ですよね。
ええ、つまり、これらのコーディングエージェントでは、出力をレビューすることを強くお勧めします。それに依存する前に。しかしLeanでは、ステートメントが正しい限り、検証するのに時間がかかりますが、それほど狂ったことではありません。ステートメントが正しければ、Leanコンパイラに頼って正確性を確認できます。
システムが生成する証明の品質
システムが生成する証明を読んだことのない人々のために、私を含めて、つまり、どんな数学者も言うように、証明を持つことはできますが、それは複雑で理解しにくいなどのこともあります。優雅な証明とは対照的に。それで、これらのシステムは今、美しさという点でどのように機能していますか。
証明は美しいと思います。私たちは国際数学オリンピアードの証明を印刷しました。
いや、でもつまり、プロの数学者に見せたとき、反応はどうですか。
非常に満足しています。繰り返しになりますが、私の言葉を鵜呑みにする必要はありません。Twitterを見ることができます。人々はAristotleを使うことに非常に満足しています。
Leanの証明は一種のアセンブリコードのようなものだと思います。非常に非常に細かいです。非常に低レベルです。証明の高レベルな理解だけが欲しい場合、それらを解釈する最良の方法は、プロセスを逆転させる脱形式化されたバージョンを通じてです。
システムがLean証明を開発して、数学者としての私のために実際に論文を書くことは可能ですか。
100%できます。既存のモデルを使うことができると思います。
ええ、ええ。それで論文を読んで、「この証明はこうすることで改善できます」と言えるわけですね。
ええ、ちなみに、今日Aristotleでそれができます。既存のLeanプロジェクトを取って、「見てみました。これは良いと理解しました。これは改善できます。だからそれを改善してください」と言えます。それが行って作業し、Leanファイルをいじって、いくつかのことを修正して、あなたのガイダンスに従ったより良いLean証明が返ってきます。
ですから、非常に柔軟なシステムだと思います。重要な点は、証明を改善するために使っているか、証明を自動形式化するために使っているか、証明を見つけるために使っているかに関わらず、最終的には形式検証されているということです。それが唯一の…
モンテカルロ木探索の役割
ええ。ええ、ええ。それで、これらのシステムの一部がモンテカルロ木探索、モンテカルログラフ探索を使用していると読んだことがあります。それが高レベルでどのように機能するか説明してもらえますか。
ええ、つまり、それがシステムの最も重要な部分です。ちなみに、私たちは非常にオープンです。アーカイブに技術報告書があり、そこに多くの詳細があります。
簡単な概要は、人々が通常AI探索について考える方法は連鎖思考を通じてです。1つのエージェントがあり、それが英語のような人間が解釈可能な言語で考え、連続した連鎖で考え続けます。
それは素晴らしいです。つまり、それは理にかなっていますが、それであなたが簡単かつ効率的にできないのは、多くのアイデアを並行して探索することです。
ですから、「2つの異なるアイデアを探索してほしい」と言うとすぐに、一方のアイデアに対してどれだけの努力を費やすかという自然な質問が生じます。そこで価値関数が登場します。そして、ニューラルネットワークからの価値関数があれば、その問題は、探索をどこに向けるかについての決定をするために、その価値関数の統計を探索木全体でどのように集約するかということです。
そこでモンテカルログラフ探索が登場します。なぜなら、実際には木ではないことがわかったからです。特定の状態に到達する複数の方法があるので、グラフがあります。
なぜすべてを探索しないのですか。
無限のお金があれば、そうします。そうします。
並列計算がありますよね。
それが木探索のポイントです。木探索は、望むだけ並列に探索できます。そして、大規模に強化学習を行うことで、非常に強力な探索システムに到達できると思います。
それで基本的にシステムは多くのアイデアをほぼ同時に探索しているわけですね。
はい。
そして、これらのアイデアの複数が報われる可能性が十分にあります。
ああ、そうです。そんなことはいつも起こります。
そして、どういうわけか、これらのアイデアのどれをあなたに提示するかにも到達します。
ええ、つまり、通常、問題を解決したら探索を停止しますが、それをもっと実行すれば、異なる特性を持つ解決策を見つけるでしょう。例えば、CPU時間がかからないかもしれませんし、短いかもしれませんし、長いかもしれません。
それを永遠に実行したときに何を得るかは未解決の質問です。ただ、通常は問題を解決したら停止する傾向があります。
新規性と未解決問題への取り組み
新規性という点では、これらのシステムは既知の結果について質問すればおそらくそれを扱えることに疑問の余地はないと思います。それで、新規性について何を知っていますか。いくつか例がありますが。
First proof問題は新規であり、AIシステムがそれらに取り組み始めることができると思います。それについていくつかの結果を公表したかもしれません。Frontier math challengesがありますが、最終的に重要なのは、私たちにとってはミレニアム懸賞問題のようなものです。
なぜなら、それらは人々が長い間気にかけてきたものだからです。そして、AIがそのレベルの未解決問題で本当に進歩を始めるときは非常にエキサイティングだと思います。
実際、超応用的で実用的な問題さえあります。例えば、非線形PDEで、進歩があれば商業的応用に実際の影響を与える可能性があるものです。数学はどういうわけかアプリケーションから遠く離れているというステレオタイプがありますが、進歩があればアプリケーションがかなり迅速になる可能性がある数学的問題があります。
ええ、つまり、例えば、デジタル経済全体の基盤となっている数論があります。それは大きなものです。人々は私たちの生活の中で数学がどれほど広く行き渡っているかをあまり理解していないと思います。
何十年も前に巻き戻すと、四色問題がありました。それはおそらく、未解決問題が本質的に解決された最初の例だったと思います。これは不公平な説明ですか。
実際には詳細を知りません。
ええ、しかし基本的に、すべての可能性を調べただけだと思います。そして検証しましたが、少なくとも数年後には、書かれた証明があったとは思いません。ただ検証して証明しただけです。詳細のいくつかはわかりませんが。
ええ、ええ、ええ、ええ、しかし今のようなそのような問題ははるかに取り組みやすくなるだろうと想像します。
まあ、私の理解が正しければ、ブルートフォースを使ったとすれば、組合せ最適化のように聞こえるので、より良いアルゴリズムがあるとは思いません。つまり、いくつかより良いアルゴリズムはありますが、見つけるのにまだしばらくかかるでしょう。もしそれが彼らのやり方だったとしたら。
1つ異なることは、あるいは当時と今の間に理論的な進歩があったかもしれません。だからより良いアプローチがあるかもしれません。しかし、1つの重要な違いは、20年前について話しているなら、Leanがなかったということだと思います。Leanはこの時点で定理証明器の競争に勝ったようなものだと思います。
ですから、当時証明を受け入れることについて何か疑問があったとしたら、他の言語を使ったからかもしれませんが、今はそのような疑問に直面しないと思います。人々はそれを受け入れると思います。
未来における数学者の役割
あなたが思い描く未来において、数学者の役割は何ですか。あなたが言ったように、数学者はこれが取り組むべき興味深い問題だと決めるでしょうが、それだけですか。
それを小さな問題として特徴づけるのは、私の考え方とは少し違うと思います。
いやいやいや、それは明らかに巨大ですが、プログラミングとの類推を作ることができるかもしれません。プログラミングでは、人々は基本的にもはや手動でコードを書くのをやめると思いますが、ソフトウェアシステムアーキテクチャを理解する人々はまだ必要になります。それは数学者がやることの良い類推ですか。彼らはもはや手動で数学をやらないかもしれません。
ええ、ソフトウェアエンジニアリングにおけるソフトウェアエンジニアの役割が何になるかについては、活発で正当な議論があります。
ええ、理論的には、その出力を見る必要が全くないほど本当に賢い超知的AIを想像することができます。私たちはそこから非常に遠いように感じます。最新のモデルをいつも使っています。
基本的なことでさえ、非常に多くの間違いをいつもしているので、どれほど近いか言うのは難しいです。1つの違いは、ソフトウェアエンジニアリングでは、それを検証するためにコードの詳細を理解する必要があることです。一方、数学では、形式的に検証できる証明システムがあるので、それほど問題ではないと思います。
言うのは難しいですが、仕事の大部分は、コンピュータに時間を費やす場所を決めることになると思います。そこで良い決定をするためには、数学的理解と、その理解を社会全体が数学者に必要とするものに結びつける能力が必要になります。
Terence Taoの視点
Terence Taoがこのトピックについて書いたことをたくさん読んだと思いますが、彼が作る良い類推の1つは、数学問題を解くことをA地点からB地点へのハイキングと想像すれば、このシステムは基本的にあなたを直接B地点に降ろします。一方、プロの数学者はA地点からB地点へハイキングし、途中で気が散って興味深いアイデアを見つけます。言い換えれば、直接のルートではありませんが、途中でそこにない繋がりを見つけて、別の方向に行くように刺激されたり、関連する問題に取り組んだりするかもしれません。それについてどう思いますか。
それはまさに正しい考え方だと思います。つまり、私がそれを次のような考えに関連づけると、基本的には学習ですよね。今のところ、アーティファクトを生成できるのは人間だけで、近い将来にはAIもそうなりますが、教育的価値、ハイキングに行って数学を学ぶことで、あなたのハイキングからの新しい理解の中で将来の数学を文脈化できるようにすることは、なくならないと思います。
ですから、要約すると、最終的にこれらのAIシステムはツールだと思います。未来の主要なエージェントではありません。人間が使用するツールだと思います。そして、人間の間で数学的理解が必要とされることは決してなくならないと思います。社会が気にかける問題にツールを適用する方法を知るために、数学的理解が必要だと思います。
数学以外の分野への応用
終わりに近づいてきたので、数学以外の分野への広範な教訓を見てみましょう。あなたがいつも私たちに思い出させてくれることの1つは、もちろんLeanは数学における特別なものだということです。それは、Tudorさん、あなた方が構築しているものの多くが数学以外の分野にはあまり適用できないかもしれないということを意味しますか。
例えば歴史エッセイを書くことにすぐに適用できるとは思いません。それについて形式検証されるものはほとんどないと思います。人間がデジタルアートを作っているとき、検証のポイントはありません。アートを作って美しさを鑑賞したいだけです。
しかし、人々が研究する他の定量的なものがあると思います。例えば、物理学は純粋に数学的ではありませんが、大きな数学的要素があり、物理学の部分を公理化して幻覚のない方法で形式的に推論できることは非常に役立ちます。
私たちのAPIのソフトウェア検証の人々からの有機的な使用も見つけました。彼らはソフトウェアプログラムをLeanプログラミング言語にエンコードする方法を持っており、その世界に入ると、Aristotleが非常に迅速に処理して、コードが正しいことを証明するか、バグを見つけます。
ですから、そこに未来があるかもしれません。法律、フランスのように法典や税法を形式化して税務申告を安くすることに未来があるかもしれません。幻覚のない論理的推論がどこで役立つかを正確に予測するのは難しいと思いますが、純粋な数学以外でも役立つと言っても間違いないと思います。
しかし、あなたが取り組んでいるこの特定の領域の重要な特性は、この形式検証ツールの存在ですね。
ええ、そして論理的基盤の上に構築されているという事実です。ですから、これらの技術が適用できる可能性のある純粋な数学以外の多くの分野があると思います。
そして正直言って、Mathlibも特別なものですよね。多くの分野にMathlibの同等物はありません。
ええ、人々はコンピュータサイエンスのためにそれを作ろうとしています。最近のCS Libの取り組みがあると思います。Mathlibが特別なのは、シリコンバレーのQuoraという会社でキャリアを始めたので、ネットワーク効果というものを学びました。
そして、Mathlibが特別なのは、オープンソース数学の最大のリポジトリだからだと思います。したがって、人々はそれに貢献したいと思い、それが最大のものになり、さらに貢献したくなります。
ですから、MathlibとLeanは、私の意見では、ネットワーク効果を確保しており、この2つが形式検証された数学と定量的推論の未来です。
人間とコンピュータの相互作用における教訓
この領域から、少なくとも人間とコンピュータの相互作用、ユーザーインターフェースの分野で他の分野にマッピングされる教訓はありますか。
この分野の興味深い点は、検証可能な真実があることだと思います。ですから、真実がある領域で作業するときのデザインパターンは、ないときとは異なります。
例えば、Aristotleを24時間、48時間、それ以上実行させることができ、最終的に正しいものが得られると確信できます。検証不可能な領域では、それほど長く実行させると、おそらく退化して、尋ねたこととは全く異なることをしています。
これら2つの領域の間でHCIの教訓は異なると思いますが、確かに、Aristotleやおそらく他の類似システムでは、このパラダイムを探索できるのは初めてです。ですから、そこで製品を構築する方法について多くの教訓を学ぶと確信しています。
ええ。それでは、Tudorさん、ありがとうございました。
ああ、どうもありがとうございました。
コメント