Presynthesis: Towards Scaling Up Program Synthesis with Finer-Grained Abstract Semantics

TL;DR

Presynthesis introduces an offline phase to construct automata and an oracle, enabling faster program synthesis by efficient pruning under abstract semantics, outperforming prior methods.

Contribution

It proposes a novel presynthesis framework with automaton and oracle construction to improve search-based program synthesis efficiency.

Findings

Framework significantly outperforms prior work in SQL, string transformation, and matrix manipulation domains.

Automaton and oracle construction enable efficient pruning during synthesis.

Finer-grained abstract semantics can be leveraged effectively with presynthesis.

Abstract

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.