Prof. Mark Santolucito
How do we build AI systems that generalize and reason, not just predict? This seminar explores neurosymbolic AI: the integration of neural networks with symbolic structures like programs, logics, and proofs. We will examine program synthesis and LLM-guided code generation, learning as program induction as a path toward genuine abstraction, and how formal methods can constrain and verify neural systems, from theorem proving in Lean to temporal logic specifications as guardrails for agents. Students will read, discuss, and present recent research papers and complete a hands-on project.
Prerequisite: Advanced Programming or equivalent.
Each week we will read and discuss 1-2 research papers. Every student will take a presentation role several times during the semester, and everyone posts a short reading response before each class. The second deliverable is a hands-on project, done individually or in pairs — building, extending, or empirically studying a neurosymbolic system — with a proposal, an in-progress presentation, and a final writeup and presentation.
Grading
| Component | Weight |
|---|---|
| Participation and reading responses | 20% |
| Paper presentation (Author) | 25% |
| Paper presentation (Champion, Critic, Implementer) | 15% (5% x 3) |
| Final project | 40% |
Every week, starting in week 3, we will have a presentation on two papers from the assigned reading. It is run as a role play: three students take a role for that paper, and the rest of the class comes ready to join the cross-examination with questions from their reading response. Sign-ups happen in Week 2. Over the semester everyone plays each role at least once — the point is that you get practice reading a paper generously and adversarially.
Author (~15 min, slides). Present the paper as if you wrote it. What problem were you stuck on, what was the key idea that unstuck it, and what do the experiments actually show? Do not narrate the paper section by section — tell us the one thing you want us to remember. You own the details: if someone asks what the ablation removed, how the search is guided, or what the DSL actually contains, you answer.
Champion (~5 min). Argue this paper deserves a best paper award. Why does the idea matter beyond the benchmark it was evaluated on — what does it unlock, and what would you build on top of it? Concede the paper’s single biggest weakness up front and explain why it does not sink the contribution. Vague enthusiasm is not championing; be specific.
Critic (~5 min). You are Reviewer 2 and you recommend reject. Attack the claims, not the authors. Good targets: claims the experiments do not support, a missing baseline that might have won, a benchmark that does not measure the thing being claimed, compute or annotation costs buried in an appendix, results that will not survive a change of domain. Close with the one experiment that would change your score — a critique you cannot turn into an experiment is an opinion.
Implementer (~5 min). Before class, get the artifact running — or fail to, and report exactly where it broke. Run it on one input the paper never considered and show us what happened.
Discussion (~20 min). Champion and Critic cross-examine each other, the Author defends, and the class joins in. By the end we should agree on what we would have to believe for this paper to be right, and on what the next paper in this line should do.
For all roles: read any one paper this work cites and any one that cites it (you choose). It is helpful to know where the idea came from and what happened to it next.
Jump to week: 1 · 2 · 3 · 4 · 5 · 6 · 7 · 8 · 9 · 10 · 11 · 12 · 13
Schedule and readings are tentative and will be adjusted as the semester progresses.
In class In pairs, start by solving some ARC v1 tasks by hand. Pick one that is interesting. Write a program (feel free to use an LLM) that solves some tasks in 3 different programming paradigms (e.g. imperative, functional, logic programming, smt).
REMOTE Lecture 9am-10am
In class Intro to Satisfiability Modulo Theories (SMT) and Inductive Logic Programming
Readings for before class (no presentations)
Homework Write a Sudoku (or similar) solver in SMT and ILP
Materials
Homework Write an enumerative program synthesis engine for programming by example
Homework Lean Tutorial
(project proposals due)
Present what you have so far, final presentation is via video upload to youtube before end of finals period.