2026-07-25 AIは数学を証明できるか？ Alpha Evolveが拓く自律的発見の現在地

出展元

https://www.youtube.com/watch?v=49shgbFP4-g

初回調査日

Aug 17, 2026 1:18 PM

キーワード

Alpha Evolve証明検証ラムゼー数計算量理論

※本記事は、Prabhakar Raghavan氏によるSIGMOD 2026基調講演「Can AI assist in Mathematics and Computer Science research?」の内容を基に作成されています。Raghavan氏はGoogleのチーフテクノロジストであり、情報検索、データ管理、Web検索、機械学習、大規模計算といった幅広い領域において影響力のある研究を行ってきた計算機科学者です。2012年にGoogleに加わる以前は14年間IBMリサーチに在籍し、その後Yahoo Researchを率いていました。カリフォルニア大学バークレー校で博士号、IITマドラスで学士号を取得しており、全米工学アカデミーの会員、ACMおよびIEEEのフェローでもあります。動画の詳細情報は https://www.youtube.com/watch?v=49shgbFP4-g でご覧いただけます。本記事では、講演の内容を要約・再構成しております。なお、本記事の内容は登壇者の見解を正確に反映するよう努めていますが、要約や解釈による誤りがある可能性もありますので、正確な情報や文脈については、オリジナルの動画をご視聴いただくことをお勧めいたします。

1. 導入

1.1 講演者紹介、講演の位置づけと全体構成

Carson： それでは、基調講演者をご紹介いたします。Googleのチーフテクノロジストであり、我々の時代において非常に大きな影響力を持つ計算機科学者をお迎えできることを、心より嬉しく思います。彼の研究は理論から始まり、情報検索、データ管理、Web検索、そして機械学習と大規模計算に至るまで、実に幅広い領域に及んでおり、我々がプラネタリースケールで情報をどう組織化し、どう推論するかという枠組みそのものを形作ってきました。2012年にGoogleに加わる以前、Prabhakarさんは14年間IBMリサーチに在籍し、その後はサニーベールでYahoo Researchを率いていました。実は昨日知ったのですが、彼はGoogleに加わる前、Mark Zuckerbergとの電話の後にFacebookからのオファーを断ったそうです。理由は明かしません。気になる方はぜひご本人に直接聞いてみてください。Prabhakarさんはカリフォルニア大学バークレー校で博士号を、IITマドラスで学士号を取得しています。全米工学アカデミーの会員であり、ACMおよびIEEEのフェローでもあり、スタンフォード大学の元客員教授でもあります。多くの権威ある賞を受賞しており、乱択アルゴリズムに関する教科書でもよく知られています。そして彼はこのコミュニティにもルーツを持っています。PODSでは、KleinbergおよびPapadimitriouとの共著によるベストペーパー賞を含む4本の論文を発表しており、SIGMODおよびVLDBには非構造化データやWebデータといった、今日ますます中心的な意味を持つようになったテーマで7本の論文を発表しています。本日は「AIは数学と計算機科学の研究を支援できるか」というテーマでお話しいただきます。AIが我々の分野に影響を与える「かもしれない」のではなく、「与えるだろう」という視点を共有していただけることと思います。それでは、Prabhakarさんをステージにお迎えしたいと思います。

Prabhakar： Carsonさん、丁寧なご紹介をありがとうございます。SIGMODを見事に開催されたすべての運営陣の皆様にお祝いを申し上げます。素晴らしい会議になることを願っています。私の講演タイトルには最後に疑問符がついています。皆さんの中には、AIが数学や計算機科学を助けることなど疑いようがないではないか、と感じる方もいらっしゃるかもしれません。それは一体何を問うているのか、と。私はこれについて、ある特定の視点から論じていきたいと思います。講演の構成をお伝えします。まずウォームアップとして、我々の研究を前進させるためにLLMを使っている進行中の取り組みからお話しします。次に講演の中心部分として、Alpha Evolveと呼ばれるLLM由来のツールを使って、複雑性理論と組合せ論においていくつかの結果を証明した話をします。そして最後の10分から15分は、この歩みがどこに向かっているのか、そしてこれがSIGMODコミュニティにとって何を意味しうるのかについて、振り返って考察したいと思います。それでは早速、最初の題材に入っていきましょう。

2. ウォームアップ事例：Google検索における負荷分散研究とLLM活用

2.1 負荷分散問題の理論と実運用の複雑性

Prabhakar： 最初の題材は、私たちが「バランスド・アロケーション」と呼んでいる設定です。これは、Google検索のようなプラネタリースケールのシステムにおける負荷分散の話でして、これは最近まで私の担当業務のひとつでもありました。この研究はGoogleフェローで検索チームのAmarさんと、Brown大学の教授であるEli Uppさんとの共同研究です。まず古典的な確率論のお話からして、それをGoogle検索のような負荷分散の設定に翻訳していきたいと思います。古典的な確率論では、n個のボールをn個のビンに投げ入れると、あるビンには大きな負荷がかかってしまうことが知られています。ところが、ボールが来るたびに1つではなく2つのビンをランダムに選び、その時点で負荷の軽い方のビンにボールを入れるようにすると、最大負荷は劇的に下がります。つまり、ランダムな選択が1つでは悪いのですが、2つの選択肢があると突然状況が良くなり、3つ、4つと増やしていくとさらに良くなっていくのです。この理屈をどう応用するかというと、Google検索に来るクエリのストリームを考えていただきたいのです。地球上のどこにでも存在しうるn個のサービングクラスタがあり、各クエリをどのクラスタに割り当てるかを決めなければなりません。ユーザーが生成したクエリですから、あまり長く待たせるわけにはいきません。あるサービングクラスタの負荷が高いところにさらにクエリを送ってしまうと、そのクエリの処理には長い時間がかかってしまいます。これは、先ほどの確率論の結果をそのまま翻訳したようなクリーンな設定に見えるのですが、実際の現場はもう少し複雑です。

Google検索で私たちが扱う大きな課題のひとつが、時間的なバーストです。これは思っているほど予測可能ではないのですが、たとえばワールドカップのサッカーの試合の最後の15分間には必ず起こる傾向があります。私たちにとって最も厄介なクエリの急増のひとつは、実はクリケットの試合から来るものです。2日前にIPLの決勝戦があったのですが、これはおそらく私たちのピーク負荷期間のひとつだったはずです。というのも、クエリが突然大量に押し寄せるだけでなく、地理的にも非常に限定された地域から来るからです。基本的にはインド亜大陸の20億人がスコアを問い合わせているような状態です。こういうことが起こったときに、たとえば一番近いデータセンターに送ってしまうと、APACのデータセンターがメルトダウンしてしまいます。もうひとつ実際に直面する現象として、リクエストには複数の優先度があるということが挙げられます。もちろんユーザーからのリクエストは最も高い優先度を享受すべきですが、システムが生成するクエリ、つまりランキングアルゴリズムを較正するためにエンジニアが実行する評価用クエリもあります。こうした状況でどう割り当てるかが問題になります。先ほど2つあるいは3つの選択の力についてお話ししましたが、そこにはクエリが来たときにランダムに選んだサービングクラスタの中から最も負荷の軽いところに送るという前提がありました。しかし、どのクラスタが最も負荷が軽いのかをどうやって知るのでしょうか。現在の負荷を知る必要があるのですが、Google検索のような実システムでは、現在の負荷に関する情報は少なくとも数秒の遅延があります。これによって興味深いアーティファクトが生まれるのですが、今日はその話はしません。遅延のある制御システムだと考えていただければと思います。そうすると振動が起き始めて、制御システムにありがちなことが一通り起こるわけです。

