技術的サマリー：等式発見における飽和スケーリング則

問題定義

本論文は、等式書き換え規則の追加によって成長する決定論的記号発見システムが、大規模言語モデル（LLM）で見られる経験的スケーリング則に類似した法則に従うかどうかを調査する。ニューラルモデルのスケーリング則（Kaplan et al., 2020; Hoffmann et al., 2022）は確立されているが、帰納的論理プログラミング、等式飽和、プログラム合成などで用いられるような決定論的基盤が、同様の成長ダイナミクスに従うかどうかは未解決の課題である。著者らは、これらのシステムにおける成長の現象論を特徴付け、発見された規則の蓄積を記述するのに単純なべき乗則がより適切か、それともより複雑な飽和関数がより適切かを検証することを目的としている。

手法

本研究は、タイプ付けの複雑さが増す 3 つの「玩具的」決定論的基盤を含む制御された実験フレームワークを採用している：

1. 算術（arith）： 加算、乗算、自由変数を含むタイプ付き文法上の等式恒等式。
2. ブール（bool）： 論理演算子（and、or、not）上の恒等式。
3. 高次リスト（list）： map、fold、cons などのプリミティブを持つ DreamCoder 由来のドメイン。

発見ループ：
システムは離散ステップ $t$ において基盤 $S$（書き換え規則の集合）を成長させる。各ステップにおいて：

• 生成器は、$S$ の現在の状態に基づいて候補等式を提案する（ランダム、構成的、頻度重み付け、または MDL-貪欲などの戦略を使用）。
• 候補は、ランダムなインスタンス化を通じて意味的妥当性がテストされる。
• 承認されたペアは一般化される（自由変数をパターン変数に置換）。
• 設定可能な承認フィルタ（「any」または「novelty」）が、規則が $S$ にコミットされるかどうかを決定する。

データ収集：
著者らは、5 つのアーキテクチャ特徴（生成器タイプ、フィルタの厳格さ、再帰深度、バッチサイズ、ランダムシード）を変化させて、これらの基盤全体で 592 個の独立した発見軌跡を生成した。彼らは時間経過に伴う総規則数 $|S(t)|$ を測定した。

モデリングアプローチ：
著者らは、均一なカバレッジと近似独立性の仮定から導出されたヒューリスティックな平均場閉鎖モデルを提案する。これにより、成長に関する微分方程式が得られる：
$$\frac{dN}{dt} = K \cdot N^k \cdot e^{-\mu N}$$
ここで、$N$ は基盤のサイズ、$k$ は生成器の再結合深度に関連し、$\mu$ は候補空間のカバレッジ割合を表す。

• 短距離（$\mu N \ll 1$）： 方程式は純粋なべき乗則 $N(t) \propto t^b$（ただし $b = 1/(1-k)$）を近似する。
• 長距離（$\mu N \gtrsim 1$）： 指数項が飽和を引き起こし、ロジスティックべき乗則形式でモデル化される。

本研究は、モデル選択に AIC を、アーキテクチャ特徴から指数 $b$ を予測するために勾配ブースティング回帰を用いて、3 つの候補モデル（純粋なべき乗則、引き伸ばされた指数関数、飽和べき乗則）をデータに適合させた。

主要な貢献と結果

1. 短距離のべき乗則ダイナミクス

592 の軌跡全体において、基盤サイズ $|S(t)|$ の成長は短距離（最大 30 エポック）で一貫してべき乗則形式 $t^b$ に適合する。指数 $b$ は、ドメインとアーキテクチャに応じて 0 から 1.15 の間で連続的に変化する。

• アーキテクチャ感受性： 単一の基盤内において、指数 $b$ はアーキテクチャの選択に非常に敏感である。5 つのアーキテクチャ特徴を用いた勾配ブースティング回帰器は、算術/ブールおよびリストの両方のドメインにおいて、交差検証された $R^2 \approx 0.82$ で $b$ を予測する。
• 基盤間転移の失敗： 算術およびブールデータ上で $b$ を予測するように訓練されたモデルは、リストドメインに適用された場合、完全に失敗する（$R^2 \approx -0.84$）。平坦なタイプ付き基盤における複合成長に最適なアーキテクチャ（例えば novelty フィルタ）は、高次タイプ付き基盤における成長を抑制する。これは、成長ダイナミクスが普遍的ではなく、基盤条件付きであることを示している。

