Teaching Fellow Tyler Holloway gives an overview of the course.
Professor Nada Amin talks about syntax-guided synthesis and enumerative search.
We set the schedule for the course.
Guest William E. Byrd presents the following paper and leads the discussion:
- William E. Byrd, Michael Ballantyne, Gregory Rosenblatt, and Matthew Might. A Unified Approach to Solving Seven Programming Problems (Functional Pearl), ICFP 2017 (interactive version)
Session top-down type-driven synthesis.
Kevin Zhang presents the following paper and leads the discussion:
- Peter-Michael Osera and Steve Zdancewic. Type-and-example-directed program synthesis, PLDI 2015 (code)
Acer Iverson presents the following paper and leads the discussion:
- Nadia Polikarpova, Ivan Kuraj, Armando Solar-Lezama. Program Synthesis from Polymorphic Refinement Types, PLDI 2016 (demo, code)
Shashi Gowda presents methods for dealing with large space of programs, such as e-graphs, Version Space Algebras (VSA), tree automata.
- Rosetta stone
- FlashMeta: a framework for inductive program synthesis (as an application of VSA)
Matt Kotzbauer and Sibi Raja present on library learning and lead the discussion.
- DreamCoder (for motivation)
- Top-Down Synthesis for Library Learning
- babble : Learning Better Abstractions with E-Graphs and Anti-Unification
Azim Raheem presents the following paper, which applies tree automata:
- Anders Miltner, Adrian Trejo Nuñez, Ana Brendel, Swarat Chaudhuri, and Isil Dillig. Bottom-up synthesis of recursive functional programs using angelic execution, POPL 2022 (code)
We will discuss the assignments in the remaining time.
Iñaki Arango and Ivy Liang present an introduction to transformers and its application to LLMs.
- Attention is all your need
- Toolformer: Language Models Can Teach Themselves to Use Tools
- Program Synthesis with Large Language Models
Binita Gupta and Sean Yang survey works on verification of output for LLMs:
- Jigsaw: Large Language Models meet Program Synthesis
- Exploring the Verifiability of Code Generated by GitHub Copilot
- Training Verifiers to Solve Math Word Problems
- I Speak, You Verify: Toward Trustworthy Neural Program Synthesis
Dr. Eamon Duede presents and leads a session on Embedded Ethics.
- (Required) Bommasani, Rishi, Kathleen A. Creel, Ananya Kumar, Dan Jurafsky, and Percy S. Liang. "Picking on the Same Person: Does Algorithmic Monoculture lead to Outcome Homogenization?." Advances in Neural Information Processing Systems 35 (2022): 3663-3678.
- (Suggested) Muller, Michael, Steven Ross, Stephanie Houde, Mayank Agarwal, Fernando Martinez, John Richards, Kartik Talamadupula, and Justin D. Weisz. "Drinking Chai with Your (AI) Programming Partner: A Design Fiction about Generative AI for Software Engineering." In HAI-GEN Workshop at IUI 2022: 3rd Workshop on Human-AI Co-Creation with Generative Models. 2022.
- (Optional) Toups, Connor, Rishi Bommasani, Kathleen A. Creel, Sarah H. Bana, Dan Jurafsky, and Percy Liang. "Ecosystem-level Analysis of Deployed Machine Learning Reveals Homogeneous Outcomes." arXiv preprint arXiv:2307.05862 (2023).
Daniel presents an introduction to program repair and its application to robotics.
- CURE: Code-Aware Neural Machine Translation for Automatic Program Repair
- Interactive Synthesis of Temporal Specifications from Examples and Natural Language
Further readings:
- A Survey on Software Fault Localization
- A Survey on Automated Program Repair Techniques
- Program Repair
Raffi Sanna presents a session on Inductive Logic Programming (ILP).
Guest lecture by Gabe Grand, who presents his work on LILO and leads the discussion. See his master thesis at MIT and the LILO preprint and code.
Session on formal mathematics with LLMs.
Andrew Sima presents the following paper and leads the discussion.
- Generative Language Modeling for Automated Theorem Proving
Prof. Nada Amin presents some demo on formal verification with LLMs, if there is time.
Ayush Noori and Will Byrd present on applications of synthesis to biomedical domains.
Useful background: LLMs, diffusion models, GANs, reinforcement learning, ILP.
Alex Bai presents the following paper and leads the discussion:
- Leveraging Rust Types for Program Synthesis
In the remaining time, we will discuss assignments and proposals.
Leonard Tang presents the following paper and leads the discussion:
- Human-level concept learning through probabilistic program induction
Grace Li presents ands leads a session on Genetic Programming.
Guest lecture by David Bieber. His works include:
- BUSTLE: Bottom-Up Program Synthesis Through Learning-Guided Exploration
- TF-Coder: Program Synthesis for Tensor Manipulations
- Show Your Work: Scratchpads for Intermediate Computation with Language Models
Guest lecture by Jesse Han on "Verified program synthesis in the age of LLMs".
Chloe Loughridge presents the following paper and leads the discussion.
- Nora Kassner, Oyvind Tafjord, Ashish Sabharwal, Kyle Richardson, Hinrich Schutze, Peter Clark. Language Models with Rationality (REFLEX)
Buffer class.
Thanksgiving.
We will decide on the schedule of presentations.
Prof. Nada Amin and Sibi Raja presents two projects:
- LLM verified with Monte Carlo Tree Search
- Belief graphs for solving 5-minute mysteries
Project presentations.
Project presentations.
Last day of classes.