2.2 LLMを用いたシミュレーションと論文執筆を巡る経験

Prabhakar： こうした状況に直面したとき、現代の計算機科学者は何をするでしょうか。プロンプトを書くのです。私の共著者であるAmarさんが書いたプロンプトをご紹介します。彼は「power of nスケジューリングを探索してほしい」と書きました。全部を読み上げるつもりはありませんが、要するに最も単純な設定を記述したものです。そして最後に、彼は「私は色の識別が苦手なので、原色を使ってください」とまで書いています。すると言語モデルが動き出し、1つのランダムな選択ではクエリの平均待ち時間がかなり高くなる一方で、それ以外の場合には大幅に下がることを示すプロットが青い線で返ってきました。ここで注目していただきたいのは、私が指を差しているこの共著者であるAmarさんが、プロンプトを書く際にやや雑だったということです。冒頭では「power of nスケジューリング」と書いているのですが、最後の段落に来る頃には n が d になってしまっていて、しかも n は別の意味で使われていました。これはまるで、教授が上の空で大学院生に指示を出し、その大学院生がそれをうまく解釈して見事にやってのけるようなものです。もしこれを高水準プログラミング言語で行っていたら、すぐにコンパイルエラーになっていたはずです。しかし、こうしたモデルはかなり頑健で、平然とやってのけてしまうのです。

私たちは優先度や時間的バーストなど、あらゆるシナリオについてシミュレーションを実行し、大量のプロットを作成しました。また定理も証明しようとしたのですが、こちらでは言語モデルにあまり運がありませんでした。ひとつ例を挙げますと、複数の優先度がある場合について証明できた定理があるのですが、ここで言語モデルは苦戦しました。プロセスを支配する確率微分方程式を正しく定式化することはできたのですが、それを解くことができなかったのです。一部のケースでは、私たち人間が言語モデルの結果を上書きして自分たちで処理しました。こうして得られたすべてのプロットと定理を言語モデルに戻して、「論文を書いてほしい」と依頼しました。すると実際に書いてくれて、私たちはある会議への投稿の準備を進めていました。ところがそこで、こういう規定に突き当たりました。「著者は言語モデルの軽微な使用は許されるが、方法論の一部として、あるいは論文の重要な部分を作成するために使用してはならない」と。私たちは「果たして言語モデルで論文の重要な部分を作ってしまったのだろうか」と自問しました。私たちの感覚としては、答えは「はい」でした。そこで、私たちはすべてのシミュレーションを手作業でやり直すことに決めました。プロンプトによって得られたものはすべて捨ててしまったのです。しかしこれは、学術的な場でAIツールを制限すべきかという問いを提起します。この点については、少し前にステージにいたJohnさんと活発な議論を交わしたテーマでもありまして、講演の最後にもう一度この話題に戻りたいと思います。

3. AIによる数学的発見の兆候：先行事例の検討

3.1 「曖昧さゆえの解決」から自律的な問題解決までの事例

Prabhakar： さて、ここからは私が本当に探し求めているものについてお話ししたいと思います。私が問うているのは、AIが何らかの数学の問題を解くのに使われたかどうかではありません。私が探しているのは、人間には成し得なかったであろう形でAIが我々を助けている兆候です。私の関心を駆り立てたのは、Tony Fangさんたちによるある論文でした。その論文には、実に正直な一文がありました。いわゆるエルデシュ問題と呼ばれる問題群についていくつか成功を収めたが、私たちが解決できた問題は、その難しさゆえではなく、その知名度の低さゆえに解決できたのだ、という趣旨のことが書かれていたのです。私はこれを、実に正直な発言だと思いました。つまり、AIが人間には成し得なかった何か華々しいことをしたわけではなく、論文が発表されて15分後には誰かしらの人間が「ああ、それならやり方を知っているよ」と言うようなものだった、ということです。一方で、もっと最近のある論文があります。これは回路計算量に関する二次下界を示したもので、非常に非自明な結果だと私は考えています。この論文を読み進めていくと、人間が構築した枠組みは確かに多いのですが、中心となる困難な部分は実際にはモデルによってなされていることがわかります。つまり、これは言語モデルが何か不可欠なことをやってのけている、というほんの小さな証拠だと言えるでしょう。

そして先週、OpenAIからある発表がありました。私はこれを実に見事な進展だと考えています。問題設定はこうです。平面上にn個の点を配置します。エルデシュはこう問いました。単位距離、つまり距離がちょうど1であるペアの数を最大化するように、これらの点をどう配置すればよいか、と。OpenAIのシステムがやったことをお伝えします。これは彼らの一般公開されている言語モデルのどれかではないと思われます。彼らも明確にはしていないのですが、彼らは非常に単純明快な問題設定のプロンプトを投げ込みました。すると、システムはそれを解き進め、定理と証明を返してきました。その定理はこう述べています。無限に多くのnについて、ある定数デルタが存在し、単位距離の数が少なくともnの1+デルタ乗になる、というものです。これは私たちが知らなかったことであり、大きな進展です。そしてこのシステムは自律的にこれを成し遂げました。私がこれを取り上げるのは、およそ80年もの間、数学者たちがこの問題を解こうと試みてきたからです。これは、ここに存在する現実的で具体的な進展だと言えます。

ここから私たちが実際に取り組んだ内容についてお話しします。私たちは数学と計算機科学の2つの設定を研究しました。ひとつは離散最適化における困難性、つまり計算量理論の話です。もうひとつは古典的な組合せ論、ラムゼー数の話です。ここで最初に申し上げておきたいこと、そして何度か繰り返し申し上げることになりますが、私たちが研究した問題は、時の試練に耐えてきたものだということです。優秀な人々が長年にわたって取り組んできた問題であり、先ほど申し上げたような「知名度の低さゆえの解決」というものには当てはまりません。これらはいずれも、Anand Nagdaさん、Abhra Takotさんとの共同研究です。

4. Alpha Evolveによる計算量理論の証明

4.1 Max Cut問題における近似困難性の証明

Prabhakar： それでは複雑性理論の設定に入っていきましょう。私たちは2つの古典的な問題を研究しました。ひとつはMax Cutで、もうひとつは巡回セールスマン問題です。後者は今回の目玉となる結果になります。両方の設定において、私たちはAlpha Evolveと呼ばれるAIツールを使いました。まず最初の結果をご説明してから、Alpha Evolveが実際に何をしているのかを説明したいと思います。というのも、AIツールが実際に何をやっているのかを理解するには、まず証明の性質をある程度理解しておく必要があるからです。

Max Cutの問題とは何でしょうか。無向グラフを与えられて、それを2つの部分に切り分け、切られる辺の数を最大化することを目指します。最小化するのは簡単ですが、最大化は難しく、正確なカットを見つけることはもちろん、ほぼ正確なカットを見つけることさえ難しいのです。これを2つではなく3つ、4つ、5つといった部分に切り分ける variant を研究することもできます。実際、私が最初にお話しする結果は、グラフを4つの部分に切り分けるというものです。無向グラフを与えられて、それを4つの部分に切り分け、切られる辺の数を最大化する、という設定を考えていただきたいと思います。

