Introduction to program synthesis (SC5401)

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

Course description

This webpage is for the course SC5401 that was offered at NTU as part of the Turing AI Scholars Program in February 2026. This is a somewhat abridged version of the course 6.5130 Introduction to Program Synthesis taught at MIT.

This course aims to give an introduction to program synthesis, an exciting 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 generate programs that do what the user wants. 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 worth 30, 40 and 30% of the final grade respectively. All assignments and deadlines will be posted here.

Date	Title	Pset
Monday February 2	Introduction to Inductive Synthesis; Bottom Up Explicit Search	Assignment 1
Tuesday February 3	Top Down and Type Directed Explicit Search; Inductive Synthesis with Stochastic Search
Wednesday February 4	Tutorial
Friday February 6	Version Space Algebras from SMARTedit to FlashFill; Synthesis with constraints	Assignment 1 due
Monday February 9	Solving constraints with SAT solvers; Component Discovery	Assignment 2
Tuesday February 10	Basics of Language Modeling for Code
Wednesday February 11	Tutorial
Friday February 13	Sampling from Large Language Models	Assignment 2 due	Project teams due
Tuesday February 24	Adapting Pre-Trained Models to New Tasks; Program Synthesis with Reinforcement Learning	Assignment 3
Friday February 27	Introduction to Functional Synthesis: Functional specifications; Inductive to Functional synthesis with CEGIS.
Tuesday March 10	A brief introduction to constraint-based verification; From verification conditions to synthesis conditions
Friday March 13	Introduction to SMT and SyGuS		Assignment 3 due
Tuesday March 17	Tutorial;