Absynthe: Abstract Interpretation-Guided Synthesis
Absynthe: Abstract Interpretation-Guided Synthesis
Loading...
Files
Publication or External Link
Date
2023-06
Authors
Guria, Sankha Narayan
Foster, Jeffrey S.
Van Horn, David
Advisor
Citation
Sankha Narayan Guria, Jeffrey S. Foster, and David Van Horn. 2023. Absynthe: Abstract Interpretation-Guided Synthesis. Proc. ACM Program. Lang. 7, PLDI, Article 171 (June 2023), 24 pages.
Abstract
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.