Introduction to program synthesis
Anouncements
Welcome to 6.S981!When/Where: TR1-2:30 in room 26-328
Join on Piazza.
Friday 11/17: Assignment 3 is now posted. You can find it here. Tuesday 10/17 I came down sick so I won't be able to lecture today, but Kavi will have office hours at the usual class time and place. Tuesday 9/26 and 9/28: I forgot to mention in lecture last week that I am traveling again this week so the 9/26 and 9/28 lectures will be on zoom again. Thursday 9/14: As mentioned in class on Tuesday, the lecture today will be on zoom. Also, the first assignment has now be released. You can find it 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 learning based techniques including language models based on transformers and reinforcement learning.
- 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, as well as neurosymbolic learning techniques that combine ideas from program synthesis with ML.
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. We are in discussions with the department to allow the course to count as a TQE in substitution of 6.820; should have final confirmation in the next couple of weeks.- Assignment 1: 20%
- Assignment 2: 20%
- Assignment 3: 20%
- Project: 40%
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 Tuesday October 4.
- 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). For team projects, each team member should submit their own proposal describing their individual understanding of the project and their expected contribution.
- 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. Each member of the team will have to present individually on their part of the 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. For team projects, each team member will need to submit an independent report; the reports of different team members can share up to 50% of common content, but the other half must reflect the contributions of each individual team member.