Search papers, labs, and topics across Lattice.
This paper introduces "presynthesis," a novel offline phase to accelerate program synthesis by precomputing a tree automaton representing program executions under abstract semantics. This automaton is then used to build an oracle for efficient pruning during synthesis, overcoming the performance bottleneck of costly pruning associated with finer-grained abstract semantics. Experiments across SQL, string transformation, and matrix manipulation domains demonstrate Foresighter, their presynthesis-based synthesis framework, significantly outperforms existing approaches.
Finer-grained abstract semantics can finally deliver on its promise of faster program synthesis, thanks to a new offline "presynthesis" phase that avoids costly online pruning.
Abstract semantics has proven to be instrumental for accelerating search-based program synthesis, by enabling the sound pruning of a set of incorrect programs (without enumerating them). One may expect faster synthesis with increasingly finer-grained abstract semantics. Unfortunately, to the best of our knowledge, this is not the case, yet. The reason is because, as abstraction granularity increases -- while fewer programs are enumerated -- pruning becomes more costly. This imposes a fundamental limit on the overall synthesis performance, which we aim to address in this work. Our key idea is to introduce an offline presynthesis phase, which consists of two steps. Given a DSL with abstract semantics, the first semantics modeling step constructs a tree automaton A for a space of inputs -- such that, for any program P and for any considered input I, A has a run that corresponds to P's execution on I under abstract semantics. Then, the second step builds an oracle O for A. This O enables fast pruning during synthesis, by allowing us to efficiently find exactly those DSL programs that satisfy a given input-output example under abstract semantics. We have implemented this presynthesis-based synthesis paradigm in a framework, Foresighter. On top of it, we have developed three instantiations for SQL, string transformation, and matrix manipulation. All of them significantly outperform prior work in the respective domains.
