AIにおける絶対的真実: Neuro-Symbolic AI

この動画は、LLM単体では到達しにくい絶対的に正しい論理推論を、Neuro-Symbolic AIによってどう補完するかを解説する内容である。人間の曖昧な自然言語をそのまま扱うのではなく、第一階述語論理やSMT solverのような厳密な記号処理系へ変換し、LLMは仮説生成に、solverは真偽判定に特化させることで、論理推論の信頼性を大きく高めるという新しい研究の意義が語られている。

Absolute Truths in AI: Neuro-Symbolic AI

All rights w/ authors:Draft-and-Prune: Improving the Reliability of Auto-formalization forLogical ReasoningZhiyu Ni1*, Z...

www.youtube.com

冒頭

こんにちは、コミュニティのみなさん。今日も戻ってきてくださって本当にうれしいです。
今日は真実をお話ししたいと思います。しかも絶対的な真実です。

そんなの不可能だと言いたくなるかもしれませんが、驚いたことに、新しい研究が出てきました。
では始めましょう。

ご覧のとおり、出発点には人間の言語があります。そこには曖昧さがあり、文脈があり、ニュアンスがあり、人間の意図があり、その他いろいろなものがあります。

そしてそこから、うまく分岐させて、検証ゲートのようなものを通していくわけです。
では、もう少し近くで見ていきましょう。

前回の構造との違い

前回の動画を覚えている方は、似たような構造が出てきたのを思い出すかもしれません。ただし、出発点はまったく別のものでした。
あのときは tenzo grid があり、高解像度の三次元乱流テンソル構造があり、そこから拡散変換アーキテクチャが広がっていました。

その中で、流体の中の特定パターンについて、将来の経路の投影を行っていました。
そして、ある一つの指標を選びました。それが不確実性の広がりでした。

私は、それは一種の auto research のようなものだと言いました。つまり、明示的な一つの指標があり、その spread function がシステム全体をさらに最適化していくという話です。

もちろん、そのとき何人かの方が、ちょっと待ってくださいと言いました。
もし counterfactual probing があって、それが diffusion model 側へ戻っていくのなら、複数のパラメータを変更できますよね、と。

そうなると、もう単一の指標には縛られません。もっと高次元な指標構造になります。
だからこれは self-learning system なのだ、と。

すでに解決済みだと思っていた問題

なるほど、auto research system と呼ぼうが、self-learning system と呼ぼうが、私はあまり気にしません。呼びたいように呼べばいいんです。
とてもきれいな考え方ですし、何を言っているのかはすぐにわかります。

ただ、ここでお伝えしなければならないのは、私はこの問題はすでに解決済みだと思っていたんです。
ええ、本当に。

2023年10月に出た Logic-LM という研究があります。
タイトルは Logic-LM: Empowering LLMs with Symbolic Solver for Faithful Logical Reasoning。University of California, Santa Barbara の研究です。

私はそれを見て、素晴らしいと思いました。
ここに問題があって、目標があって、problem formulator があって、symbolic reasoner があって、result interpreter がある。これで全部自動で解けるではないかと思ったんです。

材料科学でも使えるし、AI構造のようなものにも使える。
解決済みだ、すばらしい、と思っていました。

実際にはまったく解決していなかった

ところが、今日学んだことはまったく逆でした。
これは全然解決していなかったのです。

システムはまったくうまく動いていません。
だから、もう一度しっかり見直さなければならないし、最適化も必要です。なぜなら、今のままではこの仕組みは機能していないからです。

では見てみましょう。
今日取り上げる研究は 2026年3月18日 のものです。

今回は University of California, Berkeley と Microsoft が組んでいます。
とてもいいですね。

論文のタイトルは、Autoformalization for Logical Reasoning of RAI Structures: Improving the Reliability of the Autoformalization です。
何かが進んだわけです。では見ていきましょう。

Autoformalizationとは何か

もしこの分野にあまりなじみがない方のために言うと、autoformalization とは、人間の自然言語による推論問題を、数理的・記号的な solver が実行可能なプログラムへと変換することです。
それによって symbolic solver が、本当の意味で深い論理的演繹を実行できるようになります。