私たちが証明できたのはこういうことです。最大の4分割カットを見つけることが困難であるだけでなく、それを98.7%まで近似することさえ困難であるということです。これは些細な係数に見えるかもしれませんが、その意義については後ほど説明します。言い換えれば、最大のカットが1000本の辺だとすると、987本の辺のカットを見つけることさえ困難だということです。これはガジェット還元という手法によって示します。ガジェット還元とは何かを、忘れてしまった方のために2枚のスライドで簡単に振り返っておきます。まず、困難であることがわかっている問題から始めます。今回証明したいのは、4分割Max Cutの近似の困難性です。出発点となるのはThreeLin4と呼ばれる問題で、これは方程式の族であり、各方程式にはちょうど3つの変数があり、すべての変数はmod4です。つまり値は0、1、2、3のいずれかです。この方程式の族が左側に示されていますが、これは困難であることが知られているとしてください。ここから目標となる問題、つまり無向グラフのインスタンスを作ります。この方程式の族が与えられたときにグラフを構築し、もしこのグラフを4分割できるなら、この方程式群の解が得られる、と主張します。しかし、この方程式群を解くこと自体はほぼ不可能なので、グラフの分割も困難であるはずだ、というわけです。ガジェット還元とは、元の問題の一片、この場合は方程式群のうちの1つの方程式を取り、そこから目標問題の一片を構築するレシピです。これは概念図であって、実際に構築されるグラフそのものではありません。すべての方程式についてこの手順を行い、右側のグラフの断片をすべて糊付けすると、大きなグラフができあがります。そしてこのグラフを分割できれば、方程式群が解けたことになる、という主張になるわけです。

Alpha Evolve、これから説明するツールですが、しばらく動き続けた末に、「これが98.7%の困難性を証明するガジェットだ」と返してきました。そのガジェットは、たとえば左側にあったx1+x2+x3=0のような方程式を19ノードのグラフに変換したものであり、辺の重みは1から1429の間になっています。なぜ1429なのか、私にはわかりません。機械がそう言ったのです。1429は素数ですが、より興味深い1729ではありません。しかし、そう言われても「なぜそれを信じられるのか、正しいとどうやってわかるのか」と思われるでしょう。これは少し置いておいてください。証明の検証は、AI支援による数学全体において非常に重要な要素であり、後ほどこれに関する小さな良いアイデアをご紹介します。実は、こうしたガジェットを機械的に生成するという発想自体は完全に新しいものではありません。1996年、つまり今から30年前に、線形計画法を使ってはるかに小さなガジェットを構築した論文がありました。TrevisanさんとNatalさんによるものです。実はこれには奇妙な巡り合わせがありまして、この研究は私がIBMにいた時代に、私のグループで行われたものでした。当時は私はまったく注意を払っていなかったのですが、今はそれに大いに注目しています。

4.2 Alpha Evolveの仕組みと証明検証の方法論

Prabhakar： それでは、このガジェットを生み出した仕組みについて説明します。ここで重要な点に注目していただきたいのですが、私たちはLLMに対して「ガジェットを見つけてくれ」とは言っていません。私たちがLLMに対して行っているのは、「ガジェットを生成するプログラムを書いてくれ」という依頼です。つまりLLMはPythonコードの断片を大量に生成します。これらのPythonコードの断片がガジェット、つまりこれらのオブジェクトを生成します。私たちはこれらのオブジェクトを、最終的な証明でどれくらい良い近似係数を与えてくれそうかによってスコアリングします。成績の良いプログラム、いわば「緑色のプログラム」を再びLLMに戻して、「これらが良さそうなプログラムだ。もっとこういうものをくれ」と伝えます。これを何度も繰り返し、数千回にわたって回していきます。一方でスコアが振るわなかったものは捨てていきます。つまりAlpha Evolveがやっているのは、LLMを使ってガジェットそのものを生成・進化させるのではなく、ガジェットを生成するプログラムを、私たちが作った代理スコアリング関数によってスコアリングしながら生成・進化させることです。そして成功したプログラムが再び言語モデルに与えられて新しいプログラムを生み出します。これを別の見方で捉えると、こういうことです。誰かが証明した困難性の証明があるとして、その中にはガジェットが埋め込まれています。この証明を長い文字列だと考えてみてください。これはほとんど遺伝子編集のようなもので、元のガジェットを切り出して新しいガジェットを差し込むことで、より良い近似比が得られるのです。今回の場合、Alpha Evolveは19ノードのこのガジェットを見つけてくれましたが、これは人間が見つけたとは考えにくいものです。この点については後ほどまた触れます。

さて、このガジェットが実際に主張する定理を成立させているかどうかを検証する必要があるとお話ししました。正しいやり方は、このガジェットをあらゆる可能な方法で4分割し、網羅的に検証することです。しかしこれには何時間もかかります。一方でこの内部ループを数千回も回したいわけですから、検証のたびに何時間もかけるわけにはいきません。そこでどうしたかというと、Alpha Evolveに「検証を行うプログラムを見つけてくれ」と依頼したのです。私たちは15ノードや20ノードのグラフを大量に含む合成データセットを作成し、Alpha Evolveに「これらのグラフにおける4分割カットを検証するプログラムを出力してくれ」と依頼しました。そして、1秒以内に終わらせることを条件にしました。これは私たちが恣意的に選んだシステム定数ではあるのですが、もしガジェットを1秒で検証できるなら、1回の実行で数千回もループを回せるだろうと考えたためです。他にもいくつかの工夫を行い、言語モデルを使ってこれらのプログラムを批評させたりもしました。最終的に、うまく機能しているように見える検証プログラムができあがりました。「ように見える」というのがどういう意味かは、次でお話しします。Alpha Evolveはこの検証プログラムを作り出し、1秒で検証を行っているように見えます。それを使ってガジェットを次々と生成しているわけですが、皆さんはこう疑うでしょう。「ように見える、とは言ったが、そのガジェットが本当に正しいとどうしてわかるのか」と。実際に私たちが行ったのはこういうことです。4分割の場合、Alpha Evolveは独自のブランチアンドバウンド戦略を編み出しました。LLMがブランチアンドバウンド戦略を書いたのです。さらに、私たちが存在すら知らなかったPythonのライブラリを使って、システムレベルの最適化を数多く行いました。これによって、網羅的検証に比べておよそ1万倍の高速化が得られました。網羅的検証は誰も好んでやりたいものではありませんが、これまで数時間かかっていた検証が、1秒で終わるようになったのです。しかし今日の時点で、私はこれらの検証プログラムが実際に正確であったと皆さんに断言することはできません。では、なぜ定理を主張できるのかというと、最終的なガジェットが出力された段階で、私たちはそれを網羅的な検証プロセスにかけたからです。つまり全体の構図としては、内部ループでは高速でずさんな検証を使い、証明らしきものを吐き出させ、最後に網羅的な検証を行うということです。そしてこの場合、網羅的検証はガジェットの部分だけに対して行えばよいのです。なぜなら証明の残りの部分はそのまま保持されているからで、遺伝子編集された部分がうまく収まっているかだけを確認すればよいことになります。

このあたりで一度整理しておきましょう。Alpha Evolveは証明を生成するためにLLMを使うのではなく、証明を生成するプログラムを生成するためにLLMを使っています。これは一発勝負の実行です。プロンプトを書いて、あとは座って見ているだけで、対話的に「こうしてみたらどうか」とやり取りするわけではありません。完全に自律的なのです。Alpha Evolveは自分がこの定理の困難性を証明しているということを実際には理解していません。私たちが作った代理スコアリング関数を与えられているだけで、それだけを頼りに動いているのです。そしてガジェットは高速かつずさんに検証されており、これがなければ私たちはこうした結果には到底たどり着けず、時間切れになっていたはずです。最後にリフティングと呼ばれる過程があります。私たちが構築したのは19ノードのガジェットですが、そこから得られる定理はすべてのnについて成り立ちます。これはあらゆる還元がそうであるのと同じことです。

4.3 その他の複雑性理論の成果とTSP下界の改善

