Introduction to program synthesis
The optional recitation will be Fridays at 2-3 PM in room 56-162.
Office hours scheduled:
Office hours will be weekly on Thursdays 4-5 PM, in 32-G716 or the nearby lounge by the elevators.
PSet 1 now posted:
Pset 1 is now posted and can be found here.
PSet 2 now posted:
Pset 2 is now posted and can be found here.
PSet 3 now posted:
Pset 3 is now posted and can be found here.
This course aims to give an introduction to program synthesis, a new field
at the intersection of programming languages, formal methods and AI.
The course will explore a number of fundamental questions
around the problem of how to automatically discover
programs that do what the user expects. In particular,
the class will explore the following questions:
- The intention question: how does the user convey intent and how do we increase the likelihood that the synthesizer will produce the desired program even when the specification is ambiguous or incomplete?
- Interplay between program search and program verification: how do we ensure that the program we synthesize will actually be deemed correct by a potentially brittle verification mechanism, and how do we use a verifier to our advantage to help synthesize programs faster?
- Interplay between program synthesis and deep learning: how do you reconcile the symbolic techniques traditionally used for synthesis and verification with deep learning? We will explore this question in the context of both learning-to-synthesize and differentiable programming paradigms.
- Program synthesis beyond software engineering: the course will also discuss applications of program synthesis beyond automated programming to other domains where one has to generalize from small number of examples and produce interpretable models.
The course will be graded based on three hands-on assignments as well
as a final project where you will get to apply the concepts learned in
the course to the problem of your choice.
If you sign up to receive graduate credit for the course, the three
problem sets will involve additional problems suitable for graduate
students who will be expected to have read some of the original papers
from which the course material is derived. The final project will also
have additional requirements in terms of the depth expected of the
- Assignment 1: 20%
- Assignment 2: 20%
- Assignment 3: 20%
- Project: 40%
All psets are due at 5pm on the posted day. The late penalty will be 10 points
per day up to a maximum of 4 days.
An important part of the grade will be a term project
where students will demonstrate their mastery of
the topics covered in the course. The projects
can apply concepts from the course to a new problem,
or explore new techniqes. The project grade be based
on the following benchmarks:
Graduate vs. Undergraduate credit
- Team composition (2.5%): You must
register your team here before the Wednesday Feb. 26 through
One-page project proposal (12.5%): The proposal
should describe what you plan to do for the project.
The proposal should include information about preliminary
work towards the project (for example, references to
papers you have read related to what you plan to do, or
to tools you have decided to use).
Project presentation (10%): This will be an oral
presentation on the last week of class where you will
report on the outcome of your project.
Project report (15%): The report should be between 4 and seven
pages in the format provided. The project will be graded based
on quality of execution, originality and scope. It is not necessary
to have a positive result in order to obtain full credit.
If you are getting graduate credit for the course, the expectation in
terms of originality of the project will be higher than for undergraduate
credit. In particular, if you are getting undergraduate credit,
a project that simply compares existing techniques, for example, or that
applies an existing tool to a problem you are interested in and describes
the result is sufficient. For graduate credit, we expect some technical
novelty. This can involve exploring a variation of an existing technique,
or an application to a problem where these techniques have not been applied
before. Again, the project grade will not depend on whether the result is
positive or negative, but on how well it is executed.
The webpage for an earlier version of this course can be found