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$

翻译：合成工具近年来取得了显著成功。然而，以往的方法通常需要将源语言完整且精确地嵌入到底层求解器的逻辑中，这对于工业级语言而言难以实现。其他方法则将源语言的语义与特定构建的合成器耦合，必然将合成引擎绑定到特定的语言模型上。在本文中，我们提出了一种基于用户定义抽象语义的替代方法——Absynthe，它旨在既轻量化又与语言无关，同时有效指导程序搜索。Absynthe中的合成目标通过轻量级用户定义抽象域中的抽象规范以及具体测试用例来指定。合成引擎以抽象语义为参数，且独立于源语言。Absynthe使用实际的具体语言实现对候选程序进行测试用例验证，以确保正确性。我们形式化了Absynthe的合成规则，并描述了我们如何在Ruby实现中扩展这些关键思想。我们在SyGuS字符串基准测试上评估了Absynthe，发现它与其他枚举搜索求解器相比具有竞争力。此外，Absynthe组合抽象域的能力允许用户沿着成本谱移动，即表达力强的域能剪枝更多程序，但需要更多时间。最后，为了验证Absynthe能否作为通用合成工具，我们使用Absynthe在Python中通过数据框的类型和列标签等简单抽象合成Pandas数据框操作程序。Absynthe与基于深度学习的工具AutoPandas在同一基准测试套件上达到了同等性能。总之，我们的结果表明，Absynthe朝着通用合成方法迈出了有希望的一步，可能拓宽合成在更多领域中的应用……