Prabhakar： ここで簡単に、同様の手法によって得られた複雑性理論の他の結果にも触れておきます。Max CutとMax独立集合の両方について、一連の結果があります。この2つの古典的な困難問題はいずれも、ランダムグラフを与えられたとき、最良の答えにどれだけ近づけるか、という形をしています。私たちが示せたのは、数学的にありそうもない事象を除けば、Max Cutを最適値の5%以内で認証することはできない、ということです。複雑性理論はすべてこのような相対化された形になるのですが、これは以前の研究の上に成り立っています。私たちはまた解析を用いて、これがほぼ最良であることも示しました。ここではAIが小さな研究領域を実質的に閉じてしまったと言える事例です。手法は同様で、遺伝子編集的なやり方です。Konyagin-Uparの証明にある、約10ノードの特定の性質を持つラマヌジャングラフを取り出し、Alpha Evolveを使ってはるかに大きなラマヌジャングラフを見つけました。ラマヌジャングラフやベクトルの詳細についてはここでは触れませんが、それをはめ込むと定理が出てくる、という仕組みです。ここでも高速でずさんな検証が用いられ、ループを速く回すことができました。

複雑性理論のセクションを締めくくるにあたり、巡回セールスマン問題についてお話しします。ほとんどの方がご存知だと思いますが、簡単に振り返ります。セールスパーソンがn個の都市を訪問しなければならず、これらは距離空間上にあると仮定します。近似的に良いツアーを見つけることさえNP困難です。最良の上界は、60年前のアルゴリズムが最適値の1.5倍を達成しており、それが5年ほど前にKarlinさんたちによって1.5マイナスイプシロンにまで改善されました。このイプシロンはおよそ10のマイナス38乗というごくわずかなものです。一方で、困難性の下界としてこれまで示せていた最良の結果は、およそ10年前にKleinさんとKlobicovaさんが行った研究で、2020年に最終的に発表されたのですが、117/116より良い近似を見つけることはNP困難である、というものでした。つまり最短ツアーが116だとすると、長さ117のツアーを見つけることさえNP困難だ、ということです。これがKleinさんとKlobicovaさんの結果です。私たちが行ったのは、これを111/110にまで改善することでした。これも一見わずかな改善に見えるかもしれませんが、この係数を押し上げていくこと自体に意義があります。真の答えは4/3であろうと推測されていますが、上界と下界のいずれから見ても、私たちはまだそこには程遠いことがわかります。これは非常によく研究されてきた問題で、最初の論文は1991年のPapadimitriouさんとYannakakisさんによるもので、近似が困難であることを示しただけで、具体的な定数すら持っていませんでした。過去35年間で、私たちの結果によってこれを111/110まで引き上げたことになります。証明の構図は先ほどと同様に見えるはずです。証明を取り、あるガジェットを別のガジェットに置き換える、というものです。ただし、ここには少しひねりがあります。従来の研究には、ガジェットを改善するだけで済むというクリーンな定式化がありませんでした。そこで私たちは、KleinさんやKapinskyさんたちの複数の研究成果を組み合わせる必要がありました。つまりこのケースでは、人間が多くの下準備を行ったということです。これは、実験室にある非常に高価な装置を扱う際に、人間が入念な下ごしらえをするのに少し似ています。それが済んだところで機械に渡すと、機械はこのガジェットを使えばよい、と返してきました。ここでひとつ指摘しておきたいのですが、このガジェットをよく見ると、mod3のガジェットに期待されるような三方向の対称性を持っていません。この点には後ほど講演の最後で少し触れる意義があります。

5. Alpha Evolveによるラムゼー数研究

5.1 ラムゼー数の基礎と下界探索の全体像

Prabhakar： ここからはラムゼー数について数分お話ししたいと思います。おそらく皆さんの多くはどこかでラムゼー数に出会ったことがあると思いますが、これは組合せ論の中でも美しい分野で、その歴史はおよそ100年前に遡ります。Frank Ramseyさんはこういう観察をしました。6人をディナーに招待すると、その中には必ず互いに知り合いである3人組か、あるいは互いに見知らぬ3人組のどちらかが存在する、というものです。つまり、十分な大きささえあれば、どんなに無秩序な状態であっても、クリークか独立集合という形で秩序が必ず現れるということです。言い換えると、6ノードの完全グラフの辺を彩色すると、必ず赤い三角形か青い三角形のどちらかができる、ということです。これがラムゼーさんの示したことで、これをスライドの一番下ではR(3,3)=6と表記します。ここから、次のような問いを扱う豊かなラムゼー理論という分野が生まれました。2つの正の整数RとSが与えられたとき、RとSのラムゼー数とは何か、という問いです。RとSのラムゼー数をどう見つけるかというと、一般には分かっていません。離散数学には上界と下界を見つけるための、いわば一大産業のようなものが存在しています。ここでは下界がどのように見つけられるかをお話しします。下界は典型的には計算によって求められます。計算上の目標はこういうものです。たとえば35ノードのグラフを構築できて、そこに4人の相互の友人も6人の相互の見知らぬ者もいないとします。すると、R(4,6)は少なくとも36であることがわかります。これがAlpha Evolveによって計算で見つけられたラムゼー数の下界の表です。Alpha Evolveがどうやってこれを見つけるかというと、あるセルを取り、35ノードや91ノードなどのグラフを生成しようとするプログラムを書き、成功した場合にはそれを返してくる、という仕組みです。この図はおよそ1ヶ月前のもので、それ以降いくつかのセルが埋まりました。色の意味を説明します。青いセルは、Alpha Evolveが下界を見つけ、それが対応する上界と一致しているため最良の下界であることが確定しているケースです。こうしたケースはすべて、Alpha Evolveが見つけた下界自体は新しいものではなく、既知のものと一致しています。これは半ダースほどあります。黄色いセルは、Alpha Evolveが下界を見つけたものの、既知の上界とは一致していないケースです。上界の方が高く、その下界自体はすでに知られていたものです。ここで少し考えていただきたいのですが、下界が一致したからといって、その下界を見つけたのと同じグラフを見つけたことにはなりません。何らかのグラフがその下界を達成した、というだけのことです。そして緑色のセルは、Alpha Evolveが現在世界記録を保持しているケースです。以前の記録をサイズにして1から4ほど更新しました。これらが私たちが見つけた新しい下界です。

5.2 個別アルゴリズムの分析と過去の謎の解明

