babble: Learning Better Abstractions with E-Graphs and Anti-unification
babble: Learning Better Abstractions with E-Graphs and Anti-unification
复制标题
DOI：
10.1145/3571207
复制
发表时间：
2022-12
影响因子：
--
通讯作者：
David Cao;Rose Kunkel;Chandrakana Nandi;Max Willsey;Zach Tatlock;N. Polikarpova
中科院分区：
文献类型：
--
作者：
David Cao;Rose Kunkel;Chandrakana Nandi;Max Willsey;Zach Tatlock;N. Polikarpova
库学习通过将语料库中的公共结构提取为可重用的库函数来压缩给定的程序语料库。先前关于图书馆学习的工作受到两个限制，使其无法扩展到更大、更复杂的输入。首先，它探索了太多对压缩没有用处的候选库函数。其次，它对输入中的语法变化不具有鲁棒性。我们提出了库学习模理论（LLMT），这是一种新的库学习算法，它额外地将给定问题域的方程理论作为输入。LLMT利用e图和相等饱和来紧凑地表示程序的等价模空间，并利用新颖的e图反统一技术更直接有效地找到语料中的公共模式。我们在一个名为babble的工具中实现了LLMT。我们的评估表明，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.