SynGuar: Guaranteeing Generalization in Programming by Example

TL;DR

SynGuar is a framework that guarantees low generalization error in programming by example (PBE) synthesizers, using a dynamic calculation of the number of examples needed, improving accuracy and reducing overfitting.

Contribution

We introduce SynGuar, the first method to theoretically guarantee low generalization error in PBE synthesis by dynamically determining the necessary number of examples.

Findings

A few hundred examples suffice to bound generalization error below 5% with high probability.

SynGuar improves the accuracy of existing synthesizers on string manipulation benchmarks.

Without SynGuar, fewer arbitrarily chosen examples lead to overfitting and reduced accuracy.

Abstract

Programming by Example (PBE) is a program synthesis paradigm in which the synthesizer creates a program that matches a set of given examples. In many applications of such synthesis (e.g., program repair or reverse engineering), we are to reconstruct a program that is close to a specific target program, not merely to produce some program that satisfies the seen examples. In such settings, we wish that the synthesized program generalizes well, i.e., has as few errors as possible on the unobserved examples capturing the target function behavior. In this paper, we propose the first framework (called SynGuar) for PBE synthesizers that guarantees to achieve low generalization error with high probability. Our main contribution is a procedure to dynamically calculate how many additional examples suffice to theoretically guarantee generalization. We show how our techniques can be used in 2 well-known synthesis approaches: PROSE and STUN (synthesis through unification), for common string-manipulation program benchmarks. We find that often a few hundred examples suffice to provably bound generalization error below $5\%$ with high ($\geq 98\%$) probability on these benchmarks. Further, we confirm this empirically: SynGuar significantly improves the accuracy of existing synthesizers in generating the right target programs. But with fewer examples chosen arbitrarily, the same baseline synthesizers (without SynGuar) overfit and lose accuracy.