Prabhakar： ここで少し立ち止まって考えてみましょう。それぞれのセルについて、Alpha Evolveは下界を見つけるプログラムを出力していると申し上げました。実際には数千個のプログラムを出力し、そのうちの1つが最終的にブレークスルーをもたらすのです。生のコードをお見せするつもりはないので、代わりにGeminiを使ってコードを要約させました。これらの探索アルゴリズムのいくつかを見ていくのはなかなか興味深いものです。これらのセルそれぞれについて1つずつあると想像していただきたいのですが、実際にはすべてGitHubに公開してありますので、興味のある方はご覧いただけます。アルゴリズム14はR(3,11)の下界を求めるものでした。これは、Paleyグラフなどさまざまな多様な出発点となるグラフのプールから始めて、「適応的スコアリング」と呼ばれる手法を行う、というものです。これはすべて機械が行ったもので、人間は一切関与していません。辺を反転させ、行き詰まったら温度を再び上げるという、シミュレーテッド・アニーリングの凝った形式を行います。そしてこれは既知の最良値と一致する下界にたどり着きました。一方、R(3,13)のセルでは、まったく異なることを行っています。これがこの手法の特徴のひとつなのですが、あるセルである下界アプローチが見つかったからといって、それが次のセルの下界アプローチについて何かを示唆するわけではありません。これらは互いにかなり独立しているように見えるのです。まとめますと、それぞれのセルは、RとSの数論的な特性によって難易度が異なるように見え、成功したプログラムすべてに共通するパターンを見つけようと努力しましたが、見つけられませんでした。しかし、これらすべてのアルゴリズムを生み出したメタアルゴリズムであるAlpha Evolve自体は、すべてに共通しています。つまりある意味では単一の普遍的なアルゴリズムなのですが、それが言語モデルの持つラムゼー理論に関する知識や理解、そしてアルゴリズムやヒューリスティックに関する知識を使ってこれらの結果を生み出しているのです。これらを読んでいくと、人間が見つけてきた自然なアプローチを取り出して、それらをつなぎ合わせて成功したアプローチを作り出しているように見えます。そして興味深いことに、以前の表にあったいくつかのセル、6つほどのセルは、ロシアの謎めいたプロジェクトによって下界を証明するグラフが見つけられていたものの、そのグラフをどうやって導き出したのかはまったく説明されていませんでした。私たちにはそれがどうやって作られたのか見当もつかなかったのです。今回、私たちはそれらの下界を再現することができ、そのアルゴリズムを公表しました。これで研究者たちは、それらのセルがどのように導出されるのかを知ることができるようになりました。ここでも、高速でずさんな検証が活用されています。これらのアルゴリズムが動いている間、グラフを構築しながら「まだ73個のクリークがある、これをゼロにしなくては」「まだ47個の独立集合がある、これをゼロにしなくては」というふうに進んでいきます。この数はたいてい非常に高い値から始まるのですが、正確な数を数える必要はなく、近似的なカウントで十分だということが分かりました。Alpha Evolveはこうした非常に高速な近似カウンターを編み出してくれるのです。

6. 研究プロセス全体への考察

6.1 AIの役割の本質と人間による代替可能性

Prabhakar： それでは講演の最後の部分として、これまで辿ってきた歩みと、この先が何を示唆しているのかについて、少し振り返って考察したいと思います。これらの結果は、私が誇りに思う研究成果としてどこに位置づけられるでしょうか。独創的な研究として見れば、おそらく私のお気に入りというわけではありません。しかし、ここでの意義は結果そのものではなく、私たちがどのようにそこに至ったか、そして自律的な言語モデルがそこにどれだけ関与したか、という点にあります。私たちのAlpha Evolveの使い方は、ある意味で構文的なものです。私たちは、言語モデルが自分のやっていることを深く理解しているとは主張していません。AIは私たちがそう指示したからこそ、この証明の断片を生み出しているのです。より優れたモデルであれば、より良い意味論を伴ってさらに優れた仕事をするようになるでしょうし、実際に今構築されている新しいシステムの中には、そうしたことを行っているものもあります。証明の検証は、こうした自律システムにおける重要なボトルネックだと思いますが、ここで学んだことは、序盤の段階ではずさんであっても構わない、最後さえ厳密であれば良い、ということです。

では、才能ある人間ならこれらの結果を生み出せたのではないか、と思われるかもしれません。皆さんの中には、有名な数学者Andrew Wilesさんの逸話をご存知の方もいるでしょう。彼はフランス当局に6ヶ月間拘束され、完全に孤立していたときに最高の仕事をした、と語っています。もしかすると、この分野を本当に熟知した人物を6ヶ月間閉じ込めれば、こうした結果にたどり着けるかもしれません。しかし、19ノードもの重み付き辺を持つガジェットを紙と鉛筆で思いつけるとは、なかなか信じがたいことです。もうひとつ申し上げておきたいのですが、TSPのガジェットは非対称性を利用しており、これは新しい点です。というのも、これまでTSPの困難性のために考えられてきたガジェットはすべて対称的なものだったからです。しかし最終的には、正しい評価基準は次の2点だと思います。第一に、これらは多くの人々が長年取り組んできた、時の試練を経た問題であるかどうか。第二に、結果を発表してから15分後に誰かが「それなら手作業で同じことをやったことがある」と言い出さないかどうか、です。もしそうならないのであれば、AIがこの結果に決定的な役割を果たしたという証拠がいくらかあることになります。皆さんはこう言うかもしれません。「同じだけの計算資源を賢い人に与えたら、その人にも同じことができたのではないか」と。それが不可能だということを、疑いの余地なく証明することは私にはできません。しかしひとつの示唆を申し上げます。私たちはSATソルバーやSMTソルバーを試し、計算代数系もぶつけてみました。しかし、少なくとも私たちが符号化できた範囲では、その制約の数は途方もないものでした。問題によっては制約の数が10の300乗を超えるものもありました。もちろん、数理計画に非常に長けた友人がいれば、それをもっと切り詰められたはずだ、というのはまったくその通りです。ですから、私たちが絶対的に最先端の手法を使ったと主張しているわけではありません。しかし、従来の道具、たとえば数理計画法のようなものは、今日この問題に対しては不十分に感じられました。

私たちはここで、Alpha Evolveが実際に何をしているのかを考え始めました。LLMがプログラムの集団、今日で言えばエージェントと呼ばれるものかもしれませんが、それらを解き放ち、コードを進化させてプログラムを生成させています。つまりこの間接性が役に立っているように見えるのです。これを捉える興味深い見方のひとつとして、特に大学教員の方にはピンとくるかもしれませんが、あなたには今や1万人の大学院生がいるようなものだ、という比喩があります。「Johnさん、あなたはこのラムゼーのセルだけをやってください」というふうに指示を出せるわけです。ただ、私たちが構築したシステムでは、あるセルに取り組んでいるJohnさんが、別のセルに取り組んでいるMaryさんとまったく会話をしていません。それぞれが独立した実行になっているのです。これはラムゼー数の探索において非常に顕著に見られる特徴です。ただ、なぜ勝つときに勝つのか、私たちには本当の理解がありません。「では直接LLMにプロンプトを投げればよかったのではないか」と思われるかもしれません。冒頭の負荷分散の研究についていえば、確かにシミュレーションには役立ちました。出てきた微分方程式については、直接のプロンプトではうまくいきませんでした。そして講演の残りの部分、複雑性理論と組合せ論についてお話しした内容では、時にはモデルに最先端の結果を再構築させることさえできず、まして最先端を超える何かにたどり着かせることはできませんでした。ですから、ゼロショットのプロンプトを、コードやエージェントなど何と呼ぶにせよ、何らかの形の誘導された探索によって強化する必要があると思います。

6.2 失敗事例の欠如と数学的理解の深化を巡る考察

Prabhakar： ここで、私たちが道すがら気づいたある観察についてお話しします。言語モデルは成功談に富んでいます。数学や計算機科学における成功した論文で訓練されているからです。しかし失敗はそこには反映されません。失敗は皆さんの頭の中にとどまっているのです。ここにいらっしゃる専門家の皆さん一人ひとりが、豊富な経験をお持ちだと思います。「これは試したことがある、こういう理由でうまくいかないとわかっている」というものは、決して言語モデルには入り込みません。ですから、こうした失敗の概念を人間の頭の中から引き出して探索プロセスに組み込むことが重要になってくると思います。人間のフィードバックを伴う何らかの形の強化学習を使えば、それができるかもしれませんが、これはまだ私たちが考え続けていることです。ただ、これは重要な観察だと思います。失敗は言語モデルにはほとんど、あるいはまったく反映されない、ということです。

こうしたことから、私は数学を行うという営みそのものについて考えるようになりました。およそ30年前に書かれた、Bill Thurstonさんによる美しいエッセイがあります。彼は、数学者の仕事は定理を量産することではなく、数学に対する人間の理解を深めることだ、と論じています。もし機械が何日も何週間もかけて動き続けて、「見よ、これが答えだ」と出してきたとして、それは果たして数学的理解を深めていると言えるのだろうか、と考えざるを得ません。私にはまだ確信が持てません。ただ、最近の証明の中には、いわゆる「思考のトレース」というものを吐き出すものもあり、これらは機械が途中で何をしていたのかを理解する助けになると言えなくもありません。これは非常に強力な視点であり、理解されるべきものだと思います。