すばらしい考え方です。
Berkeley と Microsoft に感謝ですね。GitHub のリポジトリも公開されています。とてもいいです。

何が問題なのか

では、いま解くべき問題は何なのか。
何がうまくいっていないのか。

結論から言うと、現在の AF pipeline は壊れやすいのです。
プログラムが実行自体に失敗することもありますし、実行はできても人間の意味内容を誤って符号化してしまうことがあります。

つまり、私が自然な人間の言葉でシステムに伝えた内容が、そのまま一対一で記号表現へ写像されているわけではないのです。
私は自分の自然言語をシステムに理解させ、それを reformulate して数値的な solver に渡してほしいわけです。Prolog でも Lean 4 でも何でもいい。

ところが、実際にはそれができていません。
ものすごく頑張ってはいるんです。必死にやろうとしている。でも失敗するんです。

だから、私たちの小さなAIシステムを助けてあげなければいけません。
現状では、それがまだできないのです。

Transformerの限界ではなく、役割の誤用だった

この論文では、かなりの研究と実験が行われています。
ぜひ論文そのものを見てください。

彼らが実証的に示したのは、LLM が厳密な論理を扱えないのは、Transformer architecture 自体の限界ではないということです。そもそもそれは、そのために設計されたものではありません。

問題は、inductive なエンジンに deductive な仕事を autoregressive にやらせようとしていることにあります。
要するに、このシステムに、本来作られていない仕事をさせようとしているのです。

Transformer は autoregressive system です。
次のトークンを順番に予測していく仕組みです。

そこで、LLM の役割を divergent hypothesis generation に限定し、一方で convergent proof validation には exact verifier を使う。
このようにAIの使い方を変えたわけです。

すると、第一階述語論理タスクにおいて、AIは高い信頼性の上限に近づけるようになります。
しかも、ここが重要なのですが、neural network の構造を変える必要がありません。テンソル重みも含めてです。

私もこれを見たとき、えっ、なぜ、どうして、どうやってそんなことが可能なのか、もっと教えてくれと思いました。

学習時ではなく推論時に計算負荷を移す

ここでこう思うかもしれません。
つまり、LLM に数値的な symbolic solver の完全なマニュアルを丸ごと学習させて、そのために何千、何万という教師データを用意して supervised fine-tuning をする、そういう大がかりな訓練を避けたいということなのか、と。

答えは、そのとおりです。
まさにそこがポイントです。

あなたは今、symbolic AI における data starvation wall を正確に言い当てました。
そして彼らは、その問題に対する解決策として supervised fine-tuning をそもそも使わない道を探したのです。

彼らは重みテンソルを変えたくなかった。supervised fine-tuning も避けたかった。
その代わりに、計算負荷を training time から inference time へ移そうとしたのです。

世界中に巨大データセンターがあるなら、それは可能です。
つまり、複雑さを訓練時から推論時へシフトするわけです。

これが良い考えかどうかはさておき、少なくともこの論文はその方向を取っています。
TT から IT、つまり training time から inference time へ移るわけです。

LLMを完璧な解答者ではなく確率的事前分布として使う

完璧な形式化を最初の一発で吐き出させるよう、LLM に無理をさせる代わりに、彼らは LLM を本来の用途に戻して使いました。
つまり stochastic prior としてです。

Model 4 でも 5 でも 6 でも何でもいいのですが、彼らは巨大な proprietary AI を使っています。
そして three in-shot context learning examples を使いました。

要するに、AI に対して、見てください、私が求めているのはこの3つの例のようなものです、これをまねしてください、これをコピーしてください、と非常に明確に示したわけです。
重みテンソルの更新はありません。大規模な supervised fine-tuning もありません。やっているのは in-context learning です。

ですから、私のメインダッシュボードでいえば、few-shot examples を使った in-context learning の領域にいるわけです。
そしてそれを、絶対的真実を求める論理問題に対して用いるのです。

外部solverに接続しても、最初はうまくいかなかった

ここで、LLM がただの prior なら、外部 solver に接続すればいいじゃないかと思うでしょう。
Prolog でも Lean 4 でも、Python でも C++ でも、好きなものを使えばいい。

