使用冲突驱动学习的程序合成

我们提出了一种新的冲突驱动程序合成技术，该技术能够从过去的错误中学习。给定一个违反了所期望的规约的伪造程序，我们的合成算法将识别冲突的根本原因，并学习新的引理，以防止将来出现类似的错误。我们引入了等价模冲突（equivalence modulo conflict）的概念，并展示了该概念如何用于学习有用的引理，这些引理使合成器可以修剪搜索空间的大部分。我们已经实现了一种称为 Neo 的通用 CDCL 风格程序合成器，并在两个不同的应用程序域中对其进行评估，即 R 中的数据整理和列表上的函数编程。我们的实验证明了冲突驱动学习的巨大好处，并表明 NEO 优于针对这两个领域的两种最先进的合成工具 Morpheus 和 DeepCoder。

在本文中，我们提出了一种能够从其过去的错误中学习的新的冲突驱动合成算法。我们的方法受自动定理证明中冲突驱动学习的成功启发，并分析了冲突以学习指导搜索的有用引理。此外，我们的方法可以在任意 DSL 上合成程序，并且不限于任何特定的应用程序域。

在较高的层次上，我们的合成算法的总体结构类似于基于冲突驱动子句学习（CDCL）的 SAT 和 SMT 求解器的体系结构。如图 1 所示，我们的合成算法由三个关键组件组成，即 Decide，Deduce 和 AnalyzeConflict。

​ 本文的主要技术贡献有两个方面：第一，我们介绍了使用冲突驱动学习的合成范例，并提出了用于构建程序合成器的 CDCLstyle 体系结构。第二，我们提出了一种用于分析冲突和自动学习有用引理的新技术，该技术应添加到知识库中。我们的学习算法基于等价模冲突的新概念。

我们已经在 Neo 的工具中实施了建议的合成技术，并在先前的工作中探讨的两个不同的应用领域中对其进行了评估：首先，我们使用 Neo 在 R 中执行数据整理任务，并将 Neo 与 Morpheus 进行比较，针对该领域的最先进的合成器。其次，我们在列表处理程序领域评估 Neo，并将其与 DeepCoder 的重新实现进行比较，DeepCoder 是基于深度学习的最先进的合成器。我们的实验清楚地证明了从冲突中学习的好处，并表明我们的通用合成算法优于针对这些领域的最新合成器。

假设我们得到一个包含足球联赛中不同球队得分的列表，我们的目标是编写一个程序来计算最佳 k 支球队的总得分。例如，如果输入列表为[49,62,82,54,76]，并且 k 指定为 2，则程序应返回 158（即 82 76）。可以很容易地看到下面的 computeKSum 过程（使用类似 Haskell 的语法编写）实现了所需的功能：

现在，我们使用这个简单的示例和图 2 所示的小型 DSL 来解释我们的核心思想。在本节（以及整篇论文）中，我们使用程序的抽象语法树（AST）表示法来表示程序。例如，图 3 所示的 AST 对应于部分程序头

，其中每个问号都是一个尚未确定的漏洞（即未知程序）。我们认为部分程序是从每个 AST 节点到特定组件的分配。

给定 AST 表示部分程序 P（最初是单个未分配的根节点），我们的合成算法将确定如何填补 P 中的漏洞。换句话说，将部分程序视为从 AST 节点到 DSL 结构的部分分配，决定组件的目标是在 AST 中选择一个未分配的节点 N 并确定要分配给 N 的 DSL 结构。

Decide 组件。我们的技术要求由 Decide 组件进行分配，以服从已添加到知识库

中的任何引理。因此，进行与知识库一致的分配需要检查命题公式的可满足性。但是，由于通常存在许多与知识库一致的不同决策，因此“Decide”组件还会另外咨询统计模型以预测最“有前景”的任务。

