一句话：提出 Absynthe，一种语言无关、由用户自定义抽象语义引导的程序合成框架。
现有程序合成方法通常需要把源语言完整且准确地嵌入求解器逻辑，或将语言语义与专用合成器耦合，因而难以适用于工业级语言。Absynthe 提出一种基于用户自定义抽象语义的替代方案：合成目标由轻量抽象域中的抽象规约和具体测试用例给出，合成引擎由抽象语义参数化并与源语言无关，候选程序再用真实语言实现通过测试验证。作者形式化其合成规则，并在 Ruby 中实现。在 SyGuS 字符串基准上，Absynthe 与枚举搜索求解器相比具有竞争力；通过组合抽象域，用户可在表达力与代价之间权衡。作者还用类型和 DataFrame 列标签等简单抽象合成 Python Pandas 程序，效果与基于深度学习的 AutoPandas 持平，表明其有望成为通用合成方法。
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 full-featured languages.
@article{paperbot1966,
title = {Absynthe: Abstract Interpretation-Guided Synthesis},
author = {Sankha Narayan Guria and Jeffrey S. Foster and David Van Horn},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {PLDI},
year = {2023},
doi = {10.1145/3591285}
}