実際に彼らはそれをやりました。
そして結果は、うまくいかなかったのです。

そこで私は、では LLM に制御された形で全部 hallucinate させればいいのではと思いました。
実際、著者たちは GPT-4 を使って 20 個の異なる意味解釈を生成させました。

それらは英語テキストに対する 20 通りの plan です。
そして、その20個の plan をそれぞれ 20 個の formal program にコンパイルしました。

後で例もお見せします。
そして大半についてわかったのは、やはりゴミのような翻訳だということでした。

AI は、人間の自然言語から異なる意味解釈を作り出し、それを第一階述語論理に基づく symbolic solver 用の表現へ変換しようとするのですが、そこで失敗するのです。
なぜなら、symbolic solver はどれもそれぞれ独自の API を持っているからです。

たとえば 20 個の plan があったとして、そのうち 18 個は動かない。
でもそれで構わないのだ、と著者たちは言うのです。

私は少し混乱しました。
つまり trial and error なのか、と。

すると彼らは、そこがトリックなんですと言いました。
もしそう呼びたいならそうです、と。

solverそのものをテスト時の枝刈りゲートとして使う

彼らがやったのは、数値的 solver の厳格で容赦のない法則そのものを、test-time pruning gate として使うことです。
つまり、solver が矛盾を返す、あるいはこれは絶対に成立しないと判断するなら、その案はその場で落とすのです。

すると、20 個の候補のうち、本当に人間の意図を正しく翻訳していて、なおかつ結果を生成できるプログラムだけが残ります。
最後に残るのは1個か2個かもしれません。

本質的な悪魔は意味の空白を埋めること

結局のところ、autoformalization における最大の悪魔は、意味の空白を埋めることです。
つまり、ぐちゃぐちゃで曖昧な人間の言語、人間の言葉、私がAIに対して科学的タスクを説明するやり方と、本当に必要とされている冷たい数学的トポロジーや表現のあいだにある深い溝を橋渡しすることなのです。

AI が私の意図と要求を本当に理解するには、その溝を越えなければいけません。

Draft and Pruneという新しい方法論

そこで彼らは新しい方法論を導入しました。
それが draft and prune です。

この方法によって、AI研究者は supervised fine-tuning という、苦痛を伴い、壊れやすく、しかも経済的にスケールしにくいプロセスを回避できます。
実際、これは非常に時間がかかります。トレーニングデータセットを準備しなければいけないし、その後もいろいろ大変です。

クラウドに行って訓練をしなければならない。
たとえば GPT-5 クラスのモデルを SFT で訓練しようとすれば、1万ドル以上かかってもおかしくありません。

ですから、これはいい方法です。
私たちは in-context learning の世界にいるのです。

もちろん、それによって LLM の立場は変わります。
LLM は何でもできる万能選手ではなくなります。

ここでの LLM は、hyper-creative で high-variance な proposal generator です。
人間の言語を書き出す役割に特化し、絶対的真実を生成する負担は、完全に deterministic な数学的 solver に委ねます。

こうした solver は、40年、50年前、あるいはもっと昔に生み出されました。
まだこうしたAIシステムが存在する前の時代から、数学的 solver は作られてきたのです。

いま私たちは、LLM の限界を理解し、solver が必要なのだと認め始めています。
それだけの話です。

LLMには論理の規則を覚えさせるのではない

もしこれが profound shift だと言われるなら、もしかするとあなたはすでにずっとそのようにやってきたのかもしれません。
要するに、もはや LLM に数学のルールや論理のルールを教え込もうとしているのではありません。

そうではなく、翻訳を推測させているのです。
そして、その推測結果を第一階述語論理へ落とし込み、その後は meta engine が計算し、完全に適合しているかどうかを確認するだけです。

はいか、いいえか。
LLM はただの writer なのです。

LLM の統計的世界では、私たちは確率を扱います。
LLM は autoregressive system であり、次のトークンを予測します。

しかし、必要なのは deductive realm of first order logic です。
第一階述語論理には確率はありません。あるのは true と false、そしていくつかの数学的操作だけです。