7. AIと学術出版・査読を巡る論点

7.1 論文からLLMを排除すべきかという議論

Prabhakar： LLMを学術的な場から締め出すべきでしょうか。私は、もう瓶からジーニーは出てしまったと思っています。もちろんこれは私の偏った見方であることは承知しています。すでにひとつのノーベル賞が、機械学習の力なしには実現しなかったはずです。タンパク質の折り畳みを扱うAlphaFoldのことです。かつては学生が湿式実験室でタンパク質の3次元構造を決定するのに5年から6年もかかっていたところを、わずか数週間で2億個ものタンパク質が3次元に折り畳まれるようになりました。「数週間」というのは少し公平ではないかもしれません。そのシステムを設計するには多くの人間の思考が費やされたわけですから、そのすべてがそこに含まれています。しかしそれでも、2億年もかかったわけではないのです。そして私は、この議論自体があまり意味を持たないと思っています。というのも、私たちは以前の世代の科学者たちが顕微鏡や望遠鏡を使うことを禁止しなかったわけで、同様にLLMの使用を禁止すべきではないと考えるからです。先ほどJohnさんと話していたのですが、彼は「では人々が虚偽の結果を主張したらどうするのか」と言いました。確かにこれは懸念すべき点です。しかし著者として、自分の結果の正しさについては責任を負うことになります。ですから、ある結果を発表するのであれば、その結果に対して責任を持ち続けることになるわけです。とはいえ、明確な懸念があることも事実です。

7.2 LLM生成テキストの兆候とarXivの規制強化

Prabhakar： いくつかの傾向についてお話ししておきます。およそ4ヶ月前のデータを見ると、現在、計算機科学の論文のおよそ20%が、LLM支援による執筆の顕著な兆候を示しています。もちろん、それは単なる文章表現の話であって、本当の研究そのものではない、という見方もできるでしょう。この境界線を定義するのは難しいところです。しかし人々が繰り返し指摘しているのは、LLM支援による執筆では概念的な密度が高くないということです。そこには多くの直感が込められているわけではなく、代わりに滑らかで自信に満ちた、流暢な文章になっているだけで、それが必ずしも多くを伝えているわけではありません。そしてこれは、決してコミュニティにとって良いことではありません。先ほどのBill Thurstonさんの言葉に立ち返るならば、まさにその通りだと思います。

実際、arXivはより厳格な管理体制を導入しています。というのも、レビュー論文が急増したからです。LLMを使ってレビュー論文を書くことが非常に簡単になり、それが大量に引用されて、著者のH指数が上がる、というようなことが起こりました。良い話に聞こえますが、結果として質の低い論文が爆発的に増えることになったのです。ですから、これらはコミュニティが取捨選択していかなければならない本物の懸念事項です。というのも、もし完全にLLMが生成した論文、それが科学的理解を前進させるかどうかも分からないような論文を大量に排除し始めれば、私たちは今日私たちが置かれている状況、つまりLLMによる支援を受けた査読が大量に行われるという状況に陥ってしまうからです。SIGMODの査読のうちどれだけがLLMによって査読されたのか、KenさんやSudeepaさんが測定を試みたかどうか、私にはわかりません。

8. SIGMODコミュニティへの示唆

8.1 move 37に匹敵する兆候とSQL最適化への応用

Prabhakar： それでは、この話の部分をまとめて、SIGMODにとって何を意味するのかという考察に移りたいと思います。LLMがWeb研究において当たり前の存在になりつつあるのは確かですが、そこに人間を超えた決定的な能力が存在するのでしょうか。AlphaGoとイ・セドルさんとの2局目における、いわゆるmove 37に相当するようなものは存在するのでしょうか。あの一手を見た囲碁の専門家たちは、「これは人間がやりそうなことではない、真に卓越したものだ」と言いました。ずさんな証明検証というものはこれからも続いていくと思いますし、LLMに直接プロンプトを投げるのではなく、こうしたエージェントを介する間接的なアプローチには非常に強力なものがあるように見えます。

それではSIGMODの世界にとってこれは何を意味するのでしょうか。ここからは私自身が見てきたSIGMODの世界がどう進化してきたか、非常に個人的な見方をお話しします。まず分かりやすいところから始めますと、LLMは本質的には書き換えシステムです。ですから、ひとつの書き換えの形として、SQLクエリの最適化、あるいはあらゆる種類のクエリ最適化を見ることができます。すでに有望な初期の研究が行われていますし、実際にこの会議の中にもこのテーマに触れている論文があります。つまりSQL式が与えられたときに、それを書き換えてより速く動くようにする、というものです。しかしもちろん、ここでもまた検証の問題に直面します。書き換えられたクエリが、元のクエリが意図していたのと同じ結果を返すかどうか、という問題です。

8.2 データ管理の歴史的変遷と検索連動広告という市場メカニズム

Prabhakar： しかしそれを超えて、時の流れの矢がどこに私たちを連れて行くのかを考えたいと思います。過去75年間のコンピューティングを振り返ると、私にはこう見えています。最初はすべてが非常に構造化されたものでした。基本的には物理学の実験室や宇宙軌道関連の装置から出てくるデータでした。それから20年か25年が経つと、エンタープライズがその座を引き継ぎました。RDBMSと古典的なエンタープライズアプリケーションの時代です。しかし2000年頃までには、私たち全員が仕事を持つ頃には、突然、非構造化データの爆発が起こりました。何十億人もの人々がメールやWebページなどを生成するようになったからです。そして私たちはある種の難問に直面しました。データ量のほぼすべてが非構造化データである一方で、価値のほぼすべては構造化データにあったのです。私たちはこのコミュニティや他のコミュニティと共に、非構造化データという海の中からその貴重な知見の粒を取り出そうと、エンティティ抽出器のようなものを書くために多大な労力を注ぎました。そして興味深いことに、2000年頃、この問題は計算機科学のアルゴリズムによってではなく、市場メカニズムによってある程度解決されました。私たちが行ったのは、最も重要なエンティティ、単語、フレーズを抽出するという仕事を、キーワードやフレーズに入札する市場に委ねることでした。これが結果として、Webの経済を支える1兆ドル規模の市場を作り出したのです。これは、ある意味で計算機科学とミクロ経済学が驚くほどシームレスに融合して、あるCSの問題を経済学の力によって解決した最初の事例だったと言えます。

8.3 マルチエージェント協調による新たな「エージェント型非構造化データ」時代

Prabhakar： LLMのこの時代において、私たちが目にしているのは、Alpha Evolveやその後継のようなシステムが、エージェントを次々と生み出し、大量のいわゆる「思考」のトレース、大量のテキストを吐き出している、という状況です。私たちはこれを理解しなければなりません。実は、受賞対象となったビデオのひとつも、まさにこの点に触れていたことに気づきました。ここでAlpha Evolveの発展形をご紹介します。基本的には先ほどと同じ絵なのですが、今度はエージェントたちが互いを無視して自分のことだけをやるのではなく、共通のブラックボードを見て、他のエージェントが何を言い、何をしているのかを理解しようとしています。これから、私たちが今まさに開発している最中のシステムのトレース、スナップショットをお見せします。これはすでにいくつかのラムゼー記録を更新しました。まだ非常に初期の段階です。ある画面には「最終的な内訳」と表示され、「これが最適なアプローチだ」というところから始まります。これは1つのエージェントが吐き出したものです。実際に起きたことは、あるエージェントが「あるアプローチがある」と主張したものの「これ以上は無理だ」と諦めてしまい、別のエージェントがそれを引き継いで「ああ、それを仕上げる方法が分かる」と言って、実際にやり遂げた、というものでした。つまり、複数のプログラムの間である種の協調が生まれ、これが結果として新しいラムゼー数の下界につながったのです。また、あるエージェントが時々まったくのナンセンスを吐き出すこともあります。「大きなブレークスルーを見つけた」と言うのですが、これはエージェントが進捗を出さなければというストレスを強く感じているためだと思われ、まるで一部の政治家のツイートのように聞こえる主張をすることがあるのです。なかなか興味深い挙動です。

