Preliminary Material
Preliminary logic primer, P. Madhusudan (for CS173)
Notes on induction on natural numbers, P. Madhusudan (for CS173)
More notes on induction, Chandra Chekuri (for CS173)
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.
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 MusicIncomplete Certification with Box Domain Soundness and completeness of verifiers. High-level idea behind Bound Propagation. Interval analysis of neural networks.
References: Box AnalysisInvariants 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.Zonotope abstract domain Describing the zonotope shape, abstract transformers for addition, multiplication, and ReLU.
References: Zonotope abstract domain Union and Intersection of Zonotopes.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.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.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.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 .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 .