この豊かな人間言語を、たとえば最も単純な第一階述語論理へ変換することは、まったく簡単ではありません。
そして、そこでAIは失敗します。

predicate logic と呼んでも構いません。
好みの問題です。

これは、ある特定の議論領域において、対象とその関係について絶対的な命題を述べることができる数学的システムなのです。

Predicate Logicの基本要素

興味がある方のために言うと、predicate logic は5つの数学的原子から成り立っています。
まず constants があります。これは特定の対象です。Kyle でも何でも、2 でも何でも構いません。

次に variables があります。
これは対象のためのプレースホルダーです。

それから predicates があります。
性質や関係について true または false を返す関数です。

さらに logical connective があります。
何かを組み立てるための接着剤のようなものです。and、or、not、implies などです。

そして quantifier があります。
これが第一階の部分です。

たとえば、領域内のすべての要素に対して成り立つ universal quantifier がありますし、少なくとも1つの要素が存在する existential quantifier もあります。
数学で見慣れているものです。

これが最も単純な組み方です。
もちろん、私たちは最も単純な predicate logic に限定されているわけではありません。

人間の文を第一階述語論理へ訳す例

例を一つ挙げましょう。
人間の言語で言うと、Kyle と Leonor は午後には報告しないが、全員はちょうど一度だけ報告しなければならない、という文です。

妙な文ですね。
でも、この第一階述語論理への翻訳を見てみましょう。前提は2つです。1と2、それだけです。

すると、これはもはや数学にかなり近い表現になります。
論理エンジンはこれを即座に理解できます。

そこには回りくどさもありませんし、解釈の自由もありません。
定義された数学的システムです。

AI も機械も、これなら扱えます。
そして皆さんから、なぜ GPT-5 に英語のまま chain of thought で考えさせないのか、という質問をよくいただきます。

なぜ英語のまま reasoning させるだけでは駄目なのか

理由は簡単です。
LLM はそのために作られていません。

LLM は inductive で統計的な manifold です。
言語パターンを別の言語パターンへ写像することで、推論らしきものを近似しているのです。

その仕事に関しては、LLM は非常に優秀です。
ただし、私たちが本当に欲しい仕事、たとえば金融計算の真実、将来収益の正確な算出、医療処置に関する計算可能な判断、あるいは数学、化学、物理に関する厳密な正しさとなると、それでは足りません。

私たちが必要としているのは、統計的 manifold ではなく、別のものです。
統計的なデータではなく、本当のデータがほしいのです。

だからこそ、問題を新しい数学的空間へ押し込む必要があるのです。
前回の動画では、視覚から意味層へ移る話をしました。今回は、言語から別の syntax へ移るのです。

その syntax が第一階述語論理です。
言語的なおしゃべりや幻想を全部削ぎ落としたいからです。

一度問題が第一階述語論理として定式化されれば、それを deterministic algorithm、つまり典型的な solver に渡せます。
この solver は何十年にもわたって使われ、何十万もの例で battle-tested されてきました。

だから、数学的に完全な演繹をかなり保証してくれます。
hallucination にも、バイアスにも、あるいは32段階のうち14段階目でルールを忘れるようなことにも影響されません。

私が最新の LLM をテストするとき、まさにそういう失敗を見ます。

solverにはさまざまな種類がある

solver にはいろいろな種類があります。
著者たちはそれを大きく2つのグループとして示しています。

まず歴史の長い SMT solver です。
satisfiability modulo theories solver。Z3 がその代表で、Z3 Python などがあります。

彼らは論文の中で特定の課題にこれを使っていますが、一般的に言えば、SMT solver は第一階述語論理を巨大な代数制約とブール論理の網として扱います。
そして、それらの方程式や論理が両立可能かどうかを非常に積極的に最適化して探索します。

たとえば、Kyle は午後2番目のスロットでは報告しない、といった文を、そうしたコードとして表現できます。
一方で論理プログラム solver もあります。Prolog です。

論文では2つの例でこれを使っています。
ここでは forward chaining や backward chaining と呼ばれる仕組みを使い、もし A なら B といった規則を読み込み、行為の木を再帰的に探索していきます。