つまり、こうした相互作用するエージェントが進化していくシステムを立ち上げることができるということです。冗長であってもかまいません。彼らは構造的であろうとしているわけではなく、厳格なスキーマを持っているわけでもないからです。彼らが排出するデータは大量かつほとんど構造化されていないものになります。これらの排出されたトレースの解釈と、それに基づく行動は、他の要素に委ねられています。人間が消費できる量に縛られる必要はありません。ですから、SIGMODのコミュニティにとってこれが意味するのは、アクティブあるいはエージェント的な非構造化データという新しい時代に足を踏み入れつつある、ということだと思います。このコミュニティは、非構造化データに関する内容の割合が長年にわたって増加してきたという変遷をすでに経験しています。そして今、私たちは新しいエージェント的な非構造化データの時代に入っているのです。ちょっとした提案として申し上げたいと思ったのですが、あまり真剣に受け止めてほしくないので少し脇に置いておきます。しかし、これはひとつの進化のかたちかもしれません。私にとって、私たちはまさに激動のさなかにいます。私たちの周りで多くのことが変化している、非常に騒然とした領域にいるのです。そしてこれは、研究者にとって、Carsonさんが冒頭でおっしゃったように計算機科学者にとって、さらに広く科学者全般にとって、非常にエキサイティングなことです。最後に、Alan Turingさんによるこの論文、模倣ゲームについて書かれた論文の中で見つけた古典的な一節で締めくくりたいと思います。この論文の最後で、彼はさまざまな形の学習について語っているのですが、その最後にこの見事な一文があります。「私たちが見通せる先はわずかであるが、そこにはなすべきことがたくさんあるのが分かる」。ありがとうございました。

9. 質疑応答

9.1 LLM導入のタイミングとアカデミアのアクセス問題

司会： Prabhakarさん、素晴らしい基調講演をありがとうございました。質疑応答の時間を10分ほど設けております。会場にマイクがございますので、ご質問のある方はマイクの前にお進みください。すでにFelixさんがマイクに向かわれていますね。それではFelixさん、どうぞ。

Felix： ありがとうございます、Prabhakarさん。素晴らしい講演でした。手短に質問させてください。科学的なプロセスのどの段階でLLMを関与させるべきだとお考えですか。あるいは、いつからLLMを使い始めてよいのでしょうか。プロジェクト単位のレベルと、教育のレベルの両方について伺いたいです。問題についてどれくらい深く理解している必要があるのか、そして教育のどの段階からLLMを使い始めるべきなのか、という点です。

Prabhakar： ああ、なるほど。私たちはこの歩みのまだ非常に初期の段階にいると思っていまして、教育機関でも産業界でも、多くの実験が行われている最中です。正直なところ、まだ手探りの状態だと言ってよいと思います。今回の研究でも、私たちが得た成功に対してさえ、自分がどれほど慎重な態度でいるかをお分かりいただけたと思います。一方では良い気分です。私たちは時の試練を経た問題を選び、そこにLLMをぶつけて、何かを得ることができました。しかし他方で、私はまだ皆さんに「まず第1段階でこれをやり、第2段階で」といった型通りのレシピをお示しできる段階にはないと感じています。それにはまだ何年もかかると思います。その理由のひとつは、汎用モデルが非常に速いペースで進化し続けているという緊張関係があるからです。私が検索やGoogleマップのような製品にこれらのモデルを適応させようとしていた際に気づいたことですが、ある特定のアプリケーション向けにモデルをカスタマイズしようとして、事後学習などを終える頃には、主流のモデル自体がすでにさらに進歩してしまっているのです。ですから今のところは、主流モデルへの信頼を保ちつつ、時間をかけてアプリケーションごとの特化に立ち返るのがよいと思います。

司会： ありがとうございます。ここで少し負荷分散を、単純なアルゴリズムでやってみましょう。真ん中の列に移ります。

9.2 人間研究者の代替可能性と遺伝的アルゴリズムとの関係

質問者（中央列）： 素晴らしい講演をありがとうございました。分かりやすい質問をさせてください。皆さんやOpenAIから出てくるこうした結果を見るのは素晴らしいことですが、いずれもクローズドなモデルと非常に潤沢なリソースを使っているように見えます。数学やTCSの研究は今後、こうした場所に集中していくとお考えですか。私たちアカデミアの人間は、こうしたものへどうアクセスしていけばよいのでしょうか。

Prabhakar： 良い質問だと思います。私はあなたが思っているよりも楽観的です。その理由は、私がお見せした結果を生んだAlpha Evolveというものが、すでにおよそ2年前のものだからです。これは最先端ではありません。OpenAIの単位距離の結果は、おそらくかなり最先端だったと思います。しかし、大学から出てくるAlpha Evolveのようなシステム、場合によってはより優れたシステムを、私はたくさん目にしています。バークレー発のEvo Xというものもあります。大学はこうしたアイデアを非常に速く自分たちのものにしています。ですから、実際には市販の既製モデルと本当に優れたシステムのアイデアを組み合わせることで、より良い証明エンジンを構築することができるのです。無限の計算資源や最先端モデルをすべて揃える必要はないと思います。すべての恩恵を持たなくてもアカデミアの中で意味のある進展を遂げることは可能ですし、私はすでに多くの大学からそうした動きが出てきているのを見ています。ですから楽観的です。

司会： それでは右側の列に移りましょう。

質問者（右列）： おはようございます。AIが科学と数学の研究において人間を支援できるという点には、私も非常に納得しています。学生としても同意見です。私の質問はごく一般的なものです。現時点ではAIが科学や数学の研究を支援していますが、AIがこれほど急速に発展している中で、近い将来、AIは科学や数学の研究において人間を置き換えることができるとお考えですか。

Prabhakar： 私は置き換えられるかどうかということを主要な懸念事項だとは考えていません。私は1830年代、つまりおよそ200年前に書かれていたエッセイや論説の類を少し調べてみたことがあるのですが、そこで使われている言葉は、今日私たちが使っている言葉とほとんど同じなのです。「ああ、我々人間は無用になり、置き換えられてしまうだろう」というような言葉です。しかし実際にはそうはなりませんでした。起こったことは、人間が時間をかけて新しい種類の活動に確実に適応していく、ということです。ですから、皆さんの研究者として、科学者としての役割は、おそらく10年前に私たちがやっていたこととは違うものになっていくでしょうが、皆さんに何の役割もなくなり、ただ機械にすべてを任せて座って見ているだけになる、というようなことにはならないと思います。それが私の信念です。

質問者： ありがとうございます。

司会： それでは少し不公平なスケジューリングをして、中央の列に戻りましょう、こちらは列が長いので。

質問者（中央列）： Prabhakarさんに質問です。あなたはAlpha Evolveそのものについてどうお考えですか。私のグループを含め、Darwinと呼ばれる似たような取り組みが数多く行われています。

Prabhakar： 私はこれを、遺伝的アルゴリズムのLLM版のようなものだと考えています。

