Lean 4 grind中的学习型干预

# Lean 4 的 `grind` 中的学习式干预

来源：https://arxiv.org/html/2607.22972

###### 摘要

Lean 4 的 `grind` 策略将同余闭包、`e`-匹配和分支分解整合到单个自动化求解器中，并且与任何此类求解器一样，它依赖手动调优的启发式方法来决定实例化什么以及在哪里进行分支分解。这些启发式方法是学习的诱人目标，但有一个问题：由于 `grind` 的搜索是非单调的，一个对某个证明有帮助的学习式启发式方法可能会破坏另一个证明，而始终开启的替换通常净效果接近零。我们通过在库存版 `grind` 已经失败后才调用学习式干预来避免这种情况：一个由失败触发的级联，通过构造，它不会丢失 `grind` 已有的证明。我们将其应用于 `grind` 的两个内部决策。一个成本感知的 `e`-匹配过滤器解决了更多问题，运行速度也快了约 5%。一个前瞻步骤证明了五个原本会超时的定理。我们还报告了驱动该设计的负面结果：在四个基于特征的模型中，静态预测正确的分支分解并不比随机选择好，因为分支分解是否爆炸是一个运行时属性，而这些特征无法捕捉。我们的结果表明，定理证明策略中的学习作为决定何时以及如何花费有限搜索的机制最为有效，并辅以可靠的符号回退。

Lean 4, `grind`, 前提选择, 前瞻, 定理证明, 机器学习

---

## 1 引言

自动化定理证明器越来越依赖少量强大的策略作为其后端推理引擎。这使得这些策略的内部搜索决策成为学习的高杠杆目标：改进单个分支、实例化或剪枝启发式方法可以影响许多下游的证明尝试。同时，这些决策很难安全地学习。一个局部看起来更好的启发式方法可能会改变符号搜索的形状，从而产生新的爆炸式增长，导致原本可以被原始策略解决的目标准入回归问题。

