Introduction to program synthesis

Lecture0:Slide1; Lecture0:Slide2; Lecture0:Slide3; Lecture0:Slide4; Lecture0:Slide5; Lecture0:Slide6

Anouncements

Recitation scheduled: 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.

Course description

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.

Grading

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 project.

• 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.

Project

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:

• Team composition (2.5%): You must register your team here before the Wednesday Feb. 26 through this form.
• 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.

Graduate vs. Undergraduate 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 here.