一句话：提出 e-graph 引导的引理发现，使理论探索目标导向，提升归纳等式证明的效率和能力。
针对递归函数与归纳数据类型上的项等式自动证明难题：此类证明常需辅助引理，而辅助引理本身也需证明，已有引理发现方法在效率与能力之间存在权衡。本文提出 e-graph 引导的引理发现，将理论探索变为目标导向：利用 e-graph 与等式饱和高效构造并紧凑表示面向目标的证明空间，从而只探索能保证在部分证明上取得进展的辅助引理。作者实现证明器 CCLemma，并在多个基准上与三种最先进证明器比较。CCLemma 在两个标准基准上表现稳定，且在一个新的困难基准集上比次优工具多解决 50% 的问题。
The problem of automatically proving the equality of terms over recursive functions and inductive data types is challenging, as such proofs often require auxiliary lemmas which must themselves be proven. Previous attempts at lemma discovery compromise on either efficiency or efficacy. Goal-directed approaches are fast but limited in expressiveness, as they can only discover auxiliary lemmas which entail their goals. Theory exploration approaches are expressive but inefficient, as they exhaustively enumerate candidate lemmas. We introduce e-graph guided lemma discovery , a new approach to finding equational proofs that makes theory exploration goal-directed. We accomplish this by using e-graphs and equality saturation to efficiently construct and compactly represent the space of all goal-oriented proofs. This allows us to explore only those auxiliary lemmas guaranteed to help make progress on some of these proofs. We implemented our method in a new prover called CCLemma and compared it with three state-of-the-art provers across a variety of benchmarks. CCLemma performs consistently well on two standard benchmarks and additionally solves 50% more problems than the next best tool on a new challenging set.
@article{KurashigeJGBNIJ24,
title = {CCLemma: E-Graph Guided Lemma Discovery for Inductive Equational Proofs},
author = {Cole Kurashige and Ruyi Ji and Aditya Giridharan and Mark Barbone and Daniel Noor and Shachar Itzhaky and Ranjit Jhala and Nadia Polikarpova},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {ICFP},
year = {2024},
doi = {10.1145/3674653}
}