让机器学习在证明失败后介入，提升自动化推理效率。
Learned Interventions in Lean 4 grind
- 失败后才启动学习干预，避免干扰原有成功路径。
- 新方法使证明成功率略升，运行速度提升5%。
- 适合需要可靠符号回退的自动化证明场景。
Lean 4 的 grind 策略将合一闭包、E-匹配和分支拆分整合为单一自动化求解器，其性能依赖于手工调优的启发式规则来决定实例化与分支位置。这些规则虽适合学习，但因 grind 搜索非单调，学习到的启发式可能帮助一个证明却破坏另一个，持续替换通常净收益接近零。为此，我们仅在标准 grind 失败后才触发学习干预——一种失败驱动的级联机制，理论上不会丢失原本能证明的定理。我们在 grind 内部两个决策上应用该方法：一个成本感知的 E-匹配过滤器提升了少量问题的求解率，运行速度加快约5%；一个前瞻步骤成功证明了原本超时的五个定理。我们也报告了一个负面结果：四种基于特征的模型静态预测正确分支拆分，表现不优于随机，因为分支是否爆炸是运行时属性，特征无法捕捉。结果表明，学习在定理证明策略中更适合作为决定何时及如何投入有限搜索的机制，并以可靠的符号回退为基础。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。