推导。在由“Decide”组件进行每次分配后，Neo 进行推论以检查当前的部分程序是否可行。 我们的推论引擎利用了 DSL 的语义，它是每个组件的一阶规约。例如，表 1 列出了三种 DSL 结构的规约，即 take，head 和 filter。在这里，take 规约指出输出序列的最大元素和大小不大于输入序列的最大元素和大小。head 的规约相似，并指出输出的最大元素不大于输入的最大元素。最后，filter 规约指出，输出的大小（最大，最大）小于输入序列的大小（最大，不大于）。

分析冲突。我们技术的关键新颖之处在于它具有分析冲突和学习有用的引理的能力，这些引理可防止将来出现类似的错误决定。通过计算这些等价类，我们可以从当前冲突中进行概括，并学习许多其他保证不可行的局部程序。然后将此信息编码为 SAT 公式并添加到知识库中，以避免将来发生类似的冲突。

​

​ 在每次调用 Decide 之后，合成算法会推断当前决策所隐含的其他分配。这些推论是通过算法 3 中总结的传播过程得出的。

给定一个决策（H，P），Propagate 首先用乘积 p 填充孔 H； 然后，它检查此决定是否暗含了其他分配。在这种情况下，传播过程将递归调用自身以进一步传播此分配。

​ 除了识别当前决策所隐含的分配外，我们的合成过程还执行另一种形式的演绎，以修剪不符合规约的部分程序。这种演绎形式是通过算法 4 中概述的 CheckConflict 过程执行的。

​ 在本节中，我们将注意力转移到冲突分析过程上，学习新的引理以增加知识库。据我们所知，我们的方法是第一种合成技术，可以通过分析冲突的根本原因来排除无关的部分程序。

我们的学习算法的基本思想是识别等价模冲突的 DSL 操作符。

​ 我们已经使用 Java 编写的名为 Neo 的工具实现了冲突驱动的合成框架。Neo 使用 SAT4J SAT 解算器来实现“决策和传播”，并使用 Z3 SMT 解算器来检查冲突。

​ 决策。Neo 使用逻辑和统计推理的组合来识别要填充的孔以及如何填充孔。但是，我们的“决策”实现与算法 2 的不同之处在于，我们不会发出完整的 SAT 查询来确定决策是否与知识库一致。由于检查孔和零部件的每种组合的可满足性可能非常昂贵，因此我们实施的 Decide 通过单位传播来过分逼近可满足性。特别是，如果将单位传播应用于相应的 SAT 公式不会导致矛盾，则我们认为分配是可行的。请注意，将完整的 SAT 查询替换为单位传播不会影响我们方法的正确性或完整性。特别是，该算法可能比使用完整的 SAT 查询最终检测到冲突，但是它还减少了开销，而不会影响任何可靠性和完整性。由于有许多可能的作业与知识库不矛盾，因此 Neo 使用统计模型来识别“最有前途”的作业。我们当前的实现支持两种不同的统计模型，即 2-gram 模型（在 Morpheus 中使用）以及深度神经网络模型（在 DeepCoder 中描述）。虽然 2-gram 模型仅考虑当前的部分程序进行预测，但深度神经网络模型同时考虑了规约和当前的部分程序。

传播。传播的目标是识别知识库所隐含的其他分配。我们通过对相应的 SAT 公式执行单位传播来识别此类分配。

冲突检查。我们的 CheckConflict 实现遵循算法 4，并使用 Z3 查询相应 SMT 公式的可满足性。Z3 返回的无法满足的内核不能保证是最小的。由于此过程可能很耗时，因此我们不会最小化不满足要求的内核，但实际上，我们已经观察到 Z3 返回的不满足要求的内核通常很小。我们的 CheckConflict 实现对算法 4 进行了额外的优化：由于不同的部分程序可能共享相同的 SMT 规范，因此算法 4 最终多次查询同一 SMT 公式的可满足性。因此，我们的实现会记住每个 SMT 调用的结果，以避免多余的 Z3 查询。

