© 2021 Strange Loop
An increasingly favored paradigm of program synthesis is inductive program synthesis (or, programming by examples) which accepts specifications of program behavior in the form of examples. Inductive program synthesis is certainly more tractable than classical program synthesis which seeks to generate correct-by-construction programs from complete, formal specifications of their expected behavior. Moreover, because examples are easier to provide than formal specifications, inductive program synthesis has the potential to democratize programming by enabling non-experts to program with the help of synthesizers!
Unfortunately, similar to other inductive reasoning engines such as AI-based systems, inductive synthesis engines encounter challenges like overfitting, ambiguity, and brittleness. PL researchers have typically attacked these problems by applying syntactic inductive biases to the search space in the form of tailored domain-specific languages, grammars, and ranking functions. In my recent research, we are focusing on further enhancing the generalizability and robustness of such synthesis engines by applying semantic inductive biases to the search space.
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 the semantics-guided inductive synthesis approach being developed in my group.
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.