Teaching Assistants: P. Habeeb and Rekha Pai.
Link to Piazza class: Piazza class (register with code "e0307").
Program synthesis has its roots in formal methods and programming languages. The goal of program synthesis is to automatically generate a program (from a space of possible programs) which satisfies a specification written in logic. The problem has its roots in a paper by Church in 1957, and the initial breakthroughs were made by Buchi and Landweber (1969) and M O Rabin (1972), who showed that the synthesis problem is decidable for specifications written in certain logics. However, the complexity of the algorithms was too high (non-elementary to exptime) to be useful in practice.
Recent formulations have made synthesis more practical. In his PhD thesis, Solar-Lezama formulated synthesis as "sketching" , a process where part of the program is given by the user as a template and the synthesizer merely fills in "holes" in the sketch using search. Another recent formulation, due to Sumit Gulwani uses input/output examples (rather than formulas) as specifications , and uses clever search algorithms to generate appropriate programs. Sparked by these two works, there has been a resurgence or work in program synthesis in the past decade. There is an annual Sygus competition  where practical tools compete every year.
Recently there is an interesting interplay developing between program synthesis and machine learning. Machine learning uses continuous optimization methods to learn models that minimize a specified loss function, whereas program synthesis uses discrete combinatorial search to learn programs that satisfy a specification. While program synthesis produces interpretable programs, which can be formally verified, machine learning deals with noise in the inputs more gracefully. There is a rich body of recent work in combining machine learning and program synthesis to get the benefits of both approaches.
This course will have two parts:
We require students to have good knowledge in programming. We also require students to have taken an introductory course in Machine Learning (regression, classification, deep learning etc). We will not require prior exposure to program synthesis or formal methods. We will supply the necessary background in Part 1. Students will need to show initiative in reading papers for Part 2, and leading discussions in Part 2. Students will also need to do both theory and implementation for the project.
There will be three assignments in the first part of the course (one for each of the main components). The first part of the course will have a written exam around mid-semester. Students will be required to do a project in combining program synthesis and machine learning. Ideas for projects will be inspired by papers discussed in Part 2 above. We will use public benchmarks such as the ones for SyGus competitions or the data used by papers in Part 2 to evaluate projects. The overall course grade will be determined by performance in the assignments and presenatations, mid-semester exam, and the project, with weightage as below.
Weightage for evaluation:
Books and other material
Meeting schedule 3:30pm, Mondays and Wednesdays, in Room 117, CSA.
Lecture Schedule and Slides
|Jan 6, 2020||Sriram||Part a: Introduction and overview. Course introduction, tutorial
intro to synthesis, high level comparisons with ML, and detailed and
"hands-on" tutorial using the Sketch tool.
Part b: Hoare logic: Bridging Programs and Formulas.
|Slides 1(a), Slides 1(b)|
|Jan 9, 2020||Sriram||SAT Solvers
Part a: Intro to SAT, NNF, CNF, Basic DPLL with BCP and ULP.
Part b: Modern DPLL with conflict clauses and non-chronological backtracking.
|Slides 2(a), Slides 2(b)|
|Jan 13, 2020||Sriram||SMT Solvers
Part a: First order logic, theories, models, satisfiability modulo theories, common theories
Part b: Decision procedures for EUF, DIA, LIA, LRA.
|Slides 3(a), Slides 3(b)|
|Jan 16, 2020||Sriram||SMT Solvers
SMT solvers: Nelson-Oppen method for combining theories, Handling disjunctions using SAT
|Jan 20, 2020||Sriram||Synthesis using constraint solvers
Part a: CEGIS (Counter-Example Guided Inductive Synthesis) and OGIS (Oracle Guided Inductive Synthesis)
Part b: Quantifiers and model finding in SMT solvers
|Slides 5(a), Slides 5(b)|
|Jan 22, 29, Feb 3, 5 2020||Deepak||Enumerative and Deductive Search||Slides|
|Feb 06, 2020||Deepak||Model Learning based on Angulin's algorithm||Slides|
|Feb 10, 12 2020||Chiranjib||Semantic Parsing|
|Feb 25, 27, Mar 2, 2020||Chiranjib||Hidden Markov Models, Viterbi decoding, model learning||Book Chapter by Jurafsky and Martin|
Research Papers for Discussion