In the recent years, we have seen the emergence of a new research area called program synthesis. The goal of program synthesis is to enable computers to write programs from incomplete programs (a.k.a sketch), input/output examples, units tests, high-level specifications, and demonstrations. Program synthesis harnesses recent advances in constraint-solving, verification, program analysis, type-systems, symbolic execution, and machine learning to synthesize non-trivial programs. In the course, we will read papers on the foundations of program synthesis, as well as recent applications of deep learning and "Big Code" to program synthesis.

Time and Location:

• 310 Soda Hall.
• Fridays 3:30 pm - 5:30 pm for paper presentation and discussion.
• Fridays 5:30 pm - 6:30 pm for project supervision.

Instructor

• Koushik Sen
• Student volunteers: Richard Liaw and Rohan Bavishi

Course topics

• Enumerative synthesis
• Counter-example guided synthesis
• Type-based synthesis
• Syntax-directed synthesis
• Super-optimization
• Machine learning and deep learning based synthesis

Piazza Link

• https://piazza.com/class/jl8k8s764sb6jh

Project Milestones

We are expecting that you will do a project in this course to get hands on experience if you have enrolled for 3 units. The project is expected to be done in teams of 2. It is fine if the project mostly gets negative results. You can also enroll in the course for 2 units to skip the project.

1. 9/7/2018: Pick a problem domain for program synthesis and show some examples of the inputs that programmers would provide and the kind of programs you would like to synthesize based on such inputs. Inputs could be specifications, I/O examples, natural language descriptions, demonstrations, unit tests. Post it on Piazza by 9/7/2018, 3:00 pm under the #projects folder.
2. 9/14/2018: Collect a set of benchmarks containing pairs of the form (user input, desired program). We should have at least 50 such benchmarks. Create a private github repo and add the benchmarks to the repo. Share the repo on Piazza by 9/14/2018, 3:00 pm by responding to your post above.
3. 9/21/2018: Outline a plan for solving the synthesis problem and post the writeup on Piazza by 9/21/2018, 3:00 pm by responding to your post above.
4. Weekly updates from 9/28/2018 onwards. Update github repo and the post on Piazza.

Schedule

• 8/31: Chapters 1, 2, and 3 of the book at https://www.microsoft.com/en-us/research/publication/program-synthesis/, Speaker: Abdus Salam Azad and Gil Lederman
• 9/7: Combinatorial Sketching for Finite Programs, Lezama et al. (Sketch-based Search) Speaker: Paras Jain
  • Optional Reading #1: Sketching Concurrent Data Structures (Application), Lezama et al.
  • Optional Reading #2: From Program Verification to Program Synthesis (Similar in spirit, uses lattice search instead of combinatorial), Srivastava et al.
• 9/14: Oracle-guided component-based program synthesis, Jha et al. (Constraint-based Search) Speaker: Kevin Laeufer
  • Optional Reading #1 : DirectFix : Looking for Simple Program Repairs (Application to Program Repair), Mechtaev et al.
• 9/21: TRANSIT: Specifying Protocols with Concolic Snippets, Udupa et al. , SyGuS (3.4), (Enumerative Search) Speaker: Hezheng Yin
  • Optional Reading #1: Synthesis through Unification, Alur et al.
  • Suggested Reading by Koushik #1 : Scaling Enumerative Program Synthesis via Divide and Conquer, Alur et al. (TACAS '17)
  • Suggested Reading by Koushik #2 : Accelerating Search-Based Program Synthesis using Learned Probabilistic Models, (Improving the previous paper by adding probabilistic search) Alur et al. (PLDI '18)
• 9/28: Automating String Processing in Spreadsheets using Input-Output Examples, Gulwani, (Programming-by-example and Domain-Specific Inductive Synthesis) Speaker: Rohan Bavishi
  • Optional Reading #1: FlashExtract: A Framework for Data Extraction by Examples, Le at al.
  • Optional Reading #2: FlashMeta: A Framework for Inductive Program Synthesis , Polozov et al.
• 10/5: Stochastic Superoptimization, Schkufza et al. , SyGuS (3.6) (Superoptimization, Stochastic Search) Speaker: Ryan Shaffer
  • Optional Reading #1: From Invariant Checking to Invariant Inference Using Randomized Search (Application), Sharma et al.
• 10/12: Neuro-symbolic Program Synthesis, Parisotto et al. (Neural Program Synthesis) Speaker: David Chan
  • Optional Reading #1: RobustFill : Learning from Noisy Data (Successor to the above), Devlin et al.
• 10/19: DL Intro + DeepCoder - Learning to Write Programs, Balog et al. (Early paper on Neural Search over a discrete space)
• 10/26: Invited talk from Facebook
  • Neural Turing Machines, Graves et al. (First paper on Neural Computational Architectures) (2016)
• 11/02 : No Class
• 11/09:
  • Towards Synthesizing Complex Programs from Input-Output Examples, Chen et al. Speaker: Xinyun Chen
  • DialSQL: Dialogue Based Structured Query Generation - Izzeddin Gur, Semih Yavuz, Yu Su, Xifeng Yan. Speaker: Rohan Bavishi
• 11/16:
  • Neural Architecture Search: A Survey. Speaker: Paras Jain
  • Code Completion with Neural Attention and Pointer Networks - Jian Li, Yue Wang, Michael R. Lyu, Irwin King. Speaker: Hezheng Yin
• 11/30: No class
• 12/7: Project presentation in class

Tentative Schedule and List of DL+Synthesis Papers for Discussion

• DeepCoder - Learning to Write Programs, Balog et al. (Early paper on Neural Search over a discrete space) (Not very effective) (2017)
• Neural-Guided Deductive Search for Real-Time Program Synthesis from Examples, Kalyan et al. (Combining Neural Networks and Deductive Search as in Flashfill) (2018)
• Making Neural Programming Architectures Generalize via Recursion, Cai et al. (Improving generalization of NPIs) (ICLR Best paper) (2017)
• Towards Synthesizing Complex Programs from Input-Output Examples, Chen et al. (Controlling a non-differentiable machine via RL to learn parsing) (2018)
• Efficient Synthesis of Probabilistic Programs - Microsoft, Nori et al. (PLDI 15)

Reading List