等式发现中的饱和标度律：三个玩具基底与两个现实世界复现中的增长动力学现象学

# 等式发现中的饱和缩放定律 三个玩具基板中增长动力学的现象学
来源：https://arxiv.org/html/2605.23983
（2026年5月14日）

###### 摘要

我们研究了确定性等式发现基板中的增长动力学。在三个玩具领域（算术、布尔、高阶列表；n=592条轨迹）中，短程基板尺寸符合幂律N(t) ∝ t^b。在每个基板内部，b对架构敏感（交叉验证R² ≈ 0.82）；该回归*不能*跨基板迁移（算术+布尔 → 列表产生R² ≈ -0.84）。一个启发式的平均场封闭模型预测了一个饱和幂律dN/dt = K·N^k·e^{-μN}，其中纯幂律是其短程近似。三个鲁棒性检验：在4/5的玩具轨迹中(k, μ)的自举区间紧凑，而在1/5中退化；玩具数据上的样本外预测（拟合前100个周期，预测后400个）在5/5情况下由纯幂律获胜，表明玩具轨迹未达到饱和；在两个现实世界增长代理变量上结果出现分歧。NewMathlib/*.lean文件每月新增数量（mathlib4，60个月，9,701个文件）支持饱和形式，在样本外预测上优于纯幂律约7倍；Coq mathcomp每月提交数（129个月，3,083个提交）在两个测试中均倾向于纯幂律，且μ→0。动力学在两个层面是基板条件性的：基板内部架构到b的回归不能迁移，且N(t)本身的首选函数族（纯幂律 vs. 饱和幂律）因基板而异。我们提出“饱和幂律增长，具有基板条件性(k, μ)，当基板达到其饱和状态时可观测”作为工作框架。

## 1 引言

实证缩放定律已经塑造了大语言模型的工程实践（Kaplan et al., 2020 (https://arxiv.org/html/2605.23983#bib.bib1); Hoffmann et al., 2022 (https://arxiv.org/html/2605.23983#bib.bib2)）。它们刚刚开始被扩展到*发现系统*，即那些随时间通过添加规则、引理、程序或架构而增长的基板（Liu et al., 2025 (https://arxiv.org/html/2605.23983#bib.bib3); Ellis et al., 2021 (https://arxiv.org/html/2605.23983#bib.bib4); Nandi et al., 2021 (https://arxiv.org/html/2605.23983#bib.bib5)）。*确定性*符号发现——那种推动了归纳逻辑编程、等式饱和和程序综合数十年工作的方式——是否遵循类似的缩放定律，仍然是一个开放问题。

本文为玩具基板中的确定性等式发现提供了首次实证和理论研究，旨在作为现象学而非最终理论。

我们提出四个观察结果，其局限性在§6 (https://arxiv.org/html/2605.23983#S6)中说明。

1.  实证缩放定律。在跨越三个基板和七个架构自由度的592条独立发现轨迹中，基板尺寸|S(t)|在短程内遵循幂律形式t^b，其中b在算术和布尔中∈[0, 1.15]，在高阶列表域中∈[0, 0.99]。
2.  基板内部可预测性。基于五个架构特征（生成器类别、合理性过滤器严格度、递归深度、批大小、随机种子）的梯度提升回归预测轨迹指数b，在算术+布尔（n=344）中交叉验证R²=0.815±0.052，在列表域（n=248）中R²=0.818±0.073。
3.  跨基板迁移失败。在算术+布尔上训练的回归预测列表域b时得到R² = -0.84，*比*预测基板均值*更差*。促进增长的优化架构在基板间相反：在扁平类型基板中放大增长的新颖性过滤器，在高阶类型基板中抑制增长。添加`domain`作为类别特征可恢复R²=0.88。
4.  一个饱和封闭模型在某些状态下与数据一致，在其他状态下则不然。我们勾勒了一个现象学平均场推导，基于基板重写系统的均匀覆盖和近似独立假设，得到dN/dt = K·N^k·e^{-μN}。纯幂律t^b是短程近似；饱和开始于N ~ 1/μ。我们通过三个鲁棒性检验来测试该预测：在4/5的玩具轨迹中(k, μ)的自举区间紧凑，在1/5中退化；玩具数据上的样本外预测在5/5情况下由纯幂律获胜，表明玩具未达到饱和；在两个作为月度增长代理的现实世界基板上，结果出现分歧：mathlib4（新增.lean文件，60个月，9,701个文件）支持饱和形式，在样本外预测上优于纯幂律约7倍，而Coq mathcomp（129个月，3,083个提交）在两个测试中均倾向于纯幂律，且饱和项μ→0。饱和是否可观测似乎取决于基板在其自身生命周期中所处的位置。

#### 意义。

在测试的范围内，符号发现的动力学在两个层面是基板条件性的：预测基板内部b的架构参数不能跨基板迁移（R² ≈ -0.84），且N(t)本身的首选函数族（纯幂律 vs. 饱和幂律）因基板而异。我们提出“饱和幂律增长，具有基板特定的(k, μ)，当基板自身的生命周期达到饱和时可观测”作为工作框架。

## 2 设置

#### 基板。

一个*发现基板* S是一个有限的有类型等式重写规则(l, r)的集合。该系统通过从有类型项语法提出候选规则、通过随机实例化检查其语义合理性、并提交那些通过可配置接受过滤器的规则，逐渐增加发现步骤t∈N。

我们实例化三个打字复杂性递增的基板：

- • arith：在类型语法(+, *, x, y, z, 0, 1, 2)上的等式恒等式，包含3个自由变量。
- • bool：在(and, or, not, p, q, r, 0, 1)上。
- • list：受DreamCoder启发（Ellis et al., 2021 (https://arxiv.org/html/2605.23983#bib.bib4)）的高阶列表域，包含原语map、filter、fold、reverse、length、append、cons以及整数算术（+, -, *）；六个命名单参数函数（inc、dec、double、square、neg、id）；以及六个谓词（is_pos、is_neg、is_zero、nonzero、is_even、is_odd）。

#### 发现循环。

每步，系统：(i) 从*生成器*（随机、从基板派生子项的组合、频率加权、或MDL-贪婪趋向大子项）生成一批K个候选等式；(ii) 在随机环境（每对12个样本，布尔域进行全面8世界检查）下测试语义等价性；(iii) 通过将自由变量替换为模式变量来泛化已接受的配对；(iv) 如果可配置的*接受过滤器*拒绝该候选（`any`接受所有合理规则，`novelty`拒绝那些左侧已在当前S中可推导的规则），则丢弃该候选；(v) 将接受的规则提交到S。

该框架为750行Python代码。每周期墙钟时间在0.1毫秒到10秒之间，取决于架构和|S|。完整的A+B阶段扫描（n=592）在八核上不到三小时运行完成。

#### 因变量。

我们测量|S(t)|，即t个发现步骤后已提交的规则总数。以下所有缩放定律均拟合到这个单一量，对数-对数坐标。

## 3 一个现象学封闭模型

我们勾勒一个*平均场、现象学*封闭模型，以推导N(t) ≡ |S(t)|的期望形式。该推导是启发式的，并依赖于两个明确的简化假设（下面的A1, A2），这些假设忽略了规则重叠结构、非均匀候选分布以及封闭相关性；我们将这些假设明确列出，因为更严格的处理需要替换它们。

#### 生成器增长。

在第t步，生成器产生的候选数量与K·g(S)成比例，其中对于随机生成器g(S)=1，而对于有效重组深度k的组合、频率加权或MDL-贪婪生成器，g(S) ∝ |S|^k。

#### 覆盖与封闭。

每个规则(l, r)∈S重写类型候选空间的一个小部分μ∈(0,1)。对于窄类型基板（具有高阶运算符的list），μ很小；对于扁平类型基板（arith, bool），μ较大。在近似独立下，由于新颖性过滤器明确强制非冗余，因此可以说一个随机候选*不*被任何规则覆盖的概率是

ρ(S) = (1−μ)^|S| ≈ e^{-μ·|S|} (1)

对于小的μ。

#### 增长ODE。

结合：

dS/dt = K·g(S)·ρ(S) = K·S^k·e^{-μ·S} (2)

#### 短程（μS ≪ 1）。

e^{-μS} ≈ 1且dS/dt = K·S^k，积分得到纯幂律：

S(t) = ((1−k)·K·t)^{1/(1−k)} = t^b, 其中 b = 1/(1−k)。 (3)

#### 长程（μS ≳ 1）。

指数项使得dS/dt → 0。一个贴合两种状态的实用替代是*逻辑-幂律*：

S(t) ≈ \frac{a·t^k}{1+μ·t^k} (4)

该形式允许标准非线性最小二乘拟合。

#### 三个预测。

1.  短程缩放：对于k<1，纯幂律b = 1/(1−k)。
2.  在|S| ∼ 1/μ处饱和转变：低于此值，幂律拟合良好；高于此值，在模型选择下，饱和形式(4)优于纯幂律和拉伸指数。
3.  基板特定的μ：架构到b的回归跨基板迁移会失败，除非μ被编码在特征中，而实际上并非如此，因为生成器/过滤器/深度/批处理旋钮并不索引基板的覆盖几何。

所有三个预测在§5 (https://arxiv.org/html/2605.23983#S5)中测试。

## 4 实验

#### 架构扫描。

我们扫描五个特征：`generator ∈ {random, compositional, freq, mdl_greedy}`；`filter ∈ {any, novelty}`；`depth ∈ {2, 3, 4}`；`batch_size ∈ {40, 60, 80, 120, 160}`；`seed ∈ {0, ..., 4}`。

#### 轨迹阶段。

A+B阶段短程：每条轨迹30个周期，arith+bool n=344，list n=248。长程：500个周期，list域 n=5，使用compositional + any + depth=2 + bs=80。

#### 拟合。

对每条轨迹拟合三个候选增长律（幂律、拉伸指数、饱和幂律），并通过AIC进行比较。

#### 架构回归。

一个梯度提升回归器（sklearn的GradientBoostingRegressor，200个估计器，max_depth=3）基于5特征架构向量预测b。通过5折K折交叉验证（shuffle，种子=0）得到R²和MAE。

#### 跨基板回归。

仅用arith+bool训练；在list上测试。R² < 0表示模型比预测基板均值更差。

#### 基准。

Popper（Cropper and Morel, 2021 (https://arxiv.org/html/2605.23983#bib.bib6)）在一个由6个难度递增的亲属关系风格发现任务（父亲、母亲、祖父、祖先、儿子、女儿）组成的序列上运行，每个任务学到的谓词会添加到下一个任务的背景知识中。

## 5 结果

### 5.1 幂律形式，状态依赖的指数

在344+248条短程轨迹中，规则计数轨迹拟合幂律t^b，b值从0到1.15连续变化。

表1：按基板划分的短程幂律指数b分布。列表域的分布是双峰的：42%的配置由于新颖性过滤器拒绝几乎所有候选而坍缩到b≈0，而剩余的58%在[0.4, 1.0]上连续分布。在扁平类型基板中放大增长的新颖性过滤器，在高阶类型基板中则抑制增长，我们在§6 (https://arxiv.org/html/2605.23983#S6)中解释这种现象。

### 5.2 基板内部的b对架构敏感

拟合的短程指数b在各自基板内部可从架构特征回归得到：在arith+bool上交叉验证R²=0.815±0.052，在list上R²=0.818±0.073，两种情况下MAE均低于0.10。我们不将此解释为强烈的预测成就，该回归是一个在小型合成特征集上的200棵树GBR，不应过度解读为神经缩放定律拟合的类比。它显示的是，在固定基板内部，短程增长动力学并非架构不变：生成器、过滤器、深度或批大小的微小变化会产生显著不同的b值。该回归是否*跨*基板迁移将在下面测试，这是更具实质性的问题。

参见图注图 1：A+B 阶段在 arith+bool：留出缩放定律预测（R²=0.815）、b 的分布、按生成器划分的 b 与批大小关系、前 12 个架构。

### 5.3 跨基板迁移失败（R² = -0.84）

仅用 arith+bool（n=344）训练回归；在留出的列表域轨迹（n=248）上测试：

R² = -0.84，MAE = 0.376，b̂的均值 = 0.70，b的均值 = 0.36。
回归无法迁移。从机制上讲，模型学会了在 arith+bool 中 `novelty` + `mdl_greedy` + bs≥120 产生高 b，并将该经验应用于 list，而在 list 中相同的架构*摧毁了*增长。在合并回归中添加 `domain` 作为类别特征可恢复 R²=0.883±0.024。

参见图注图 2：跨基板迁移失败。左：预测 vs. 实际 b，arith+bool → list，R²=-0.84。中：列表域 b 分布（n=248，均值 0.36，双峰）。右：R²比较，基板内部 +0.82，跨基板 -0.84，使用 `domain` 特征的合并回归 +0.88。Domain 是一个非冗余特征。我们使用的架构旋钮并未编码基板的封闭几何；§3 中的 μ 是缺失的变量。

### 5.4 长程：与 n=5 一致的假设

该证据的范围。我们将五条列表域轨迹扩展到 500 个周期（约 N 的 3 个数量级），并在六个轨迹窗口拟合所有三个候选增长律。我们预先强调，这仅仅是单个域、单个架构族（compositional + any + depth=2 + bs=80）的 n=5 条轨迹；在相关轨迹上的 AIC 判别可能不稳健，并且饱和形式是从一个小候选集中选出的，部分原因是因为它是我们的封闭模型所预测的。我们将本节视作与饱和假设*一致*的证据，而非确认。该设计的局限性在 §6 (https://arxiv.org/html/2605.23983#S6) 中列出。

表 2：按用于拟合的轨迹长度划分的 AIC 获胜者。在每个窗口≥200 个周期时，饱和幂律在每条轨迹中都获胜。在所有≥200 个周期的窗口中，饱和幂律 (4) 在所有情况下都优于纯幂律和拉伸指数。