Efficient Synthesis with Probabilistic Constraints

Abstract

We consider the problem of synthesizing a program given a probabilistic specification of its desired behavior. Specifically, we study the recent paradigm of distribution-guided inductive synthesis ( digits ), which iteratively calls a synthesizer on finite sample sets from a given distribution. We make theoretical and algorithmic contributions: ( i ) We prove the surprising result that digits only requires a polynomial number of synthesizer calls in the size of the sample set, despite its ostensibly exponential behavior. ( ii ) We present a property-directed version of digits that further reduces the number of synthesizer calls, drastically improving synthesis performance on a range of benchmarks.