面向下的度量用于自底向上的枚举合成
Oriented Metrics for Bottom-Up Enumerative Synthesis
AI总结：
本文提出面向下的度量用于自底向上的枚举合成，通过四种技术减少搜索空间，提升合成效率。
摘要：
在语法引导的合成中，一个挑战是减少搜索空间的庞大尺寸。我们观察到，大多数搜索空间不仅仅是程序的扁平集合，但可以赋予一种我们称之为定向度量的结构。定向度量测量程序之间的距离，就像普通度量一样，但设计用于操作具有方向性的设置。我们的重点是字符串和位向量领域，在这些领域中，如连接和位运算将输入转换为输出的方式是非对称的。我们为这些领域开发了几种新的定向度量。定向度量旨在减少搜索空间，我们提出了四种技术：（i）将搜索空间修剪到真实值周围的球体，（ii）通过由定向度量诱导的等价性来分解搜索空间，（iii）抽象定向度量（因此等价性）并对其进行细化，（iv）通过学习抽象信息来改进枚举顺序。我们承认这些技术受到文献发展的启发。通过理解它们在定向度量中的根源，我们可以显著增加其适用性和效率。我们将这些技术整合到一个新的合成算法中，并在新的求解器中实现了该算法。值得注意的是，我们的求解器在计算定向度量时是通用的。我们在字符串和位向量领域进行了实验，并在状态最先进的情况下，性能提高了超过一个数量级。
英文摘要：
In syntax-guided synthesis, one of the challenges is to reduce the enormous size of the search space. We observe that most search spaces are not just flat sets of programs, but can be endowed with a structure that we call an oriented metric. Oriented metrics measure the distance between programs, like ordinary metrics do, but are designed for settings in which operations have an orientation. Our focus is on the string and the bitvector domains, where operations like concatenation and bitwise conjunction transform an input into an output in a way that is not symmetric. We develop several new oriented metrics for these domains. Oriented metrics are designed for search space reduction, and we present four techniques: (i) pruning the search space to a ball around the ground truth, (ii) factorizing the search space by an equivalence that is induced by the oriented metric, (iii) abstracting the oriented metric (and hence the equivalence) and refining it, and (iv) improving the enumeration order by learning from abstract information. We acknowledge that these techniques are inspired by developments in the literature. By understanding their roots in oriented metrics, we can substantially increase their applicability and efficiency. We have integrated these techniques into a new synthesis algorithm and implemented the algorithm in a new solver. Notably, our solver is generic in the oriented metric over which it computes. We conducted experiments in the string and the bitvector domains, and consistently improve the performance over the state-of-the-art by more than an order of magnitude.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
