October 7, 2022
Synthesis of recursive programs has received long-standing and continued interest in the past decade. Among variety of specifications to synthesis problems, input-output examples are easiest to provide by non-experts. However, examples, as specification, are inherently ambiguous, and are especially so for recursive programs. Early works in the field rely on examples that resemble the complete recursion traces to enable performant synthesis algorithm. Recent works, while lifting the requirement by coming up with new examples algorithmically, fail to account for the semantics imposed by the chosen examples. To address the issue, we present trace-guided synthesis for recursive functional programs from examples. Our method explores program space along with their semantic space characterized by recursion traces, where the search of consistent programs and recursion traces guide each other. As a result, the trace-guide algorithm produces a satisfying program space categorized by recursion traces (or their abstractions), allowing us to pick programs by not only syntactic but also semantic features. We have implemented the approach in a prototype called SyRup and showed that it outperforms prior works in terms of generalizability of synthesized programs.
About Yongwei Yuan
Yongwei Yuan is a third-year PhD student in Department of Computer Science at Purdue University working with Prof. Roopsha Samanta. His research interest lies in program synthesis, and more broadly formal methods for programming tools.