現代のAIにおける"推論"とは何か

35,100 文字

YouTube

作成した動画を友だち、家族、世界中の人たちと共有

www.youtube.com

ニューロシンボリックプログラミングは、ニューラルネットワークと古典的なシンボリックコードを組み合わせてモデルを表現するという人工知能へのアプローチです。Alpha proofの例を挙げられましたが、言語モデルを使ってコードを生成し、そのコードを実行して、フィードバックを得て、それを使って更なる決定を下すエージェントたちも、実際に新しいシンボリックなことをしているんです。なぜなら、Pythonインタープリタというシンボリックなツールを使っているからです。
極めて低レベルな言語、いわばアセンブリ言語のような世界があって、そこで機械に時間をかけてどんな抽象化が有用なのかを見つけ出させるということも考えられます。これには大きな価値があると思います。人間が想像もしなかったようなことを発見できる可能性があるからです。それによって新しい種類の数学、新しい種類の物理学、新しい種類の生物学を可能にし、人間はまだ理解していませんが、このAIは理解しているという高レベルな構成要素を発見することができます。
そして、その構成要素を使って簡潔なプログラムやモデルを構築し、驚くべきことを成し遂げることができます。そこからブートストラップして、全く新しい数学と計算の世界を構築していくわけです。そのような世界を想像することができます。
MLSTは、機械学習ワークロード向けのモデルサービングプラットフォームであるSense MLが提供しています。プラットフォームにログインすると最初に目にするのがSASオプションで、これは本当にシンプルなオプションです。OpenAIと同じように、アクセストークンを入れてリクエストを送信すれば、最新のオープンソースモデルすべてにアクセスできます。しかも、より高速で安価です。サインアップすると10個の無料クレジットがもらえるので、1円も使わずに実験ができます。
先日行ったジェナディCEOとのインタビューもご覧ください。MLSTはTuur AI Labsが提供しています。これはチューリッヒのベンジャミン・クルアが立ち上げた研究所で、最近ARCチャレンジの優勝者であるMins AIを買収しました。彼らの唯一の目的は、できるだけ早くAGIを実現することで、特にARCチャレンジに注目しています。チューリッヒにいる方で毎月のミートアップに参加したい方、MLリサーチャーとしてベンと一緒に働きたい方は、ぜひ連絡してください。tabs.aiまでどうぞ。
MLSTへようこそ。
ありがとうございます。お招きいただき光栄です。
こちらこそありがとうございます。まず、あなたの経歴についてお聞かせいただけますか？
テキサス大学オースティン校のコンピュータサイエンスの教授をしています。今年はロンドンのGoogle DeepMindで客員研究員も務めています。もともとは推論とプログラミング言語のシンボリック手法の研究が専門でしたが、この10年間は機械学習にも深く関わってきました。現在は、シンボリック手法と機械学習の両方に足を踏み入れているといえます。
素晴らしいですね。さて、車で来る途中に推論について興味深い会話をしましたね。
はい、その通りです。推論とは何でしょうか？
私にとって推論とは、ある程度見る人の目にかかっているものです。見れば分かるというような性質のものですね。しかし、AI分野での定義という観点からすると、いくつかの基準を念頭に置くことが重要だと考えています。
推論を構成する要素として、まず数学やプログラミング、計画立案といった、歴史的に深い思考や推論と結びつけられてきたタスクでうまく機能することが挙げられます。システムがこれらのタスクで既存の手法と比べて優れた性能を示すなら、それは推論能力の向上を示していると言えるでしょう。
モデルが推論を行うか行わないかは二値的な問題ではないと考えています。むしろ定量的な尺度であり、時間とともにその尺度での進歩を見ることができます。これは推論の「何を」の部分、つまりモデルが推論を行うために何をするのかという点についてです。
また、「どのように」という問題もあります。この点は「何を」の考慮とは分けて考えることが有用だと思います。なぜなら、推論を行うための方法は多岐にわたるからです。最近、いくつかの手法が注目を集めていますが、他の種類の手法も存在します。
これは興味深い点ですね。人間至上主義者の中には、私たちの推論の方が優れていると主張する人もいます。ジョン・サールはその有名な例で、機械では容易に複製できない複雑な物理的因果関係があると主張しましたが、シミュレーションにおいては、推論しているかのように振る舞わせる方法が無数にあることには同意できますよね。違いは何でしょうか？
そうですね、ここでもまた基準を決める必要があります。非常に難しい数学の問題を解くために膨大な計算リソースを使うシステムがあったとして、それは推論と言えるのでしょうか？あなたの定義によれば、おそらくそうは言えないでしょう。
しかし、難しい数学の問題を解決できるなら、それは推論を行っていると主張することもできます。また、ロバスト性の側面もあります。物理世界で起こったことをシミュレートして、その軌跡を再現し、「同じことだから推論ではないのか」と言うこともできますが、実際の現象は多くの異なる状況で推論を行うことができます。
確かに言語モデルは、特定の種類の推論について訓練されると、その設定内で汎化することができます。しかし、スイスチーズのように穴だらけなのも事実です。
テストセットの汚染という問題がありますよね？
はい、モデルが推論を行うための追加の基準として、このようなロバスト性が必要だと指摘されました。前の点に戻りますが、計算予算も考慮すべき要素かもしれません。巨大なクラスターで5,000時間もの計算を要する数学の問題を解くのは、厳密には推論とは言えないかもしれません。
しかし、私の考えでは、まず定義、つまり基準を決めて、それからシステムがそれらの尺度で進歩しているかどうかを議論する必要があります。人間らしい振る舞いに基づいてモデルが推論を行っているかどうかを判断するのは、私の好みからすると少し曖昧すぎます。
人間化の課題がありますね。存在の証明として人間が行っているということがありますが、AIの観点からすれば、人間のシミュラクラムを作ることは特に良いとは言えないでしょう。ただ、推論の強さにはある種のスペクトラムがあると私は考えています。
言語モデルは非常に膨れ上がった回路を作り出し、異なる状況で同じ回路を再利用していないように見えます。私たちには、非常に簡潔な抽象的なモチーフを反映する驚くべき能力があります。認知心理学者の中には、これらのモチーフには何か根本的なものがあると主張する人もいます。それは宇宙の仕組みかもしれませんし、少なくとも私たちの認知の仕組みです。しかし、それは言語モデルの働き方とは異なるように見えます。
完全に同意します。私たちは長年、このような、より模倣的で構成的なモデルを主張してきました。抽象化は現代の言語モデルには欠けている人間の本質的な能力だと思います。
しかし、これはまた「どのように」という部分に入っていくと思います。達成したい目標、特定のタスクを実行するという定義と、それをどのように達成するかという方法は分けて考えるのが有用だと考えています。
明示的な抽象化メカニズムを持つモジュラーモデルの使用について、これから私の研究や他の人々の研究の例を話し合うと思いますが、異なる訓練目標を持つ言語モデルのクラスが出現し、明示的にモジュール性を扱っていなくても、ロバスト性を達成できる可能性はあると思います。
そのような可能性が全くないとは言えませんが、最近の言語モデルから見てきたものすべてを考えると、ロバスト性に関して何か根本的な課題があるように思えます。私にとって、抽象化とモジュール性のメカニズムは、これらの目標を達成するための良い賭けになるでしょう。
OpenAIのGPT-4は推論を行っているのでしょうか？
私にとっては推論における一つのマイルストーンです。まだまだ改善の余地はありますが、先ほど議論した基準、つまりプログラミングタスクや数学の問題を解く能力において、以前のモデルよりも大幅に優れているように見えます。私にとっては、推論できるモデルに向かっての一歩です。
興味深いですね。では、それが推論を行っている状況、つまりあなたの基準に合っている状況があると言えますね？
はい、そう言えると思います。推論を行っているといえる状況はあります。そして、推論を行わない状況もあります。様々な理由が考えられます。計算的な理由で、例えばNP困難な問題を解こうとして文脈を使い果たしてしまうかもしれません。あるいは、訓練を受けていない領域で推論を試みるかもしれません。
しかし、原理的にはこれらの制限は克服できると思いますか？
GPT-4に他の多くのものを追加することで、これらの制限を克服する大きな一歩を踏み出せると思います。
ここで私が曖昧にしてきたことがいくつかあります。それこそが本当の問題だと思います。GPT-4のような存在に、より良い推論タスクの性能を達成するために、どのような追加要素が必要なのか。私にとっては、より多くのグラウンディングメカニズムを持つことや、より強力なシンボリックツールを使用することなど、明確な候補があります。しかし、これは推測であり、今後数年でこれらの手法が実際に機能するかどうかを見ていくことになるでしょう。
ニューロシンボリックへのシフトを見るのは興味深いですね。コネクショニズム分野の多くの人々、例えばアンドレ・カーパシーは「ソフトウェア2.0」について語り、ヒントンも同様に、言語モデルはすべてを行うことができる、つまり emergent symbolic reasoningを行うことができ、エンドツーエンドで訓練できるという考えを持っています。
今、私たちが目にしているのは、Alpha GeometryやAlpha Proof、そして一般的に、これらのハイブリッドシステムです。また、ジェネラリーも同様です。私は、ロバスト性への道は、特定のことをうまく行うための特定のアーキテクチャを構築することだと考えています。完全に一般的な白紙の状態のものではロバストに機能しないと思いますが、あなたもそのような傾向を感じていますか？
その通りです。私たちの多くは以前からニューロシンボリック手法を提唱してきましたが、最近では、このという用語が不要になってきていると感じています。なぜなら、ニューロシンボリック手法が実際にあらゆる場所に存在しているからです。
Alpha Proofは素晴らしい例ですが、言語モデルを使ってコードを生成し、そのコードを実行し、フィードバックを得て、それを使って更なる決定を行うエージェントたちも、実際にニューロシンボリックなことを行っていると言えます。なぜなら、Pythonインタープリタというシンボリックなツールを使用しているからです。
とはいえ、私にとってより興味深い問題は、単語そのものではなく、これらの組み合わせが具体的にどのような形を取るかです。いくつかの例を見てきました。例えば、Alpha Proofでは、Leanインタープリタやプルーバーからフィードバックを得るニューラルモデル、機械学習モデルがあります。これは非常に堅固なグラウンディングの形を提供しています。
この傾向は他の形でも、より広い設定でも見られると思います。必ずしも極めて領域特化である必要はありません。人間の言語や混沌とした信号から、この種の推論メカニズムへの橋渡しとして純粋なニューラルモデルが機能する世界を想像することができます。
公理なしに推論は存在できるのでしょうか？
素晴らしい質問ですね。これも再び、推論で何を意味するかによります。数学的推論について話す時、その全体の目的は特定の公理から特定の結論へと至ることです。したがって、私たちが理解している数学的推論は、公理なしでは本当に意味をなさないと思います。
物理的推論についてはどうでしょうか？そこではすべて、私たちが特定の場所にいて、特定の物理法則がある状況に依存しています。私にとって、その法則が異なる世界で推論が起こることを想像することはできますが、その場合でも公理は存在します。ただし、異なる公理を持つことになります。
推論システムを組み合わせることはできますか？
もちろんです。実際、私たちは常にそれを行っています。数学的推論システムと、例えば自然科学で人々が使用する実験的・経験的な推論方法を組み合わせています。これは科学的発見を行う際によく見られることです。
将来的には、異なる能力を持つ多くの異なる推論システムを持ち、それらがすべて集まって、部分の総和以上のものになると想像できます。
AlphaZeroについてはどう思いますか？それは推論だと思いますか？そしてなぜですか？
再び、これは間違いなく強力なシステムで、伝統的に推論とされるタスクで非常に重要な進歩を遂げています。私にとって、これは一種の行動主義的な定義です。推論システムのように見え、推論タスクでうまく機能するなら、それは何らかの推論を行っているということです。
つまり、アヒルのように見え、アヒルのように鳴くなら、アヒルのようなものということですね。
ニューロシンボリックプログラミングとは何ですか？
ニューロシンボリックプログラミングは、ニューラルネットワークと古典的なシンボリックコードを組み合わせてモデルを表現する人工知能へのアプローチです。
例えば、シーンの中に特定の種類のオブジェクトが現れるかどうかについて、知覚に関する決定を行うニューラルモジュールがあり、そこからベクトルが出力され、それらのベクトルを処理するシンボリック手法があるようなプログラムを想像できます。
モデルがどのようなものであるべきかについての知識がある場合、多くの場合これは理にかなっています。そうすれば、シンボリックコードを使用してそれらの事前知識の一部を基本的にエンコードすることができます。
また、解釈可能性が問題となる場合にニューロシンボリックモデルを使用することも考えられます。例えば、ある生物学的プロセスを理解しようとしている場合、完璧なブラックボックスの神経予測器を得ることはできますが、科学者が実際にそれを理解して実験を導くのは難しいかもしれません。
しかし、科学者が伝統的に使用する表記法の形で、より機械的にモデル化されたものがあれば、私にとってそれらはすべて単なるプログラムです。物理方程式やダイナミカルシステムの定義など、これらはすべて様々な種類のプログラムです。
そして、簡単にシンボリックに表現できない部分に対して特定の神経部分を持つ、そのようなプログラムとして機械的に表現されたモデルがあれば、それは別の潜在的な応用となるでしょう。
かなり曖昧な用語のように見えますね。例えば、フリッシェは、ニューラルネットワークを使用してプログラムの生成をガイドする離散的なプログラム検索について話しています。あなたの研究では、例えば関数を表現したり、ある種の事後検証プロセスを行ったりするのに使用できます。つまり、物事が正しい軌道に乗っていることを確認するためにです。そして他にも多くの具現化があります。かなり曖昧なものですね。
そうですね。ニューロシンボリックプログラミングという用語を定義した時、非常に正確にしたいと思いました。しかし、先ほど議論したように、「ニューロシンボリック」という言葉は多くの異なる形で使用されており、意味を完全に失ってしまったと言えるほどです。
しかし、ニューロシンボリックプログラミングについて話す時、非常に具体的なことを意味します。つまり、これらのハイブリッドモデルを表現できるプログラミング言語を持ち、シンボリックコードとニューラルネットワークの組み合わせを持ち、そしてそれらのプログラムを発見するために使用される手法の集合を持っています。これらの手法は部分的にニューラル、部分的にシンボリックかもしれません。典型的には、それらは両方の混合です。
番組の多くのファンは、ケビン・エリスとタノン・B他による「DreamCoder」論文をご存知でしょう。記憶が正しければ、ドメイン固有言語があり、覚醒フェーズと、このニューログ指導の検索があり、抽象化のための睡眠があり、などがありましたよね。その考えに関連していますか？
その通りです。この分野で過去数年間に登場した手法にはいくつかのカテゴリーがあります。大きな課題の一つは、固定されたプログラミング言語で作業してその言語でプログラムを見つけようとするだけでなく、実際に明示的な抽象化を行い、新しいプリミティブを発見しようとするライブラリ学習です。これらのプリミティブはその後プログラミング言語に追加されます。
DreamCoderはこのカテゴリーに分類されます。DreamCoderでは、非常に低レベルな言語であるラムダ計算から始め、徐々により大きな、より大きなモジュールを発見していきます。これらは実際には抽象化です。これらの非常に低レベルなプログラムにパターンを見出し、それらをモジュールに抽象化し、そして再利用するのです。
彼らが持っていたプログラミング言語は純粋にシンボリックでしたが、簡単に一般化することができ、実際に最近ではそのような作業が行われています。そして、これらのニューラルネットワークとラムダ計算の項の混合であるプログラムを想像することができます。
そして、これらのライブラリ関数を発見し、またプログラム合成の検索を行うために使用した方法は、すべてニューラルでした。現代的なものにすることを想像できます。発表されてからそれほど時間は経っていませんが、大規模言語モデルを使用してプログラムとその抽象化を提供するように、2024年のディープラーニングに適応させることができます。
興味深いですね。つまり、DreamCoderは言語モデルを使用していなかったし、ハードコードされたDSLを持っていました。私が興味を持つのはプリミティブの性質です。例えば、チューリングマシンの空間を検索したり、ラムダ計算を使用したり、ジョシュ・テンベはスが認知心理学の大ファンで、私たちには認知の根本的な生来の事前知識があるので、それらの事前知識を検索すべきだと考えています。
おそらく特定のタスクを行うように訓練されており、つまりARCチャレンジのために訓練することができます。そうすると、それは基本的に「DSLの中で私が種を蒔いた事前知識のどのような組み合わせが、この特定のことに対して機能するスキルプログラムを生成するのか」と言っているようなものです。つまり、どこから始めるのかという質問と、訓練しているタスクがどの程度ライブラリの学習に影響を与えるのかという疑問があります。
私にとって、事前知識の問題は開かれています。人間には認知的な事前知識の集合があるかもしれませんが、それらが何であるかは必ずしも知らないかもしれません。しかし、事前知識の存在が、プログラム合成問題やライブラリ学習問題を解く能力を大幅に向上させることは確かです。
それは、プログラミング言語に合理的な一連のプリミティブがすでに存在する場合、すべてをゼロから発見する必要がないということを意味します。しかし、極めて低レベルな言語から始め、事前知識のような種類のものを全く持たず、合成や他の基本的な操作だけを持ち、そこからプログラミング、数学、物理学の全宇宙を発見していく世界を想像することもできます。
生成されたプログラムが理解できなくても問題ないのでしょうか？これは、この議論のテーマとなるでしょう。なぜなら、もちろんあなたは定理証明にも取り組んでいるからです。数学者たち自身がもはやこれらのことを行わず、この巨大な空間を検索するためにコンピュータに頼っているという話について。
しかし、この離散的なプログラム検索に関して、多くの抽象化と多くの興味深い効率性を含むプログラムを作成しているかもしれませんが、それらは非常に解読が困難に見えます。
その通りです。解釈可能性の問題と能力の問題は区別すべきだと思います。解釈可能性には確かに潜在的な価値があります。特に科学的発見のような応用領域では、解釈可能性を本当に重視します。また、安全性とセキュリティの観点もあり、後ほど議論しますが、本当に堅牢で能力のあるモデルを構築するために何が必要かという問題とは分けて考えるのが有用だと思います。
極めて低レベルな言語、一種のアセンブリ言語を持ち、私はラムダ計算をそのようなものと考えていますが、そこから時間をかけてどのような種類の抽象化が有用なのかを機械に発見させる世界があると思います。これには大きな価値があると考えています。なぜなら、人間が想像もしなかったようなことを発見できる可能性があるからです。
それによって、新しい種類の数学、新しい種類の物理学、新しい種類の生物学を可能にする可能性があります。そのような可能性を全く排除しません。この抽象化のアイデアは、その体制でも価値があると思います。なぜなら、それは高レベルな構成要素を発見することを意味するからです。確かに、人間はまだ理解していませんが、このAIは理解しているのです。
しかし、その構成要素を使って簡潔なプログラムやモデルを構築し、素晴らしいことを成し遂げ、そこからブートストラップして、全く新しい数学と計算の世界を構築していくのです。そのような世界を想像することができます。
この分野でのあなたの研究について教えてください。LLMを使用し、型指向の検索や学習から検索を行うこのアーキテクチャを作成されましたが、それについて教えていただけますか？
この分野でいくつかの取り組みを行ってきました。以前は、プログラム合成のためのシンボリック手法に多くの取り組みを行っていました。その設定では、プログラミング言語があり、当時は論理的な制約や一連の例によって定義されていたプログラミングタスクがあり、そしてタスク仕様に合うプログラムを見つけるという検索問題を定義していました。
これらのシンボリック手法にはスケーラビリティの課題がありましたが、ディープラーニングが登場した時、私たちは皆その方向に移行し、このニューラルガイド付きのプログラム検索が非常に強力なアプローチとなりました。
そこでの手法の一部は、これらの古いシンボリックなアイデアとディープラーニングのアイデアを組み合わせました。例えば、型指向のニューラルプログラム合成に関する結果がありました。強く型付けされた言語でプログラムを生成し、その言語の型システムが剪定メカニズムとガイダンスメカニズムとして機能します。
明らかに合理的ではないプログラムを排除し、また特定の種類のサブゴールに焦点を当てるのを助けます。定理証明の世界で起きていることを考えると、実は非常に密接に関連しています。
Leanは実際には非常に強力な型システムを持つ関数型プログラミング言語です。そして、例えば数学的証明の検索でのある種のステップを排除するために定理証明器からフィードバックを使用する時、このアイデアのバージョンを実際に使用しているのです。
しかし、私たちはしばらくの間このことを考えていました。そして、プログラミング言語の世界から生まれたより広いプログラム合成コミュニティも、この問題について考えていました。
これはまだ、固定されたプログラミング言語があり、その言語でプログラムを探しているという文脈の中でのことです。
しかし、ここで関連する他のアプローチもあります。例えば、ニューラル緩和を使用した結果があります。アミッシュ・シャが主導し、私の長年の共同研究者であるイソン・ユー、そしてジェニファー・ソンと私の元学生のD・ベルマとの論文があります。
これはプログラムのニューラル緩和を使用してプログラムの検索のためのヒューリスティックとして使用するというものでした。アイデアはこうです：プログラムの検索を行っていて、これらの不完全なプログラムを徐々に埋めていくとします。何もない状態、つまり大きな穴のあるコードから始めて、徐々により多くのコードを追加していきます。
ここでの一つの課題は、常に不完全なプログラムを扱っているため、特定の決定が価値があるかどうかをどのように知るかということでした。つまり、特定の不完全なプログラムをプールに保持すべきか、それとも捨てるべきかということです。
そこでのアイデアは、その穴に、そのプログラムを完成させる可能性のある方法の空間があるということです。その穴に入れることができる多くのシンボリックな離散的な項がありますが、その代わりにニューラルネットワークを入れ、そこにある種の部分集合関係があります。
これらのニューラルネットワークは、プログラミング言語内の任意のシンボリックプログラムよりも表現力が高いため、ニューラルネットを十分によく訓練すれば、任意のシンボリックプログラムで得られるよりも良い損失が得られるという性質があります。
これにより、その穴にこのニューラルネットワークを差し込んだ後に得られる損失を、その時点から先でシンボリックプログラムを使用して達成できる最善の結果の下限として使用できるという議論につながります。
これは次に、A*やBranch and Boundなど、古典的な検索アルゴリズムのヒューリスティック検索を導くために使用することができます。GOIの時代からこれらのアルゴリズムの全体があり、今ではこれらの種類のアルゴリズムをこれらのニューラル緩和で加速することを想像しているのです。
このようなアイデアはすでにありました。一般的に、ニューラルネットワークを離散的なプログラムの緩和、つまり連続的な近似として使用できるか、そしてそのような緩和をどのように使用できるかという問題を多く検討してきました。
他のより最近の取り組みでは、LLMを使用したシンボリック回帰の文脈でのライブラリ学習に関する最近の論文があります。ここでも同様の多くのことを行っています。プログラムの検索、抽象化の実行などですが、今回はLLMを使用しています。
特に、LLMは伝統的な検索の指針として非常に優れた方法となり得ます。例え遺伝的アルゴリズムや型指向の列挙のような伝統的なプログラム検索を行っているとしても、そのような検索を導くニューラルネットワークとしてLLMを使用することを想像できます。
さらに、先ほど話したような種類の抽象化のためのツールとしてLLMを使用することも想像できます。例えば、DreamCoderでは、抽象化は次のように行われます：うまく機能したプログラムのセットを見て、それらのプログラムで繰り返し現れる構文的な部分構造を見つけます。
そして、「これは潜在的に再利用できるモジュールだ」と言うわけです。それがライブラリの一部になります。問題は、プログラムの大きなプール内でこのような共通の部分構造を特定することは非常に難しい場合があるということです。
この目的のために使用された記号的な方法がありましたが、それを行わずに、代わりにLLMを使用することができます。それはどのようなものでしょうか？
アリア・ジーワイとオーレルが主導し、マイルズ・CRI・クランマーとオマール・セラスとともに、今年のニューリップスに発表される論文を読むべきです。基本的なアイデアは、LLMを抽象化装置として使用するというものです。
LLMに「これらのプログラムに現れる共通のパターンは何か」と尋ね、その自然言語での推論能力（これは議論の余地のある用語ですが）、少なくともプログラムの構文にパターンを見つけ、それを自然言語で説明する能力を使用して抽象化を行うのです。そしてそれを使って概念を学習します。
マイルズ・クランマーの大ファンです。彼は数年前にシンボリック回帰に関する画期的な論文を書きましたね。それも別の形のニューロシンボリックプログラミングですか？また、言語モデルのシンボリック分解について話す人もいます。この粘土の塊から始めて、確率的勾配降下を行い、そこから何らかのシンボリック構造を取り出すというアイデアです。魅力的なアイデアですね。
その通りです。まず最初の質問に答えると、シンボリック回帰はプログラム合成の一形態だと考えています。実際に行っていることは、データセットが与えられ、その中からデータセットによく合う式を見つけようとしているのです。式は単なる特別な種類のプログラムです。
したがって、私たちが話してきた手法の一部、例えばこのニューラル許容ヒューリスティクスは、シンボリック回帰の設定で行われました。データセットによく合うプログラムを見つけようとしているのです。
しかし今では、遺伝的プログラミングのアプローチや、まずニューラルネットワークを訓練してからそれをシンボリックプログラムに蒸留するというアプローチを超えて、これらの種類の戦略を超えて進むことができると想像できます。
このシンボリック回帰問題を解決するために、LLMを本当に大いに使用することができます。それはどのように使用できるのでしょうか？一つの観点は、LLMを使用してプログラムの検索を基本的に行う、またはプログラムの検索を導くことができるということです。
特に、進化的検索について話していると仮定しましょう。LLMを使用してプールにあるプログラムの交叉や突然変異を行うことを想像できます。また、LLMを使用して抽象化を行うこともできます。
つまり、LLMに高性能なプログラム内に現れているいくつかの概念を提案するように依頼し、それらの概念がその時点でのプログラムの検索を条件付けるようになるのです。
最近、サバール・カムティと話をしました。彼には「LLM modulo」というアーキテクチャがあります。彼は「LLMは非常にクリエイティブなので、この空間を探索し、最後に検証器を付けることができる。つまり、実際に正しい結果を得た時にそれを選び出すことができる」と言いました。
しかし、私は彼と少し意見が合わなかったのです。なぜなら、確かにLLMにクリエイティブなことを見つけさせ、例えばLLMガイド付き検索を行い、LLMに抽象化をさせる時、それらは依然として訓練データに寄生的であり、それは創造性のギャップがあることを意味するからです。
私たちはもっと豊かな創造性の源にアクセスできるように思えます。そして、このライブラリを構築していく中で、ある時点でライブラリの重みが創造的能力に影響を与えるのではないかという問題があります。
素晴らしい質問です。シンボリック回帰のような設定では、最終的にデータによるグラウンディングという利点があります。実際に行っていることは、いくつかの経験的な観察を行い、それらの観察に合う式を見つけようとしているのです。
したがって、LLMによってクリエイティブに構築された新しい候補があった時、実際にそれをデータセットで評価し、どれだけうまく機能するかを確認することができます。これにより、完全に軌道を外れることを防ぐことができます。
事前知識の質問に関して、はい、その通りです。LLMは以前見た事前知識に基づいています。LLMを純粋にブラックボックスのゼロショット方式で使用している場合、LLMが以前見たものによってのみ制約されることになります。
しかし、この事前知識にはまだ価値があると付け加えたいと思います。なぜなら、新しい科学を行う時、通常は他の人々が以前に行った科学に基づいて構築しているからです。LLMは、様々な種類の科学論文や数学の問題などの形でそれを見ているはずです。
しかし、このゼロショットブラックボックスモデルに縛られる必要はありません。LLMを使用してクリエイティブに候補を生成し、これらの候補を経験的に評価し、その経験を使用してモデルをさらに微調整するループを想像することができます。
完全に白紙の状態のLLM、おそらく言語に関する基本的な知識はあるが、科学的知識はほとんどないLLMから始めて、すべての種類の科学的タスクで徐々に構築し、様々な種類の仮説がどのように機能したかを見て、実世界からのフィードバックを得ることも想像できます。
おそらく新しい実験を行うことさえできるかもしれません。因果関係について推論し、試すべき新しい実験を決定し、それらの実験の結果の形でフィードバックを得て、それを使ってさらに微調整を行うことができます。
単にLLMをブラックボックスとして使用し、最後に検証器を付けるよりもずっと多くのことが可能です。
その通りですね。創造性についてはいつも議論があります。デミス・ハサビスは創造性のラダーについて話し、発明的なものが最高レベルだと言っています。もちろん、ユニコーンを想像したり、実世界では見たことのないものを想像したりすることはできます。なぜなら、それらは私たちが理解しているものの凸包の中にあるプリミティブで構成されているからです。
しかし、プログラム生成の文脈では、言語モデルには非常に多くの自由度があります。自然言語や作られた言語、プログラミング言語など、様々なものを理解します。そしてコードを生成したり、DSLを使用したりすることができます。
それでも、これらのプログラムを実行すると、停止しないかもしれないし、有効でないかもしれません。つまり、これらが良いプログラムであることを確認するためには、もう一段階必要なように見えます。
その通りです。ちなみに、プログラムが数回のテストで正しく実行されたかどうか以外にも、プログラムのより深刻な種類の分析を行うことができます。しかし、最終的には、はい、それらの外部ツールから追加のフィードバックを得ています。そして問題は、それをどうするかということです。
そのフィードバックを使って、このプログラムを保持するかどうかを決めることもできますが、さらに多くのことができます。LLMに戻ってこの情報を使用し、基本的にそれをさらに訓練し、プログラムの書き方を導くことができるかもしれません。
人間のプログラマーを考えると、そのように起こります。コードを書き、様々なことを試し、特定の種類のプログラムが機能し、特定のものが機能しないことを確認します。コンパイラ、型チェッカー、インタープリタからフィードバックを得ます。そして、それを使ってコーディングの方法も改良していきます。
停止問題についても同様です。私の頭の中では、これは2次のアルゴリズムで、1000個のデータポイントがあり、90秒後でもまだ実行中なら、おそらく何か問題があるということです。Control Cを押して戻り、バグを修正します。
プログラムの停止を証明することについては大きな研究の蓄積があります。原理的には決定不能な問題であっても、実際にはプログラムの終了を証明する文献があります。その仕組みは、プログラムの終了を証明することは実際には帰納的な議論を展開することだということを認識しています。
つまり、プログラムの1ステップを実行するたびに、その値が厳密に減少するような式があることを示すのです。ループを考えてみましょう。「iがnより小さい間、何かを実行し、iをインクリメントする」というループを書いたとします。
このプログラムが終了することは、アラン・チューリングにもかかわらず分かります。理由は非常にシンプルで、ループの各ステップでこのiをインクリメントしており、それはある程度までしか上がることができないからです。つまり、n-iという値があり、これは毎ステップで厳密に減少し、プログラムの構造上、ゼロまたは設定した下限以下には下がれないのです。
ここで行っているこの種の推論は、帰納的証明の例です。ただし、プログラムに適用されているだけです。この種の帰納的証明を自動的に発見することについては多くの研究があります。これらは実際には非常にシンプルなシンボリック式です。
LLMや他の種類の機械学習技術を使用して、この種の議論を探索することを想像できます。
それについて2点あります。おそらくチューリングの有名な証明について触れるべきですね。彼は停止問題について背理法で証明しましたよね？また、もし私の理解が正しければ、帰納法による証明でプログラムが停止することを示せる特定のケースを指摘されていますが、そのような証明ができないプログラムの空間も存在することを認めますか？
それらの帰納的証明を自動的に発見することについては何も言及していません。私の指摘は、人々が書くほとんどのループや再帰において、これらのプログラムが終了する理由の議論は非常にシンプルであり、様々な種類の手法を使用してそのような証明を探索できるということです。
基本的な列挙でもかなりうまく機能しますが、この問題を解決するためにより現代的な機械学習技術を使用することも想像できます。しかし、自動化され、必ず終了し、すべてのプログラムで機能する方法を持つことは不可能です。
問題は、現実的なプログラム、つまり人々が書くプログラムに対してこれが機能するかどうかです。現実的なプログラムに対しては、終了を証明するためにこれらの戦略のいくつかを試すことができ、それが機能しない場合は、「ここに問題がある、修正してください」と言うだけです。
そのプログラムがまだ機能する理由があるかもしれませんが、そのプログラムを無視して問題を解決する別の方法を見つければよいのです。
私の共同ホストのDr. Dgarは、チューリングマシンに非常に興味を持っています。彼は、言語モデルについて、LLMシステムについて話しているのではなく、単なる言語モデルについて話していると言います。彼は、それらは有限状態オートマトンであり、チューリングマシンはまだコントローラーとしてプッシュダウンオートマトンのような有限状態オートマトンを持っていると言います。
そして彼は、確率的勾配降下では発見できないFSAクラスのアルゴリズムの空間があり、これは停止問題のためだと言います。彼は、この停止問題のために、そのようなアルゴリズムを見つけることはできないと言っています。私は、あなたが以前この分野で行われた興味深い研究を指摘されていたと思います。彼はそれに魅了されると思いますが。
はい、プログラム合成にグラジエント降下を使用することについては多くの研究がありました。私にとって、チューリングマシンを探索することは単なるプログラム合成の一形態です。ただプログラミング言語が非常に低レベルで、すべてのプログラムがこの1つのカウンター、つまりテープと、有限状態マシンであるコントローラーにアクセスできるだけです。
私にとって、これは非常にシンプルな種類のプログラミング言語です。計算理論の数学的証明において有用だったのは、それが非常にシンプルだったからです。しかし、プログラミングの観点からは、チューリングマシンに特別なものはないと思います。チューリングマシンについて行える推論は、他のより広いプログラムのクラスについても同じような議論ができます。
あなたが言及している理由で、プログラムを見つけるためのグラジエント降下を行うこれまでの多くの研究は、あまり成功していません。そのため、人々は歴史的に、ある種の離散的な検索を行い、その検索プロセスを様々な方法で導くためにニューラルネットワークを使用したいと考えてきました。
DreamCoderでのニューラルネットワークの使用はその一例ですが、プログラムを書いたり検索を導いたりするためのLLMの使用も、これらの例です。
興味深いですね。チューリングマシンには、メモリを拡張するという素晴らしい能力があります。最初からやり直して訓練する必要はなく、「もっとデータが必要だ、もっとデータが必要だ」と言って、メモリに追加すればいいのです。
人々は、言語モデルを取り、RAGを行うように訓練できると言います。おそらく訓練プロセス中にデータベースから情報を取得したり、コード実行を行うように訓練したりできます。そして、「基本的にチューリング空間を探索しているのではないか？」と言えます。
πのn番目の桁を計算するプログラムを生成することができ、これは任意の実行時間を持つ何かですが、それをツール上で実行し、結果を戻すことができます。しかし、私には種類の違いがあるように感じます。でも、その違いは何でしょうか？そうすることと、ネイティブにチューリング空間を探索できる機械を持つことの違いは何でしょうか？
では、理解しようとしています。チューリングマシンプログラムの定義をDSLとして持つことを想像できます。各プログラムがチューリングマシンであるプログラミング言語を定義できます。私にとって、これは計算理論の教科書を開いて、チューリングマシンの定義に行けば見つかるものです。これは単なるプログラミング言語です。構文があり、意味論があります。
では、この言語でプログラムを生成するためにLLMを訓練することと、LLMがすでに行っている他の種類のプログラム合成との間に、根本的な違いはあるでしょうか？Pythonコードの生成とチューリングマシンの生成の間に、私は根本的な違いはないと思います。
しかし、あなたが描写しているのは少し異なることだと思います。この生成に使用されているプロセス、つまりそのプロセスは有限状態プロセスなのか、それともチューリングマシンのようなものなのか、という点です。これは非常に興味深い質問だと思います。
本当に言っているのは、特定の方法で訓練された次のトークンを予測するだけの言語モデル、そして有限量の情報を取得できる大規模にスケールアップされたオートリグレッシブモデルの代わりに、あらゆる種類の生成を行う大規模にスケールアップされたチューリングマシンを持つことができるということです。それは非常に興味深いアイデアだと思います。
はい、その通りです。私が理解するのに時間がかかったのは、チューリングマシンのコントローラーは有限状態オートマトンだということです。つまり、言語モデルの重みの集合が存在し、プッシュダウンオートマトンのようなものでメモリを拡張することができます。ただし、確率的勾配降下ではそれを見つけることができません。
もう一つは、インターネットスケールのチューリングマシンとその説明のデータセットを持つことを原理的に想像できるということに完全に同意します。説明が重要だと思うのは、私たちが何らかの方法で指示できる形でないと、チューリングマシンの言語モデルを持つ意味がないからです。
しかし、ここでも生成されるものと、それをどのように生成するかという区別をしたいと思います。二つの可能性があります。一つは、チューリングマシン言語モデルであれ、RNNの言語モデルであれ、Transformerの言語モデルであれ、何らかの言語モデルを使用して、このチューリングマシン言語でプログラムを生成するというバージョン1です。
バージョン2は、この言語モデル自体がチューリングマシンであり、この無制限のメモリにアクセスし、この無限のテープから情報を探すことができるという、あなたが指摘した特定のポイントです。これは非常に興味深い提案です。
私の唯一の躊躇は、アーキテクチャはそれほど重要ではないことが分かってきているということです。本当に重要なのはスケールです。State Space ModelsやRNNを大規模にスケールアップすることに関する新しい結果がたくさんあり、Transformerが特に能力を発揮するように見えた多くのタスクが、非常にスケールアップされたRNNでも実行できることが分かってきています。
したがって、このチューリングマシンアーキテクチャが素晴らしい新しい能力につながる可能性はありますが、おそらくもっと多くの証拠を見てから判断したいと思います。とはいえ、それは間違いなく探求する価値のある非常に興味深いアイデアです。
はい、実用的な目的では、モデルをスケールアップできるので関係ないという反論は常にありますね。私も、Min LSTM、State Space Models、Mamba、これらすべてにとても興味を持っています。なぜなら、これらは私たちのモデルサイズを10倍にすることを可能にするかもしれないからです。
そして、モデルが私たちが行いたい合理的なすべての種類の計算を行うのに十分な大きさになるという質問は常にあります。しかし、その反論は、時には問題について長時間考えることがあるということです。
Keithは常にLinuxオペレーティングシステムを例として挙げます。現在の技術的な複雑さと成熟度のレベルに到達するために、本当に複雑な人工物を設計する必要があったということです。そして、それらを100倍にしても、これらのモデルの手の届かないところにあるように見えます。
その通りです。はい、私は単なるオートリグレッシブ言語モデルのパラダイムを超えるアルゴリズムを持つことを強く信じています。だからこそ、人間が提供した機密データの分析、コンピュータセキュリティやコンピュータセキュリティに関連するトピックについての一般的な質問への回答、議論の的となるトピックや研究分野に関する事実情報の提供、歴史的な残虐行為の説明、教育目的でのスキャマーやハッカーが使用する戦術の説明、軽度の暴力や趣味のロマンスなどの成熟したテーマを含む創作的な執筆、武器、薬物、性、テロリズム、虐待、冒涜など、教育的文脈で利用可能な情報の提供、脱税などの合法だが倫理的に複雑な活動についての議論などを話してきたのです。
しかし、私にとって、これらの方法の力は言語モデルの内部アーキテクチャからではなく、これらの異なる種類のグラウンディングメカニズムがニューラルネットワークと協力する方法のより高レベルなアーキテクチャから来ると思います。
LLMsの異なるニューラル実装が劇的に良い結果をもたらす可能性はあります。それについては少し懐疑的かもしれませんが、もっと証拠を見たいところです。しかし、私にとって非常に明確なのは、これらの種類のより高レベルなアーキテクチャを持ち、あらゆる種類のニューラルネットワークをこれらの種類のシンボリックグラウンディングメカニズム、実世界での実行、人間からのフィードバックなど、これらすべてと組み合わせることで、今日私たちが持っているものよりも良いものが得られるということです。
そして私にとっての課題は、これらの様々な種類のグラウンディングメカニズムからのフィードバックをニューラルネットワークにどのように戻すかということです。そしておそらく、そうする際に特定の種類のニューラルアーキテクチャの方がずっと良いかもしれませんが、それについてはまだ判断を保留しています。
あなたの言うことに本当に同意します。一つ気づいたことは、現在、確実に実世界のアプリケーションを構築する方法は、アーキテクチャとプロセスを使用することです。これらの複雑さを克服する唯一の方法です。おそらく、それが唯一のトレードオフです。
しかし、問題に対してより多くのエンジニアリングとアーキテクチャを投入すればするほど、その問題に対してロバスト化されますが、同時に他の問題に対する一般性を奪っているようにも見えます。そのため、理想的には非常にシンプルな、かなりシンプルでドメイン一般的なアーキテクチャを見たいのですが。
そのため、数学を例に取ってみましょう。私にとって、数学は多くの異なる種類の問題を解決するための非常に有用なモデルです。例えば、物理学、生物学、プログラミングを行う場合、数学は有用です。日常的な論理的推論にも数学は有用です。
したがって、世界のモデルの数学的健全性について厳密なフィードバックを与えることができるツールの使用は、私にとって非常に理にかなっています。そのため、おそらくそれを、方法を適用できる領域の種類に対する制限とは考えないでしょう。
同様に、コード実行について、私にとってコードは世界のモデルを表現する非常に一般的な方法です。プログラムには常に意味論が伴います。プログラムを実行し、分析し、最悪のケースの動作について推論することができることは、私にとって大きな制限を課すものとは思えません。
私にとってのアイデアは、かなり一般的なこれらの種類のグラウンディングメカニズムを持ち、それらを柔軟に組み合わせる方法を持つことです。多くのことをハードコードしないでしょう。特定のアプリケーションにこれらの方法をデプロイする際にハードコードするかもしれませんが、フレームワークは完全に一般的であるべきです。
Leanの証明、コード実行、ニューラル予測、そしておそらく自然言語処理やビジョンも、なぜなしに、これらすべての異なる種類のモジュールの新しい種類の複雑な組み合わせを記述できます。これらすべての異なるモジュールを新しい種類のモデルに組み合わせることを可能にし、そして適切な組み合わせを見つけるためにAIシステムに任せることができます。
LASeRアーキテクチャについて教えていただけますか？
LASeRアプローチの目標は、プログラムの検索を導くためにLLMを使用し、高性能なプログラムで何が起こっているかを説明する抽象化を生み出すことです。これは、データセットとプログラムまたは式の言語があり、高性能な式を見つけようとするシンボリック回帰の文脈で行われました。
以前のアプローチでは進化的検索を使用し、その検索プロセスの一部を指示するためにLLMを使用する研究もありましたが、私たちが本当に探求したかったのは、LLMを使用して高性能なプログラムに現れる高レベルの説明や高レベルの概念を生み出すことができるかということでした。
進化的検索がある候補のプールを生み出し、これらの候補を持っているデータを使用して実際に評価するプロセスを想像できます。これがグラウンディングメカニズムとして機能します。今、高性能な候補がいくつか残っています。
そこでLLMを使用して、これらの高性能なプログラムに現れる共通のテーマを説明し、それらのテーマ、それらの概念を記憶し、それらを使用して検索も導きます。
このようなアプローチの大きな魅力の一つは、LLMが持つ科学的な事前知識をすべて使用していなくても、テキストの断片をより高レベルの概念に抽象化するLLMの能力は、依然として非常に役立つということです。
私たちはこのアプローチを、標準的な方程式の再発見、具体的にはファインマン講義のすべての方程式の再発見という問題に適用しました。これはMax Tegmarkらによって提案されたAI Feymanの論文でのタスクです。さらに、いくつかの合成ベンチマークでシステムを評価し、また実際にLLMスケーリング則の新しい発見にも使用しました。
教えてください。
はい、もちろんです。ここでは、チンチラ則を超えて、LLMのデータだけを使用して新しい法則を見つけ出そうとしました。例えば、パラメータ数、データセットのサイズ、訓練に使用されたショット数などの情報があり、またデータセットの特性もあり、そして性能があります。
そこで、LLMの振る舞いを説明するシンボリック則を発見できるかという質問をすることができました。私たちが発見したのは、チンチラ則とは少し異なる法則でした。これは、何か異なるものでありながら、同様に説明力のあるものを見つけたいという私たちの目的でした。詳細については論文をご覧ください。
それに加えて、完全に合成的なタスクでもシステムを評価しました。そこでも、この概念学習のアイデアが違いを生み出すことが分かりました。問題領域に対するLLMの事前の理解を無視したとしても（これは実世界のアプリケーションでは、既存の知識の上に構築しているのだから、無視すべきではないと主張しますが）、LLMを使用する別の方法として、抽象化のためのツールとして使用することができます。
メラニー・ミッチェルの研究にも触発されています。彼女はこの分野で研究を行っていますが、繰り返し抽象化を行うことについて本当に興味深い点があるように思えます。
その通りです。固定された外部ループがあり、上へ上へと進んでいくように見えます。それについて教えてください。
それは理にかなっています。現在LASeRで行っているのは、もう少し洗練されていません。私たちの抽象化は単に自然言語で記述されていますが、時間が経つにつれて抽象化がより高レベルになるように意図的に設計された、より象徴的でプログラム的な形で表現された抽象化を持つ世界を想像することができます。
これは私たちが行っていないことですが、DreamCoderには存在していると言えます。なぜなら、DreamCoderではライブラリモジュールを発見すると、それらのライブラリモジュールを使用して新しいプログラムを書くことができ、さらにそれらを抽象化することができるからです。
したがって、この抽象化プロセスは自然に、より高レベルのモジュールを発見する方向に向かっています。
これは、私にとって本当にワクワクすることだと一言コメントしていただけますか。現在、例えばDreamCoderはARCチャレンジでSOTAではありませんが、これが正しい方向だということを骨の髄まで感じています。残念ながら、SOTA追求と、そういったことのために、この本当に革新的な研究に十分な注目が集まっていないように思えます。これについて、あなたはどうお考えですか？
SOTAの追求は本当に不幸な傾向だと思います。また、これはリソースの誤った配分でもあります。SOTAを追求することに適している企業はあります。探索と活用の両方が必要で、SOTAの追求は活用になるでしょう。十分に定義されたアプローチがあり、それをスケールアップし、以前にはできなかった新しい問題を解決しているのは素晴らしいことです。
しかし、この探索の方向性も非常に重要です。残念ながら、SOTAの追求がそれを少し妨げているのですが、同時に、新しい興味深いアルゴリズムを生み出している人々も多くいます。
おそらく必要なのは、探索から活用へのより良いアークです。つまり、例えばDreamCoderのようなこのアルゴリズムがあったとして、それをどのようにスケールアップするのか。私たちのLASeR手法は、LLMを使用することでそれを少しスケールアップする一つの方法です。しかし、他のアプローチもあるかもしれません。
また、これを非常に大量の計算で実行し、何が起こるかを見ることにつなげる方法という問題もあります。これは私たちがまだ行っていないことですが、確実に興味を持っている方向性です。様々なパートナーと話をして、これを大規模にスケールアップする方法がないか探っています。そして、それを行った時に何が起こるかを知ることにとても興味があります。
あなたは数学的発見について広範な研究をされていますが、論文の一つで、2026年までにAIの共同研究者が得られるかもしれないとコメントされていましたね。なぜそうお考えですか？
実際にそれは、私が大いに尊敬するTarrinTaが指摘したことでした。申し訳ありません。私も実際にその意見に同意します。私たちはAIにとって非常にエキサイティングな時期にいると思います。
数学論文や、重要な数学的要素を含むコンピュータサイエンスの論文において、唯一の著者ではありませんが、重要な貢献者としてのAIが、そう遠くない将来に可能になるはずだと想像できます。
では、それは具体的に何を意味するのでしょうか。数学が行われる方法、そして実際に理論的コンピュータサイエンスで起こることを考えると、かなり厳密な定義があります。そして証明もありますが、究極的にその目的は人間の査読者と読者を納得させることです。
つまり、ミスを犯す可能性があり、考慮していなかったコーナーケースがあり、その結果として証明が破綻する可能性があります。これは今日の数学の方法における一つのリスクです。
もう一つは単なるスケーリングです。数学の方法に根本的に問題があるとは考えなくても、これまでは不可能だった計算ツールを使用して数学をスケールアップする機会があります。
それが意味するのは、非常に大規模なソフトウェアシステム、例えばLinuxカーネルやGoogleのクラウドインフラストラクチャを考えると、これらは個々の人間が必ずしも完全に理解できないほど極めて複雑なシステムです。人々はこれらのシステムを高レベルな抽象化で理解し、特定のコンポーネントの低レベルな詳細をすべて知っているかもしれませんが、システム全体の詳細な見方を持っている人は本当にいない、少なくとも非常に少ないと言えます。
数学の証明を考えると、歴史的に数学は個々の貢献者を重視してきました。数学者について考える時、証明を生み出し、その証明のすべての詳細を知っている、または少なくともそれらの詳細を理解している人を想像します。
しかし、おそらく個々の人間がすべての詳細を理解できないような、極めて複雑な数学的定理を持つ世界を想像してください。しかし、全体的な証明は人間が管理できる部分に分解できるという保証はまだあります。コードを書くのと同じように、数学でもそれができるのでしょうか？それはどのようなものでしょうか？
これは、Leanのようなシステムが提供する素晴らしい機会だと思います。そして、AIコパイロットがコードを書くことをずっと容易にしたのと同じように、数学の証明を書くAIコパイロットを想像することができます。
これらすべてが可能であるとすれば、新しい種類の数学、人間とAIの新しい協力のモダリティ（これはTaが広く話してきたことです）があり、このプロセスを推進するAIが私たちを10倍生産的にします。AIを共同著者として持つ新しい論文につながると思いますか？私は「はい」と言うでしょう。
必ずしもAIを共同著者としてリストアップする必要はないかもしれません。なぜなら、計算機や電卓を共同著者としてリストアップしないのと同じように、このツールがあってそれが多くのことを行ったということを受け入れるだけでしょう。しかし、より高いレベルでは依然として人間の創造性があり、それらが共同著者となるでしょう。しかし、AIは確実に、今日では数学の大学院生がしなければならないような多くのことを行うでしょう。
興味深いですね。多くの人々は数学的定理を、個々の数学者や少数の数学者が考え出し理解した、かなり簡潔な単位として考えています。最近まで、これが大規模にスケールするとどうなるかについて考えてこなかったと思います。
そして、はい、査読者を納得させる必要があり、あなたは査読者が、それが非常に大規模で解読が難しくなっているにもかかわらず、コンピュータによって発見された場合、より信頼を置く傾向があると言っています。
私は、査読者が証明のすべての詳細を理解する必要があるのかさえ疑問に思います。おそらく査読者は証明の高レベルなコンポーネントを理解し、証明の低いレベルの部分が正しく行われているという保証を持つだけでよいのではないでしょうか。
コードを読む時、「このコードが行ったシステムコールは、アセンブリレベルで正しく実装されているのか」とは考えません。それはLinuxカーネルの実装者が適切に解決したと想定することです。
同様に、証明が高いレベルの抽象化にあり、その下に、当然のことと考えられる低レベルの構成要素がある証明を想像することができます。また、大きなシステムをソフトウェアで構築する時のように、システムを部分に分割し、これらの責任を異なる人々に渡し、物事が確認されるべきインターフェースがあり、そしてユニットレベルでもエンドツーエンドでもテストがパスする限り、このシステムが大丈夫だと受け入れるだけです。
同様に、数学の証明についても同じような分解を持つべきかもしれません。例えば、フェルマーの最終定理のような大規模で複雑な証明を考えてみましょう。個々の人間が証明するのに非常に長い時間がかかりました。しかし、今では分解を行い、1000人の数学者のチームが部分を見て、それらの部分が正しく行われていることを前提として、すべての人が局所的な義務を果たせば、フェルマーの最終定理を証明するというグローバルな目標が真になることを保証する方法があるかもしれません。
この大きな全体を局所的な義務に分解するというアイデアに魅了されています。Linuxオペレーティングシステムを見てみましょう。局所レベルでこれらの人間が理解できるインターフェースモジュールを持つことによって、何らかのボトルネックが導入されると思いますか？
つまり、言語モデルが非常に強力になり、常にコード全体を再生成できる未来を想像できますが、それはコードのチェックインには悪夢となるでしょう。なぜなら、「ジョン、私はジョンのコンポーネントを壊してしまった、このインターフェースが変更され、あちらのスキーマも変更された」というようになるからです。
一貫したインターフェースを持つために、局所モジュールの複雑さを増やす必要があるという興味深いトレードオフが常にあると思いますか？
そうですね、これは解釈可能性と能力の議論に戻ります。原理的には、完全に低レベルのアセンブリコードで書かれたLinuxカーネルを作ることは可能です。それはモジュラーではなく、このような人間が理解できるインターフェースを持ちません。しかし、それでも証明可能に安全です。
つまり、Linuxカーネルが満たすべき性質について、人間が書き下ろした高レベルな目標があり、そしてAIが大規模なアセンブリ言語コードの塊を生成し、さらにこのコードが実際に正しいことを示す正式な証明もあるということです。
では、なぜ反対するのでしょうか？問題は、そのようなAIは現時点では幻想であるということです。仕様を行う最上位レベルを除いて、人間の介入なしに信頼性の高い大規模なコードを生成できるAIは実際には持っていません。
また、時間とともに要件は進化し、このLinuxカーネルの保守に人間が関与できる道筋を持ちたいと思うかもしれません。同じような議論が数学的証明にも当てはまると思います。
数学がすべて、ただボタンを押すだけで行われる世界があります。つまり、数学者が定理を思いつき、定理を述べ、そしてボタンを押すと、AIが入っていって、人間の解釈可能性のような種類のものなしに、可能な限り最低レベルで証明を生み出します。しかし、例えばLeanの証明チェッカーのような証明チェッカーが証明を確認してくれます。
これは原理的には可能だと思います。実際には、私たちはそこからはるか遠くにいます。したがって、少なくとも短期的には、少なくともモジュール境界で解釈可能な証明を持ちたいと思います。そして、人間が高レベルなプロセスの設計に関与し、機械が低レベルな詳細の世話をするのです。
しかし、人間の関与がますます少なくなっていく世界を想像することもできます。ただし、それは数学の目的は何かという疑問を投げかけることになります。数学の目的の一部は、それが楽しく、世界について何かを教えてくれることです。
しかし、数学が純粋に道具的なもの、つまり特定の種類の化学反応が起こるかどうかを予測するために数学を行うのなら、それは今日でもMathematicaやMATLABを使用して多くのシミュレーションを行うのと同じように、AIに任せることができるかもしれません。
この分野でのいくつかの進展について教えていただけますか？この分野で多くの研究をされていますが、人々は何を見るべきでしょうか？
いくつかの異なる方向性があります。最も研究が進んでいるのは定理証明で、ここにはいくつかのバージョンがあります。
一つのバージョンは、Leanのような言語で定理の形式的な記述から始め、この定理の証明を探索するというものです。Leanのようなフレームワークでは、証明は単なるコードのようなもので、その設定ではタクティクスと呼ばれる一連の指示です。
そして、目標が証明されるようなタクティクスの列を見つけることは、実際には特定の仕様を達成するプログラムを見つけることと同じです。これについては多くの研究があります。
最も有望なアプローチは、ニューラルネットワークの使用とLean環境での実行を組み合わせ、適用したタクティクスが良い結果をもたらしたかどうかについてフィードバックを得て、そのフィードバックを使用してさらに生成を行うというものです。そこで起こっているのはそういうことです。
また、自然言語による問題記述を持ち、多くの場合、Chain of Thoughtの変形のような純粋に非形式的な手法を使用して数学的推論を行う非形式的定理証明に関する研究もあります。しかし、時にはこれらの2つのアプローチを組み合わせることもあります。
シャン・ウォラックらによる素晴らしい論文があり、自然言語モデルを使用して高レベルの証明スケッチを生み出し、その証明スケッチを使用して形式的な証明器を導くというものでした。
それが一つの方向性です。形式的な定理証明と非形式的な定理証明です。また、あまり探求されていない他の興味深い問題もたくさんあります。
一つの本当に魅力的な方向性は、一種のオープンエンドな探索です。数学で本当に必要なものは何か、AIは何に貢献できるのかを考えると、より良い予想を創造的に考え出し、証明自体だけでなく、証明したい定理の記述も考え出すという大きな機会があります。
これは非常に重要な方向性だと思いますが、残念ながらこれまであまり研究がなされていません。しかし、この問題に非常に興味を持っているいくつかの研究グループがあります。
例えば、ノア・グッドマンは最近、証明器を導くための内在的なモチベーションを使用することについて、本当に素晴らしい論文を発表しました。そこでのアイデアは、新しい主張を生み出すエージェントと、それらを証明しようとする別のエージェントがいるということです。
つまり、実際に数学で起こることと同じように、予想を立てるプロセスと証明するプロセスの間の相互作用があるのです。
昨晩、あなたのCoPrA論文を読みました。とても興味深かったです。Leanについて高レベルな話はすでにしましたが、もう少し詳しく説明していただけますか？
基本的には、定理があり、そしていくつかの義務があり、そしてアルゴリズムは言語モジュールを使用してこれらのレマを解決し、そして義務がなくなるまで再帰的に自身を呼び出す、というものでした。おそらく発見的な部分は、このレマデータベースから適切なレマを見つけるために言語モジュールを使用することでした。これは魅力的なアーキテクチャですね。それについて教えていただけますか？
はい、もちろんです。ここで他のすべてのLean定理証明や形式的定理証明の取り組みと共通しているのは、形式的な証明器の全体的な構造です。
そこでのアイデアは、出発点となる目標、証明したい最上位の定理があり、そしてこの目標を徐々にサブゴールに簡略化するこれらのタクティクスを適用していくということです。しばらくすると、タクティクスの良い列を選択したと仮定すると、証明すべき目標が残っていなくなり、そうすると完了です。定理が証明されたということです。これはただのLeanで、AIとは何の関係もありません。
問題は、AIをどのように使用してスマートな方法でタクティクスを選択できるかということです。そこでCoPrA論文はいくつかの貢献をしました。
一つは、微調整なしで、単に大規模言語モジュールを使用するということでした。タクティクスを推測するようにプロンプトを与えただけでした。これは、形式的な証明データで明示的に微調整されたモデルを使用した以前の研究とは異なります。
私たちにとって驚くべきことだったのは、ブラックボックスモデルでさえも、言語がかなり難解であるにもかかわらず、この種の形式的な証明に対して合理的なタクティクスを予測できたということです。
しかし、重要な点は、単に言語モジュールに問い合わせるだけでは十分ではなかったということです。このLLM moduloというものも行う必要がありました。LLMによって予測されたタクティクスを得て、それを使用して実際に変更を加え、基礎となるLeanフレームワークでそのタクティクスを実行し、そして新しい状態、証明すべき新しい一連の義務を得て、それで前に進むということです。
LLMは実際に現在の義務が何であるかを見ることができ、また過去からいくつかのメモリも持っており、これらすべてがより大きな検索に組み込まれています。そしてこの検索プロセスはバックトラッキングを行い、何が失敗し、何が機能し、何が失敗したかを記録し、その情報すべてがLLMの生成プロセスを導くために使用されています。それが一つのアイデアです。
もう一つのアイデアは、検索を行うということです。ここでの直感は、数学を行う時、通常は他のプロジェクトからの定義を使用し、他のプロジェクトからのレマを使用するということです。
これらの外部知識ベースを使用するというアイデアは、もともとメタでAI数学研究を行っているカイユー・ヤンが主導したReProverモデルで導入されました。このReProverモデルは微調整されていましたが、ここで私たちが探求したかったのは、大規模言語モジュールを数回のショットで使用して同じようなことができるかということでした。
そして、外部データベースから取得した知識を使用できることが分かりました。これが示しているのは、この種の非常に難解な形式的定理証明の設定でさえも、文脈内学習が大きな効果を発揮できるということです。
はい、GPT-3.5 TurboとGPT-4で試され、GPT-4で大きな改善が見られたと指摘されました。検索を取り除き、検索は劇的に役立ちました。約60ステップに制限されたと思いますが、おそらく長く続けばさらに良かったでしょう。そしてバックトラッキングには、私は今悪い状態にいるから戻るというような概念があったと思いますが、それはどのように機能したのでしょうか？
Leanのような形式的なフレームワークの良いところは、どのような状態が悪いのかについての情報を得られるということです。証明の特定の状態にいて、特定の一連の証明義務があるとします。役に立たない、または実際に現在の状態で適用できないタクティクスを取ると、フィードバックを得られます。
または、例えば、すでに見た状態に戻っていることに気づき、状態空間で無限ループに陥ることになるのであれば、それも避けるべきことです。このような情報は、LLMをより広い検索プロセスに明示的に組み込むことで得ることができます。
しかし、この論文での主な発見は、この設定でも文脈内学習が興味深いものになり得るということだと思います。60に制限したのは、アカデミックな計算予算で作業していたからで、また当時GPT-4はかなり高価でした。
しかし、モデルが安価になるにつれて、このようなLLMプラス検索プラス、Leanや他のフレームワークを通じた外部グラウンディングによって、どこまで進めることができるかを見るのは本当に興味深いと思います。
特に、経験的イタレーションを行う意欲がある場合、つまりデータを収集し、それを使用してモデルをさらに微調整し、そのようにして続けていく場合、かなり遠くまで行けると思います。
いくつかのことについて興味があります。到達可能性という概念に興味があります。データベースにたくさんのタクティクスがあり、そしてタクティクスの凸包が到達可能な空間を与えるという、私たちが指摘してきた概念があります。
しかし、おそらくタクティクスで到達できない目標状態を持つ定理の例があるはずですよね。それについて説明していただけますか？
実際に、何でも見つけることができる本当に低レベルなタクティクスがあります。その目標状態に導くタクティクスの列が存在するかもしれませんが、それが非常に長く複雑で、AIがそれを見つけることができないかもしれません。そしてそれは頻繁に起こります。証明できない記述はたくさんあります。
一つの興味深い問題は、このような低レベルのタクティクスをより高レベルのタクティクスに抽象化できれば、より良い結果が得られると期待できるかということです。私はその答えはイエスだと思います。
数学の学生がどのように進歩するかを考えてみてください。本当に基本的な代数から始め、あるいはさらにその前に算術から始め、そして代数に進み、突然大きな飛躍があり、微積分に進み、確率を学び、さらに抽象的になり、複素数に進みます。
このように、人間の学生は数学を学ぶ過程で抽象化の階層を通過していきます。これらの抽象化の目的は、よりロバストになり、より多くの種類の問題を扱えるようになることです。多くの点解を一般解に統合しているのです。
AI数学のこの文脈でも、そのアプローチが価値があると想像できます。低レベルのタクティクスのセットから始めますが、おそらくDreamCoderのような方法で、より抽象的なタクティクスを発見し、それらを使用してさらに多くの証明を行い、そしてある時点で物事が爆発的に広がり、新しい種類の数学を発見することになるでしょう。
解像度は漏れやすさにどのように関係していますか？物理学を考えると、ニュートン力学と相対性理論などがありますが、より高レベルの抽象化に依存することで漏れが生じるのでしょうか？
この形式的証明の設定では、そうはなりません。理由は、Leanや他のフレームワークの設計方法として、確実性がなければ証明は受け入れられないからです。より高いレベルの抽象化にいたとしても、その高レベルのプリミティブの実装を、実際に健全な低レベルのプリミティブで実装することになります。
しかし、もちろんそうでないバージョンも想像できます。例えば、一部の低レベルまたは証明の義務が単に経験的なバージョンの数学のAIを想像できます。
ある記述が普遍的な数学的法則ではなく、おそらく特定の場所と時間の性質であるという記述を行っているとします。つまり、単に経験的に評価する述語があるかもしれません。それを確率的な述語にすることで数学的な意味を与えることはできますが、選択した分布が正しいかどうかは分かりません。
その場合、解像度が高レベルになればなるほど、より多くの不確実性が生じることになりますが、そのレベルより上で形式的な数学を使用している場合は、行っている主張について、ある程度の保証はまだ得られるでしょう。
自然科学で数学を使用する時とそれほど違いはありません。経験的な観察を行っており、そこにはノイズがありますが、ある時点でそれらをよりクリーンな数学的モデルに抽象化し、そのモデルに基づいて行うすべての推論は、あなたの仮定、モデリングが正しいという条件付きになります。
これは、より粗い粒度のモデルを持っている場合、結論についてより多くの不確実性を持つことになるという点で、それほど違いはないと思います。それは0か1である必要はありません。完全に確実か、完全に不確実かである必要はありません。
最近、デイビッド・スパイビーと話をしました。彼は応用圏論でよく知られています。彼は、私たちの認識論的フレームワーク全体が、私たちが尋ねる質問からほぼ導き出されると言っていました。
定理と、定理の有用性、そして定理を作り出す上での人間の役割について話す時、同じようなことがあるのではないかと思います。これらの質問を尋ねる理由が何らかの形であるはずです。それはどこから来るのでしょうか？
多くの数学において、それは実世界の問題を解決するという目標に触発されていたと思います。なぜ人々が幾何学を考え出したのか、なぜ微積分を考え出したのかを考えると、世界がどのように機能するかを理解し、それを新しいことを行うため、実世界のエンジニアリングの課題を解決するために適用するという、非常に実用的な目標があったと思います。
そして、私はそれがしばしば出発点だと思いますが、もちろん、エレガンスという動機もあります。そして好奇心もあり、単なるポイントソリューションではなく、エレガントで統一された解決策を持ちたいと思います。
また、「この定義でこのような仮定を行ったが、これらの定義をこのように変更したらどうなるだろうか」という好奇心もあります。私は、日常生活で見られる現象をモデル化するというアイデアと、「これを行ったらどうなるだろうか」と単に尋ねる好奇心という動機、そして点解をより抽象的な何かに統一するという、これらのアイデアを組み合わせれば、そこから多くの数学が得られると思います。
それについてもう少し詳しく説明していただけますか？これを分解するとしたら、本当に良い数学的定理とは何でしょうか？
私はプロの数学者ではないので、おそらくこの質問に答えるのに最適な人ではありません。おそらく、コンピュータサイエンスについて、特に理論的コンピュータサイエンスの論文について話すことはできます。なぜなら、そのコミュニティから来ているからです。
そこで私は、まず興味深さという問題があると思います。興味深いとは何でしょうか？問題は、クリーンであるべきだと思います。解決しようとしている問題は、クリーンな記述であるべきです。
n個の異なるケースを持つこの奇妙な定義を思いついて、それについての特定の定理を証明したいというようなものではないはずです。比較的簡潔でエレガントな何かであるべきです。
そして、新規性があるべきです。以前にこれのn個のバージョンを見たことがあり、以前のモデルの1つの証明を少し修正すれば証明が出てくるように感じられるなら、それは追求する価値がありません。
したがって、新規性とエレガンスが大きな基準だと思います。そして、特にコンピュータサイエンスにおいては、有用性も考慮事項だと思います。
コンピュータサイエンティストがある種の理論に関心を持つ理由は、その理論が実世界の計算プロセスをモデル化するからです。例えば、オンラインアルゴリズムへの関心があったのは、オンラインでデータを処理する必要のある実際のコンピュータシステムがたくさんあったからです。
アルゴリズム的ゲーム理論への関心があったのは、インターネットが登場し、突然、伝統的な中央集権的な計算世界の見方から離れることになったからです。代わりに、インターネットはこの巨大なコンピュータであり、すべてのエージェントが自分自身の目的に動機づけられているが、広告オークションやその他の多くのオンライン調整メカニズムを使用して調整を行っていました。
これが、アルゴリズム的ゲーム理論に関する興味深い研究すべてにつながりました。「K個の異なるエージェントがいて、均衡に到達しているとしましょう」という均衡、つまり市場の均衡があります。しかし、従来のゲーム理論とは対照的に、多項式時間で均衡に到達できるのかと尋ねたいのです。
この均衡は到達可能なだけでなく、計算的に到達可能なのでしょうか？私の見方では、多くの興味深いコンピュータサイエンスの理論は、数学と以前のコンピュータサイエンスのこれらの長年の原理を取り、それらをコンピュータシステムの実践的な問題から触発された新しい設定、新しいモデルに適応させることで生まれてきました。
ゲーム理論は本当に美しい例ですね。私はエージェンシーに興味があります。これは自然界の現象の素晴らしい例です。そして、それは行動のある種のダイナミクスを美しく区分けします。そして、このゲーム理論というものを作り出し、それもエージェントの概念を使用しています。
それは多くの複雑なシステムをモデル化する、この不合理な効果を持っています。モデル内で異なるスケールでエージェントをモデル化することを選択し、さらにモデル内で異なるスケールを混ぜ合わせることさえできます。
しかし、本当に良い定理の定義に戻ると、クリーンについて話されましたが、チョムスキーはLLMは言語の理論ではないと言いました。なぜなら、彼が考える言語と、不可能な言語や何か無作為なものとの間のクリーンな区分がないからです。この区分について何か言えることはありますか？
LLMは訓練セットにあるものと、その構成物を何でも生成すると思います。したがって、LLMが主に美しい定理と美しい文学で訓練されていれば、生成するテキストにもそのような側面が見られると思います。
しかし、そのクリーンさ、そのエレガンスは微妙です。単に特定の美の高レベルな動機に従うだけではなく、一貫性を持つことも重要です。多くの場合、例えば私がLLMを執筆に使用する時、このパラグラフは本当によく書けていて素晴らしいのですが、次のパラグラフは少し異なります。
個々には問題ないかもしれませんが、2つを組み合わせると何か恐ろしいものになってしまいます。このエレガンスのアイデアは、定理の小さな部分がクリーンに記述されているから全体がクリーンに記述されているというわけではない、一種のグローバルな概念だと思います。
私にとって、LLMがエレガントな定理の記述を生み出せるかどうかは、非常に開かれた問題です。答えがノーかイエスかは分かりません。
アブレーション研究で、ゼロショットのGPT-4から始めて、記憶が正しければ2.3%程度だったと思います。そして、このCoPrAアルゴリズムと検索とバックトラッキングのすべてを使用して、約30%まで幅広く及びました。
しかし、テストセット汚染について常に心の奥に引っかかるものがあります。そして、それについて少し作業をされましたね。それについて話していただけますか？
これはLLMベースのアプローチでは非常に難しい問題です。汚染のために結果が出ているのではないかという懸念は常にあります。私たちはこの問題に対処するためにできることを行いました。
それは、まず私たちが追加したすべての追加部分を取り除いて、LLMに証明を最後まで生成するように依頼しただけの場合、あなたが言及したように約2%しか成功しなかったことを示しました。
また、生成された多くの証明を見て、インターネット上で似た例を一生懸命探しましたが、見つけることができませんでした。これは汚染の産物ではないという別の指標です。
しかし、汚染は間接的な役割を果たした可能性があります。おそらく私たちが見つけることができなかった、LLMが以前に見た似たような種類の問題があるかもしれません。それは確かに可能性としてありますが、私は、AI研究のこの時点では、このリスクを非常に意識しつつも、LLMを使用し続けるしかないと感じています。
サバールと話した時、彼はブロックスワールドの計画問題を解く際に、ミステリーブロックスワールドバージョンを作成し、すべてのトークンをスクランブルしたと言っていました。そして、確かにそれは性能の大きな低下を引き起こしたそうです。しかし、これは本当に把握が難しいですね。
はい、その通りです。標準的なベンチマークでは、これは大きなリスクです。合成ベンチマークを使用することを想像できると思います。CoPrA論文で私たちが取ったアプローチは、完全に任意の合成ベンチマークには適していないと思います。
なぜなら、全体的なポイントは、LLM内の事前知識が新しいタクティクスを見つけるのに役立つということだったからです。しかし、最近取り組んだ別の論文があり、シンボリック回帰の文脈でLLMを使用した概念学習に関するものでした。
そこでもLLMを検索フレームワーク内で使用しました。この場合は進化的検索のプロセスでした。先ほどの会話で言及したこの論文では、概念の抽象化にもLLMを使用し、これらの抽象的な概念を使用して検索プロセスを導きました。
その場合、合成問題でも実験を行い、そこでもLLMが役立つことが分かりました。理由は、何らかの事前知識を使用していなくても、テキストの例に基づいて高レベルの概念を生み出すというLLMの抽象化能力が役立つからです。
しかし、それはCoPrAアプローチの一部ではなく、完全に合成的な問題を思いついても、CoPrAがそれほどうまく機能するとは考える理由がありません。
素晴らしいですね。最後に、人々はどこであなたの研究について詳しく知ることができますか？
私の名前をGoogle検索していただければ、ウェブサイトにたどり着けます。そこからすべての論文にリンクが張られています。また、Twitterアカウントもあります。単に「swarat」です。
しかし、技術的な何かについて本当に議論したい場合は、メッセージを送っていただければ、喜んでさらにお話しさせていただきます。
素晴らしいです。私たちはご言及いただいた論文をすべて画面に表示します。SWさん、素晴らしい会話をありがとうございました。
私からもありがとうございました。私も本当に楽しませていただきました。