その仕事は論理プログラム表現だけです。
あるいは、自分の領域、自分の仕事、自分の複雑性に特化した numerical solver を使うこともあるでしょう。

私自身がよく扱うのは constraint satisfaction problems、つまり CSP solver です。Python constraint などですね。
これも preprint の中で主に論理演繹に使われています。

ここで重要なのは、LLM が論理をやっているわけではないということです。
論理をやっているのは solver であり、C++ であり、外部 solver です。

論理的演繹は、組合せ最適化のようなパズルに極めて強く集中します。
私が新しい LLM や VLM をテストするとき、まさにそこを見ています。

そして、はっきり言えますが、CSP solver を内部で立ち上げたAIシステムを私はまだ一度も見たことがありません。
彼らは Python で解こうとはします。それは正しい方向への一歩ではありますが、まだ赤ちゃんの一歩です。

私が本当に見たいのは CSP solver です。
でも、それはまだ起きていません。

だから言えるのです。
はい、最新の LLM でさえ、ここには問題があります。

明確に変数を定義し、可能性を系統的に消去していく。
それはまだ単なる Python コードに留まっています。

この研究から得られる示唆

では、この研究から何がわかるのか。
少しフラストレーションがたまる内容です。

私たちは、こうした問題はもう解決済みだと思っていました。
でも、きちんと実験して、きちんと検証してみると、まだ多くの問題が残っているのです。

LLM が translator としてだけ機能するとき、それは単に英語を抽象的な数学式に翻訳しているのではありません。
実際には、私の英語による問いを、たとえば Z3 Python のような、非常に特定的で癖の強い API に翻訳しているのです。

あるいは、どんな solver を使うにせよ、その solver 固有の厳密な syntax に合わせて変換しているのです。
そして、Gemini でも Opus でも何でもそうですが、彼らはインターネット全体に近いデータで学習しているので、どこかにこうした知識が潜在的に入っています。

だから、たった3つの例を与えるだけで、著者たちの実験では、それで十分だったそうです。
LLM はすぐに何をすべきかを理解したのです。

その3つの例が、こうした非常に特殊な API 構造への完璧な翻訳を生み出す鍵になったわけです。

Draft and Pruneは極めて実用的な方法

この draft and prune という方法は非常に実用的です。
私の人間の言葉、たとえば、これをやりたい、それからあれをやりたい、数学的変数を用意して、温度を上げて、塩分濃度を上げて、これをしてあれをして、といった記述を、厳密な SMT solver 向けの特定の Python 方言に翻訳するのは、LLM にとってあまりにも難しい。

だからこそ著者たちは、20 個の draft interpretation を生成させました。
そして、solver 自身の容赦ない性質に最終判断を委ねたのです。

solver 自身が judge となって、内部に論理矛盾を含む候補を切り刻んでいくわけです。

solver に慣れている方ならわかると思いますが、私も問題を定式化するとき、最初は8個のパラメータしか考えていないことがあります。
そして、その8個のパラメータで Python コードを書いてくれ、と頼む。

すると一見きれいなコードが生成されるわけです。
でも実際には、私が2つのパラメータを忘れていることがある。たとえば温度を忘れている、といった具合です。

もしここで、流体力学や理論物理向けに最適化された numerical solver を使えば、その solver は最初の時点で、いや、あなたには12個のパラメータが必要ですよ、と教えてくれるかもしれません。
コンピュータシミュレーションを始める前に、系がちゃんと定義されるにはそれだけ必要だと。

つまり、長年にわたって検証されてきた方法を使うのは、本当に助けになるのです。
もちろん Python プログラムは書けます。でもその Python プログラムの中では、私がパラメータを見落とすかもしれないし、最新の方法論を知らないかもしれない。

solver を使えば、その solver はただ一つの仕事のためだけに最適化されていて、その仕事においては最良の選択肢なのです。
ですから、これは完全に理にかなっています。

自分で C++ を最適化したり書いたりする必要はありません。
そんなのは正気の沙汰ではないですから。

直接プロンプトしてsolver用Pythonを書かせる

