CS846: FMxAI

Federico Mora · Fall '26 · Tues 3:00-5:50pm · DC 2585

The goal of this course is to help every student create a novel piece of research at the intersection of formal methods and artificial intelligence. To do this, we will discuss important ideas in this space and collaborate to refine each other's work.

Grading

Our meetings will be centered around paper discussions and in-class activities. Attendance, reading of assigned papers, and participation are essential. The grading scheme reflects that:

Participation

The best way to achieve the goal of the course is through active participation. That means completing the assigned readings before class, engaging in discussions during class, helping other students understand the material, providing constructive feedback to other students, and doing your best on all assessments.

This class is not a competition. There is no curve or anything resembling a curve. The goal is for everyone to learn and create something new, and your behavior should reflect that. In particular, your actions should never make another student feel stereotyped, unwelcome, uncomfortable, or unsafe. Not only would these actions be wrong, but there is a great deal of research that shows how they damage students' course performance (e.g., see "stereotype threat"). Please take care, so we can create a class in which all students feel supported and respected.

Discussion Leads

Students will submit discussion lead preferences through a LEARN quiz due Sep 15. Discussion lead assignments will be sent out on Sep 16.

There will be three kinds of readings: research papers, textbooks, and blog posts. For research papers, discussion leads will present a review with four components:

For textbooks, discussion leads will give a 30-minute tutorial. The goal is to gain an in-depth understanding of foundational concepts as a class. Students can follow the textbook content as closely as needed. For blog posts, students will lead a 30-minute deep-dive into the blog content. This can include slides, a code demo, or any other pedagogical activities.

Projects

Every project must contain new research—a new idea or insight—and an element of both formal methods and artificial intelligence. Students can work in groups of up to three.

The main deliverables (in chronological order) will be:

  1. proposal (due Oct 09);
  2. mini presentation (Nov 03);
  3. final presentation (Dec 08); and
  4. report (due Dec 18).

Guidelines for Proposal

The proposal must contain a problem definition, a literature survey, and an intuition for a possible solution. It should be at most one page long and use a reasonable format (margins, font, etc.).

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 10 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, a description of the approach, and final results. The final presentation should be at most 20 minutes long.

Guidelines for Report

The report should be a conference paper-style write-up. For example, students can use the AAAI-27 format and include the following sections:

  1. introduction;
  2. technical background;
  3. approach;
  4. evaluation;
  5. related work; and
  6. conclusions/future work.

Schedule

On paper discussion days, there will be at least two assigned readings and corresponding student-led presentations.

Date Description Read
Sep 15 Introduction and overview 1, 2
Sep 15 Discussion preferences due
Sep 22 Agents and tool-use ATU 1, ?
Sep 29 Constraints on LLM outputs CLO 1, ?
Oct 06 Generating system constraints GSC ?
Oct 09 Proposals due
Oct 13 Reading week
Oct 20 Satisfiability (modulo theories) SAT 1, ?
Oct 27 Program verification PVE 1, ?
Nov 03 Mini presentations day
Nov 10 Superoptimization SUP ?
Nov 17 Theorem proving TPR ?
Nov 24 Machine-learning verification MLV 1, ?
Dec 01 Bonus 1, ?
Dec 08 Final presentations day
Dec 18 Reports due

Reading Bank

The readings will be drawn from the following bank of papers, textbooks, and blog posts, which cover nine themes: agents and tool-use ATU; syntactic and semantic constraints on LLM outputs CLO; generating system constraints GSC; satisfiability (modulo theories) SAT; program verification PVE; superoptimization SUP; theorem proving TPR; machine-learning verification MLV; and neuro-symbolic programming NSP.

Title Link
LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers Olausson et al., EMNLP '23 ATU
Reinforcement Learning from Human Feedback, Chapter 13 Lambert, Textbook '26 ATU
Towards Verifiably Safe Tool Use for LLM Agents Doshi et al., ICSE-NIER '26 ATU
How To Generate Text: Using Different Decoding Methods For Language Generation With Transformers von Platen, Blog '20 CLO
Constrained Adaptive Rejection Sampling Parys et al., ICML '26 CLO
Type-Constrained Code Generation with Language Models Mündler et al., PLDI '25 CLO
Synthetic Programming Elicitation for Text-to-Code in Very Low-Resource Programming and Formal Languages Mora et al., NeurIPS '24 CLO
Mining Specifications Ammons et al., POPL '02 GSC
Learning Context-Free Grammars for Grammar-Constrained Decoding via Declarative Agentic Programming with Guarantees Cheang et al., arXiv '26 GSC
A Neurosymbolic Approach to Natural Language Formalization and Verification An et al., CAV '26 GSC
Introduction to Neural Network Verification, Chapters 4, 6 (7 optional) Albarghouthi, Textbook '26 SAT
Guiding High-Performance SAT Solvers with Unsat-Core Predictions Selsam and Bjørner, SAT '19 SAT
Learning to Solve SMT Formulas Balunović et al., NeurIPS '18 SAT
SATzilla: Portfolio-based Algorithm Selection for SAT Xu et al., JAIR '08 SAT
MedleySolver: Online SMT Algorithm Selection Pimpalkhare et al., SAT '21 SAT
Domain-Specific Hyperspecialization (For SAT) Green, Blog '26 SAT
Getting Started with Dafny: A Guide Leino, Textbook '23 PVE
AutoVerus: Automated Proof Generation for Rust Code Yang et al., OOPSLA '25 PVE
VERINA: Benchmarking Verifiable Code Generation Ye et al., ICLR '26 PVE
Large Language Model Powered Symbolic Execution Li et al., OOPSLA '25 PVE
Program Synthesis is Possible Sampson, Blog '18 SUP
Stochastic Superoptimization Schkufza et al., ASPLOS '13 SUP
Faster Sorting Algorithms Discovered Using Deep Reinforcement Learning Mankowitz et al., Nature '23 SUP
Mathematical Discoveries from Program Search with Large Language Models Romera-Paredes et al., Nature '23 SUP
Generative Language Modeling for Automated Theorem Proving Polu and Sutskever, arXiv '20 TPR
Hilbert: Recursively Building Formal Proofs with Informal Reasoning Varambally et al., ICLR '26 TPR
Postmortem for Kernel Soundness Bug #14576 de Moura, Blog '26 TPR
Introduction to Neural Network Verification, Chapters 1, 2, 3, 5 Albarghouthi, Textbook '26 MLV
VNN-LIB 2.0: Rigorous Foundations for Neural Network Verification Roy et al., CAV '26 MLV
Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification Wang et al., NeurIPS '21 MLV
Learning Differentiable Programs with Admissible Neural Heuristics Shah et al., NeurIPS '20 NSP

Accommodations

The course is designed to help every student create a novel piece of research. If you find that a change is needed, please come talk to me so that we can work together to achieve the goal of the course through alternate means. One of the best ways to work together is to talk about potential issues and solutions as early as possible. For example, if you already know that you would benefit from accommodations, please meet with me so we can develop an implementation plan together.

AI Use Policy

Careful use of AI tools is allowed. Please refer to the libraries' guide on citing and disclosing AI use, the copyright advisory committee's warning, and the university's guidelines regarding university data.

References