English

Efficient Synthesis with Probabilistic Constraints

Programming Languages 2019-05-22 v1

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.

Keywords

Cite

@article{arxiv.1905.08364,
  title  = {Efficient Synthesis with Probabilistic Constraints},
  author = {Samuel Drews and Aws Albarghouthi and Loris D'Antoni},
  journal= {arXiv preprint arXiv:1905.08364},
  year   = {2019}
}
R2 v1 2026-06-23T09:14:13.062Z