我们在 `grind`（Lean FRO, 2024 (https://arxiv.org/html/2607.22972#bib.bib1)）中研究这个问题，这是 Lean 4 证明助手（Moura and Ullrich, 2021 (https://arxiv.org/html/2607.22972#bib.bib2)）的一个较新策略。它通过在同余闭包、基于 `e`-匹配的引理实例化和分支分解的单一过程中组合 SMT 风格的自动化（Moura and Bjørner, 2008 (https://arxiv.org/html/2607.22972#bib.bib4)）将其集成到 Lean 中。它的许多决策都是启发式的：保留哪些 `e`-匹配实例，下一步分解哪个目标，以及以什么顺序探索产生的分支。单个证明可能涉及数千个这样的选择，这使得 `grind` 成为一个自然的地方，用来询问学习指导是否有帮助。

大多数交互式定理证明的机器学习工作都作用于策略或证明步骤层面，如第 2 节 (https://arxiv.org/html/2607.22972#S2) 所述。相反，我们查看一个策略内部，并修改其一些内部选择，而不是替换策略本身。这保持了原始搜索过程在循环中：库存版 `grind` 既提供基线也提供回退。

主要的复杂之处在于 `grind` 的搜索是非单调的。`e`-匹配可能增长得非常快，因此一个短期内看似更好的选择可能会使整体搜索变得更糟。在我们的实验中，始终开启的学习式替换具有这种特性：它们解决了一些库存版 `grind` 遗漏的目标，但也破坏了库存版 `grind` 已经能够证明的目标。因此，我们更保守地使用学习。我们不是尝试从静态特征预测正确的选择，而是在库存版 `grind` 失败后触发一个廉价的前瞻。这给出了一个由失败触发的级联：首先尝试库存版 `grind`，并且仅对未解决的目标应用干预。结果，干预不会危及 `grind` 已经解决的证明。

我们用可运行的 Lean 代码评估这种设计。我们的实现包括一个成本感知的 `e`-匹配过滤器和一个前瞻步骤，该步骤证明了一些超越库存版 `grind` 的定理。我们还报告了一个负面结果：用于预测下一个分支分解的静态模型表现不比随机选择好。因此，教训并非神经网络模型应该取代 `grind` 的启发式方法，而是学习最好用于定位静态选择失败的地方，并在符号回退背后引导有限搜索。

我们的主要贡献是：

1.  我们将失败触发的学习式干预形式化为一种在非单调定理证明策略内部进行学习的安全部署模式。
2.  我们在 `grind` 内部实现了两个 Lean 原生干预：一个成本感知的 `e`-匹配过滤器和一个用于分支分解的有界前瞻过程。
3.  我们展示这些干预在定理层面提升了性能，且不牺牲基线解决率：`e`-匹配过滤器在 855 个留出定理上带来了微小的速度和成功提升，而前瞻级联以零回归拯救了五个原本库存版 `grind` 会超时的定理。
4.  我们展示了对于可挽救的分支分解决策，静态特征预测是不够的：四个学习策略在最关键的地方未能击败随机选择，这表明分支爆炸主要是搜索的一个动态属性。

---

## 2 相关工作

### SAT 和 SMT 中的学习式启发式方法

我们研究的选择——分支的目标和保留的实例化——接近于 SAT 和 SMT 求解器中使用的分支、重启和实例化启发式方法。关于学习此类启发式方法有长期的工作。NeuroSAT（Selsam 等, 2019 (https://arxiv.org/html/2607.22972#bib.bib15)）通过单比特监督学习求解器；Graph-Q-SAT（Kurin 等, 2020 (https://arxiv.org/html/2607.22972#bib.bib16)）使用图网络作为 CDCL 的分支策略；而 FastSMT（Balunović 等, 2018 (https://arxiv.org/html/2607.22972#bib.bib17)）学习组合 Z3 策略策略。这些系统从特征评估当前状态。我们的分支分解拯救实验表明，这对于 `grind` 内部的选择是不够的：在高影响决策上，静态评分不比随机选择好（表 1 (https://arxiv.org/html/2607.22972#S5.T1)）。问题在于一个分支的成本通常在采取之后才可见。因此，我们的积极结果使用前瞻而不是纯粹的静态预测。

### E-图和等式饱和

`grind` 通过同余闭包维护一个 e-图，这与等式饱和系统（如 egg（Willsey 等, 2020 (https://arxiv.org/html/2607.22972#bib.bib18)））使用的基本数据结构相同。在这些系统中，一个核心问题是通过决定何时应用重写规则来控制 e-图增长。我们的 `e`-匹配过滤器解决了 `grind` 内部的类似问题：它试图在低价值实例化被添加到 e-图之前丢弃它们。这个过滤器的失败也很有用。附录 B (https://arxiv.org/html/2607.22972#A2) 中描述的重尾、引理多样的爆炸表明，简单的剪枝规则不足以在所有情况下控制增长。

### 交互式定理证明中的学习

交互式定理证明中大多数基于学习的工作作用于策略或证明步骤层面。例子包括生成证明步骤的语言模型（Polu and Sutskever, 2020 (https://arxiv.org/html/2607.22972#bib.bib7); Yang 等, 2023 (https://arxiv.org/html/2607.22972#bib.bib9)）、学习策略策略（Gauthier 等, 2021 (https://arxiv.org/html/2607.22972#bib.bib10)）和神经指导的证明搜索（Lample 等, 2022 (https://arxiv.org/html/2607.22972#bib.bib8); Silver 等, 2018 (https://arxiv.org/html/2607.22972#bib.bib6)）。前提选择和榔头系统则检索有用的引理用于外部证明器（Alemi 等, 2016 (https://arxiv.org/html/2607.22972#bib.bib11); Blanchette 等, 2016 (https://arxiv.org/html/2607.22972#bib.bib12); Czajka and Kaliszyk, 2018 (https://arxiv.org/html/2607.22972#bib.bib13)）。我们的设置不同：我们保持策略固定，只学习其内部的一些选择。这保持了原始符号搜索作为基线和回退。

### 算法选择和组合

我们的失败触发级联与算法选择和组合求解器（如 SATzilla（Xu 等, 2008 (https://arxiv.org/html/2607.22972#bib.bib19)））有关。组合方法通常基于实例的特征预先选择一个求解器或配置。我们的级联在更晚的时间做出决策。它首先运行库存版 `grind`，然后仅在未解决的目标上调用学习过程。这避免了提前预测学习是否有帮助，而这正是静态特征在我们的实验中处理得很差的预测问题。

---

## 3 将学习集成到 `grind` 中

`grind` 运行一个动作循环，可以模式化地看作：

```
solvers ▷ instantiate ▷ splitNext ▷ mbtc.
```

该循环重复进行，直到达到不动点或心跳用尽。每次通过时，子求解器传播已知事实、实例化引理、分解目标或关闭分支。

我们在不分支策略的情况下，在三个地方可以插入学习指导：(i) `e`-匹配实例过滤器，可以在低价值实例化进入同余结构之前丢弃它们；(ii) 分支目标选择，由 `splitNext` 实现；(iii) 前提增强，在搜索开始前选择要断言的事实。一切都是 Lean 原生且具有亚毫秒延迟。我们在附录 A (https://arxiv.org/html/2607.22972#A1) 中总结了数据、特征和留出评估协议。

学习组件故意很小。在这种设置中，模型应用的位置比其大小更重要，我们在附录 B (https://arxiv.org/html/2607.22972#A2) 中的缩放结果支持这一点。`e`-匹配过滤器是一个二元分类器，对每个候选实例化的证明相关性进行评分——它是否会在最终证明项中出现。它使用被实例化引理的特征，包括其标识、头部符号、结论标记和前提标记；当前目标的匹配特征；以及一些数值信号，如 `e`-匹配轮次和该引理之前被证明有用的次数。这些形成一个 135 维的向量，输入到一个三层 MLP (135→64→32→1) 中，使用二元交叉熵训练。分支研究模型同样小：在目标和候选级别特征上的 MLP 和梯度提升树（附录 C (https://arxiv.org/html/2607.22972#A3)）。

---

## 4 改进 1：成本感知的 `e`-匹配过滤器

`e`-匹配（Moura and Bjørner, 2007 (https://arxiv.org/html/2607.22972#bib.bib3)）将量化引理实例化到当前 e-图上，该 e-图由同余闭包（Nelson and Oppen, 1980 (https://arxiv.org/html/2607.22972#bib.bib5)）维护。许多实例化对证明没有帮助，但它们仍然消耗工作——每个匹配都会增加事实或项，后续求解器组件必须维护，而单个量化引理可能以多种方式匹配。

我们在每个实例特征上训练一个轻量级分类器，并在 `e`-匹配调用点使用它来丢弃低价值实例化。在一个包含 855 个定理的留出测试集上，该过滤器运行速度快约 5%，并且额外比库存版 `grind` 多解决了 +2 个定理。训练数据扩大 20 倍并未拓宽其适用范围，这表明引理标识机制存在局限性，而非示例不足。因此，我们将该过滤器视为一个有用的速度组件，也是静态评分不足之处的证据。

---

## 5 改进 2：用于分支分解的前瞻

当 `e`-匹配和同余闭包停止取得进展时，`grind` 回退到分支分解。它选择一个事实并分支到其可能的情况上，例如 `x = 0` 与 `x ≠ 0`，然后在每个分支上分别继续搜索。分支目标从一个候选池中使用固定的数值打破平局选择。一个好的分支分解可能很快关闭目标，而一个糟糕的分支分解可能创建分支，这些分支会增长直到策略超时。

为了研究这个选择，我们使用了一个预言机实验。在每个有多个候选的决策点，我们强制依次测试每个候选，固定证明的其余部分重新运行 `grind`，并记录结果。每个强制运行都是选择该候选的政策的实际执行。总共，我们收集了来自 `numina` 上 4,120 个多候选决策点的大约 16K 个强制选择结果。

### 主要好处在于能力而非速度。

一个总是选择最廉价分支分解的预言机将分支分解的总数仅减少约 4%。更有趣的情况是库存版 `grind` 的失败。在 675 个决策点中，`grind` 选择的分支分解导致超时。在这些决策点中，有 97 个（14%）至少有一个在同一时间点可用的其他分支分解可以在没有新引理或额外搜索的情况下关闭目标。我们将这些称为可挽救的失败：它们是那些仅仅选择另一个可用候选就能挽救证明的决策点。

例如，在像 `1/(x+1) + 1/(x+2) = 1/x` 这样的有理方程中，`grind` 可能会分支到一个事实，使一个分支进入爆炸状态并最终超时。另一个可用的分支分解会在几步之后关闭目标。在这些可挽救的决策点上，库存版 `grind` 的挽救率按构造为 0%，而均匀随机的替代方案成功率为 57%；参见表 1 (https://arxiv.org/html/2607.22972#S5.T1)。这为更好的分支分解策略留下了空间。

### 静态预测在可挽救的失败上没有击败随机选择。

我们尝试了四种选择挽救分支分解的策略：一个梯度提升成本模型（Chen and Guestrin, 2016 (https://arxiv.org/html/2607.22972#bib.bib20)）、一个在留出成本指标上验证的生成排序规则、一个厄运/价值模型，以及一个失败感知的成功分类器（在逐决策留出数据上候选 AUC 0.85）。在可挽救的决策点上，没有一个优于随机选择；参见表 1 (https://arxiv.org/html/2607.22972#S5.T1)。这些模型在整体上有很强的聚合指标，可能对简单或中位数决策有帮助，但恰好是在 `grind` 自身启发式方法出错的决策点上，静态模型的预测与 `grind` 的信号高度相关，以至于它们倾向于以相同的方式犯错。缺失的信息是分支分解是否会导致分支爆炸，这似乎是一个动态属性，而不是由我们的静态特征所捕捉到的，如附录 C (https://arxiv.org/html/2607.22972#A3) 所述。

**表 1：静态特征策略在可挽救的分支分解失败上没有击败随机选择。前瞻成功是因为它尝试分支分解，而不是从静态特征预测其结果。**

| 策略（针对可挽救的分支分解失败） | 挽救率 |
| --- | --- |
| `grind`（库存启发式方法） | 0% |
| GBM 成本模型 / 生成规则 | 30–46% |
| 价值-厄运 / 失败感知分类器 | 46–53% |
| 均匀随机 | 57% * |
| **1-步前瞻（已实现）** | **100% *** |

前瞻通过将分支分解选择转变为一个小型实验来捕捉大部分好处。对于每个候选，该策略制作一个目标的临时副本，强制在该副本上进行分支分解，并在副本上运行 `grind` 有限步数。当这个有界子搜索在副本中证明目标时，我们说一次试验关闭；父策略提交给第一个这样的候选，并丢弃其他副本。由于试验实际执行了分支分解，它观察到了静态模型所遗漏的动态行为。因此，问题不在于前瞻能否识别出挽救的分支分解，而在于尝试它需要多少成本。

在可挽救的决策点上，一个时间上限为 15 秒的试验恢复了 90% 的可挽救失败。即使