冲突分析。我们的 AnalyzeConflict 实现对第 4 节中介绍的算法进行了两个附加的优化。首先，我们的实现并未将所有学习到的引理保留在知识库中。特别是，由于“决策和传播”的效率对知识库的大小很敏感，因此我们的实现使用启发式方法来识别可能没有用的引理，并定期将其从知识库中删除。其次，我们的实现执行优化以促进等价模冲突的组件的计算。

回溯。与基于 CDCL 的 SAT 求解器相似，Neo 可以通过分析从 AnalyzeConflict 获得的引理来执行非按时间顺序回溯。我们的实现采用标准的 SAT 求解器启发式方法，可回溯到所有 di 决策中的第二高决策级别。此策略通常导致非按时间顺序回溯，并导致算法同时撤销多个分配。

新领域实例化 Neo。作为一般的合成框架，可以通过提供合适的 DSL 和每个 DSL 构造的相应规约，在新的领域中实例化 Neo。如前所述，这些规约并不需要精确，并且通常没有充分说明构造函数的功能，无法在性能开销与修剪搜索空间之间取得良好的平衡。我们目前已经实现了 Neo 的两个实例化，其中一个针对 R 中的数据整理任务，另一个针对功能范式中的序列操作。对于这两个领域，我们的规约均以无量词的 Presburger 算法表示。更具体地说，对于数据争用域，我们使用先前工作中考虑的相同 DSL 和相同规约。对于序列操作域，我们使用与以前的工作中相同的 DSL，但是要编写自己的规范，因为它们在 DeepCoder 设置中不可用。特别是，我们的规约捕获了序列的大小，序列的第一个和最后一个元素的值以及序列的最小和最大元素。我们的经验表明，在新的域中实例化 Neo 不需要太多的人工。例如，我们花了不到一天的时间就在前面提到的两个域中实例化 Neo。

​ 在我们的第一个实验中，我们将 Neo 与 Morpheus 进行了比较，Morpheus 是一种最先进的合成工具，可以自动执行 R 中的数据整理任务。Neo 与 Morpheus 相似之处在于，这两种技术都使用推论来修剪搜索空间，Morpheus 使用几种特定于域的启发式方法，这些启发式方法专门针对表转换。相反，Neo 不使用任何此类特定于域的启发式方法，而是直接应用第 3 节中介绍的通用合成算法。为了公平地比较工具，我们使用 Morpheus 所用的同一套 R 库方法实例化 Neo。此外，由于 Morpheus 使用 2-gram 模型对搜索进行优先排序，因此我们在 Neo 的 Decide 组件中也使用了相同的统计模型。与 Morpheus 一样，我们在从 Stackoverflow 收集的 15,000 个代码段上训练了 2-gram 模型。

​ 标准检查程序的选择。我们在由 50 个具有挑战性的数据处理任务组成的数据集上比较 Neo 和 Morpheus。在这 50 个标准检查程序中，有 30 个对应于用于评估 Morpheus 的最困难的，其中以合成时间来衡量难度。我们还包括从 Stackoverflow 帖子中收集的 20 个其他标准检查程序。为了确保这些基准测试具有足够的挑战性，我们仅考虑那些包含在答案中的所需程序，以及包含 12 个以上 AST 节点和至少四个高阶组件的程序。、

​ 结果。我们的第一个实验的结果总结在图 6 中，该图绘制了累积的合成时间（y 轴）与所解决的标准测试程序数量（x 轴）的关系。从该图可以看出，Neo 在合成时间以及在 5 分钟时间内解决的标准测试程序数量方面均明显优于 Morpheus。尤其是，Neo 可以以 19 秒的平均运行时间解决 90％的标准测试程序，而 Morpheus 可以以 68 秒的平均运行时间解决 64％的标准测试程序。这些结果表明，我们提出的合成方法能够胜过专门针对数据整理任务的特定领域合成工具。

