ここに来られて光栄です。ロンドンでの滞在を本当に楽しんでいます。おもてなしも素晴らしいですね。
さて、今日はAIについてお話しします。皆さんもご存知の通り、AIは世界を変えようとしています。そして、科学や数学の分野も変わっていくと私は考えています。
AIは素晴らしい技術ですが、時には過大評価されることもあります。魔法のような技術ではありません。AIの仕組みを詳しく見てみると、確かに数学は使われていますが、驚くほど高度な数学は使われていない場合がほとんどです。
非技術的に説明すると、AIは基本的に「推測マシン」です。テキストの質問や何かの入力を与えると、テキストや画像、数字などの出力を生成するソフトウェアです。
その仕組みは、数学的にはかなり平凡です。入力を小さな単位に分解し、各単語などを数字としてエンコードします。それらの数字に重みをかけて組み合わせ、場合によっては切り捨てます。そしてまた重みをかけて組み合わせるという作業を数百回繰り返します。数学的には実際かなり退屈なプロセスです。
重みの見つけ方はもう少し興味深いですが、魔法ではありません。しかし、あらゆる種類のタスクを加速することができます。
私がよく使う例えは、この世界で動力飛行が発明されていなかったとしましょう。車やトラック、船など、陸上と海上の移動手段しかない状況です。そしてある時点で誰かがジェットエンジンを発明します。
最初は小さなおもちゃのようなものですが、だんだん大きく強力になっていきます。最終的には、最速の陸上車両の10倍の速さで移動できるようになります。
しかし、まだ飛行機を発明する必要があります。エンジンを車に取り付けただけでは良い結果は得られません。それは良いアイデアではありません。輸送に対する考え方を変える必要があります。新しい安全プロトコルや計器、物理法則を理解する新しい方法を設計しなければなりません。
それでも魔法ではありません。スタートレックのテレポーターのようなものではありません。物理法則に従いますが、異なるスケールで動作するのです。
AIもそのようなものです。実際、私たちが日常的に使用している多くのソフトウェアと似ていますが、一つ重要な違いがあります。
私たちが普段使うソフトウェアは、どちらかというと退屈で創造性に欠けます。同じ入力に対して毎回同じ出力が得られます。例えば、ウェブブラウザにアドレスを入力すると、そのアドレスにあるものが表示されます。
ソフトウェアはしばしば非常にうるさく、ちょっとしたミスでも大変なことになります。間違ったウェブアドレスを入力すると、別の場所に飛ばされてしまいます。しかし、非常に予測可能です。
これは、現代のAIツール、特にここ1年ほどで登場した大規模言語モデルとは正反対です。実際には数年前から存在していましたが、人間レベルの理解力を持つようになったのはごく最近のことです。
これらのAIツールははるかに創造的です。プログラミング言語を正確に学ぶ必要はありません。自然言語、つまり普通の英語で入力できます。間違いをしても、AIはあなたの意図を理解しようとします。
しかし、その代償として信頼性や予測可能性が失われます。同じクエリを2回入力しても、異なる回答が得られます。また、回答が正しいという保証もありません。先ほど言ったように、これは推測マシンです。他の質問に対する正解に近い回答を推測しようとしますが、自分で考えて生成しているわけではありません。
しかし、時にはAIが行うことは驚くべきものです。GPT-4が最初にリリースされた昨年、その能力をテストする論文がありました。
その中で、数学オリンピックの問題を与えました。これは非常に難しい高校生向けの数学コンテストです。実際、今まさにバースで開催されています。私も今週末に閉会式に出席する予定です。
また、私たちのホストであるXTXも、AIが数百人の優秀な高校生数学者しか完璧に解けない問題を解けるかどうかを見るための大規模なAIコンペティションに資金を提供しています。
彼らは多くの最近のオリンピック問題をAIに与え、時々AIは完全に正解を出しました。ここに彼らが公開した回答があります。おそらく読むのは難しいでしょうが、これは非常に挑戦的な問題で、高校数学の上位層の学生向けのものです。
GPT-4は段階的に、この特定の問題に対して完全に正しい証明を提供しました。
しかし、これは非常に選りすぐられた例です。彼らは数百の問題をテストし、成功率は1%程度だったと思います。つまり、うまくいくときは驚くべきものですが、うまくいかないときは恥ずかしいほど悪いこともあります。
同じ論文で、彼らは単純な算術問題「7 × 4 + 8 × 8」を計算するよう求めました。AIの反応を見ると、推測していることがわかります。内部に計算機を持っているわけではありません。
現在、より従来型の計算を組み込むためのプラグインを構築しようとしていますが、基本的には推測しているだけです。黒板に立たされて質問に答えるよう求められた学生のようなものです。かろうじて暗記した表を思い出しながら、即興で答えを出そうとしているのです。
まず、答えは120だと推測しました。しかし、少し間を置いて、説明が必要かもしれないと考えました。そこで、段階的な説明をすると言い、7 × 4と8 × 8をそれぞれ計算し、それらを合わせました。すると、最初の推測とは異なる答え92が出ました。
実験者が「最初に120と言いましたよね」と指摘すると、「あれは誤字でした。正しい答えは92です」と言いました。
つまり、少なくとも現在のレベルでは、これらの技術には本質的に正確さの基準がありません。人々は段階的に考えさせ、単に答えを推測するのではなく、このように解くよう強制する実験を試みています。それはある程度効果がありましたが、これらは一種のハックです。
専門家ほど信頼性はありませんが、時には専門家レベルの出力、あるいは少なくとも専門家レベルの出力に似たものを生成することがあります。
では、このような技術をどのように使用すればよいでしょうか。これは私たちが慣れているものとは異なる種類の技術です。
私たちは間違いを起こす技術に慣れています。悪い出力を生成する様々な種類の悪い技術がありますが、通常、プログラムや技術が何か悪いものを生成した場合、それが悪いことはわかります。本物のものとは異なって見えます。
しかしAIは設計上、これらの重みは可能な限り正解に似た答えを生成するように選択されています。したがって、間違っている場合でも、非常に説得力があるように見えます。
これは、既存のパラダイム、つまり何かが良く見えるか悪く見えるかを判断する既存の感覚を使用している場合、危険な組み合わせです。特に、実際に害の可能性がある分野に適用しようとする場合、例えば医療決定や金融決定にAIを使用しようとする場合などです。
あるいは、例えばセラピストとしてAIを使用する場合もそうです。これらのテキスト生成器は潜在的に素晴らしい仲間になる可能性がありますが、非常に悪いアドバイスを与える可能性もあります。
潜在的な可能性はあるものの、安全性がまだ確立されていない分野が多くあります。ジェットエンジンを発明した場合と同じです。すぐに何か飛行する乗り物を作ることはできますが、一般の人々が安全に使用できるようになるまでには数十年かかります。
しかし、今日では航空機による移動は、マイル単位で見ると最も安全な移動手段です。明らかに危険な技術であるにもかかわらずです。
つまり、これらの問題は解決可能であり、解決されるでしょう。しかし、安全性について実際に考える必要があります。単に起こると想定することはできません。
一方で、リスクがそれほど大きくない応用分野もあります。例えば、このプレゼンテーションの背景スライドはすべてAIによって生成されたものです。おそらくすでに気づいているかもしれませんが、AIにはまだ不完全な点があります。テキストの生成はまだ苦手で、少しずつ改善されているところです。
しかし、リスクはほとんどありません。説得力があれば良いのです。背景画像は私の講演の主要部分ではありません。
つまり、リスクが非常に許容できる応用分野があるのです。
科学の分野では特に、エラーやバイアスのリスクを軽減する方法があります。科学は検証、特に独立した検証に関するものだからです。
AIの予測不可能だが非常に強力な出力と、人間による検証を組み合わせて、がらくたをフィルタリングし、良いものだけを残すことができるセットアップがあれば、本当に多くの潜在的な応用が見えてきます。
別の例えを挙げると、現在の科学は、ある程度の飲料水を生成する蛇口のようなものです。しかし、これらの蛇口が生成できる量には限界があります。そして突然、10倍、100倍の液体を生成できる大きな消火ホースが現れました。しかし、その形では飲用に適していません。
しかし、飲用に適さない部分をフィルタリングする浄化装置があれば、突然、大量の飲料水を手に入れることができます。
これが、私が科学と数学が向かっていく方向だと考えているものです。
これはすでに様々な形で始まっています。多くの科学分野では、問題を解決するための良い候補を見つけることがボトルネックとなっています。
例えば、創薬の分野で特定の病気の薬を見つけたいとします。それを合成し、自然界から見つけるか、既存の薬を修正して新しい薬を作る必要があります。そして、第1相試験、第2相試験と、何年もかかる試験のプロセスを経なければなりません。非常にコストがかかります。
最大手の製薬会社だけが、最終的な承認まで全てのプロセスを負担できるのです。
テストする多くの薬が実際には効果がなく、途中で断念しなければならないこともあります。時には幸運にも、目的とした病気には効かなくても、他の何かに有益であることがわかることもあります。しかし、それでも多くの試行錯誤が必要です。
候補の数を減らす方法があれば…例えば、AIを使用してタンパク質をモデル化することができます。これはすでに行われています。
十分なデータがあれば、既存の臨床試験のデータに基づいて、様々な薬の機能をモデル化し始めることができます。AIを使用して、様々な病気に対する有望な薬の候補を見つけることができます。
しかし、その後にはまだ臨床試験が必要です。つまり、科学的検証の金字塔はまだ存在しますが、100の候補をテストする代わりに、効果のあるものを見つけるまでに10個だけをテストすれば良いかもしれません。
他の多くの科学分野でも同じです。材料科学は大きな勝利が期待される分野の一つです。例えば、室温で機能する新しい超伝導体を見つけたいとします。これは数十年来の聖杯のような課題です。
人々は異なる材料を試し、通常は失敗します。時には大きな発表をしても、結局失敗することもあります。
しかし、ここでも高価な合成プロセスをスキップし、AIを使用して候補の数を大幅に絞り込むことができれば、それは革新的な変化をもたらします。
実際、これらの科学的問題の設計部分だけでなく、合成そのものもAIによって自動化されつつあります。人々は、時には危険な化学物質を組み合わせるプロセス全体をより自動化された方式で行うことができるAI駆動の研究室を開発しています。
これは、高価なテストのための候補を減らすことで大きな加速が見られる一つの分野です。
もう一つの分野は、モデルの加速です。現代の世界では、あらゆるものをモデル化する必要があります。気候では、大気やその他の地球科学的プロセスをモデル化する必要があります。新しい高速道路を建設したい場合は、交通をモデル化したいでしょう。
基本的にすべての複雑なシステム、例えば経済のモデル化などを行います。宇宙論では宇宙をモデル化したいと考えています。
しかし、モデルはしばしば物理法則を実行する必要があります。例えば、今後20年間の地球の気候をモデル化したい場合、特定の物理法則があり、多くのデータを取り、物理法則を実行します。
しかし、正確にするためには、非常に小さな時間ステップを使用する必要があります。地球を非常に小さなグリッドに分割し、スーパーコンピューターを使用する必要があります。
気候予測を行うには数ヶ月かかります。例えば、二酸化炭素レベルがこのレベルだった場合、20年後に何が起こるかを知るためには、合理的な精度の答えを得るまでに数ヶ月かかります。
しかし、AIは原則的にこれを大幅に短縮することができます。AIができることは、既存のシミュレーションの大量のデータ、つまりこれらのスーパーコンピューターを使って苦労して得られたすべてのモデルを学習し、データに見られなかった入力に基づいて結果を予測するための最適なフィットを見つけることです。
数ヶ月かかっていたものが、数時間で可能になります。私の意味がわかりますか。人々は気候シミュレーションの分野ですでに成功を収めています。従来のスーパーシミュレーションの精度を数ヶ月ではなく数時間で再現することができるのです。加速は本当に驚くべきものです。
気象予報では、すでに予測の速度が10,000倍になっています。これは気象予報全体が10,000倍速くなったということではありません。いくつかの理由があります。
一つは、これらの出力の信頼性をどのようにベンチマークするかまだわかっていないことです。また、多くのこれらの予測では、シミュレーションプロセスは一つのステップにすぎません。データのシミュレーションステップがあり、実際の世界の測定値を取り、それをモデルに入力する必要があります。
これは現在、特に気候モデリングでは大きなボトルネックになっています。データを収集し、AIを実行する前にフォーマットするだけでも大きな問題です。しかし、実際に展開され始めています。
特にハリケーンのような稀な事象に有用です。既存のハリケーンのデータを学習し、物理法則を実際に実行することなく、リアルタイムでハリケーンの上陸地点を国立気象局よりも正確に予測できた成功例もあります。
つまり、シミュレーションがボトルネックになっているあらゆる場所で、これは素晴らしい使用例となります。
そうですね、気候モデリングについて言えば、これが開く一つの可能性は、現在はシナリオを実行するのに数ヶ月かかるため、IPCCや気候変動の予測を見ると、3つか4つのシナリオしか提供されていません。これは、彼らが負担できる計算量がそれだけだからです。
しかし、AIを使えば数千のシナリオを実行でき、はるかに豊かな予測を得ることができます。
私は数学者なので、AIが数学をどのように変革する可能性があるかに本当にわくわくしています。すでに孤立した使用例はありますが、まだ革命は起こっていません。しかし、それは来ると思います。
多くの主要な利点があり、欠点は少ないです。他の多くの分野と比べて、数学にAIを適用することのダウンサイドは少ないのです。例えば、AIに数学の問題を解かせて、不正解の解答を出したとしても、世界の終わりではありません。
さらに重要なのは、これらの証明を独立して検証できることです。数学では、証明が正しいか正しくないかという標準があります。AIを信頼する必要はなく、実際に他のコンピューターソフトウェアを使用して証明の正しさを検証することができます。
また、他の多くの問題には数学的な要素があるため、AIが数学的推論を改善できれば、他の多くの使用例でAIをより有用にする非常に広い可能性が開けるかもしれません。
特に、証明支援と呼ばれる別の技術と非常にうまく組み合わせることができるはずです。証明支援は一種のコンピューターソフトウェアで、実際にはコンピューター言語のようなものです。
通常のコンピューター言語では、出力は実行可能なプログラム、つまり実際に何かを行うものですが、証明支援言語は、物事を実行するのではなく検証するように設計されています。特定の陳述が正しいという証明書を生成します。
これらは数学だけでなく工学でも使用されています。プログラマーが言ったことを100%確実に行うことを本当に確認したい電子ソフトウェアがあります。例えば、飛行機の回路など、このボタンが正確にこの動作をすることを確認したいものです。
ソフトウェアを使用して電子機器を検証する方法がありますが、同じ技術で証明を検証することもできます。
しかし、残念ながら非常に時間がかかります。現在、中規模の問題の証明を書くのに数ヶ月かかりますが、それを形式化するにはさらに10倍以上の時間がかかります。
しばしば一人では行えず、グループで行う必要があります。しかし、速くなってきています。ここに小さな表があります。
数学では多くの有名な結果があり、それらが証明されてから何十年も後に最終的に形式的に検証されましたが、そのプロセスはしばしかなり長い時間がかかりました。
例えば、四色定理についてお聞きになったことがあるかもしれません。これは70年代に証明されましたが、2000年代になってようやく形式化されました。
強セファルディ予想は98年に証明されましたが、非常に複雑だったため、証明が正しいかどうか多くの疑念がありました。著者のトーマス・ヘイルズは、それを形式化するための20年計画を提案しました。12年で達成できて非常に喜んでいました。
例えば、ピーター・ショルツは…彼はロックファンなので、彼のプロジェクトを「液体テンソル実験」と名付けました。彼は2020年に証明した非常に難しい結果を検証するプロジェクトを提案し、それはたった18ヶ月で完了しました。
最近、私と共著者たちは共通ロリク予想を解決しました。昨年11月に証明し、すぐにこれが現代の形式化技術がどのように機能するかを見るための良いテストケースになると決めました。20人ほどの大きなグループで3週間で形式化することができました。
つまり、時間は短くなってきていますが、まだすべての定理がすぐに形式化されるほど便利ではありません。
聴衆の中にケビン・バザードがいますが、彼は最終定理を形式化する計画を持っています。彼は5年で重要な部分を形式化できると予想しています。全体を行うとは主張していませんが。
はい、これらの支援はより速くなってきています。現在のところ、スピードアップはほとんど従来の方法によるものです。これらの言語を使用するためのより良いソフトウェアライブラリを開発してきました。GitHubのような最新のコラボレーションツールを使用して、多くの人々が協力して作業する方法を調整しています。
これらのプロジェクトの良い点の一つは、通常、数学者が協力して作業するのが非常に難しいことです。5人程度のチームで協力するのはそれほど悪くありませんが、20人で協力しようとすると、全員が他の人の数学を信頼しなければなりません。これは実際に大きなボトルネックになっています。
そのため、他の科学分野で行われているような大規模な数学プロジェクトはまだありません。しかし、形式化プロジェクトは拡張可能です。実際にとても楽しいです。20人、50人のプロジェクトを実行でき、その多くはプロフェッショナルの数学者ではありません。プログラミングのバックグラウンドを持つ人たちかもしれません。
しかし、彼らは有用な貢献をします。言語が人々がアップロードするすべてのものが実際に正しいことを確認するため、純粋に人間の協力で必要とされるのと同じレベルの信頼は必要ありません。
そのため、本当に大規模な数学プロジェクトを可能にしています。
しかし、人々はこの形式化プロジェクトをさらに加速するためにAIを使用し始めています。このスライドは、フルーイ予想の形式化プロジェクトの一つのステップです。これは特定の文で、エントロピーに関するものですが、正確に何であるかは重要ではありません。
これが必要だった主張です。そして、この言語で1行か2行の証明がありました。これはleanと呼ばれる言語で、検証に使用されました。正確にどのようなコードが必要か考えなければなりません。leanはとてもうるさい言語です。
しかし、GitHub Copilotというソフトウェアツールがあり、この特定のケースでこの特定の行の正しい証明を提案しました。実際には2行目だけが必要で、1行目は実際にはコンパイルされません。しかし、正しいものに十分近かったため、実際に機能しました。
私たちはAIを使用して、これらの証明の小さなステップを自動的に埋めることを始めています。時間が経つにつれて、1行の証明だけでなく、2行の証明、3行の証明を自動的にAIで行うことができるようになると思います。
最終的には、実際に従来の方法よりも速くなると思います。将来的には、証明を書く一般的な方法は、AIに口述することになると想像しています。ただ話をして、学生に説明するようにAIに証明を説明します。学生が質問をし、私たちが説明する各ステップで、AIは形式的に検証しようとします。
できれば素晴らしいですし、できなければ戻ってきて、ただ行ったり来たりを繰り返します。これは従来の方法で数学を行うよりも速くなると思います。
また、証明を少し変更して、仮説の一つを変更したい場合、通常は1行1行変更する必要があり、多くの間違いを犯します。しかし、現在の技術でさえ、証明の小さなパラメーターを変更するのははるかに速くなっています。間違いを全く犯さないことが保証され、変更が必要な行だけを変更すればよいのです。実際に形式的に行う方がはるかに便利です。
はい、AIと数学には大きな相乗効果があると思います。そして、大規模な数学の時代が来るでしょう。
はい、多くのことが進行中です。先ほど言及したように、XTXが後援するAI数学コンペティションがあります。希望的には、今週末のIMO数学コンペティションで勝者を発表できると思います。それを楽しみにしています。
以上が私のプレゼンテーションの最後です。ありがとうございました。
[音楽]
素晴らしい。次の部分では、約30分間のファイアサイドチャットを行い、その後、聴衆からの一般的な質問を受け付けます。
これは本当に興味深い講演でした。私も実際にあなたのスライドをかなり興味深く見ました。最初に気になったのは、GPT-4が信じられないほどの成功を収めた例を示し、それがチェリーピックだと言及したことです。そして、破滅的な計算の例も見ました。あなたの仕事から、AIがどのような種類の問題をより適切に解決できるかについて、何か感覚はありますか？
そうですね、AIは人間の知能を行っているわけではありません。人間が難しいと感じることをAIは簡単に感じ、人間が簡単だと感じることをAIは難しく感じます。これは非常に興味深い分野です。
私が思うに、AI研究が教えてくれているのは、人工知能というよりも人間の愚かさについてです。例えば、言語を話すこと、人間のように会話することは、知能の頂点と考えられていました。他の動物にはできないからです。
しかし、これらのAIツールが行っているのは、次に言う言葉を予測することです。テキストの文字列を生成し、各文字列に対して、次に来る可能性が最も高い単語を確率的に見つけています。
基本的には、携帯電話の自動補完ボタンを何度も押すことの洗練されたバージョンです。通常はがらくたを生成しますが、ある時点を超えると、実際にかなり一貫性のあるものになります。
私たちが気づいたのは、私が今あなたに話しているやり方は、基本的に次に言う言葉を思いつくことです。本当に即興で話しているのです。そして、これらのツールも同じことをしています。次に来るものを良い推測をしているのです。
そのため、人間には複雑に見える数学的な議論でも、AIはうまく処理します。各ステップが前のステップから論理的に導かれるもの、多くのステップがあるかもしれませんが、そのような文脈ではAIは非常にうまく機能します。
一方で、数値問題を解くよう求められると、AIは推測しています。算術問題のように、異なる可能性のある結果が多すぎるのです。7 × 4 + 8 × 8 を与えられても、もっともらしく見える異なる数字がたくさんあります。AIは一から計算しているわけではありません。
分かります。ある意味、誰かが話しているのを聞いて、「14 × 25は何ですか？」と聞かれて、「わかりません、420？」と言うようなものですね。実際には間違っているかもしれませんが、推測しただけです。しかし、それはある程度もっともらしく聞こえるということですね。
次の質問ですが、あなたは多項式フリーマン・ロス予想をLeanに入れたと話しました。それは時間のかかる作業ですが、どのような動機があったのでしょうか？
そうですね、私はかなり前から機械支援による数学の方法に興味を持っていました。おそらくフラストレーションからです。数学には楽しい部分がたくさんありますが、退屈な部分もたくさんあります。
すべてをより簡単にする方法があるはずだという感覚を本当に感じています。そのため、かなり長い間、数学をより簡単にする方法を探していました。
先ほど言及したピーター・ショルツ、彼は非常に著名な数学者でフィールズ賞受賞者でもありますが、彼が行った注目度の高い形式化の取り組みに私は非常に興味を持ちました。
実際、その結果を証明する数ヶ月前に、自分でLeanを学びました。驚いたことに、他の言語、例えばPythonやCなどに似ていますが、哲学が少し異なります。しかし、学ぶのはそれほど難しくありませんでした。実際、構文などについてはChatGPTを少し使って助けてもらいました。
そのため、1ヶ月かかりましたが、痛みを伴いながらも、自分で証明した単純な定理の一つを形式化することができました。練習のためです。
しかし、私が本当に興味を持ったのは、形式言語が大規模な協力を可能にする能力です。先ほど言ったように、これは数学ではまだ本当に起こっていません。
しかし、20人との素晴らしい協力がありました。グループチャットでは常に何かが起こっていて、本当に楽しかったです。
なるほど。その特定の問題について、あなたはそれが真であることをかなり確信していたのですね。単に真であることを確認したかったのではなく、これを練習として行いたかったということですね。
そうです。これらの形式的な証明支援には多くの応用があります。最も明白なのは、100%の正確性を保証することですが、はい、協力を可能にすることもできます。
私は、数学におけるAIの使用を、ある程度の正確性の保証を持って可能にすることもできると思います。これは実際に非常に重要です。
私にはもっと夢があります。実際に新しいプロジェクトを始めています。数論にはたくさんの結果があり、それらを自動化し、統一し、機械に自動的に解かせたいと思っています。しかし、すべての数値計算が実際に正しい結果を出すという理論的保証が本当に必要です。
巨大な不透明なプログラムを実行しただけだと言われても、どうやってそれを審査すればいいでしょうか。そのため、これらの証明支援は、数学の自動化のあらゆる種類で大きな役割を果たすと思います。
なるほど。あなたは協力について多く言及しました。あなた自身も多くの協力をしていることは明らかです。Leanのようなものに変換することは、証明が正しいことを確認できるコードですが、人々がこれを行うインセンティブ構造をどのように考えていますか？
ある意味で、英語で書いたり、LaTeXで書いたりして提出すれば、すでに研究論文のクレジットを得ていますよね。このインセンティブの問題をどのように見ていますか？
そうですね、私たちの慣行を少し変える必要があるでしょう。
学術出版システム、特に数学の分野ではすでに負担がかかっています。論文はますます長くなっています。レフェリーを見つけるのが難しくなっています。レフェリーは無給のサービスで、数学者が他の数学者のために行っています。
そして、論文はますます複雑になっています。ある時点で、論文がある大きさを超えると、最も技術的な部分を形式化する必要があるでしょう。レフェリーが1行1行チェックする時間の無駄を避けるためです。重要性や意味を確認したいのであって、すべての行が正しいかどうかをチェックする必要はありません。
そのため、出版システムが変わって、形式化を奨励し始める可能性があります。
しかし、私たちの資金調達システムも変える必要があるかもしれません。現在、助成金がどれだけ成功したか、あるいは昇進できるかを判断する方法は、出版物の数とどこで出版されたかがまだ非常に重要です。
形式化された証明に特化したジャーナルがいくつか出始めています。それは助けになるかもしれません。
しかし、資金提供機関も、出力を測定する新しい方法を見つける必要があるでしょう。例えば、100の異なる結果を一度に形式化するGitHubプロジェクトに10,000行貢献したとしても、それは論文ではありません。しかし、それでも非常に重要な貢献です。
そのような貢献を測定する方法を見つける必要があります。これは難しい問題です。
なるほど。あなたは実際に合同数学会で、Leanと形式化を数学コミュニティに紹介する講演をしましたね。正直に言うと、私は実際にLeanで何かを形式化したことはありません。形式化の行為は、問題を解決する行為そのものよりも、何か日常的で簡単だと感じますか？
そうですね、それは異なるスキルです。時々パズルを解くようなものです。
物事をより低いレベルで考えることを強制されます。多くの場合、これらのLeanプロジェクトは、人間が書いた証明から始まります。つまり、従来の論文スタイルで書かれたものです。
そして、「ブループリント」と呼ばれるものを書きます。これはまだ人間の言語で書かれていますが、数学者が論文を書くのに使用するのと同じ言語、LaTeXを使用します。しかし、非常に詳細です。
例えば、「これは明らかに真である」と言うかもしれない部分を、実際にはレンマを作成し、2行の証明を与えます。大きな定理を数百の小さな部分に分解し、それぞれが2行か3行の証明を持つようにします。
そして、プロジェクトを作成し、人々が異なる小さな部分を担当し、「この部分を形式化します」「この部分を形式化します」と言います。皆が独立して行い、それが連鎖的につながっていきます。
大きなものを小さな原子的なステップに分解する思考プロセスは、基本的なことについて考えることを強制します。本当に基本的なこと、例えばこのパラメーターは実数であるべきか整数であるべきかなど、通常は考えないようなことについても考えます。
通常はそれほど重要ではないと思いますが、突然重要になります。定義をどの順序で配置するか、エッジケースをどのように扱うかなども考えます。
そして、多くの場合、議論が機能する本質的な部分を分離することになります。
時々、何かを証明して、どのようにしたのかわからないことがあります。自分自身に驚かされるのです。
しかし、実際に正しく行ったという内部的な安心感の追加レベルを与えてくれます。
この質問をした理由は、あなたはフィールズ賞受賞者なので、これらの物事を見るとき、あなたには非常に簡単に見えるかもしれませんが、他の人々、例えば私のような人にとっては少し時間がかかるかもしれないからです。
私が言おうとしているのは、証明を形式化することを考えるとき、ある意味で形式化のアーキテクチャという一つの部分と、そしてすべてのサブ問題に分解することは可能でしょうか？そして、各サブ問題について、実際にどの程度の数学的背景が必要なのでしょうか？
私が聞いているのは、これがある意味で因数分解可能かどうかを理解しようとしているのです。
はい、そうですね。これらの形式化プロジェクトの素晴らしい約束は、高レベルの概念的スキルを低レベルの技術的スキルから切り離すことです。
過去の数学者は両方を行う必要がありました。大きな絵を見ることができ、かつ正確にこれらの計算を行うことができなければなりませんでした。
これが一種の制限要因になっていました。数学は非常に習得が難しい分野だという評判がありますが、実際にはこのためです。
小学校や高校では、多くの場合、これらの技術的なスキル、例えばこの導関数をどのように正確に計算するかなどに焦点が当てられています。概念は教えられません。
あるいは、小学校では概念がぼんやりとした形で教えられるかもしれませんが、何も計算できません。そして高校では計算は教えられますが、概念を理解していません。大学院に行って初めて、すべてがつながります。これは実際にはかなりもったいないことです。良いことの多くを見逃してしまいます。
しかし、これらのプロジェクトを使えば、驚くべきことに、この組み合わせ論のプロジェクトに貢献した人々の多くは、この分野の専門家ではありませんでした。実際、数学者でさえない人もたくさんいました。
彼らはプログラミングが得意で、数学に近い分野にいたかもしれません。学部レベルの数学教育を受け、それを楽しんだけれども、学者にはならなかった人たちです。しかし、彼らには非常に具体的なタスクがあります。AからBにどのように5行で到達するか、というようなものです。
特定の人々は論理パズルが非常に得意で、彼らにとってはとても適しています。
将来的には、AIもこれらのプロジェクトに参加することができると想像しています。プログラミングが必要な100のことのリストをスキャンして、「このアルゴリズムで、これら20のことを行うことができます」と言うかもしれません。
つまり、あなたは人々が数学を進める方法について、かなり異なるアーキテクチャを提案しているのですね。仮説的に、もしあなたが数学科の責任者だったとして – あなたがそうであるべきだと言っているわけではありませんが – もし30年の時間枠で考えるとしたら、どのようなことを考えるでしょうか？
平均的な教員が約30年在籍すると仮定して、採用やその他のことについて考えるとき、将来に備えて設計できるものがあるとしたら、どのようなことを考えますか？
良い質問ですね。未来を予測するのは危険です。
しかし、私はあなたに聞いています。なぜなら、あなたは全体を俯瞰的に見ることができるからです。だからこそ、これは非常に興味深い質問だと思います。
はい、私は教員が変化に対してオープンであってほしいと思います。
先ほど言ったように、数学研究において、一般の人々がより大きな役割を果たすようになると思います。現在はほとんどありません。他の分野では市民科学がありますね。天文学では、アマチュアが彗星を発見したりします。生物学では、蝶を同定する人々がいます。
しかし、数学では、アマチュア数学コミュニティを使用できるのはごく周辺部分だけです。部分的には、信頼の問題があります。彼らの出力の多くは残念ながらプロフェッショナルレベルではありません。
また、数学言語を話す技術的な難しさもあります。しかし、AIとこれらの形式的な証明支援の両方により、これらの問題は解決可能になるかもしれません。
私は他の科学分野とのより広範な協力も想像しています。AIは科学者同士の対話も可能にします。例えば、私が生物学者と話したいと思っても、遺伝子をどう表現するかわかりません。しかし、AIが翻訳者を提供するかもしれません。
すでに、AIが可能にした新しいエコシステムのデータベースが見られます。多くの異なる科学分野の人々が同じシステムにデータを入力し、本当に全体論的なマルチモーダルな見方を作り出しています。
非常にエキサイティングな学際的な発展が起こっています。
また、将来的には異なるタイプの科学者が出てくると思います。数学では、アイデアを考え出し、解決策を見つけ、それを書き上げ、助成金を申請し、講演をするなど、すべてを行う必要があります。
しかし、これらの技術を使えば、異なる数学者が異なることに特化することができます。例えば、プロジェクトマネージャーがいて、低レベルの証明作業はあまり行わないかもしれませんが、人々を組織し、特定のタスクに向けて指示を出すのが非常に得意な人がいるかもしれません。
数学を十分に理解していて、物事を適切なサイズの部分に分割し、各部分を適切な人に割り当てる方法を知っているかもしれません。
それは有用なスキルになり得ます。ソフトウェア開発と同じです。50年前は、個々のプログラマーが巨大なソフトウェアの全体をプログラムし、すべてを行っていました。しかし今では、ソフトウェア開発は多くの異なる専門的な仕事に分割されています。数学も同じ道を辿ると思います。
なるほど。それは他の科学部門のように聞こえ始めていますね。技術者を持つことなども。
では、あなたが数学科の責任者だけでなく、大学の学部長だったとしたらどうでしょうか？つまり、これがさらに進んでいくとして…再び、特にあなたに聞いているのは、最初に言ったように、あなたはほとんどすべてのことを行っているように見えるからです。
同時にこれほど多くのことに触れている人はそれほど多くありません。大学の学部長について話すのをやめて、大学の学長まで行きましょう。なぜなら、実際に私が言おうとしているのは、数学についてです。
あなたはある意味で数学を代表しています。私たちがこれらすべての人工知能が登場するのを見ているとき、数学の役割は何でしょうか？ある意味で、コンピューターサイエンスの人々が最初にこれは彼らのものだと言いたがるかもしれません。しかし、ここであなたは証明と論理に取り組んでいて、これはある意味で根本的なものです。
学術環境の大きな枠組みの中で、数学、数学科、数学研究者の役割をどのように考えますか？
そうですね、境界線はかなりぼやけてくると思います。
まだ数学だけを行う人々もいるでしょう。専門化の美しさは、数学を行うことの一つの側面を選んでそれに特化できることです。
しかし、科学の多くの分野、社会科学さえも、そして人文科学でさえも、より定量的になってきています。
何かが良いか悪いかを知るだけでは十分ではありません。どれくらい良いのか、どれくらい悪いのか、数字が必要です。確実性を測定する方法が必要です。
すべてのデータと、データに適用するすべてのAIモデルを解釈する方法が必要です。
私は、科学のあらゆる分野がより数学化されていると思います。理論的な数学もまだ必要です。
約20年前、私は実際に信号処理に関わっていました。ある統計学者が、非常に少量のデータから高解像度の画像を作成できる技術を発見しました。
実際、この問題は多くの分野で何度も再発見されていました。地震学で現れ、天文学で現れ、高解像度の画像を作成する必要がある多くの分野で現れました。
多くの異なる科学者が、偶然にある特定の技術が非常にうまく機能することを発見しました。それはL1最小化と呼ばれています。しかし、なぜそれがうまく機能するのか、誰も説明できませんでした。
地震学者がこれを実現したとき、人々は「これは地震学者だけが使える手法だ」と思い、それは広まりませんでした。天文学や他の分野でも同じでした。
しかし、私たちがこれを発見したとき、実際にはこれらの統計学者が発見し、私のところに来て、ランダム行列に関する純粋な数学の問題として提示しました。
実際、私の最初の考えは、彼らが間違いを犯しているということでした。そんなに悪い入力からそんなに良い出力を得ることはできないと思いました。
しかし、理論的に彼らが行っていることを反証しようとする中で、実際にそれが機能する可能性のある唯一のシナリオを発見しました。それが実際に起こっていたことでした。
私たちは論文を書きました。そして、理論的な保証があったので、他の数十の分野がこれを見始めました。現在、この技術は圧縮センシングと呼ばれ、至る所で使用されています。
例えば、現代のMRI機械はこれを使用して、MRIスキャンを10倍速く行います。
なるほど。もう一段階上げてみましょう。これは少し異なる質問ですが、研究をどのように組織するかについてです。
現在、商業的な研究所が研究を行っているのを見ることができます。彼らは実際に、数学的定理を証明する方法を理解しようとしています。これらの研究所の背後で、定理を証明する方法を理解しようとする多くのクローズドソースソフトウェアを作成しています。
彼らの中には、ミレニアム懸賞問題の1つを解決したいと思っている人もいるかもしれません。しかし、これらはすべてある意味で閉じたドアの後ろで起こっています。
同時に、非常に大きな国家研究予算があり、ある意味で旧式の研究に資金を提供しています。
私たちオープンソースの学者が取り残されないように、何か変化が必要だと思いますか？
そうですね、特にAIの分野では、民間企業は桁違いに多くのリソースを持っています。
そして、それは近い将来変わることはないでしょう。部分的には、民間セクターがこの技術の大きな可能性を見ているからです。
最大のモデルを開発し、商業化し、商業製品を作るなど、学者が競争することはできません。
しかし、いくつかの…例えば、政府がリソースをプールすることができます。
現在のAIモデルについて一つ言えることは、特定の問題のために新しいネットワークを訓練したい場合、データを収集し、どのモデルを使用するかを見出す必要があります。
そのまま使えるものはありません。あるいは、あったとしてもほぼ確実にがらくたを生成するでしょう。
しかし、異なる科学のための標準化されたモデルがあり、ハイパーパラメーターの推奨される選択肢のガイドラインがあり、訓練に使用できる標準的なデータセットがあれば…
これらの種類のものの中央リポジトリがあれば、確実に役立つでしょう。
人々が構築できるオープンソースモデルを持つこと…
実際、競争は非常に重要な側面だと思います。多くのイノベーションは特定の課題によって推進されてきました。例えば、この画像認識ベンチマークの成功率をこのパーセンテージ以上に上げることができるか、というようなものです。
そうすれば、実際に定量的に、どの技術が本当に進歩をもたらしているか、どれが単なる誇大広告なのかを見ることができます。
現在のAIモデルは本当にエネルギー集約的で計算集約的です。研究室に実際に設置できるコンピューターに収まるような、より軽量なモデルを見つけるための研究が必要になるでしょう。
そのため、これは確かに公的資金が非常に有用である可能性のある一つの分野だと思います。
なるほど。AIに関するこのような開発を行っている民間組織のトピックに関連して、1月頃にDeepMindがAlpha Geometryと呼ばれるものを開発したというニュース記事がありました。これは国際数学オリンピックの幾何学問題を解決できるというものでした。
あなたは、これらの小さな部分のためにLeanコードを書くのを助けるようなツールがあるかもしれないと話していました。幾何学の分野で何かが起こったように聞こえますが、非常に限られた国際数学オリンピックの領域についてです。
最初の質問は、あなたはこれについて聞いたことがありますか？そして、そのような結果を見てどの程度驚きましたか？
そうですね、それは非常に素晴らしい仕事です。私たちはオリンピックレベルの問題が今年解決されるとは予想していませんでした。一般的な見解では、3年から4年のタイムラインだったと思います。
それは興奮させると同時に、少しトリッキーでもあります。しかし、実際には進歩はしばしば安価なトリックから来るものです。
特にオリンピックの幾何学の問題について言えば、例えば三角形があって、角度について特定の仮定がある場合、これは実際に解決可能な問題であることが知られている数学の領域です。
これは「決定可能な理論」と呼ばれるものです。すべての文を書き下せば、AIがこれらの問題を解くためのアルゴリズムが実際にありました。
問題は、既存のアルゴリズムが二重指数関数的に遅かったことです。一度に20の文と1つの結論を持つと、標準的なアルゴリズムを実行する実用的な方法はありませんでした。
しかし、ショートカットがあります。例えば、この幾何学の問題で、インスパイアされた構築を行うことができれば – 例えば、2つの既存の点の中点などの新しい点を1つ追加し、その新しい座標に基づいて情報を再配置すれば – 時々、問題の複雑さを劇的に減らすことができます。
そのため、AIは基本的に1つか2つのインスパイアされた構築を見つける必要があっただけで、そして残りの問題を解決するためにより標準的な代数的解決ツールを適用しました。
実際、それは戦略的に配置された少量のAIに過ぎませんでした。しかし、この一般的なプロセスは拡張可能かもしれません。
非常に難しい数学の問題を解く上で最も困難なステップの1つは、しばしば適切な中間的なステップを見つけることです。AがBを意味することを証明したいとき、AがCを意味し、CがBを意味するという適切な文Cを見つけることができれば、それぞれのステップが元の問題の半分の難しさになり、それは大きな進歩です。
適切な鍵となる中間的なものを見つけることは本質的です。そして、いつかAIがそれを得意になるかもしれません。
今のところ私たちにはそのためのデータがありません。AIは今のところ、大量のデータがある場合にのみ機能します。Alpha Geometryの成功の秘訣の一部は、テストするための多くの合成的な幾何学の問題を生成したことでした。
私たちには、数学者が実際にどのように証明を書くかについての良いデータがありません。時々冗談で、数学者にカメラを設置して、彼らが実際に仕事をしているところを観察し、AIにそれを学習させる必要があると言います。これは実現可能ではないと思いますが。
なるほど。それは学科の責任者になったらできることですね。最後の質問を一つだけさせてください。AIと数学オリンピックに関連して、幾何学はそれほど大きな驚きではなかったかもしれません。他の科目で、もしAIがそれを行えたら「おや、これは大変なことだ」と言うようなものはありますか？
「大変なこと」という言葉は適切ではないかもしれません。そう言うべきではありませんでした。むしろ、「これは本当に重要だ」というような感じでしょうか。
そうですね、過去5年から10年で、私は人間にとって難しいと思われることが、しばしば数学にとっては簡単であることを学びました。
90年代には、チェスが人間の活動の頂点だと考えられていました。そしてAIがそれを解決しました。これは現在のAIではなく、より伝統的なAIでしたが。
しかし、それはトリックでした。ブルートフォースでした。碁は人間が独自にできることだと考えられました。そして、異なる技術が基本的に碁を解決しました。
そして、画像認識、音声認識、翻訳など、一つずつこれらのことがすべて落ちていきました。
詩を作ったり芸術を作ったりすることは、AIが行う最後のものの一つだと考えられていましたが、現代のAIモデルが最初に模倣できたものの一つでした。
そのため、私たちの難しいものの概念は実際に再調整が必要だと思います。問題は、つい最近まで私たちには一つの機能する知能モデルしかなかったということです。
今、私たちはおそらく1.5のモデルを持っていると言えるかもしれません。
タオ氏に大きな拍手をお願いします。ありがとうございました。
コメント