CS 521 - Advanced Topics in Programming Systems: Trustworthy AI Systems (Fall 2023)

Lecture Schedule

Aug 22

Introduction, motivation, course policy The challenges of building trustworthy AI systems; robustness, interpretability, and accuracy of ML models; challenge of building reliable systems with ML components; deep learning models as loop-less programs. Introduction to adversarial examples, examples of robust adversarial attacks, adversarial music.

Aug 24, 29

Adversarial Attacks Adversarial attacks, Types of attacks, FGSM, Explanation for existence of adversarial inputs, Carlini and Wagner's optimization trick for targeted attacks, Universal Attacks

First Paper on Adversarial Examples FGSM Carlini and Wagner Attack Auto Attack Universal Adversarial Perturbations

Turtle Printing Attack Adversarial Stickers Adversarial Music Wireless Attack LLM Attack

Aug 29, 31

Adversarial Training Formulation of Adversarial Training as a Min-Max Optimization Problem, PGD defense

FGSM Defense PGD Defense Fast Adversarial Training TRADES

Sep 5, 7

Verification with Box Formally specifications for neural networks, Completeness and soundness of verifiers, Box verification

General framework for Verification with Abstract Interpretation Box Verification Generating specifications

Sep 21, 26

Zonotope abstract domain Describing the zonotope shape, abstract transformers for addition, multiplication, and ReLU.

References: Zonotope abstract domain Union and Intersection of Zonotopes.

Sep 28

DeepPoly abstract domain Describing the DeepPoly shape, abstract transformers for affine transformation and ReLU, backsubstitution, and application to verifying robustness against geometric perturbations and of audio classifiers.

References: DeepPoly abstract domain Verifying robustness against geometric perturbations with DeepPoly Verifying audio classifiers with DeepPoly.

Oct 3, 5

Randomized Smoothing and Probabilistic Verification

References: Randomized Smoothing for L2 Norm Randomized Smoothing for General Shapes Randomized Smoothing for Geometric Perturbations Probabilistic Verification for DNNs Framework for Probabilistic Verification.

Oct 5

Complete Verification Mixed-Integer Linear Programming (MILP), complete verification of ReLU-based networks using MILP.

References: MILP for Complete Verification MILP+Abstract Interpretation Multi-Neuron relaxations for ReLU Strong Multi-Neuron MILP formulations for ReLU.

Oct 10,12,17

Adversarial Training and Provable Defenses Formulation of adversarial attack as a min-max optimization problem, PGD defense, Differentiable Abstract Interpretation, Building Provable Defenses, Combining Adversarial Training and Provable Defenses, L-Infinity Distance Networks

References: Adversarial Training with PGD Differentiable Abstract Interpretation Training with Interval domain Combining Adversarial Training and Provable Defenses L-Infinity Distance Networks .

Nov 16

Neural Network Explanations Black-box and White-box explanations, Local and global explanations, LIME, Saliency Maps, Smoothed gradients, Integrated gradients

References: LIME Saliency Maps Integrated gradients Smoothed gradients .

See Resource page for links to resources.

Introduction to Neural Network Verification, a book by Aws Albarghouthi

Lecture Schedule and Slides Fall 2022

Aug 22: Introduction, motivation, course policy The challenges of building trustworthy AI systems; robustness, interpretability, and accuracy of ML models; challenge of building reliable systems with ML components; deep learning models as loop-less programs. Introduction to adversarial examples, examples of robust adversarial attacks, adversarial music.
Aug 24: Specifications for neural networks: Robustness of a network as a Hoare triple of a program. Discussion of various analysis techniques for proving robustness and finding attacks.
References: Adversarial Examples, Synthesizing Robust Adversarial Examples, Adversarial Music
Aug 29, 31: Incomplete Certification with Box Domain Soundness and completeness of verifiers. High-level idea behind Bound Propagation. Interval analysis of neural networks.
References: Box Analysis
Sep 7: Invariants and Abstract Interpretation Basics Concrete set semantics, alternate domains and interpretation over them, monotonic functions and lfp, Galois connections, sound abstract interpretation, illustration using the Box/Interval domain for neural networks/programs.
References: Introduction to Abstract Interpretation by Bruno Blanchett has a readable introduction to abstraction interpretation.

Sep 9: Zonotope abstract domain Describing the zonotope shape, abstract transformers for addition, multiplication, and ReLU.
References: Zonotope abstract domain Union and Intersection of Zonotopes.

Sep 26: Logics, logical theories, SMT solvers Propositional logic and SAT solvers; First order logic over a single structure and a class of structures; Theory of reals with addition, with addition and multiplication are decidable; theory of integers with addition is decidable; theory of integers with addition and multiplication (even quantifier-free) is undecidable; SMT solvers; example of proving that a zonotope abstract transformer for union of two zonotopes is sound using SMT solver for a quantified FO formula.
References: Calculus of Computation by Manna and Bradley; , Logic in Computer Science - Madhusudan Parthasarathy.

Sep 28: DeepPoly abstract domain Describing the DeepPoly shape, abstract transformers for affine transformation and ReLU, backsubstitution, and application to verifying robustness against geometric perturbations and of audio classifiers.
References: DeepPoly abstract domain Verifying robustness against geometric perturbations with DeepPoly Verifying audio classifiers with DeepPoly.

Oct 3: Topics for Course Project Complete Verification Description of the possible topics for the course project, Mixed-Integer Linear Programming (MILP), complete verification of ReLU-based networks using MILP.
References: MILP for Complete Verification MILP+Abstract Interpretation Multi-Neuron relaxations for ReLU Strong Multi-Neuron MILP formulations for ReLU.

Nov 5,7,12: Adversarial Training and Provable Defenses Formulation of adversarial attack as a min-max optimization problem, PGD defense, Differentiable Abstract Interpretation, Building Provable Defenses, Combining Adversarial Training and Provable Defenses, L-Infinity Distance Networks
References: Adversarial Training with PGD Differentiable Abstract Interpretation Training with Interval domain Combining Adversarial Training and Provable Defenses L-Infinity Distance Networks .

Nov 14: Neural Network Explanations Black-box and White-box explanations, Local and global explanations, LIME, Saliency Maps, Smoothed gradients, Integrated gradients
References: LIME Saliency Maps Integrated gradients Smoothed gradients .

CS 521 - Advanced Topics in Programming Systems: Trustworthy AI Systems (Fall 2023)

Lecture Schedule

Prerequisite Resources

Lecture Schedule and Slides

Lecture Schedule and Slides Fall 2022