一句话：提出 LLMT 库学习算法，利用 E-Graph 和等式饱和及 E-Graph 反合一，高效提取可复用库函数，压缩优于 SOTA。
库学习通过从程序语料中提取公共结构为可复用库函数来压缩程序。现有方法探索过多无用候选函数，且对句法变化不鲁棒。本文提出库学习模理论（LLMT），额外接收问题领域的等式理论。LLMT 用 E-Graph 和等式饱和紧凑表示模理论等价的程序空间，并用新颖的 E-Graph 反合一技术更直接高效地发现公共模式。作者实现工具 babble，评估表明其压缩效果优于最优方法且快数个数量级，定性评估显示 babble 能在先前无法处理的输入上学习可复用函数。
Library learning compresses a given corpus of programs by extracting common structure from the corpus into reusable library functions. Prior work on library learning suffers from two limitations that prevent it from scaling to larger, more complex inputs. First, it explores too many candidate library functions that are not useful for compression. Second, it is not robust to syntactic variation in the input. We propose library learning modulo theory (LLMT), a new library learning algorithm that additionally takes as input an equational theory for a given problem domain. LLMT uses e-graphs and equality saturation to compactly represent the space of programs equivalent modulo the theory, and uses a novel e-graph anti-unification technique to find common patterns in the corpus more directly and efficiently. We implemented LLMT in a tool named babble. Our evaluation shows that babble achieves better compression orders of magnitude faster than the state of the art. We also provide a qualitative evaluation showing that babble learns reusable functions on inputs previously out of reach for library learning.
@article{paperbot2070,
title = {babble: Learning Better Abstractions with E-Graphs and Anti-unification},
author = {David Cao and Rose Kunkel and Chandrakana Nandi and Max Willsey and Zachary Tatlock and Nadia Polikarpova},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {POPL},
year = {2023},
doi = {10.1145/3571207}
}