AI 中文总结
研究精益4研磨策略中学习干预，通过在常规研磨失败后调用，应用于内部决策，如成本感知匹配过滤器和前瞻步骤取得成效，还发现基于特征模型静态预测案例拆分效果不佳，表明学习可助决定何时及如何进行有界搜索。
AI 中文摘要
精益4的研磨策略将同余闭包、匹配和案例拆分结合到一个自动求解器中，与任何此类求解器一样，它依赖于手动调整的启发式方法来决定实例化内容和案例拆分位置。这些启发式方法是学习的诱人目标，但存在一个问题：由于研磨的搜索是非单调的，一种有助于一个证明的学习启发式方法可能会破坏另一个证明，而且总是开启的替代方法通常净收益接近零。我们通过在常规研磨失败后才调用学习干预来避免这一问题：一个由失败触发的级联，从构造上看，不会丢失研磨已经有的证明。我们将其应用于研磨的两个内部决策。一个成本感知匹配过滤器解决了更多问题，运行速度快约5%。一个前瞻步骤证明了五个原本会超时的定理。我们还报告了推动该设计的负面结果：在四个基于特征的模型中，静态预测正确的案例拆分并不比随机猜测好，因为拆分是否会爆炸是一个特征无法捕获的运行时属性。我们的结果表明，在定理证明策略中进行学习作为一种决定何时以及如何进行有界搜索的机制最为有效，并由可靠的符号回退支持。
英文摘要
Lean 4's grind tactic combines congruence closure, E-matching, and case-splitting into a single automated solver, and like any such solver, it relies on hand-tuned heuristics to decide what to instantiate and where to case-split. These heuristics are tempting targets for learning, but there is a catch: because grind's search is non-monotone, a learned heuristic that helps one proof can break another, and an always-on replacement usually nets out near zero. We avoid this by invoking a learned intervention only after stock grind has already failed: a failure-triggered cascade that, by construction, cannot lose a proof grind already had. We apply it to two of grind's internal decisions. A cost-aware E-matching filter solves slightly more problems and runs about 5% faster. A lookahead step proves five theorems it otherwise times out on. We also report the negative result that motivated the design: across four feature-based models, statically predicting the correct case split is no better than random, because whether a split explodes is a runtime property that the features do not capture. Our results suggest that learning within theorem-proving tactics is most effective as a mechanism for deciding when and how to spend bounded search, backed by a reliable symbolic fallback.