2. 長距離の飽和仮説

著者らは、閉鎖モデルが予測するように成長が最終的に飽和するかどうかをテストした。

• 玩具データ（リストドメイン）： リストドメインの 5 つの軌跡を 500 エポックに延長すると、200 エポックを超える軌跡において、飽和べき乗則モデルがインサンプルの AIC 比較で勝利する。しかし、アウトオブサンプル予測（最初の 100 エポックに適合させ、次の 400 エポックを予測）は、5 つのケースすべてで純粋なべき乗則によって勝利する。著者らは、玩具軌跡は実際には 500 エポック以内に飽和領域に到達していないと結論づける。インサンプルにおける飽和モデルの選好は、おそらく外挿が不十分な適合のアーティファクトである。
• 実世界データ（Mathlib4）： Mathlib4 ライブラリにおける月次の新しい .lean ファイルの追加（60 ヶ月、9,701 ファイル）の分析は、飽和形式を支持する。飽和モデルは、アウトオブサンプル予測において純粋なべき乗則を約 7 倍（RMSE 3,279 対 23,896）上回り、Mathlib4 が飽和領域に到達したことを示唆している。
• 実世界データ（Coq Mathcomp）： Coq Mathcomp ライブラリにおける月次コミットの分析（129 ヶ月）は、純粋なべき乗則を支持する。飽和パラメータ $\mu$ はゼロに崩壊し、純粋なべき乗則はアウトオブサンプル予測において飽和モデルを約 67 倍上回る。これは、Mathcomp がまだ飽和領域に到達していないことを示唆している。

3. 現象論的枠組み

本論文は、以下の作業枠組みを提案する：「飽和領域に達した基盤で観測可能な、基盤条件付き $(k, \mu)$ を伴う飽和べき乗則成長」。ダイナミクスは 2 つのレベルで条件付きである：

1. 成長指数を予測するアーキテクチャパラメータは、異なる基盤タイプ間で転移しない。
2. 成長を記述する関数ファミリー（純粋対飽和べき乗則）は、基盤の特定のライフサイクル段階に依存する。

意義と主張

本論文は、決定論的等式発見のスケーリング則に関する最初の経験的かつ理論的調査として位置づけられ、決定論的な理論ではなく現象論を提供する。

• 控えめな範囲： 著者らは明確に、証拠が 3 つの玩具的基盤と 2 つの実世界の代理（コミット数/ファイル数に依存する粗いもの）に限定されていると述べている。彼らは、玩具データにおけるアウトオブサンプル予測の失敗により、長距離の玩具結果は「確認されたものではなく、整合的なもの」であると認めている。
• 主要な洞察： 主要な発見は、記号発見ダイナミクスが基盤条件付きであるということである。アーキテクチャ全体で普遍性を仮定することが多いニューラルスケーリング則とは異なり、ここでの成長挙動は、基盤のタイプシステムの特定の「閉鎖幾何学」（カバレッジパラメータ $\mu$）に大きく依存する。
• 将来の方向性： 著者らは、この作業を「玩具的現象論」から「真の現象」へと引き上げるために必要な 3 つの具体的なアップグレードを特定している：
  1. コミット数だけでなく軌跡レベルの詳細さを持つ非玩具的基盤での再現。
  2. 飽和モデルに対する成功したアウトオブサンプル予測的予測。
  3. 基盤の組み合わせ論（例えば、タイプエントロピー）から飽和パラメータ $\mu$ の理論的導出を行い、基盤間転移を反証可能にする。

本論文は、飽和が妥当な領域において観測データと整合的である飽和べき乗則フレームワークは、すべての記号発見システムに対する普遍的な法則ではないと結論づけている。この作業は、潜在的な「記号発見の統計力学」のための出発点として機能する。