だから、今ではAIモデルに対して直接こう言えるわけです。
この論理パズルを読んで、Z3 ライブラリを使った Python スクリプトを書き、問題を厳密にモデル化し、解を出力してください、と。

本当にそれだけで済むこともあります。

Draft and Pruneの完全なパイプライン

もし draft and prune の完全なパイプラインを見たいなら、とても単純です。
要素は3つだけです。

最初に人間の言語があります。
どんな文でもいい。

次に LLM が plan を作ります。
正確には20個の plan です。

そのうちの一つは、たとえばこんなものです。
学生と時間帯のための boolean matrix を作成する。Kylie と Leor の2人については、午後のスロットでは false に制約する。なぜなら、彼らは午後には報告しないからだ。

ここで何が起きているかというと、すでに最適化が始まっているのです。
そしてその後、Z3 Python コードへの翻訳が行われます。これがそのフォーマットです。

solver は表現形式を非常によく最適化しています。
そして当然、solver の深さとは何なのかと聞きたくなるかもしれません。

ではそこに行きましょう。

Z3の背後で本当に起きていること

たとえば Z3 は SMT solver です。
satisfiability modulo theories solver ですね。

Python で add などと書くとき、Python がそのコードを通常の意味で実行しているわけではありません。
Python は wrapper として機能しており、その背後で目に見えない第一階述語論理の数学的グラフ構造を組み立てています。

ここが solver の強力さを理解するポイントです。
グラフが組み上がると、Python はそれを本格的な C++ engine に渡します。

そしてその C++ engine が、演繹論理の絶対法則を実行するのです。
これこそが、数学的 solver、数値的 solver の利点です。

AIの全体地図の中での位置づけ

これを私の小さな可視化に統合してみましょう。
これが、今日のAI全体の景色です。

今日話していたのは in-context learning の部分です。
few-shot の例を3つ与えて、LLM に解そのものを出させるのではなく、これは論理問題だから、それ自体では論理を解けないので、外部 solver に接続させるのです。

その solver はインターネットのどこかにあるかもしれないし、ローカルドライブにあるかもしれません。
そして 20 回の翻訳による drafts を作って、あとは運を天に任せる。

その中のどれか一つが正しいことを祈るわけです。
これが satisfiable な解決策なのかと私に聞かれれば、20 drafts でも 40 drafts でもやって、一つ当たることを祈るしかない、と答えるでしょう。

これが科学的なやり方かと言われると、まあ科学的ではあります。
ただ、ちょっと面白い世界ですよね。

でも、何が起こっているのかははっきり理解できます。
では結果をお見せします。実際に動くのか、と皆さん思うでしょうから。

ベンチマーク結果

GitHub リポジトリはすでにお見せしました。
ここに結果があります。

ここには classical prompting 全体があり、そして autoformalization があります。
この二つのブロックを見ていきます。

ここではある特定の benchmark だけを見ます。
すると、chain of thought など通常の prompting だけだと、GPT-4 Omni でたとえば 38 くらいです。

ところが、古い autoformalization、たとえば Clover を使うと、38 から 46 に上がります。
おお、何か効いているぞという感じです。

性能はたしかに上がっている。
しかし、この動画で紹介している新しい DMP、この新しい方法論に行くと、一気に 80% まで上がるのです。

つまり DMP は本当に機能している。
見事な 80% です。

では、いったい DMP は LLM のどんな隠れた物理を引き出して、この 30%、40%、60% の谷を越え、80% に到達したのか。
方法論としては美しい。

でも、私はこう思うのです。
本当にこれが私の求めているものなのだろうか、と。

パス数とコンパイル成功率

次に見せられた結果が、これまた非常に説得力がありました。
ここでは path の数が示されています。

plan を1つだけ使う場合から、20回分の plan を使う場合まであります。
LLM がベストを尽くしているわけです。

私は普段、自分の LLM とよく対話します。
自分の意図を説明し、背景情報を与え、並行実験をしていればその結果も渡す。情報は多いほどいい。

そして、ここで問われる単純な指標は、生成されたコードが Python の syntax error なしにコンパイルされたか、きちんと走ったか、です。
pruning をしない場合、この値は最初の1本目からすでにほぼ100%近く、2つ3つの plan に増やすとほとんど 100% で飽和します。

