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.

Some links:

• Relaxed Machines: namin/relaxed-machines
• VerMCTS: namin/llm-verified-with-monte-carlo-tree-search
• Dafny Sketcher: namin/dafny-sketcher
• dafny-annotator: metareflection/dafny-annotator
• Software archaeology of Eurisko: namin/eurisclo
• LeanDisco: namin/LeanDisco
• Holey: namin/holey
• Argument Debugger & Argir: namin/argument-debugger & namin/argir

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).
  • 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
  • PLDI’21
  • Royal Society
  • code
• Stitch: Top-Down Synthesis for Library Learning
  • POPL’23
  • code
  • docs
• LILO: Learning Interpretable Libraries by Compressing and Documenting Code
  • ICLR’24
  • code
• Application to recovering Chinese characters: Finding structure in logographic writing with library learning
  • CogSci’24

Thursday, October 2

Paul Krogmeier, postdoctoral fellow, will give a guest lecture. Some papers:

• Reading of the day: 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).

Reading guide from Paul:

• Focus on reading of the day.
• First, read Sections 1, 2, and 4.
• Second, read the problem statements in Sections 5 and 6.
• Rest of the paper is very optional, including the proofs.
• Read with an eye toward conceptual differences with DreamCoder and library learning
• Paul will talk about “Axiom synthesis” and “Languages with…”, but they can be skimmed.

Week 6

Tuesday, October 7

Mike leads a session on automated theorem proving.

• Reading of the Day: Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models (paper)

• Extra: Proving Theorems Recursively (paper, alt)

Thursday, October 9

Jeremy leads a session on programming prompts.

• Prompting Is Programming: A Query Language for Large Language Models (PLDI’23) (paper).

Week 7

Tuesday, October 14

Richael leads a session on jailbreaking and particular solutions involving PL+AI.

• Reading of the day: R2-Guard: Robust Reasoning Enabled LLM Guardrail via Knowledge-Enhanced Logical Reasoning (paper).
• Optional reading: Constitutional Classifiers: Defending against Universal Jailbreaks across Thousands of Hours of Red Teaming (paper)

Thursday, October 16 (Assignment 1 Due)

Dat Nguyen Thanh, postdoctoral fellow, will give a guest lecture on prompt optimization and tool orchestration.

• Reading of the day: GEPA: Reflective Prompt Evolution Can Outperform Reinforcement Learning (paper).
• Extra: Optimizing Instructions and Demonstrations for Multi-Stage Language Model Programs (paper).
• Code: DSPy.

Week 8

Tuesday, October 21

Milligan leads a session on evaluating “intelligence”.

• On the Measure of Intelligence (paper). See also ARC Prize.
• Sudoku-Bench: Evaluating creative reasoning with Sudoku variants (paper).

Thursday, October 23

Suhwan leads a session on neural causal modeling.

• Neural Algorithmic Reasoning with Causal Regularisation.

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

Jeffrey leads a session focusing on SWE-Search: Enhancing Software Agents with Monte Carlo Tree Search and Iterative Refinement (paper).

Thursday, November 6

Arya leads a session on using DSPy for his research, SwizzlePerf: Hardware-Aware LLMs for GPU Kernel Performance Optimization (paper).

Week 11

Tuesday, November 11

Theo leads a session on AlphaGeometry (blog, paper) and AlphaGeometry 2 (paper).

Thursday, November 13

Each student briefly discusses a library/software artifact that they plan to use or that inspires them.

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.

TF Matthew Retchin presents his research.