babble：使用E图和反统一学习更好的抽象
babble: Learning Better Abstractions with E-Graphs and Anti-Unification
摘要：
库学习通过从语料库中提取公共结构来压缩给定的程序语料库，从而将其转换为可重用的库函数。之前关于库学习的工作受到两个限制，这阻止了它扩展到更大，更复杂的输入。首先，它探索了太多对压缩无用的候选库函数。其次，它对输入中的句法变化不鲁棒。我们提出了图书馆学习模理论（LLMT），一个新的图书馆学习算法，另外作为输入的方程理论为一个给定的问题域。LLMT使用e-graph和等式饱和来表示等价模理论的程序空间，并使用一种新的e-graph反统一技术来更直接有效地发现语料库中的公共模式。我们在一个名为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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
