MANTIS: Semantics-driven Inductive Program Synthesis

The dream of classical program synthesis is to generate programs from complete, formal specifications of their expected behavior. An increasingly favored paradigm of synthesis is inductive program synthesis, where specifications of program behavior are provided in the form of examples. Inductive program synthesis not only helps make program synthesis more tractable, but also has the potential to democratize programming!

Unfortunately, inductive synthesis engines encounter challenges like overfitting, ambiguity, and brittleness, similar to other inductive reasoning engines such as AI-based systems. PL researchers have typically attacked these problems by applying syntactic biases to the search space in the form of tailored DSLs, grammars and ranking functions. In this talk, I will show how one can further enhance the generalizability and robustness of such synthesis engines by applying semantic biases to the search space.

References:
1. Augmented Example-based Synthesis using Relational Perturbation Properties.
S. An, R. Singh, S. Misailovic and R. Samanta. POPL 2020.
2. SemCluster: Clustering of Imperative Programming Assignments Based on Quantitative Semantic Features.
D. M. Perry, D. Kim, R. Samanta and X. Zhang. PLDI 2019.
3. Qlose: Program Repair with Quantitative Objectives.
L. D'Antoni, R. Samanta and R. Singh. CAV 2016.