| Date | Topic | Resources |
|---|
| Jul 30 | Introduction to course and logistics; why
bother about formal methods in machine learning? | Slides |
| Aug 2 | Specifying properties of ML components |
Slides |
| Aug 6 | More on specifying properties of ML components; importance of abstraction in reasoning about large ML components |
Slides |
| Aug 9 | More on the theory of abstraction: Galois connection and its properties; illustration with interval abstract domain |
Same slides as above |
| Aug 13 | Computing abstract transitions; illustrating computation of abstract post-condition of a neural network using interval domain |
Slides |
| Aug 16 | Discussion on Galois connection, and its use in verifying properties of neural networks. The DeepPoly abstract domain for verifying local robustness properties of neural networks: abstracting ReLUs and complexity of computing linear bounds in terms of inputs |
DeepPoly paper: Sec 1, 2, 3, 4 (prior to 4.2) |
Aug 27 | DeepPoly abstract domain: abstracting sigmoids, tanhs, maxpool and affine transformations. Using DeepPoly to verify robustness with correlated perturbation of inputs. |
DeepPoly paper: Sec 4.2, 4.3, 4.4 |
Aug 30 | Using linear relaxation based perturbation analysis (LiRPA) for obtaining bounds of outputs of neural networks
|
Dual norms: some intuition
ɑ-CROWN paper : Sec 1, 2.1, 2.3
|
| Sep 3 | More discussion on ɑ-CROWN; using ɑ-CROWN in conjunction with
branch-and-bound, incompleteness in the absence of LP based feasibility checks, building
a complete verifier using ɑ-CROWN, LP feasibility checks and branch-and-bound
|
ɑ-CROWN paper : Sec 2.2, 3.1, 3.2, 3.3, 3.4, Appendix A
|
Sep 4
(Compensation) | Discussion on computation of matrices in LiRPA approaches; soundness of LiRPA and ɑ-CROWN; re-visiting why LP feasibility checks are necessary for completeness of ɑ-CROWN with branch-and-bound
|
ɑ-CROWN paper : all section; Paper showing computation of matrices: Appendices A, B
|
| Sep 6 | Using Lagrangian multipliers to model split ReLU constraints: intuition, formulation, justification
|
β-CROWN paper : Sec 1, 2, 3.1
|
Sep 7
(Compensation) | Re-visiting the role of the Lagrangian multiplier in modeling split constraints in β-CROWN; using branch-and-bound with β-CROWN algorithm, and its soundness and completeness
|
β-CROWN paper : Sec 3.1, 3.3, 3.4 (Appendix A for details of bound matrix calculations)
|
| Sep 10 | Discussion of Quiz 0 solutions, and solutions to
some practice problems, discussion of course projects. Introduction to shield synthesis in reinforcement learning
|
Shield synthesis paper : Sec 1
|
| Sep 13 | Discussion of Quiz 1 solutions. Introduction to shielding: preemptive and post-posed shields, basics of reinforcement learning and reactive systems
|
Shield synthesis paper : Sec 1, 2, 3
|
| Sep 24 | Recap of basics of reinforcement learning, reactive systems, Mealy machines, infinite games and illustration with water-tank example
|
Shield synthesis paper : Sec 1, 2, 3
|
| Sep 27 | Constructing abstractions of MDPs, safety automata and game graphs. An algorithmic view of how to compute winning regions and winning strategies from game graphs
|
Shield synthesis paper : Sec 3, 4
|
| Oct 1 | Mealy machine synthesis from game formulation for pre-emptive and post-posed shields, examples of shielded systems in action, how shielding folds into the learning process. Introduction to probabilistic shields, motivation for going beyond non-probabilistic shields
|
Shield synthesis paper : Sec 5, 6, 7, 8
Prob shielding paper : Sec 1, 2
|
| Oct 4 | Construction of MDP from observed behaviour of adversaries, computation of action-values, using thresholds to select δ-safe actions, properties of δ-safe shielded MDPs
|
Prob shielding paper : Sec 2, 3.1, 3.2, 3.3
|
| Oct 8 | Recap of probabilistic shield synthesis steps, computing minimum probability of reaching an unsafe state in an MDP, overview of techniques used to address scalability concerns
|
Prob shielding paper: Sec 3.3, 3.4, 3.5, 4 (optional)
|
| Oct 11 | Introduction to logical abduction based
explanation of neural network decisions: modeling networks using first-order formulas, modeling conditional linear constraints using mixed integer linear programming, an iterative abduction procedure.
|
Abductive explanation paper : Sec 1, 2, 3
Slides for abductive explanations |
| Oct 15 | Big-M encoding of conditional linear constraints as MILP; more on finding abductive explanations: subset-minimal and cardinality-minimal explanations, algorithm for each kind of explanation, relation of abductive explanations and adversarial input generation, understanding experimental results |
Abductive explanation paper : Sec 3, 4, 5
Slides for big-M encoding |
| Oct 18 | The problem of synthesizing "explainable" interpretations of black-box ML models; role of hypothesis class; basics of Probably Approximately Correct (PAC) learning: sample complexity, learning best hypothesis from within hypothesis class, explanation of PAC learning guarantee and how it differs from obtaining an ideal explanation of black-box model
|
Pareto interpretation paper : Sec I, II, IV
Slides |
| Oct 22 | Need for Pareto-optimal (PO) interpretations, finding a single PO point using single-objective optimization techniques; weighted MaxSAT, inter-reduction to integer linear programming, weighted MaxSAT with hard and soft clauses, use in symbolically encoding Pareto-optimal interpretation synthesis; explaining encoding of syntactic requirements of hypothesis class, and of matching of sample output for a given (symbolic interpretation)
|
Pareto interpretation paper : Appendix A, Sec III A, B
Slides |
| Oct 25 | Further discussions on symbolic encoding of Pareto-optimal interpretation as a weighted
MaxSAT instance, going from one Pareto point to multiple Pareto points, generalizing to other classes of
explanability and correctness measures, making sense of experimental results |
Pareto interpretation paper : Appendix A, Sec III C, V
Slides |
| Oct 29 | Scaling challenge for FM in ML; Monitoring with guarantees as a pragmatic solution. Markovian assumption, PAC guarantees for monitors, randomized register monitors |
Monitoring paper: Sec 1, 2 |
| Nov 1 | Monitoring Markov chains with guarantees: randomized register monitors (RRM) as probabilistic programs, induced probability on output computed by RRM, definition of RRM states, runs, and semantics; Probabilistic Specification Expressions (PSE) and their use; frequentist monitor synthesis problem definition and illustration |
Monitoring paper: Sec 2.2, 3.1, 3.2 |
| Nov 5 | Discussion of Hoeffding's inequality and its use in synthesis of frequentist monitors; use of auxiliary random variables; monitor synthesis for division-free PSEs and for PSEs with division; taking care of dependent multiplications, addressing space requirements when combining frequent and infrequent sequences of random events |
Monitoring paper: Sec 4, Appendix A.2 |
| Nov 8 | Detailed discussion of frequentist monitoring algorithm. Concluding remarks for course |
Monitoring paper: Sec 4 |