技術要約：大規模言語モデルを用いた実行可能な思考連鎖型記号回帰（Executable Chain-of-Thought Symbolic Regression）による自動的な物理的発見

1. 問題の定式化

記号回帰（Symbolic Regression, SR）は、観測データから説明可能なコンパクトな解析法則の発見を目的とする。現代的なシステムは、遺伝的プログラミング、スパース識別、およびニューラル・シーケンス・モデルを用いてSRのスケールを拡大してきたが、依然として重大な課題が残っている。仮説空間は式の深さに伴って超指数関数的に増大し、代数的に異なる木構造であっても、有限のサンプルにおいては観測上区別がつかない場合がある。さらに、ドメイン内での誤差が低いことは、物理的に意味のある法則であることを保証しない。

LLM（大規模言語モデル）を活用した最新のアプローチは、科学的およびプログラミング的な知識を利用することで、SRに強力な事前分布を注入している。しかし、既存のLLMベースのSR手法は、通常、思考連鎖（Chain-of-Thought, CoT）を型のない自然言語のメモ書きとして扱っている。これにより、以下の3つの決定的なギャップが生じる：

1. 妥当性と有効性の乖離（Plausibility vs. Validity）： LLMは馴染みのある物理的形態を提案する可能性があるが、中間的な記述が形式的な変換になっていない場合、変換後やアンチ・メモライゼーション（記憶回避）ベンチマークにおいて失敗する。
2. 適合性と識別性の乖璃（Fit vs. Identifiability）： 複数の候補が同じサンプルを補間できる一方で、次元の再スケーリング、対称操作、または漸近極限の下では一致しない可能性がある。
3. 終端検証とプロセス検証（Terminal vs. Process Verification）： 検証は通常、生成後にのみ適用されるため、中間ステップが制約に違反した場合に探索分布を再形成することができない。

対処すべき核心的な問題は、SRを、根拠のない自然言語の論理ではなく、**型定義された導出（typed derivations）**のシーケンスに対する推論としてどのように定義するかである。ここでは、中間状態が実行可能であり、反証可能であり、かつ再利用可能であることが求められる。

2. 手法：CoT-SR

著者は、CoTを実行可能な記号的導出グラフ（Symbolic Derivation Graph, SDG）として定式化したCoT-SRというフレームワークを提案する。最終的な方程式を直接生成するのではなく、本システムは導出の軌跡 $\tau = (h_0, a_1, h_1, \dots, a_T, h_T)$ を探索する。ここで、$h_t$ は記号的な仮説であり、$a_t$ は型定義された変換である。

2.1 記号的導出グラフ (SDG)

SDGは、最適化された定数と物理的型を持つ標準化された式をノードとする有向グラフである。エッジは、以下の6つのファミリーからなる実行可能な変換を表す：

• $a_{inst}$: 実装（Instantiation）
• $a_{comp}$: 合成（Composition）
• $a_{nondim}$: 無次元化（Non-dimensionalization）
• $a_{sym}$: 対称性書き換え（Symmetry rewriting）
• $a_{limit}$: 極限書き換え（Limit rewriting）
• $a_{res}$: 残差因数分解（Residual factorization）

LLMは提案事前分布として機能し、圧縮された推論状態 $s_t$ に基づいてエッジ $(a_t, \eta_t)$ を示唆する。極めて重要な点は、LLMは最終的な法則を決定するのではなく、記号的エグゼキュータによってインスタンス化され、数値的に最適化される「アクション」を提案する点にある。

2.2 型定義された検証義務 (Typed Verification Obligations)

本フレームワークは、**厳密な許容制約（exact admissibility constraints：ハードフィルター）と経験的証拠スコア（empirical evidence scores：ソフトランキング信号）**を区別する。

• 厳密な義務（Exact Obligations）： 構文の妥当性と次元の型。単位が提供されている場合、型付き文法が次元の一貫性を強制する（例：$\log$ や $\exp$ は無次元の入力を必要とする）。これらのチェックに失敗したエッジは、事後確率がゼロとなる。
• 経験的証拠（Empirical Evidence）： 対称性の等変性、極限挙動、数値的安定性、および残差の有用性。これらは、適格な軌跡をランク付けするためにスコア化される（例：$v_{sym}, v_{lim}, v_{stab}$）が、形式的な証明にはならない。

2.3 検証重み付き軌跡事後分布

探索目的は、独立した方程式ではなく、軌跡全体に対して定義される。事後確率は以下の通りである：
$$p(\tau | D, \kappa) \propto \exp\left( \sum \log q_\theta(a_t, \eta_t | s_{t-1}, \kappa) - E(\tau) \right)$$
ここで、エネルギー関数 $E(\tau)$ は、データの適合度、記述長（最終的な法則およびエッジの複雑さ）、および検証証拠への違反に対するペナルティを含む。これにより、LLMの提案事前分布と、データの適合度および科学的制約が単一の探索目的関数へと統合される。

2.4 能動的反証 (Active Falsification)

