CS5733 Program Synthesis

CS5733 Program Synthesis

Overview

Program Synthesis, the problem of automatically generating programs from user requirements, is a classic problem in Computer Science. These requirements can take several forms like formal logical formulas, input-output examples, and more recently, using higher-level inputs like images and natural languages. The motivation for synthesis stems from the fact that it is often easier for the user to convey the intent of the program compared to writing the complete program. Additionally, synthesis can also help in generating correct-by-construction programs, this can be particularly fruitful for tasks that are error-prone and/or safety-critical systems. Program synthesis sits at the intersection of programming languages, automated reasoning, and machine learning. This interdisciplinary nature of the field has sparked significant interest in recent years, with exciting developments in each of these areas.

This course will offer a broad study of the theory and practices of program synthesis. We will cover different classes of program synthesis techniques, like inductive synthesis vs. deductive synthesis, top-down vs. bottom-up, etc., and introduce underlying foundations for each class. The course will also cover major recent developments in the field, like type-driven synthesis, synthesizing domain-specific programs, and neuro-symbolic syntheses combining ML and PL techniques for program synthesis.

Pre-requisite(s): Open to CSE BTech 3rd year, 4th year, MTech and PhD students. No formal pre-requisite, expected background: Discrete Maths, Software Development Fundamentals and Data Structures.

Others please drop me an email about your interest and your department and course.

Classroom and Timings
Schedule
Textbook and Resources
  • Instructor-provided list of research papers.
  • Program Synthesis, Foundations and Trends® in Programming Languages. S. Gulwani, O. Polozov and R. Singh. ISBN: 978-1-68083-292-1
  • Types and Programming Languages (MIT Press) First Edition, Benjamin C. Pierce. ISBN: 9780262162098
  • Neuro-symbolic Programming, Foundations and Trends® in Programming Languages. Swarat Chaudhuri, Kevin Ellis, Oleksandr Polozov, Rishabh Singh, Armando Solar- Lezama and Yisong Yue.
Evaluation
Item Nos. Weight (%)
Paper Reviews 9 40
Class Attendance _ 5
Course Project 1 50
Class Participation - 5

 

Reading List and Paper Reviews
Review Content

A review should start with a short, neutral summary of the paper (1-2 paragraphs), followed by a list of paper’s main contributions/insights, and a list of its limitations. Finally, answer specific questions posted for this paper on the Google Classroom about the paper List (if any). Our goal is to get you to think deeply and critically about the paper, not to test you. You won’t be graded on the correctness of your reviews; any non-trivial review will get you 5%.

Reading List
  • Week 2:

    • EUSolver Rajeev Alur, Arjun Radhakrishna, Abhishek Udupa: Scaling Enumerative Program Synthesis via Divide and Conquer. TACAS’17

    • Questions:
      • What does EUSolver use as behavioral constraints? Structural constraint? Search strategy?
      • What are the main two pruning/decomposition techniques EUSolver uses to speed up the search? What enables these techniques?
      • What would a naive alternative to decision tree learning be for synthesizing branch conditions? What are the disadvantages of this alternative?
    • Submit Responses Here
  • Week 3:
    • Euphony Woosuk Lee, Kihong Heo, Rajeev Alur, Mayur Naik: Accelerating Search-Based Program Synthesis usingLearned Probabilistic Models. PLDI’18
    • Questions:
      • What does Euphony use as behavioral constraints? Structural constraint? Search strategy? How are they different from EUSolver?
      • Consider Fig 2b, where the synthesizer is unrolling the sentential form Rep(x,”-“,S). When the search is guided by a PHOG, it considers the weighted productions shown in Fig 2a (top). What would these productions look like if we replaced the PHOG with a PCFG? With 3-grams? Do you think these other probabilistic models would work as well as a PHOG?
      • Consider Example 3.2. Explain in English the intuitive meaning of h(S) = 0.1 and why it is the case.
      • Consider Theorem 3.7. Give an example of sentential forms $n_i$ , $n_j$ and set of points pts such that n_i and n_j are equivalent on pts but not weakly equivalent.
    • Submit Responses Here
  • Week 4:
    • A partial reading break.
  • Weel 5:
    • Yu Feng, Ruben Martins, Osbert Bastani, and Isil Dillig. 2018. Program synthesis using conflict-driven learning.
    • Questions
      • What does Neo use as behavioral constraints? Structural constraint? Search strategy?
      • Consider the component specifications given in Table1, What family of logic and theory (if any) do these specifications belong? Are the specifications for the partial programs, i.e. SAT encoding of Programs (as done in Definition 4.1) from the same family?
      • Consider Table1 again, add a specification reverse function for the list as well. Further show, adding these, what will be the new specification for the partial program generated by replacing head in Figure 3 with reverse.
      • Analyze conflict on the new partial program given in the previous question. Find the MUC if there is a conflict.
    • Submit Responses Here
Project ideas

Disclaimer All information on this class website is tentative and subject to change. This course is inspired significantly from other Program Synthesis classes at MIT, UCSD, and UW Madison. Please, check them as well.