​ 不同组件的影响。图 7 评估了 Neo 中不同组件对数据争夺测试程序的影响。特别是，我们将 Neo 解决的检查程序测试数量与“baseline”，“ml”，“deduce”和“learn”四个变体进行了比较。“baseline”变体使用带有随机决策器深度优先搜索，只能解决 10％的测试程序。“ml”变体使用 Morpheus 的 2-gram 模型作为决策器，这进一步将解决测试程序的数量提高到 20％。通过结合统计推理和推论，“deduce”变体将已解决测试程序的数量从 20％显着提高到 70％。最终，Neo 达到了最佳性能，通过结合所有这些成分，可以解决 90％的测试程序。

​ 在我们的第二个实验中，我们将 Neo 与重新实现的 DeepCoder 进行了比较，DeepCoder 是使用深度学习指导搜索的最先进的合成工具。因为 DeepCoder 擅长操纵列表的功能程序，所以我们使用与 DeepCoder 相同的 DSL 构造在相同的域上实例化 Neo。但是，由于 DeepCoder 并未利用组件规范规约来修剪搜索空间，因此我们还为每个 DSL 结构编写了一阶规约。为了公平地比较工具，我们还使用了 DeepCoder 中使用的相同的深度神经网络模型。我们在 1,000,000 个随机生成的程序及其相应的输入输出示例中训练了我们的深度神经网络模型。

​ 结果。该实验的结果总结在图 8 中，该图还绘制了运行时间与已解决测试程序的数量之间的关系。从图 8 中可以看出，Neo 在运行时间和在 5 分钟时间内解决的测试程序数量方面胜过 DeepCoder。特别是，Neo 可以以平均 99 秒的运行时间解决 71％的测试程序。相比之下，DeepCoder 可以解决 32％的测试程序，平均运行时间为 205 秒。

​ 在我们的第三个实验中，我们通过将 Neo 与 Neo 进行比较，进一步评估了冲突驱动学习的好处，Neo 是不执行冲突分析的 Neo 版本。换句话说，Neo 与 Neo 相同，除了它不调用 AnalyzeConflict 过程并且不向知识库添加引理（除了阻止当前分配外）。为了确保 Neo 不会引起不必要的开销，我们还修改了 CheckConflict 过程以给出是/否答案，而不是产生最小的不满意内核。

该实验的结果总结在图 10 和 11 中。具体地说，图 10 在 7.1 节中的数据整理基准上比较了 Neo 与 Neo ，而图 11 显示了在 6.2 节中使用的序列操作基准的相同比较。从这些数字可以看出，学习对 Neo 的整体表现产生了非常显著的积极影响。具体来说，在数据争用领域中，Neo 的基准测试超时了 30％，平均运行时间为 38 秒。另一方面，Neo 仅在测试程序的 10％时超时，同时保持平均运行时间为 19 秒。如图 11 所示，在序列操作域中，学习的效果甚至更好。具体来说，Neo 在 44％的测试程序中超时，其平均运行时间为 199 秒。相比之下，Neo 仅在 29％的测试程序上超时，平均运行时间为 99 秒。

我们基于冲突驱动学习的思想提出了一个新的合成框架。给定一个伪造的违反规约的部分程序，其核心思想是推断出一个引理，该引理可用于防止将来发生类似的错误。我们的合成算法通过识别等价模冲突的 DSL 结构来推断这些引理，这意味着用一个组件替换另一个组件会导致另一个不可行的程序。

我们已经在名为 Neo 和实例化 Neo 的合成框架中针对两个不同的应用程序域实现了这些想法，这两个应用程序域是数据整理和序列操作。我们已经使用了 130 个测试程序评估 Neo，这些基准与数据整理和序列转换任务有关。我们的评估表明，Neo 优于分别在这两个领域专门研究的最新合成工具 Morpheus 和 DeepCoder。我们的实验还表明，冲突驱动的学*提高了合成器的功能。

在将来的工作中，我们有兴趣在更多应用程序域中实例化 Neo。由于冲突驱动的学习在涉及大量组件的领域中特别有用，因此我们计划使用 Neo 来合成需要使用许多不同库的程序。

本文由南京大学软件学院 2020 级硕士研究生刘智彪翻译转述