Strange Loop

Program Synthesis: A Dream Realized?

The dream of program synthesis seeks to automatically create programs that conform to a user’s intent. Classically,  program synthesis has been framed as a problem of generation of correct-by-construction programs from complete, formal specifications of their expected behavior. An increasingly favored and more tractable paradigm of program synthesis, however, is inductive program synthesis. Broadly construed, inductive program synthesis can be framed as a problem of generalizing partial specifications of program behavior, such as a set of input-output examples, into programs that are potentially correct over the entire input domain.   Unfortunately, similar to other inductive reasoning engines such as AI-based systems, inductive synthesis engines encounter challenges like overfitting, ambiguity, and brittleness. Thus, while the synthesized program may indeed conform to its partial specification, it may not exhibit the intended behavior on unseen inputs. PL researchers have been trying to tackle these problems through syntactic inductive biases applied to the space of candidate programs. However, the dream of program synthesis is yet to be realized.   In this talk, I will present a gentle introduction to classical and inductive program synthesis, illustrate common problems faced by inductive reasoning engines and common inductive biases used to offset the problems, and describe my group’s semantics-guided approach to improve the generalizability and robustness of inductive synthesis engines.

Roopsha Samanta

Roopsha Samanta is an Assistant Professor the Department of Computer Science at Purdue University. She leads the Purdue Formal Methods (PurForM) group and is a member of the Purdue Programming Languages (PurPL) group. Before joining Purdue in 2016, she completed her PhD at UT Austin in 2013, advised by E. Allen Emerson and Vijay K. Garg, and was a postdoctoral researcher at IST Austria from 2014-2016 with Thomas A. Henzinger. She is a recipient of the 2019 NSF CAREER award. Roopsha's research interests are in program verification, program synthesis, and concurrency. She like to work at the intersection of formal methods and programming languages to develop frameworks to assist programmers write reliable programs. Her current research agenda is centered around two themes—formal reasoning about distributed systems and semantics-guided inductive program synthesis and repair.