すごいと思いますよね。
ところが pruning を入れると、最初はかなり低く始まり、そこから漸近的に上がっていき、しかも 100% に到達する前に plateau してしまいます。

でも注意してください。
これは間違った指標なのです。

なぜなら、これは LLM が solver 用のバグのないソフトウェアを書けたかどうかを示しているだけだからです。
それはつまり、存在しない論理世界を丸ごと hallucinate していても通ってしまう可能性があるということです。

現実に対応していない。
自分勝手な条件を発明し、それを hallucinate しているだけかもしれない。

ですから、そういう論理世界はフィルタリングしなければいけません。

本当に重要なのは意味的正確性

次に見るべき第二の指標は accuracy です。
つまり、コンパイルされたコードが、本当に私の問題の真の意味論理を捉えているのか、ということです。

それこそが、ここで最適化したい核心的な問題だったのです。
では、それを見てみましょう。

pruning なしの青い線では、すぐに 40%ちょっとのところで plateau します。
ところが pruning ありの黄色い線を見ると、accuracy は最初から 90%近くに達しているのです。

これは興味深いですね。
こうして見ると、20 paths も本当に必要なのかと思うかもしれません。

しかし、もう一方の図を見ると、コードが syntax error なくコンパイルされるためには、やはり 20 paths が必要かもしれないとも思えてきます。
Python、翻訳、第一階述語論理、C++ wrapper、さまざまなもののあいだに面白い相互作用があるのです。

とはいえ、この pruning の性能は印象的です。

Neuro-Symbolicな推論時スケーリング

これが最後にお見せしたかった、いわば nano banana graph です。
テーマは inference time における neuro-symbolic scaling です。

LLM はたくさんの美しいアイデアを出してくれます。
20個、50個のアイデアがある。これが LLM の stochastic drafts です。

私がある特定のタスクを与えると、LLM はそうした候補を作り出します。
しかしそのあと、私たちは symbolic solver の連続体、あるいはトポロジカル空間に入っていきます。

そこでは solver が問題を厳密に検査し、これは不可能だ、これは間違っている、これは論理に反している、これは数学的あるいは論理的演繹と両立しない、と次々に言ってくれるのです。
その結果、多くの経路はそこで即座に止められます。

そして一部の経路だけが symbolic solver の中を先へ進み、最後に解へと至る。
つまり、本当に ground truth を提供してくれるのは solver なのです。

これは実に魅力的です。
そしてこの翻訳作業はすべて LLM がやっています。

post-training はまったく必要ありません。
使っているのは pre-training で獲得した知識と、3つの例による in-context learning だけです。

著者たちがテストした単純な問題については、それだけでシステムは Z3 Python solver の syntax complexity をすぐに習得できました。
数値的・記号的 solver の syntax ですね。

これは良いことです。
つまり、価値連鎖の中での LLM の位置づけが変わるのです。

LLM は、私の願い、タスク、問い合わせを理解し、それを複数の複雑度で定式化します。
そして、その先で理論物理や量子場理論などの数学的 solver が、それを理解し、解を見つける。

最終的に私は、数学的に正しい、理論物理的に正しい解を手に入れることができます。
LLM は、solver に渡すためのあらゆる可能な prompt 構造、つまり solver の特定 syntax に合わせた翻訳文を書いているだけなのです。

結論

つまり、純粋な LLM scaling だけではうまくいきません。
必要なのは、この neuro-symbolic scaling です。

symbolic solver と、純粋な数学、そして C++ による純粋な solver 演算が一緒に働くことで、はじめて本当の解が得られる。
LLM 単体では、それはできません。

この新しい研究について、少しでも楽しんでいただけたならうれしいですし、少しでも洞察が得られたなら何よりです。
AI システムだけではまだうまくいかないと知って、少しフラストレーションを感じたかもしれません。

でも、この解決策は一つの workaround です。
まずは試してみましょう。本当に機能するか見てみましょう。

私は物理学で試してみるつもりです。
また結果をご報告します。

少しでも楽しんでいただけたならうれしいです。
次の動画でまたお会いしましょう。