CS846: FMxAI
This course surveys important ideas and literature at the intersection of formal methods and artificial intelligence.
Grading
Our meetings will be centered around paper discussions. Attendance, reading of assigned papers, and participation are essential. The grading scheme reflects that:
- 25% participation;
- 25% discussion lead; and
- 50% project.
Discussions
Every student will lead a paper discussion.
Projects
Every project must contain new research---a new idea or insight---and an element of both formal methods and artificial intelligence.
The main deliverables (in chronological order) will be:
- proposal;
- mini presentation;
- final presentation; and
- report.
Guidelines for Proposal
The proposal must contain a problem definition and a brief literature survey. It should be at most one page long and use a reasonable font.
Guidelines for Mini Presentation
The mini presentation should cover the contents of the proposal, a quick status update, and a timeline for the remainder of the term. The mini presentation should be at most five minutes long.
Guidelines for Final Presentation
The final presentation should build on the mini presentation. It should contain an updated problem definition, an updated literature survey, and final results. The final presentation should be at most 15 minutes long.
Guidelines for Report
The report should be a conference paper-style writeup.
Schedule
TBD: we will read and discuss a small subset of the papers in the reading bank.
Reading Bank
The readings below span twelve themes: SSC syntactic and semantic constraints on LLM outputs, LCD learning constraints from data, ATU agents and tool-use, SAT satisfiability and satisfiability modulo theories, PRA program analysis, AUF autoformalization, NSP neuro-symbolic programming, SUP superoptimization, TPR theorem proving, MLV machine-learning verification, PRP program repair, and TST testing. Use the dropdown in the table's rightmost column to narrow the list to a single theme.
| Title | Link | |
|---|---|---|
| Learning Regular Sets from Queries and Counterexamples | Angluin, I&C '87 | LCD |
| Mining Specifications | Ammons et al., POPL '02 | LCD |
| SATzilla: Portfolio-based Algorithm Selection for SAT | Xu et al., JAIR '08 | SAT |
| Stochastic Superoptimization | Schkufza et al., ASPLOS '13 | SUP |
| Learning to Superoptimize Programs | Bunel et al., ICLR '17 | SUP |
| Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks | Katz et al., CAV '17 | MLVSAT |
| Learning to Solve SMT Formulas | Balunović et al., NeurIPS '18 | SAT |
| DeepProbLog: Neural Probabilistic Logic Programming | Manhaeve et al., NeurIPS '18 | NSP |
| Guiding High-Performance SAT Solvers with Unsat-Core Predictions | Selsam and Bjørner, SAT '19 | SAT |
| How To Generate Text: Using Different Decoding Methods For Language Generation With Transformers | von Platen, Blog '20 | ATUSSC |
| Learning Concise Models from Long Execution Traces | Jeppu et al., DAC '20 | LCD |
| Proving Data-Poisoning Robustness in Decision Trees | Drews et al., PLDI '20 | MLV |
| Generative Language Modeling for Automated Theorem Proving | Polu and Sutskever, arXiv '20 | TPR |
| MedleySolver: Online SMT Algorithm Selection | Pimpalkhare et al., SAT '21 | SAT |
| PICARD: Parsing Incrementally for Constrained Auto-Regressive Decoding from Language Models | Scholak et al., EMNLP '21 | SSC |
| Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification | Wang et al., NeurIPS '21 | MLV |
| Neural Network Verification with Proof Production | Isac et al., FMCAD '22 | MLV |
| HyperTree Proof Search for Neural Theorem Proving | Lample et al., NeurIPS '22 | TPR |
| LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers | Olausson et al., EMNLP '23 | ATUAUF |
| Scallop: A Language for Neurosymbolic Programming | Li et al., PLDI '23 | NSP |
| Grammar Prompting for Domain-Specific Language Generation with Large Language Models | Wang et al., NeurIPS '23 | SSC |
| Automated Repair of Programs from Large Language Models | Fan et al., ICSE '23 | PRP |
| Large Language Models Are Zero-Shot Fuzzers: Fuzzing Deep-Learning Libraries via Large Language Models | Deng et al., ISSTA '23 | TST |
| CODAMOSA: Escaping Coverage Plateaus in Test Generation with Pre-trained Large Language Models | Lemieux et al., ICSE '23 | TST |
| Synthetic Programming Elicitation for Text-to-Code in Very Low-Resource Programming and Formal Languages | Mora et al., NeurIPS '24 | AUFSSCPRP |
| LLM Meets Bounded Model Checking: Neuro-symbolic Loop Invariant Inference | Wu et al., ASE '24 | LCDPRA |
| Specgen: Automated Generation Of Formal Program Specifications Via Large Language Models | Ma et al., ICSE '25 | AUFLCD |
| Let a Neural Network Be Your Invariant | Giacobbe et al., NeurIPS '25 | LCDPRA |
| Large Language Model Powered Symbolic Execution | Li et al., OOPSLA '25 | PRA |
| Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving | ByteDance, Arxiv '25 | TPR |
| Learning Context-Free Grammars for Grammar-Constrained Decoding via Declarative Agentic Programming with Guarantees | Cheang et al., Arxiv '26 | ATULCDAUF |
| Reinforcement Learning from Human Feedback, Chapter 13 | Lambert, Textbook '26 | ATU |
| A Neurosymbolic Approach to Natural Language Formalization and Verification | An et al., CAV '26 | AUF |
| Agentic Verification of Software Systems | Tu et al., FSE '26 | PRA |
| Domain-Specific Hyperspecialization (For SAT) | Green, Blog '26 | SAT |
| Constrained Adaptive Rejection Sampling | Parys et al., ICML '26 | SSC |
| ChopChop: A Programmable Framework for Semantically Constraining the Output of Language Models | Nagy et al., POPL '26 | SSC |