The schedule below is tentative and may change throughout the semester.
📹 Video recordings will be automatically added to Media Space immediately after class (registration is required to access these videos). I will not post every video link individually.
We are thrilled to have four invited guest lecturers this semester – see this page for their talk abstracts and bios.
| Lecture | Date | Topic | Readings | Homework |
|---|---|---|---|---|
| L1 | 08/27 | Introduction (slides) | ||
| L2 | 08/29 | Introduction to formal methods (Formal Modeling, Logic, Satifiability problem) (slides) | ||
| L3 | 09/03 | Solving SAT problem (DPLL, machine learning for solving SAT problems, NeuroSAT) (slides) | NeuroSAT ML for SAT MapleSAT | |
| L4 | 09/05 | Satisfiability Modulo Theory (Concept, Decision Procedures, DPLL(T)) (slides) | HW1 out | |
| L5 | 09/10 | Satisfiability Modulo Theory (wrap up); Verification problems in machine learning (slides) | ||
| L6 | 09/12 | Neural network verification (Satisfiability problem, MILP, LP formulations) (slides) | ||
| L7 | 09/17 | Neural network verification (bound propagation method) (slides) | ||
| L8 | 09/19 | Neural network verification (branch and bound) (slides) | Beta-CROWN | |
| L9 | 09/24 | Neural network verification (branch and bound, bound propagation on general computation graph) (slides) | See important notes about class presentation on slides | |
| L10 | 09/26 | Neural network verification (falsification, training verifiable NNs, and practical verifiers) (slides) | ||
| L11 | 10/1 | Neural network verification (methods for improving verification) | [5] [6] | |
| L12 | 10/3 | Formal methods for other ML models | [7] [8] | Project proposal due 10/5, HW2 out |
| L13 | 10/8 | Falsification and adversarial attacks | [14] [16] | |
| L14 | 10/10 | Verification for reasoning and explanability in ML | [1] [2] | |
| L15 | 10/15 | Verification of learning-enabled control systems | [12] [13] | |
| L16 | 10/17 | Verification of NN applied to robotics and graphics | BaB-ND, Spelunking-the-deep | Presented by Keyi Shen and Ruize Gao |
| L19 | 10/22 | Guest Lecture (Prof. Jingbo Wang) | More info | Guest lecture on Zoom [link 1] |
| L20 | 10/24 | Guest Lecture (Prof. Samuel Chevalier) | Guest lecture on Zoom [link 1] | |
| L21 | 10/29 | Mid-semester project presentation + Feedback | Check Canvas announcement for details | |
| L22 | 10/31 | Mid-semester project presentation + Feedback | Check Canvas announcement for details | |
| L23 | 11/5 | Guest Lecture (Prof. Stanley Bak): Safe Autonomy for Cyber-Physical Systems using Surrogate Verification | More info | Guest lecture on Zoom [link 2] |
| L24 | 11/7 | Automated Theorem Proving Part I: concepts and resolution refutation (slides) | ||
| L25 | 11/12 | Automated Theorem Proving: Part II: interactive theorem provers (slides) | ||
| L26 | 11/14 | Automated theorem proving with large language models | [18] [19] | HW3 out on Nov 17 |
| L27 | 11/19 | Machine learning and foundation models for math problems | [20] [21] | |
| L28 | 11/21 | Guest Lecture (Prof. Vijay Ganesh) | More info | Guest lecture on Zoom [link 3] |
| 11/26 | Fall Break | |||
| 11/28 | Fall Break | |||
| L29 | 12/3 | Final project presentations | Slides due on 12/3 at 2 pm (before class) | |
| L30 | 12/5 | Final project presentations | ||
| L31 | 12/10 | Final project presentations | ||
| 12/19 | Final Report Due |