複数の記号的法則がデータに対して同等の適合度を示す曖昧さを解消するため、CoT-SRは能動的反証ループを採用する。システムは、高事後確率を持つ記号的等価クラスが最大の予測不一致を示すプローブ位置 $x^*$ を特定する。この機能は、オラクル、シミュレータ、または実験インターフェースの利用可能性に依存する。 利用可能な場合、システムは $x^*$ においてこれらのソースにクエリを投げ、事後分布を更新し、互換性のないメカニズムを抑制または反証する。これにより、SRは受動的な曲線適合から、そのようなインタラクティブな環境が存在する場合の反復的な仮説識別へと変貌する。

3. 主な貢献

1. 実行可能な思考連鎖（Executable Chain-of-Thought）： 著者による、SRを型定義された記号的導出グラフ上の推論として定式化。自由形式の論理を、機械的にチェック可能な前提条件と事後条件を持つ代数的アクションに置き換えた。
2. 検証重み付き軌跡事後分布： データ適合度、複雑さ、および明示的な検証信号（次元、対称性、安定性）を、事後的なアドホック・フィルタとしてではなく、探索プロセスに統合した統一的探索目的関数。
3. 反例の能動的取得（Active Counterexample Acquisition）： 生き残った仮説間の不一致を最大化する新しい測定箇所を提案するメカニズム。これにより、オラクルまたはシミュレータが利用可能な設定において、反復的な科学的反証を可能にする。
4. 包括的なベンチマーク・プロトコル： Feynman, SRBench, SRSD, Nguyen, および LLM-SRBenchにわたる評価。これらは、記憶、補間、外挿、および物理的妥当性を分離するように設計された診断を含む。

4. 実験結果

評価は、厳密な回復、分布外（OOD）外挿、ノイズ耐性、および探索効率を含む複数のベンチマークに及ぶ。

• 厳密な回復（Exact Recovery）： CoT-SRは、ベンチマーク全体で平均 79.2% の厳密な回復率を達成し、PySR (55.0%)、PhySO (62.4%)、LLM-SR (69.2%) などのベースラインを大幅に上回った。この利得は、アンチ・メモライゼーション・タスク（LLM-SRBench: 61.9% vs. 42.0%）で最も顕著である。
• 複雑性： CoT-SRはよりコンパクトな式を生成する。平均演算子数は、LLM-SRの 23.4、PySRの 31.2 に対し、18.6 であった。
• OOD汎化： 外挿タスクにおいて、CoT-SRは 0.871 のOOD $R^2$ を達成し、LLM-SR (0.781) や PhySO (0.721) を上回った。これは、単なる補間ではなく、物理法則へのより高い準拠を示している。
• ノイズ耐性： 10%のガウスノイズ下において、CoT-SRは 43% の厳密な回復率を維持した（LLM-SRは 25%、PySRは 18%）。
• 探索効率： CoT-SRは、高い回復率を得るために必要なユニークな記号的仮説数 (315) およびLLM呼び出し回数 (61) が少なく、これはハードな義務による無効な分岐の早期削減によるものである。
• 能動的反証： 合成オラクルを用いたベンチマークにおいて、提案された不一致ガイド型のプローブ選択は、ランダムサンプリングや不確実性サンプリングを上回り、事後分布を正しい等価クラスへと効果的に集中させた。このモジュールは、オラクルへのクエリが許可されているタスクにおいて評価されている。
• アブレーション研究： 実行可能な導出トレースを削除すると、性能が最大（81.2% から 70.4% へ）低下し、プロセスレベルの検証の必要性が確認された。次元検証および能動的反証も、それぞれ有意かつ明確な改善をもたらした。

5. 意義と主張

本論文は、CoT-SRが、LLMを「科学的真理の神託」として扱うのではなく、「記号的アクションの事前分布」として扱うことへの転換を提示していると主張している。出力の科学的信頼性は、実行可能な環境と、導出過程で蓄積される明示的に型定義された証拠によって担保される。

著者が強調する主な相違点は以下の通りである：

• プロセス対終端検証： 「LLM + SR + 物理フィルタ」のように、チェックを最後に行うのではなく、CoT-SRは検証を探索の軌跡の中に統合している。これにより、システムは単に最終候補を破棄するのではなく、失敗した変換の場所や種類を利用して探索を再方向付けすることができる。
• 監査可能な出力： 最終出力は単なる方程式ではなく、方程式、実行可能な導出トレース、および機械的にチェック可能な証拠記録を含む「検証を伴うアーティファクト」である。これにより、科学者はどの制約（例：次元、漸近挙動）が特定の代替案を排除したのかを正確に検証できる。
• 主張の謙虚さ： 著者は、数値的チェック（対称性、安定性）は形式的な証明ではなく、あくまで経験的証拠であることを明記している。また、提供されたメタデータ（単位、対称性）への依存や、現在の焦点が偏微分方程式（PDE）や確率的法則ではなく、閉じた形式のスカラー関係にあるといった限界も認めている。極めて重要な点として、能動的反証コンポーネントは、識別的な測定を提供するオラクルまたはシミュレータが存在するシナリオに限定されている。

本研究は、自動科学において、生成的な事前分布（LLM）と、機械的にチェック可能な制約および反証証拠を分離することが、堅牢で物理的に意味のある発見を生み出すために不可欠であることを示唆している。