FALL 2024 Edition
Emerging ML models (like deep neural networks) tend to be complex, fragile, non-robust, and uninterpretable. This makes it extremely challenging to build reliable real-world systems that incorporate ML components. We need trustworthy ML as well as robust system design to achieve end-to-end correctness of systems.
In this course, we will study recent developments at the intersection of formal methods (FM), programming languages (PL) and machine learning (ML) research towards the development of trustworthy AI-based systems. Some topics planned covered for the course are:
Please note that this is an in-person class. However, the first 4 lectures will be held virtually. The lecture details will be communicated soon. Attendance is mandatory. If you're unable to attend a class, please notify the instructor with a valid reason.
12/02/2024: HW5 is released on Gradescope. Due on 12/13, 11:59 pm CT.
11/20/2024: Class project reports are due on 12/15, 11.59 pm CT.
11/20/2024: Project presentations will be during lectures on 12/3, 12/5, 12/10. Check campuswire for details.
11/08/2024: HW4 is released on Gradescope. Due on 11/20, 11:59 pm CT.
10/19/2024: HW3 is released on Gradescope. Due on 10/25, 11:59 pm CT.
10/17/2024: Mid-sem project reviews on 10/28 and 10/31 during office hours.
10/04/2024: HW2 is released on Gradescope. Due on 10/11, 11:59 pm CT.
09/22/2024: Project proposals are due on 09/30, 11:59 pm CT.
09/13/2024: HW1 is released on Gradescope. Due on 09/20, 11:59 pm CT.
08/19/2024: First 4 lectures will be conducted virtually. The details will be sent out through email shortly.
08/19/2024: The website is up!
We will compute the final grade using the following table:
Activity | Grade | Details |
---|---|---|
Homeworks | 50% |
|
Project | 40% |
|
Participation | 10% |
|
We will use Gradescope for homework submissions. We will share the details to enroll in the course there soon.
We will drop the lowest scored homework for grading.
Each homework accounts for 12.5% of the grade.
Each student has a total of three additional days throughout the term to accommodate late submissions for homework assignments. This cumulative allowance can be used at the your discretion across different assignments.
If you submit more than 5 minutes late for an assignment, then it is considered as using one full day of the late submission allowance.
Once you exhaust the three-day late submission allowance, any further late homework submissions will result in a penalty.
Project teams should not consist of more than 2 members.
We will specify some course projects based on the material covered in the lectures. You can also propose project, but it must be approved by the course staff.
Date | Topic | Notes | Related readings |
---|---|---|---|
08/27 | Lecture 1. Course Introduction |
Slides / Video | Turtle Printing Attack, Adversarial Stickers, Adversarial Music, Wireless Attack, LLM Attack |
08/29 | Lecture 2. Adversarial Attacks |
Slides / Video Adversarial attacks, Types of attacks, FGSM, Explanation for existence of adversarial inputs |
First paper on Adversarial Examples, FGSM |
09/03 | Lecture 3. Adversarial Attacks (continued) |
Slides / Video / Notes FGSM, Explanation for existence of adversarial inputs, Carlini and Wagner's optimization trick for targeted attacks |
Carlini and Wagner attack |
09/05 | Lecture 4. Adversarial Attacks (continued) |
Slides / Video Carlini and Wagner attack, Projected Gradient Descent, Universal Adversarial Perturbations, Intro to Adversarial Training |
Universal Adversarial Perturbations, Auto Attack |
09/10 | Lecture 5. Adversarial Training |
Slides Formulation of Adversarial Training as a Min-Max Optimization Problem, PGD defense |
FGSM Defense, PGD Defense, Fast Adversarial Training |
09/12 | Lecture 6. Adversarial Training (continued), Attacks on LLMs |
Slides TRADES, Adversarial attacks on LLMs |
TRADES, Gradient-based attack on LLMs, Jailbreaking LLMs, Red-teaming LLMs |
09/17 | Lecture 7. LLM Attacks, Neural Network Verification with Box |
Slides of LLM attack/Slides of Box GCG attack on LLMs, Formal specifications for neural networks |
General framework for Verification with Abstract Interpretation, Generating specifications |
09/19, 09/24 | Lecture 8,9. Neural Network Verification with Box |
Slides Completeness and soundness of verifiers, Box verification |
General framework for Verification with Abstract Interpretation, Box Verification |
09/26,10/01 | Lecture 10,11. Neural Network Verification with MILP |
Slides Introduction to MILP for sound and complete neural network verification. |
MILP for Complete Verification, MILP+Abstract Interpretation,Multi-Neuron relaxations for ReLU, Strong Multi-Neuron MILP formulations for ReLU |
10/03 | Lecture 12. Neural Network Verification with DeepPoly |
Slides Introduction to DeepPoly for sound and precise, but incomplete neural network verification. |
DeepPoly abstract domain, Verifying robustness against geometric perturbations with DeepPoly, Verifying audio classifiers with DeepPoly |
10/08-10/17 | Lecture 13-16. Certified Training |
Slides Interval Back Propagation, DiffAI, COLT, SABR, UAP Certified Training, Certified Training against Geometric Perturbations |
IBP, Differentiable Abstract Interpretation, COLT, SABR, UAP Certified Training, Certified Training for Geometric Perturbations |
10/22-10/24 | Lecture 17-18. Explanations |
Slides LIME, Anchors, Saliency Maps, Integrated Gradients, Smoothed Gradients |
LIME, Anchors, Saliency Maps, Integrated Gradients, Smoothed Gradients |
10/29-11/07,11/14 | Lecture 19-22,24. RLHF |
Slides | PPO, DPO, Best of n sampling, RLHF theory |
11/12 | Lecture 23. Syncode |
Slides | Syncode |
11/19-11/21 | Lecture 25-26. Visual Question Answering |
Slides | Neural-Image QA, IEP, NS-VQA |
12/03-12/10 | Lecture 27-29. Class project presentations |
Grade | A+ | A | A- | B+ | B | B- | C+ | C | C- | D | F |
---|---|---|---|---|---|---|---|---|---|---|---|
Score | [95,100] | [90,94] | [85,89] | [80,84] | [75,79] | [70,74] | [65,69] | [60,64] | [55,59] | [50,54] | [0,49] |
In our commitment to academic excellence and ethical scholarship, we emphasize the importance of academic integrity in all aspects of our course. Academic integrity is central to the development of individual responsibility and scholarly credibility. Please be aware that the use of Large Language Model (LLM) tools, including ChatGPT, is strictly prohibited in the completion of any coursework and assignments in this class, unless explicitly specified otherwise. These tools, while valuable in certain contexts, do not align with our commitment to original thought and individual academic effort.
As part of this course, it is essential for all students to familiarize themselves with the University of Illinois at Urbana-Champaign Student Code, which is an integral component of our syllabus. Special attention should be paid to Article 1, Part 4, which focuses on Academic Integrity. You can access and review the Student Code at http://studentcode.illinois.edu/.