babble:LearningBetterAbstractionswithE-GraphsandAnti-Unification
babble：利用E-Graph和反统一学习更好的抽象
库学习通过从程序语料库中提取公共结构到可重用的库函数来压缩给定的程序语料库。先前关于库学习的工作受到两个限制，这两个限制阻碍了它扩展到更大、更复杂的输入。首先，它探索了太多对压缩无用的候选库函数。其次，它对输入的句法变化不健壮。
我们提出了库学习模理论（LLMT），这是一种新的库学习算法，它还接受给定问题领域的等式理论作为输入。LLMT使用e-graphs和等式饱和来紧凑地表示等价于模理论的程序空间，并使用一种新的e-graph反统一技术来更直接和高效地在语料库中找到共同模式。
我们在名为babble的工具中实现了LLMT。我们的评估表明，babble实现的压缩速度比现有技术快几个数量级。我们还会提供一个定性评估，显示babble在以前库学习无法触及的输入上学习可重用函数。
CCS概念：软件及其工程→函数式语言；自动编程。
其他关键词和短语：库学习，e-graphs，反统一
1引言
抽象是管理软件复杂性的关键。有经验的程序员通常会将共同的功能提取到库中，以更清晰、更简洁的方式表达他们的意图。如果这个过程可以从代码中自动提取有用的抽象，那会怎样？库学习试图用技术来回答这个问题，通过提取公共结构到可重用的库函数来压缩给定的程序语料库。库学习有许多潜在的应用，从重构和反编译[Jones等人2021；Nandi等人2020]，到模拟人类认知[Wang等人2021；Wong等人2022]，以及通过专门针对选定问题领域的目标语言来加速程序合成[Ellis等人2021]。
考虑图1中的简单库学习任务。左侧，图1a显示了Wong等人[2022]中的一个2dcadDSL的三个程序语料库。每个程序对应于由多个旋转线段组成的规则多边形组成的图片。右侧，图1b显示了一个学习到的库，其中有一个名为f0的函数，它抽象了缩放规则多边形的构造。然后可以使用学到的f0将三个输入程序重构为更简洁的形式。f0是否是这个语料库的“最佳”抽象通常很难量化。在本文中，我们遵循DreamCoder[Ellis等人2021]，并使用压缩作为库学习的度量，即目标是减少语料库在AST节点中的总大小（从208减少到72图1）。重要的是，语料库的总大小包括库的大小：这防止了库学习生成太多过于特定的函数，而是偏向于更通用和可重用的抽象。
**库学习可以表述为一个程序合成问题，分为两个阶段：生成候选抽象，接着选择那些能产生最佳（最小）重构语料库的抽象**。最先进的技术实现于DreamCoder[Ellis等人，2021]，但在扩展库学习到更大和更现实的输入时，存在两个主要限制：
-候选生成不够精准：DreamCoder会生成许多无用的候选抽象，减慢了选择阶段和整个算法的速度。
-该技术纯粹是句法性的，因此无法对表面上的变化具备鲁棒性。例如，人类程序员会立即知道表达式`2+1`和`1+3`可以使用抽象`λx.x+1`进行重构，因为加法是可交换的；而纯粹的句法库学习方法无法生成这种抽象。
在本文中，我们提出了**基于理论（等式）库学习（LLMT）**的新算法，解决了上述两大限制。
**通过反统一实现精准候选生成**。为了使候选生成更精准，LLMT利用了两个关键观察：
-有用的抽象必须在语料库中至少使用两次。例如，在包含两个程序`2+1`和`3+1`的语料库中，不需要考虑抽象`λx.3+x`，因为它只能在一个地方使用，因此只会增加语料库的大小。
-抽象应该“尽可能具体”以适应给定的语料库。例如，在同样的语料库中，抽象`λx.x+1`优于更通用的`λxy.x+y`，因为它们都适用于同样的两个表达式，但后者应用的代价更高（它需要两个参数）。
换句话说，有用的抽象对应于与原始语料库中某些子项匹配的最不通用模式；这种模式可以通过反统一（AU）[Plotkin1970]计算出来。例如，反统一`2+1`和`3+1`生成了模式`X+1`，并通过对模式变量`X`进行抽象，可以推导出所需的候选库函数`λx.x+1`。类似地，在图1中，可以通过反统一语料库中的蓝色和棕色子项推导出抽象`f0`。
**通过E-Graphs实现鲁棒性**。为了使候选生成更具鲁棒性，LLMT还接收特定领域的等式理论作为输入，并使用该理论找到与原始语料库语义等价但具有更多语法结构相似性的程序。例如，在算术领域中，我们期望理论中包含方程`X+Y≡Y+X`，表明加法是交换的。给定包含`2+1`和`1+3`的语料库，该规则可用于将第二个表达式重写为`3+1`，从而发现共同的抽象`λx.x+1`。
这种方法的主要挑战是在与原始语料库语义等价的程序的大空间中进行搜索。为此，LLMT依赖于e-graph数据结构和等式饱和技术[Tate等人2009；Willsey等人2021]来计算和表示语义等价程序的空间。为了在此空间上实现高效的库学习，我们提出了一种新的候选生成算法，该算法使用动态规划高效地计算由e-graph表示的子项对之间的所有反统一集。
最后，在此设置中选择最优库归结为从e-graph中提取出包含公共子表达式的最小项的问题。该问题在其一般形式中极具计算复杂性，现有的方法在可扩展性方面有限[Yang等人2021]。因此，我们提出了一种新的e-graph提取算法，称为**目标子表达式消除**，该算法利用特定领域的知识来减少搜索空间，并通过束搜索支持近似，以权衡准确性和效率。
贡献。总结来说，本文做出了以下贡献：
基于等式理论的库学习：一个可以结合任意领域特定的等式理论来使学习对句法变化更加健壮的库学习算法；
e-graph反统一：一个使用从术语扩展到e-graphs的反统一机制高效生成候选抽象集的算法；
有针对性的公共子表达式消除：一种新的近似算法，用于在存在公共子表达式的情况下从e-graph中提取最佳术语。
2概述
我们通过一个运行示例来说明LLMT，该示例建立在图1的基础上。图1中的输入语料库是用Wong等人[2022]的2dcadDSL编写的，它具有以下原语：
也就是说，一个六边形边变形xform(line,[1,0,0.5,0.5/tan(/6)])重复六次，每次旋转2/6弧度，得到的单位六边形再被缩放2倍。
然而，仔细观察图1中的两个蓝色六边形，我们会注意到一些奇特之处。图1中xform(repeat...,[1,0,0,0])的两个出现是无操作：它们仅将一个图形按1的因子缩放，既不旋转也不平移。如果代码是手工编写的或从低级表示（像Szalinski这样的工具[Nandi等人2020]）反编译的，这些冗余的变换可能不会出现；但它们对于我们希望使用纯句法技术学习最优抽象0至关重要。
图3显示了图1中语料库的简化和“更自然”的版本，它消除了这些无操作变换。正如图中所示，这导致纯句法技术学习了一个不同的函数1，它抽象了一个未缩放的单位多边形。因为缩放变换现在在抽象之外，所以它必须重复五次。结果，尽管简化的输入语料库C比原始语料库A更小（196个AST节点而不是208个），但它的压缩版本D更大（81个AST节点而不是72个）！换句话说，句法库学习对于保持语义的代码变化是不健壮的。
在本节的剩余部分，我们将说明babble如何使用我们的新算法——基于等式理论的库学习（LLMT）——实现这一点。
简化的DSL。在本节的剩余部分，我们使用一个定制版本的2dcadDSL，增加了以下额外构造：
这些可以在原始DSL中表达，并且如果给定适当的语料库，甚至可以通过库学习发现；为了简化表述，我们在这里将它们视为原语。
2.1使用E-Graphs表示等价项
为了在库学习中利用等价关系，babble接受领域特定的等式理论作为输入。对于我们的运行示例，让我们假设该理论包含一个单一的等式：
**该等式规定任何图形等价于自身缩放为1的情况**。有了这个等式后，就可以将语料库C“重写”成语料库A，并通过纯句法技术从中学习到最优的压缩语料库B。挑战在于，语料库C可以被重写成无限多的其他语料库；如何选择能够最大化句法对齐、从而增加发现最优抽象机会的语料库？
与其尝试猜测最佳的等价语料库，或逐个枚举它们，babble使用**等式饱和技术**[Tate等人2009；Willsey等人2021]。等式饱和技术以一个术语和一组重写规则为输入，找到在给定规则下与等价的所有术语空间；这得益于e-graph数据结构提供的高度共享特性，可以紧凑地表示生成的空间。
图4（左）展示了通过等式饱和技术为图3中的蓝色术语构建的e-graph——在简化的DSL中表示为`repRot(side(6),6,2/6)`——使用重写规则（1）。图中的蓝色部分代表原始术语，灰色部分则是通过等式饱和技术添加的。e-graph中的实线矩形表示e-nodes（类似于常规的AST节点），而虚线矩形表示e-classes（表示术语的等价类）。重要的是，e-graph中的边从e-nodes指向e-classes，这使得可以紧凑地表示子项中存在变化的程序：例如，将e-class1作为repRot节点的第一个子节点，可以同时表示术语`repRot(side(6),6,2/6)`和`repRot(scale(side(6),1),6,2/6)`，而不重复它们的共同部分。此外，由于e-graphs可以有循环，因此它们也可以表示无限多的术语集：例如，e-class1表示的术语形式包括：`side(6)`，`scale(side(6),1)`，`scale(scale(side(6),1),1)`，等等。由于这个e-graph表示了在重写规则（1）下所有等价术语的空间，因此我们库学习中寻找的术语，即`scale(repRot(side(6),6,2/6),1)`，也被包含在e-class0中。
2.2通过E-Graph反统一生成候选
在使用给定的等式理论通过等式饱和运行从给定语料库构建e-graph之后，库学习的下一步是生成候选模式，这些模式捕捉语料库之间的句法相似性。挑战在于生成足够少的候选以使库学习可行，但足够多以实现良好的压缩。我们使用图4（右）中的e-graph来说明候选生成，它代表了我们语料库的一部分，包括（饱和的）蓝色和棕色术语。回想一下，最佳模式——对应于缩放多边形抽象0——是：
先前在DreamCoder上的工作通过从语料库中随机选择一个片段，然后随意替换选择的子术语与模式变量来生成模式。例如，为了生成模式0，DreamCoder需要选择整个棕色子术语作为一个片段，然后决定对其子术语8和2进行抽象。这种方法成功地将候选集从所有句法上有效的模式限制为至少在语料库中有一个匹配的模式；然而，由于选择要抽象的子术语的方式太多，这个空间仍然太大，无法在短程序的小语料库之外全面探索。在babble中，由于等式饱和，这个问题更加严重，因为e-graph通常包含比原始语料库多出指数级或无限多的程序。
通用性过滤器。为了在babble中进一步修剪可行候选集，我们确定了两类可以安全丢弃的模式，要么是因为它们太具体，要么是因为它们太抽象。首先，像repRot(side(8),,2/8)这样的模式可以丢弃，因为它对于这个语料库来说太具体了：相应的抽象只能应用一次，本质上是将唯一匹配的术语repRot(side(8),8,2/8)替换为(repeat(side(8),,2/8))8，这只会向语料库中添加更多的AST节点。其次，像repRot(side(),,)这样的模式可以丢弃，因为它对于这个语料库来说太抽象了：它匹配的所有地方，更具体的模式repRot(side(),,2/)也会匹配；使用更具体的模式可以更好地压缩，因为在它的应用中实际参数既更少也更小：f62/6和f82/8与f6和f8相比。
因此，我们的第一个关键见解是将候选集限制在与（饱和的）语料库中的某些子术语对匹配的最具体的模式。例如，模式0是最具体的模式，它匹配这两个术语
术语反统一。计算与两个给定术语匹配的最具体模式称为反统一（AU）[Plotkin1970;Reynolds1969]。AU通过简单的自顶向下遍历两个术语来工作，用模式变量替换任何不匹配的构造器。例如，要反统一术语（3）和（4），我们从两个术语的根开始；由于两个AST节点共享相同的构造器scale，它成为模式的一部分，我们递归进入子节点。我们最终遇到一个不匹配，左侧的术语是6，右侧的术语是8；所以我们创建一个新的模式变量，并记住反替代={(6,8)→}。当我们在角度的分母中遇到不匹配时，我们在中查找不匹配的术语对(6,8)；因为我们已经为这对创建了一个变量，我们简单地返回现有的变量。最后的不匹配是scale的第二个子节点中的(1,2)；由于这对尚未在中，我们创建第二个模式变量，。此时，得到的反统一结果是模式0（2）。
反统一单个术语对是简单且高效的。然而，在LLMT中，我们希望反统一所有可能在任何与原始语料库等价（模给定的等式理论）的语料库中出现的子术语对。
明确枚举由e-graph表示的所有等价语料库，然后对每对子术语进行AU是不可行的。相反，babble直接在e-graph上执行反统一。
从术语到E-类。我们首先解释如何反统一两个e-类。这个操作以一对e-类作为输入，并返回一组主导反统一器，即一组模式，这些模式（1）匹配两个e-类，并且（2）保证包括两个e-类表示的术语对的最具体模式中的最佳抽象。
考虑计算图4（右）中的e-graph的e-类1和4的AU(1,4)。AU仍然作为自顶向下的遍历进行，但在这种情况下我们必须检查两个e-类是否有任何共同的构造器。在这种情况下，它们确实有：一个side构造器和一个scale构造器。让我们首先选择两个side构造器并递归进入它们唯一的子节点，计算AU({6},{8})。这两个e-类没有匹配的构造器，所以AU简单地返回一个模式变量，类似于术语反统一；这产生了1和4的第一个模式：side。
然而，记住1和4也有匹配的scale构造器。这就有趣了：这些构造器涉及一个循环（它们的第一个子节点是父e-类本身）。如果我们让AU跟随这个循环，反统一器的集合就变得无限：
幸运的是，我们可以展示side主导了这个集合中的所有其他模式，因为它们的模式变量——在这种情况下，只是——匹配相同的e-类，但它们也更大（在第4节中我们将展示这种支配关系如何让我们修剪其他模式，不仅仅是由循环引起的模式）。因此，AU(1,4)简单地返回{side}。
对于两个多边形的根e-类，0和2，按照相同的逻辑，AU(0,2)产生了模式0（2），这是学习最优抽象所必需的。
从E-类到E-图。为了获得所有候选抽象的集合，我们需要对e-graph中所有e-类的对进行反统一。显然，这些计算有重叠的子问题（例如，我们必须计算AU(1,4)作为AU(0,2)和AU(0,3)的一部分）。
为了避免重复工作，babble使用了一个高效的动态规划算法，以自底向上的方式处理所有e-类的对。
2.3通过有针对性的公共子表达式消除进行候选选择
现在我们来说明babble中库学习的最后步骤：给定由e-graph反统一生成的候选抽象集，目标是选择一个子集，以便为整个语料库提供最佳压缩。例如，为图3中的语料库生成的候选包括：
简化为E-Graph提取。为了克服这个困难，我们再次利用e-graph和等式饱和。我们的第二个关键见解是，选择最优的抽象子集可以简化为在存在公共子表达式的情况下从e-graph中提取最小术语的问题。
为了说明这种简化，让我们将注意力限制在仅有的两个候选抽象0和1上，如上所述。babble将每个候选模式及其相应的抽象转换为一个重写规则，该规则在语料库中引入一个局部-抽象，然后应用；对于我们的两个抽象，这些规则是：
将这些规则应用于图4（右）中的e-graph的结果如图5所示。例如，你可以看到e-class2（代表缩放-2的八边形）现在存储了另一种表示形式：082。e-class0（单位六边形）使用0或1都有表示，因为这个类匹配了上述重写规则（5）和（6）。还要注意，因为-抽象的定义也存储在e-graph中，等式饱和可以使用这些规则在其主体内部进行应用，使得一个函数使用另一个函数：例如，存储在0定义中的一个术语是
一旦我们为所有候选抽象构建了带有局部lambda的e-graph版本，剩下的就是从这个e-graph中提取最小的术语。棘手的部分是我们希望只计算重复lambda的大小一次。例如，在图5中，0被应用了两次（在0和2中）；如果术语提取选择这两个e-节点，我们希望将它们的第一个子节点（0的定义）视为公共子表达式，其大小只对最终表达式贡献一次。直观地说，这是因为我们可以将这些lambda“提升”到顶层的let绑定中，从而只定义一次0，并用名称替换每个局部lambda。
带有公共子表达式的提取是一个已知但极其困难的问题，传统上被简化为整数线性规划（ILP）[Wang等人2020；Yang等人2021]。由于ILP方法的可扩展性非常有限，我们开发了一个定制的提取算法，通过使用领域特定知识和近似来更好地扩展。
提取算法。使提取更高效的主要思想是，对于库学习，我们只对共享某种类型的子术语感兴趣：即，-抽象。因此，对于每个e-类，我们只需要跟踪每个可能的库（即每个-抽象的子集）的最佳术语。更准确地说，对于每个e-类和库，我们跟踪（1）库的最小大小（2）使用这个库重构的程序的最小大小（将-抽象计为单个节点）。我们通过e-graph自底向上计算和传播这些信息。一旦这个信息被计算出来并传播到根e-类（代表整个语料库），我们就可以简单地选择总大小最小的库。
例如，对于图5中的e-类2，对于空库，库的大小是0，最小程序的大小（scale(repRot(side(8),8,2/8),2)）是9；对于库{0}，库的大小是9，最小程序的大小（028）是3；而对于库{1}，库的大小是7，最小程序的大小（scale(18,2)）是4。显然，对于这个e-类，引入库函数还没有回报（0+9<7+4<9+3），因为每个只能使用一次。然而，当我们向根移动时，情况就变了。对于0和2的父e-类，引入{0}和{1}的成本已经被摊销了：使用空库的最小程序大小是17，而使用{0}或{1}的最小程序大小是7，所以{1}已经值得引入了（9+7<0+17）。包括更多带有缩放多边形的程序最终使得库{0}成为四个子集中最有利可图的。
由于在更大的语料库中，跟踪所有候选抽象的子集是不可行的，babble提供了一种通过使用束搜索方法在可扩展性和精度之间进行权衡的方式。
3在术语上进行库学习
在本节中，我们对术语语料库上的库学习问题进行了形式化，并阐述了我们的第一个核心贡献：通过反统一生成候选抽象。第4节将这种形式化推广到e-graph上的库学习。为了便于解释，我们首先对库学习的形式化是一阶的，即初始语料库本身不包含任何-抽象，所有学习到的抽象都是一阶函数（babble实现没有这个限制）。
3.1预备知识
模式。如果X是一个可枚举的变量集，T(Σ,X)是模式的集合，即可以包含来自X的变量的术语。如果一个模式的每个变量只出现一次，则称该模式是线性的：∈vars().occurs(,)=1。一个替换=[1→1,...,→]是从变量到模式的映射。我们写()表示将应用于模式，其定义为标准方式。我们定义替换的大小size()为其右侧的总大小。
如果存在使得′=()，则模式比（或匹配）′更一般，写为′；我们将这样的记为match(′,)。例如，+1+，其中match(+1,+)=[→1]。关系是模式上的偏序，并且诱导了一个等价关系1～212∧21（在变量重命名上等价）。在以下内容中，我们总是根据这个等价关系区分模式。
两个模式1和2的连接——也称为它们的反合一器——是匹配两者的最一般模式；连接在～上是唯一的。注意T(Σ,X),,,=是一个连接半格（Plotkin的子化格[Plotkin1970]的一部分）。因此，连接可以推广到任意一组模式。
一个上下文C是一个模式，其中包含一个区分变量的单一出现。我们写C[]——在上下文C中的——作为[→](C)的语法糖。一个重写规则是一个模式对，写为12。将重写规则应用于术语或模式，写为()，在标准方式中定义：如果1，则()=(match(,1))(2)，否则未定义。模式可以使用规则在一步中重写为，写为→1，如果存在一个上下文C使得=C[′]并且=C[(′)]。这个关系的反射-传递闭包是重写关系→R，其中R是一组重写规则。
压缩术语。压缩术语T(Σ,X)的形式为：
换句话说，压缩项可能包含一个带有零个或多个绑定符号的λ抽象应用于相同数量的参数。需要注意的是，这是一种一阶语言，因为所有抽象都被完全应用了。重要的是，我们定义了size，使得λ抽象的多次出现只被计算一次。为简化计算，应用项的大小被定义为，也就是说，抽象节点本身不增加大小。
压缩项上的Beta归约，记作，以通常的方式定义。
问题描述。现在我们可以将库学习问题形式化如下：给定一个项∈T(Σ)，目标是找到最小的压缩项，它能归约到（即→）。之所以可能比更小，是因为它可能包含多次相同-抽象的出现（应用于不同的参数），但这些-抽象的大小只计算一次。图6展示了一个例子。
尽管在一般情况下，解决方案可能包括具有自由变量的嵌套λ（定义在外部λ中），但在本文的其余部分中，我们将注意力限制在全局库学习上，其中所有的λ都是闭合项。这样做的动机在于库学习的目的在于为给定问题域发现可重用的抽象。图6中的解决方案已经具有这种形式。
3.2模式驱动的库学习
在高层次上，我们的库学习方法是使用原始语料中出现的模式作为压缩语料中-抽象的候选主体。查看图6中的示例，乍看之下，单独使用原始语料中的模式似乎不足够，因为2的主体包含了1的一个应用。或许令人惊讶的是，这并不是问题：关键思想是我们可以通过反转求值→将压缩成，并且由于求值顺序是应用性的，在每一步中重写的子项都不会包含任何-简约式。
压缩。更正式地说，给定一个模式，我们将其压缩规则（简称为规则）定义为重写规则。
换句话说，我们首先使用2重写整个术语，然后使用1在引入的抽象体内进行重写（注意这种压缩顺序与应用性评估顺序相反）。语料库中的第二个术语类似地进行压缩；第三个术语使用1在单步中压缩。尽管从上面的重写序列中并不明显，但由于共享了-抽象，如图6右侧所示，得到的压缩语料库确实比原始的更小。
3.3修剪候选模式
在本节中，我们将讨论在构建术语重写问题的-规则集R时，哪些模式可以被丢弃不考虑。
我们可以展示，具有非负成本的模式可以安全地丢弃，即：存在另一种仅使用P\{}的压缩，其结果至少一样小。
平凡模式。基于此分析，任何具有骨架大小skeleton()≤1的线性模式都可以被丢弃，其中skeleton()=size()|vars()|是的“骨架”大小，即没有变量的主体。直观地说，的骨架太小，无法支付引入应用的费用。在这种情况下，cost(,_)>0，不管它被使用多少次。我们称这样的模式为平凡模式。平凡模式的例子是和+。
单一匹配的模式。我们可以展示，在语料库中只有一个匹配的模式也可以被丢弃。如果在中只有一个匹配，那么它在任何的压缩中最多只能出现一次。如果是线性的，cost(,_)=1+|vars()|，这总是正的，所以可以被丢弃。但是，对于非线性模式，即使只有一个步骤也可以通过变量重用来减小大小，又该怎么办呢？结果发现，任何只有一个匹配的非线性模式总是可以被一个更优的无变量的零元模式替换。
4图书馆学习模等式理论
4.1顶层算法
我们可以将等式理论下的库学习问题(LLMT)形式化为：给定一个项和一组引发等价关系≡的等式，目标是找到一个压缩后的项，使得（对于某个'，并且的大小最小。
4.2经由E图反统一的候选生成
图10定义了这一操作，使用了两个相互递归的函数来反统一e-类和e-节点。请注意，e-节点的反统一总是在非空上下文中调用。第一个方程对具有相同构造函数的两个e-节点进行反统一：在这种情况下，我们递归地反统一它们的子e-类，并返回结果的笛卡尔积。第二个方程适用于具有不同构造函数的e-节点：如同项反统一的情况，这将生成一个模式变量。处理e-图的一个很好的副作用是我们不需要跟踪反替换来保证每对子项映射到相同的变量：因为任何重复的项都由相同的e-类表示，我们可以简单地使用e-类id和作为模式变量,的名称。
第二组方程定义了e-类的反统一（我们暂时忽略dominant，它将在稍后解释）。第一个方程适用于和已经被访问的情况：在这种情况下，我们打破循环并返回空集。否则，最后一个方程将反统一两个e-类中的所有e-节点对，并在更新的上下文中合并结果。需要注意的是，除非两个e-类中的所有e-节点都有相同的构造函数，否则这将添加一个模式变量；我们在第2节中为了简化省略了这一细节，但在babble中实现了这一功能，并且常常产生更优的模式。例如，考虑图4（右）中的1和2的反统一：虽然它们有相同的构造函数scale，但实际上是比scale更好的抽象这两个e-类的模式，因为与模式scale的实际参数（side(6),1,repRot(side(8),8,2/8),和2）相比，模式的实际参数（side(6)和scale(repRot(side(8),8,2/8),2)）的总大小是相同的，而模式本身却更小。这种情况的发生是因为类1表示了多个不同的项，而与兼容的项在这种情况下比与scale兼容的项更小。
5候选模式选择通过E-图提取
在生成候选抽象之后，LLMT算法调用`select_library`来挑选出能够最好地压缩输入语料库的候选模式子集。本节描述了我们选择最佳库的方法，称为目标化公共子表达式消除（targetedcommonsubexpressionelimination）。
库选择作为E-图提取
回顾一下，候选选择从一个e-图G′开始，该e-图表示使用候选模式P压缩初始语料库及其等效项的所有方式。我们将子集LP称为库。用L压缩e-类的最佳大小可以计算为以下两个部分的大小之和：(1)仅使用库L中的库函数并且不计算λ-抽象大小的最小项∈JK，以及(2)库L中每个的最小版本。需要注意的是，定义L中的抽象的成本只计算一次，并且L中的抽象可以用于压缩L中的其他抽象。我们的目标是找到一个L，使得用L压缩的根e-类的大小最小。
给定一个特定的库，我们可以通过相对简单的自顶向下遍历e-图来找到最小项的大小。因此，一个幼稚的库选择方法是枚举P的所有子集，并选择能够在根节点处生成最小项的子集。不幸的是，随着P的大小增加，这种方法变得不可行。
利用部分共享结构
为了计算e-类的成本集合，`babble`取所有e-节点成本集合的并集。然而，这样做会导致成本集合的大小指数级增长。为了解决这个问题，我们定义了一个部分排序化简（reduce），它只剪枝那些明显次优的成本集合。给定e-类成本集合中的两个对(L1,1)和(L2,2)，如果L1L2并且1≤2，那么L2就被L1包含，可以从成本集合中移除，因为L1即使在更少的库函数下也可以更好地压缩这个e-类。实际上，这种优化剪枝了具有冗余抽象的库，即两种不同的抽象可以用来压缩相同的子项。
BeamApproximation（光束近似）
即使有了部分排序化简，为每个e-节点和e-类计算成本集合仍可能指数级增长。为此，`babble`提供了限制每个成本集合中库的大小和每个e-类存储的成本集合大小的选项。这会产生一种光束搜索风格的算法，其中每个e-类的成本集合都会被剪枝，如图11所示。这个剪枝操作首先过滤掉具有超过个模式的库，然后按总成本（即使用成本和库的大小之和）对剩余的库进行排名，最后返回这个集合中的前个库。
6评估
我们通过两个定量研究问题和一个定性问题来评估`babble`及其背后的LLMT算法：
**RQ1.**`babble`是否能比最先进的库学习工具更好地压缩程序？
**RQ2.**LLMT中的主要技术（反统一和等式理论）对算法的性能是否重要？
**RQ3.**`babble`学到的函数是否具有直观意义？
基准选择
我们使用了两套基准来评估`babble`，如表1所示。第一套基准源自DreamCoder研究[Ellisetal.2021]，并作为公共仓库提供[Bowers2022]。DreamCoder是当前最先进的库学习工具，使用这些基准允许我们进行面对面的比较。DreamCoder的基准被分为五个领域（每个领域有不同的DSL）；我们选择了其中两个领域——List和Physics——因为我们对它们的理解最为深入，适合添加等式理论。
第二套基准，称为2dcad，来自Wongetal.[2022]。这项工作收集了一个大型图形DSL程序库，目的是研究生成的对象与其自然语言描述之间的关系。这个数据集的“Drawings”部分包含1,000个程序，分为四个子领域（见表1），每个子领域有250个程序。
我们在AMDEPYC7702P处理器（2.0GHz）上运行了所有基准。每个基准都在单核上运行。DreamCoder的结果来自基准仓库[Bowers2022]；DreamCoder在AMDEPYC7302处理器（3.0GHz）的8核上运行。
6.1与DreamCoder的比较
为了解答RQ1，我们将`babble`与最先进的DreamCoder工具[Ellisetal.2021]进行比较，使用的是其自己的基准。DreamCoder的基准适用于它的工作流程；虽然库学习任务的输入在概念上是一组程序（或仅一个大程序），每个输入到DreamCoder的都是一组程序的集合。每组是从同一个程序合成任务（DreamCoder管道的早期部分）输出的程序集合。在通过库学习压缩程序时，DreamCoder是通过连接每组中最压缩的程序来最小化程序的成本，换句话说：
DreamCoder采用这种方法来为其库学习组件提供许多相同程序的变体，以便在不同合成问题的解决方案程序之间引入更多的共享结构。
为了在`babble`中实现DreamCoder的基准，我们使用e-图来捕捉一个组中的程序变体的概念。由于组中的每个程序都是相同合成任务的输出，`babble`将它们视为等效，并将它们放在同一个e-类中。
**结果。**我们在DreamCoder基准套件中的五个领域上运行了`babble`。结果如图12所示。总结来说，`babble`在来自DreamCoder领域的基准测试中，始终能实现比DreamCoder更好的压缩比，而且速度比DreamCoder快1-2个数量级。
-“BabbleSyn”忽略等式理论，仅进行语法库学习。
-“EqSat”仅使用等式饱和（EqualitySaturation）和等式理论中的重写来优化程序。该配置不进行任何库学习。
6.2大规模2dcad基准测试
上一节展示了`babble`的性能远超现有技术。在本节中，我们展示和讨论了在2dcad领域基准测试中运行`babble`的结果。这些基准测试来自Wongetal.[2022]，比DreamCoder数据集中的基准测试大得多（大约10倍到100倍），DreamCoder无法处理这些数据集。
我们还观察到Nuts-and-bolts数据集中包含多个冗余转换，例如第2节运行示例中出现的“按1缩放”。这些冗余在缺少等式理论时可以帮助找到抽象。然而，它们不应该是`babble`所必需的，因为LLMT可以在需要时引入这些冗余。因此，我们从Nuts-and-bolts数据集中移除了所有现有的冗余转换，并在转换后的数据集上运行了`babble`。结果见表2的最后一行。在修改后的数据集上，`babble`使用等式理论时实现了相同的压缩效果，但在没有等式的情况下，表现比未修改的数据集差。
**定性评估。**图14突出了`babble`从2dcad基准测试中发现的一些抽象。我们在每个基准测试上运行了`babble`并应用了学到的抽象来可视化它们的使用。有关学习的库的可用性和可读性的问题难以回答，我们将这留待未来的工作。然而，图14显示`babble`确实识别出了在不同基准中相似的公共结构，这使得其输出更易于重用和解释。
首先，我们回顾第1节的Nuts-and-bolts示例：图14显示`babble`学到了缩放多边形（ngon）抽象，这适用于数据集中的多个程序。我们还看到`babble`一贯地为Nuts-and-bolts和Vehicles发现了类似的“形状环”抽象。最后，正如Gadgets示例所示，`babble`为整个模型及其组件都找到了抽象。在这种情况下，它学习了抽象整个外形的函数`gadget_body`，同时也学习了抽象外形把手的`dial`函数。
**Stitch**。两种方法的核心区别在于，Stitch侧重于提高纯语法库学习的效率，而`babble`通过添加等式理论来提高其表达能力。虽然`babble`将库学习分为两个阶段——通过反统一进行候选生成和通过e-图提取进行候选选择——Stitch算法则在分支限界的自顶向下搜索中交替进行生成和选择阶段。从“顶层”模式\(X\)开始，Stitch逐步对其进行细化，直到进一步细化不再有收益。为了快速剪枝次优的候选模式，Stitch通过将该模式在语料库中每次匹配的压缩量相加来计算其压缩的上界（由于未考虑匹配可能重叠，因此该上界是不精确的）。对于没有通过这种方式剪枝的候选模式，Stitch通过搜索重写的最佳匹配子集来计算其真实的压缩量，这被称为“重写策略”。`babble`的提取算法可以视为Stitch的重写策略的一种泛化：前者在同时搜索模式的子集以及如何将其应用于语料库时，后者则一次只考虑单个模式，并且只搜索最佳的应用方式。由于前者的搜索空间要大得多，`babble`使用了束搜索近似，而Stitch的重写策略是精确的。总结而言，两种方法的主要优缺点如下：
-`babble`能够在考虑等式理论的情况下学习库，而Stitch不能；
-Stitch为一次学习一个最佳抽象提供了最优性保证，而`babble`可以同时学习多个抽象，但牺牲了理论上的最优性。
**其他库学习技术**。Knorf[Dumancicetal.2021]是一个用于逻辑程序的库学习工具，它与`babble`类似，也分为两个阶段。他们的候选生成阶段类似于Stitch中的上界计算，而选择阶段则使用现成的约束求解器。探索他们的基于约束的技术是否可以推广到逻辑程序之外将是很有趣的。
一些研究发展了有限形式的库学习，其中只能抽象出某些特定类型的子术语。例如，ShapeMod[Jonesetal.2021]为DSL语言ShapeAssembly中表示的3D形状学习宏，仅支持对数值参数（如形状的尺寸）进行抽象。我们之前的工作[Wangetal.2021]从图形程序中提取共通结构，但仅支持对原始形状进行抽象，并在程序的顶层应用这些抽象。这些限制使得库学习问题在计算上更具可处理性，但也限制了所学抽象的表达能力。
有几种神经程序合成工具[Dechteretal.2013;Iyeretal.2019;Lázaro-Gredillaetal.2018;Shinetal.2019]使用统计技术学习编程惯用法。其中一些工具使用了“探索-压缩”算法[Dechteretal.2013]，通过迭代枚举一组程序并找到一种解决方案，从而揭示使得这些程序集最大程度压缩的抽象。这与`babble`用于指导提取的公共子表达式消除方法类似。
**反统一的应用**。反统一是发现程序中共同结构的一个成熟技术。它是自底向上的归纳逻辑编程[CropperandDumancic2022]的核心思想，也被用于软件克隆检测[Bulychevetal.2010]、示例编程[Razaetal.2014]和学习重复代码编辑[Mengetal.2013;Rolimetal.2017]。这些应用可能也会受益于`babble`的反统一概念，特别是在处理语义保持变换时更具鲁棒性。
**使用e-图进行合成和优化**。虽然传统上e-图在SMT求解器中用于促进不同理论之间的通信，但一些工具已展示其在优化和合成中的应用。Tateetal.[2009]首次使用e-图进行等式饱和：一种通过重写优化具有循环的Java程序的技术。此后，多个工具使用等式饱和来寻找与输入程序等效但更优的程序[Nandietal.2020;Panchekhaetal.2015;VanHattumetal.2021;Wangetal.2020;Willseyetal.2021;Wuetal.2019;Yangetal.2021]。`babble`使用了针对e-图的反统一算法（结合领域特定的重写），这是之前工作中没有展示的。此外，之前的工作要么使用贪婪的提取策略，要么使用ILP基础的提取策略，而`babble`使用了一种新的目标公共子表达式消除方法，我们认为它可以用于许多其他等式饱和的应用，特别是考虑到它可以通过束搜索进行近似。
8结论与未来工作
我们介绍了基于理论的库学习（LLMT）技术，该技术用于从一组程序中学习抽象，同时结合用户提供的等式理论。我们在babble中实现了LLMT。我们的评估显示，babble在压缩效果上比现有技术快几个数量级。在较大的2dcad程序基准套件上，babble学习到了合理的函数，这些函数能压缩一个以前过大而无法使用库学习技术的数据集。
LLMT和babble提出了许多未来工作的方向。首先，我们的评估表明，等式理论对于实现高压缩率至关重要，但这些理论必须由领域专家提供。近期的自动化理论合成工作，如Ruler[Nandietal.2021]或TheSy[SingherandItzhaky2021]，可能会帮助用户完成这一任务。其次，LLMT使用e-图反统一来生成有前景的抽象候选，但这种方法并不完整，可能遗漏了一些能够实现更好压缩的模式。未来一个令人兴奋的方向是将LLMT与更高效的自顶向下搜索方法结合起来，如Stitch[Bowersetal.2023]。这具有挑战性，因为Stitch依赖于快速计算给定模式压缩的上界，通过求和每个匹配中的局部压缩来实现。这种上界并不容易直接扩展到e-图，因为在e-图中，同一模式的不同匹配可能来自于语法变体的不同，且需要在抽象带来的压缩和不同语法变体之间的大小差异之间进行权衡。