Programming "Programming by Example" by Example

Abstract

Programming by Example (PbE) is an increasingly popular model for writing programs to automate repetitive tasks, such as those common in data wrangling. In this paradigm, the user presents a set of input/output pairs, and an inductive synthesizer responds with a program that satisfies these examples. However, due to performance limitations, these synthesizers must be specialized to the domain at hand. Frameworks like PROSE have been developed to ease the implementation burden when writing synthesizers for domain-specific languages (DSLs), but they remain relatively inaccessible to those who are not experts in programming languages and synthesis. We identify three key challenges facing the users of such tools: designing DSLs, writing deduction rules, and debugging. In order to remove these barriers, we present a new interaction model for developing inductive program synthesizers by example. Rather than write an explicit DSL grammar, the developer communicates their intended domain implicitly, by providing a corpus of programs in a general-purpose language. From these examples, a compiler infers an embedded DSL and outputs an inductive synthesizer for this specialized domain. We demonstrate the viability of this approach with VERSE (VERified Synthesis Engine), a Coq implementation of the Programming "Programming by Example" by Example (PbE^2) interaction model. VERSE comprises a toy general-purpose language and its library of operators, the aforementioned DSL compiler, and a synthesis engine that uses top-down deductive search à la PROSE. It is architected to enable an end-to-end, mechanically verified proof of correctness; this component is under ongoing development. VERSE's implementation is publicly available at https://github.com/gtanzer/verse .