Program Synthesis

Established: January 1, 2010

Publications

Videos

Groups

Overview

Introduction

Program synthesis is the task of automatically discovering an executable piece of code given user intent expressed using various forms of constraints such as input-output examples, demonstrations, natural language, etc. Program synthesis has direct applications for various classes of users in the technology pyramid:

  • (100s of millions of) End Users (people who have access to a computational device but are not expert programmers): Helping them to create small snippets of code for performing repetitive tasks, simple data manipulation. In other words, enabling them to bring their creativity to life!
  • (Billions of) Students and Teachers: Intelligent tutoring systems (pdf, video) that support solution generation (the step-by-step solution to a problem is like a program! PLDI 2011, IJCAI 2013b), problem generation (of a certain difficulty level and that exercises use of certain concepts AAAI 2014, IJCAI 2013b, CHI 2013, AAAI 2012, AAAI 2015), automated grading (PLDI 2013, IJCAI 2013a) , and digital content creation (CHI 2012). Interestingly, all of these activities can be phrased as program synthesis problems.
  • Software Developers: Help synthesize mundane pieces of code.
  • Algorithm Designers: Help discover new algorithms

Recent advances in AI-style search techniques and formal reasoning techniques based on SAT/SMT solvers have made it possible to efficiently synthesize small programs. I strongly believe that the program synthesis technology is now set to create the next revolution in computing. And hence I spend most of my time working in this area: “devHIeloping new program synthesis techniques and incorporating them into easy-to-use tools” with the goal of democratizing effective use of computational devices, thereby enabling people to bring their creativity to life!

Selected Invited Talks

Dimensions in Program Synthesis [PPDP 2010]

Application Target User User Intent Search Technique
Web Search Strategies [KDD 2014] End Users Logic Natural Language Processing + Implicit Table Inference
Spreadsheet Formulas [SIGMOD 2014] End Users Natural Language Natural Language Processing + Type-based Synthesis
Smartphone Scripts [MobiSys 2013] End Users Natural Language Natural Language Processing + Type-based Synthesis
Data Extraction (from text files and web pages) [PLDI 2014] End Users Examples Version Space Algebra
Data Extraction (from semi-structured spreadsheets) [PLDI 2015] End Users Examples Version Space Algebra
String Transformations [POPL 2011, VLDB 2012, CACM 2012, ICML 2013] End Users Examples Version Space Algebra + Machine Learning
Number Transformations [CAV 2012] End Users Examples Version Space Algebra
Table Transformations [PLDI 2011] End Users Examples Version Space Algebra
XML Transformations [AAAI 2014, PLDI 2014] End Users Examples
Text Transformations [UIST 2013] End Users Set or Sequence of Examples
Geometry Drawings [CHI 2012] End Users Sketch
Geometry Ruler/Compass Constructions [PLDI 2011] Students/Teachers Logic
Geometry Proof Problems [AAAI 2014] Students/Teachers Examples
Algebraic Proof Problems [AAAI 2012] Students/Teachers Examples
Procedural Math Problems [CHI 2013] Students/Teachers Examples
Natural Deduction Problems [IJCAI 2013] Students/Teachers Examples
Grading of Introductory Programming Assignments [PLDI 2013] Students/Teachers Sample Solution Edit-distance based search using Sketch
Grading of Automata Constructions [IJCAI 2013] Students/Teachers Sample Solution Edit-distance based Search
Recursive Programs [CAV 2013] End Users Examples Goal-directed Search
Biological Synthesis [Distraction 2013] First-time PL parents (lack of) Logic Template-based and Inductive
Vectorized Code [PPoPP 2013] Software developers Loop to be vectorized Combination of Deductive and Inductive Synthesis
API Discovery and Code Completion [PLDI 2012] Software developers Partial Expression Type-based search and ranking
Program Inverses [PLDI 2011] Software developers Templates PathTesting-based synthesis + SMT solvers
Bit-vector Algorithms [PLDI 2011, ICSE 2010] Algorithm designers (Logic or Examples) + Components SMT solvers
Graph Algorithms [OOPSLA 2010] Algorithm designers Logic Inductive Learning + SAT solvers
Undergraduate Textbook Algorithms [POPL 2010] Algorithm designers Logic + Templates Invariant-based synthesis + SMT solvers
Switching Logic [ICCPS 2010, VMCAI 2009] Embedded-system designers Logic + Templates (Inductive Learning + Numerical Methods) or SMT Solvers

People