Schedule
Week 1
Tuesday, September 2
First day of class. TF Matthew Retchin lead a discussion on the taxonomy of neurosymbolic programming.
Thursday, September 4
TF Matthew Retchin leads an introductory session.
- Hybrid computing using a neural network with dynamic external memory (PDF) by Graves et al. in Nature 2016.
Week 2
Tuesday, September 9
Gabriel Poesia, incoming Kempner fellow, will give a guest lecture.
- (NeurIPS 2024) Minimo: Learning Formal Mathematics From Intrinsic Motivation (code, paper).
- (Dafny 2025) dafny-annotator: AI-Assisted Verification of Dafny Programs (code, paper, blog).
Thursday, September 11
No class.
Week 3
Tuesday, September 16
We set the schedule for the course.
Thursday, September 18
Prof. Nada Amin discusses her work at the intersection of formal verification and LLMs.
Week 4
Tuesday, September 23
Simon leads a session on mathematical reasoning with LLMs.
- Reading of the day:
- _DeepSeek-R1 incentivizes reasoning in LLMs through reinforcement learning _ ((Nature’25)[https://www.nature.com/articles/s41586-025-09422-z])
- Extra: DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models (PDF).
- Reasoning Gym.
- Open Proof Corpus.
Thursday, September 25
Dennis leads a session on constraint decoding, grammar aligned and semantically constrained.
- Reading of the day: ChopChop: a Programmable Framework for Semantically Constraining the Output of Language Models (paper).
Week 5
Tuesday, September 30
Valerio leads a session on program synthesis and library learning, with a focused reading on DreamCoder (PLDI’21 edition).
- DreamCoder: growing generalizable, interpretable knowledge with wake–sleep Bayesian program learning
- Stitch: Top-Down Synthesis for Library Learning
- LILO: Learning Interpretable Libraries by Compressing and Documenting Code
- Application to recovering Chinese characters: Finding structure in logographic writing with library learning
Thursday, October 2
Paul Krogmeier, postdoctoral fellow, will give a guest lecture. Some papers:
- Synthesizing DSLs for Few-shot Learning (OOPSLA’25) (PDF).
- Synthesizing Axiomatizations using Logic Learning (OOPSLA’22) (PDF).
- Languages with Decidable Learning: A Meta-theorem (OOPSLA’23) (PDF).
Week 6
Tuesday, October 7
Mike leads a session on automated theorem proving.
TODO: select a set of papers to study, including a reading of the day.
Thursday, October 9
Jeremy leads a session on programming prompts.
- Prompting Is Programming: A Query Language for Large Language Models (PLDI’23) (paper).
- TODO: also consider other approaches to programming prompt, e.g. DSPy.
Week 7
Tuesday, October 14
Richael leads a session on jailbreaking and particular solutions involving PL+AI.
- R2-Guard: Robust Reasoning Enabled LLM Guardrail via Knowledge-Enhanced Logical Reasoning (paper).
Thursday, October 16 (Assignment 1 Due)
Joker class.
Week 8
Tuesday, October 21
Milligan leads a session on evaluating “intelligence”.
- On the Measure of Intelligence (paper).
- Sudoku-Bench: Evaluating creative reasoning with Sudoku variants (paper).
Thursday, October 23
Suhwan leads a session on neural causal modeling.
Week 9
Tuesday, October 28 (Project Proposals Due)
Zekai leads a session focusing on Statically Contextualizing Large Language Models with Typed Holes (OOPSLA’24).
Thursday, October 30
Discussion on project proposals.
Week 10
Tuesday, November 4
Thursday, November 6
Week 11
Tuesday, November 11
Thursday, November 13
Week 12
Student Presentations of their Ongoing Projects
Tuesday, November 18
Thursday, November 20
Week 13
Tuesday, November 25
Project workout.
Thursday, November 27
Thanksgiving.
Week 14
Tuesday, December 2
Last day of class.