Advanced Topics in Programming Systems: Trustworthy AI Systems

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:

  • Formal Verification of ML models using abstraction and constraint solvers
  • Symbolic explanations of deep neural networks
  • Training ML models with Logic and Knowledge
  • Learning symbolic concepts (code, program synthesis, invariants)
  • Proving correctness of systems with ML components
  • Neurosymbolic machine learning
  • Safety threats to Large Language Models
  • Securing Large Language Models with RLHF

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.

 

News  

  • 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!


 Lectures:
 Every Tuesday / Thursday
 9:30 AM - 10:45 AM
 Location: 2233 Everitt Laboratory
 Forum: Campuswire

 Instructor:
 Gagandeep Singh
 Assistant Professor
 Computer Science, UIUC
 ggnds@illinois.edu
 Office hour:
 Every Thursday
 11 am - 12 pm, SC 4214

 TA:
 Isha Chaudhary
 Computer Science, UIUC
 isha4@illinois.edu
 Office hour:
 Every Monday
 4 pm - 5 pm, SC 4124

Overview  

Prerequisites

Students should have taken CS173 (or a similar course) and know basic proofs using induction and proof by contradiction (as taught in CS173). Some background on computability theory (as taught is CS374) would be good. Having taken a course in machine learning (like CS446) would be good.

Grading Policy

We will compute the final grade using the following table:

Activity Grade Details
Homeworks 50%
  • A total of 5 homeworks involving theory and coding. Check policy below.
Project 40%
  • Check policy below.

Participation 10%
  • Attendance (>= 90%) and discussion in lectures.


Homework Policy

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 Policy

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.

 

Tentative Schedule  


For all video recordings: https://mediaspace.illinois.edu/channel/channelid/354083292
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


 

Tentative Grading Scale  

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]
 

Academic Integrity  

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/.