Absynthe：抽象解释引导的程序综合
Absynthe: Abstract Interpretation-Guided Synthesis
AI总结：
本文提出语言无关的 Absynthe，用用户自定义抽象语义引导搜索并以具体测试验证，在 SyGuS 与 Pandas 基准上达到具竞争力结果。
摘要：
近年来，程序综合工具取得了显著成功。然而，以往方法通常需要将源语言完整且准确地嵌入到底层求解器的逻辑中，这种做法对于工业级语言而言十分困难。另一些方法则将源语言的语义与专门构建的综合器耦合在一起，从而不可避免地使综合引擎绑定于特定语言模型。本文提出 Absynthe，这是一种基于用户自定义抽象语义的替代方法，旨在兼具轻量性和语言无关性，同时仍能有效引导程序搜索。Absynthe 中的综合目标由轻量级用户自定义抽象域中的抽象规约以及具体测试用例共同指定。综合引擎由抽象语义参数化，并且独立于源语言。Absynthe 使用真实的具体语言实现，依据测试用例验证候选程序，以确保正确性。我们形式化了 Absynthe 的综合规则，并描述了如何在 Ruby 实现中扩展这些关键思想。我们在 SyGuS 字符串基准测试上评估了 Absynthe，发现它与其他枚举搜索求解器具有竞争力。此外，Absynthe 组合抽象域的能力使用户能够在成本谱系上进行权衡：表达能力更强的抽象域可以剪枝更多程序，但需要更多时间。最后，为验证 Absynthe 可作为通用程序综合工具，我们使用 Absynthe，借助类型和数据帧列标签等简单抽象，在 Python 中综合操作 Pandas 数据帧的程序。Absynthe 达到了与 AutoPandas 相当的水平，后者是面向同一基准套件、基于深度学习的工具。总之，结果表明 Absynthe 是迈向通用程序综合方法的有前景一步，有望将程序综合的适用性扩展到更多……
英文摘要：
Synthesis tools have seen significant success in recent times. However, past approaches often require a complete and accurate embedding of the source language in the logic of the underlying solver, an approach difficult for industrial-grade languages. Other approaches couple the semantics of the source language with purpose-built synthesizers, necessarily tying the synthesis engine to a particular language model. In this paper, we propose Absynthe, an alternative approach based on user-defined abstract semantics that aims to be both lightweight and language agnostic, yet effective in guiding the search for programs. A synthesis goal in Absynthe is specified as an abstract specification in a lightweight user-defined abstract domain and concrete test cases. The synthesis engine is parameterized by the abstract semantics and independent of the source language. Absynthe validates candidate programs against test cases using the actual concrete language implementation to ensure correctness. We formalize the synthesis rules for Absynthe and describe how the key ideas are scaled-up in our implementation in Ruby. We evaluated Absynthe on SyGuS strings benchmark and found it competitive with other enumerative search solvers. Moreover, Absynthe's ability to combine abstract domains allows the user to move along a cost spectrum, i.e., expressive domains prune more programs but require more time. Finally, to verify Absynthe can act as a general purpose synthesis tool, we use Absynthe to synthesize Pandas data frame manipulating programs in Python using simple abstractions like types and column labels of a data frame. Absynthe reaches parity with AutoPandas, a deep learning based tool for the same benchmark suite. In summary, our results demonstrate Absynthe is a promising step forward towards a general-purpose approach to synthesis that may broaden the applicability of synthesis to more $\ldots$
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