質問者： なるほど。もう少し深い洞察はありますか。どれだけこれを触ってこられたかを踏まえて。

Prabhakar： 深い洞察というほどのものはありません、Raghuさん。あなたの説明はかなり的確だと思います。私が付け加えるとすれば、こうした単純なアーキテクチャ、つまりLLMがプログラムを次々と生み出して進化させていくという形は、現時点ではおそらく最良の状態にあるとは言えず、私たちはもっと考える必要があるということです。特に、私たちが最初に踏み出した一歩は、異なるエージェントを孤立させるのではなく、互いにコミュニケーションを取らせるようにするということでした。ここで登場するのが共通のブラックボードで、そこから何が本物なのかをどう見極めるか、彼らが主張していることの中から何を蒸留するか、という点が非常に興味深いテーマになってきます。

質問者： それに関連して、もう少し踏み込んで伺いたいのですが。遺伝的な世代交代と候補の進化、そしてそれがスコアリングされていく過程を見ると、私がこれまで見てきたどのバリエーションにおいても、シミュレーテッド・アニーリングのような従来のものに見られる厳密な探索空間という要素が明確に欠けているように思います。なぜこの結びつきがまだなされていないのでしょうか。

Prabhakar： なるほど。私はこの分野に取り組んでいる者として、そしておそらくあなたのグループもそうだと思いますが、私たちはこれを実際に厳密な探索空間だと考えています。複数のエージェントが関わる場合でも、これらは巨大な探索空間なのです。ひとつには、多くの場合、明確な勾配を持っていません。あるエージェントが「私はかなり暖かくなってきた、みんなこっちに来てくれ」と言うような概念は存在せず、勾配が非常に緩やかなのです。これを緩和するひとつの方法として、私が以前に述べたコメントがありますが、失敗をもっと取り込む必要があるということです。というのも、どんな機械学習の問題でも、正の事例だけでは達成できないからです。負の事例が重要になってきます。ですから、これはここに非常に重要な要素として組み込まれるべきだと思います。ただ、大勢の人間が座ってこれらとやり取りする時間を割くことなしに、どうやってそれを実現するのか、私にはまだ分かりません。ただ、AlphaGoでは強化学習を通じてそれを何とか乗り越えたわけで、私たちもここで似たようなことができるのではないかと期待しています。

司会： それでは左側の列に移りましょう。

9.3 望遠鏡の比喩、論文評価軸の転換、形式検証の限界

質問者（左列）： こんにちは、講演ありがとうございました。素晴らしかったです。あなたは、かつて科学者たちが問題を解くために望遠鏡や顕微鏡を使っていたが、今は私たちがLLMを使っている、とおっしゃいました。あれらは解剖学的な問題を解くためのものでした。あなたは、LLMも同じ種類の問題を解くとおっしゃっているのでしょうか。

Prabhakar： 私が申し上げたのは、あくまで比喩としてです。つまり、私たちは天文学全体を、たとえば現在問題になっているような、最も強力な望遠鏡がほとんどの天文学者に利用可能ではないという理由で軽視したわけではありません。そうした望遠鏡はチリやハワイなどにわずか半ダースほどしかなく、特定のスペクトルの形を見たいのであれば、それらの場所のどれかにいなければなりません。しかし天文学の99%はそうした望遠鏡の外で行われています。それに対して、LLMは多くの研究者にとって手の届くところにあります。この部屋にいる皆さん全員が、最先端のLLMを手に入れることができます。チリなどに行く必要はありません。その意味で、これらはより広く応用可能であり、より広く利用可能なものだと思います。それが私の比喩的な論点でした。

質問者： ありがとうございます。

司会： それではまた長い列になっている中央の列に戻りましょう。

質問者（中央列）： あなたは公正なAIの利用と不公正なAIの利用についてお話しされました。LLMは今や私たちのほとんどよりも上手に文章を書きます。多くの人が、研究者として評価される対象は論文であるべきではない、と言っています。私たちが研究の成果として作り出すべきものは、コードやデータ、何らかの構造やプロトコルであるべきだ、と。そして人間に読ませたければ、ボタンを押せばテキストが出てくる、というようにすべきだ、と。それでは、こうしたAIの利用によって、出版プロセス、研究サイクル全体はどのように変わっていくとお考えですか。

Prabhakar： 良い質問ですね。皆さんの中には、有名な数学者Terence Taoさんが出しているビデオをご覧になった方もいるかもしれません。その中で彼は、数学は今やLeanによる証明としてカプセル化され、提出されるべきだ、と語っています。そしてあなたがおっしゃったように、それを人間向けの説明としてインスタンス化することができる、ということですね。

質問者： ちなみに、私はJanisと呼ばれています。Johnとお呼びいただいてもかまいませんが。

Prabhakar： 失礼しました、Janisさん、Johnさんとお呼びしてしまいましたね。実のところ、Taoさんの世界観では、すべてがLean証明の中に捉えられます。しかし、そこに至るにはまだ少し早いと思います。その理由をお話しします。最良のLeanコンパイラでも、今のところ扱えるのはせいぜい数千個の文でして、それではフェルマーの最終定理には到底足りません。まして将来、もっと大きな予想を扱うとなれば、なおさらです。ですから、私たちはあなたが指摘されているより広い論点に向けて、こうしたツールを構築している最中なのだと思います。もし私が大量のコードやデータを世に出したとして、それを異なる読者向けに知的に消費できる機械があるのか、ということです。私たちはそのためのインフラを構築していかなければならないと思います。

質問者： すばらしいです。ありがとうございます。

司会： それでは右側にいきましょう。

質問者（右列）： 講演ありがとうございました。私の質問は、数学的証明において人間にできることとLLMにできることの境界線についてです。あなたはLeanについて触れられましたが、実はデータ管理の分野でも、クエリの正しさなどのために定理証明を使う検証可能なデータシステムに関する研究があります。こうした手法、定理証明のようなものは、あなたがたのアプローチにも応用できるとお考えですか。というのも、あなたがたは主にインスタンスを生成する方向に進んでいらっしゃるように思うので。これは可能でしょうか。

Prabhakar： ええ、実際に、私たちの研究と並行する形で、検証をLeanの証明器によって行うという豊かな研究の流れが存在します。ただし、現状ではLeanは、ある主張をコンパイルして証明するのにまだかなり時間がかかる点を覚えておいていただきたいと思います。これこそが、私たちがさらに先まで進めた理由だと考えています。私たちは、ずさんで潜在的に不正確ではあるものの、非常に高速な検証を許容する姿勢を取ったからこそ、はるかに先まで進むことができたのです。Leanにはまだ道のりがあると思います。こう言い換えてもよいでしょう。もしあらゆる段階で形式検証を要求するのであれば、到達できる深さはおのずと限られてしまう、ということです。お分かりいただけますでしょうか。

質問者： はい、分かりました。ありがとうございます。

司会： それでは時間の都合上、質疑応答はここで締めさせていただきます。Prabhakarさんはコーヒーブレイクの間も会場にいらっしゃると思いますので、残りのご質問がある方は、コーヒーを片手にぜひ直接お声がけください。最後になりますが、改めてこの場に来ていただき、お考えを共有していただいたことに感謝申し上げます。この講演を1年後にもう一度していただいたら、どんな内容になっているのだろうかと考えてしまいます。それほどのスピードで私たちは進歩しているのですから。この先どうなるか、楽しみに見ていきましょう。最後に、基調講演をしていただいたお礼として、簡単な記念品をご用意しています。ジェネラルチェアの方に、記念品をお渡しいただくようお願いしたいと思います。

Prabhakar： ありがとうございます。

司会： それでは改めて、大きな拍手をお願いいたします。