# Efficient Synthesis with Probabilistic Constraints

## TL;DR

This paper improves probabilistic program synthesis by proving polynomial bounds on the number of calls needed and introducing a property-directed method that enhances efficiency on benchmarks.

## Contribution

It provides theoretical bounds for DIGITS and introduces a property-directed variant that significantly reduces synthesis calls.

## Key findings

- DIGITS requires only polynomial calls relative to sample size
- Property-directed DIGITS reduces synthesis calls substantially
- Enhanced performance demonstrated on various benchmarks

## 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.

---
Source: https://tomesphere.com/paper/1905.08364