Machine learning is increasingly being deployed in
applications like autonomous driving, unmanned aerial vehicles,
automated screening of applicants for jobs, automated screening for
loans etc. In most of these applications, there is a need for
guarantees on safety, fairness, unbiased-ness in decision making.
Existing techniques for developing and training learning models
however come with few provable guarantees in this regard. The problem
of guaranteeing desirable behaviour of machine learning models is
inherently hard, both because state-of-the-art learning models are
very large, and also because specifying precise properties of these
models, especially for perceptual tasks like image recognition, is
difficult. On the other hand, the field of program (and hardware)
verification has matured over the last four decades to produce tools
that are routinely used in the industry. This course will try to
bridge these two areas and teach students how techniques grounded in
formal methods, that have been immensely successful in
program/hardware verification, can be adapted to reason about
guarantees in various machine learning settings. The intent
is to introduce students to an area of significant
importance that leverages advances in both formal methods and machine
learning.
Pre-requisites
| UG students | CS228, CS213, CS337 or equivalent can be taken along with this course |
| PG students | Either CS433 or CS719 or CS771. CS725 is recommended but not
essential |
Course Logistics
- There will be weekly office hours for clearing doubts. You must send
email by noon of the office hour day f you wish to attend office hours.
- Students are required to read the required reading material
(roughly 3 hours per week) in order to keep pace with this course.
- Piazza will be the primary platform for discussion and query answering.
Meeting Schedule
| Lecture Hours | LT 106 | Mon and Thu, 2.00-3.30 pm |
| Office Hours | CC 314 | Thu, 5-6pm (please send email to instructor if you wish to come for office hour) |
Evaluation and assessment
| Midsem | 25% |
| Endsem | 25% |
Project
Group registration deadline: Fri, Aug 29 | 25% |
Quizes + in-class evaluations
Quizes on Fri, Aug 29 (8:30-9:30pm) and Fri, Oct 17 (6:30-7:30pm) | 25% |
- There will be ungraded practice assignments, that may require use of publicly available tools.
- All exams/quizes will be open-book.
- If you miss an exam for a genuine reason, contact the instructor immediately.
- Each graded quiz will carry equal weightage towards the 25% weightage for all quizes.
- Informal discussion among students for the purpose of clarification is strongly encouraged.
- There will be zero tolerance for
dishonest means like copying solutions from others in any
quiz, exam, project. Anybody found indulging in such
activities will be summarily awarded an FR grade. The
onus will be on the supposed offender to prove his or her
innocence.
- If you are unsure about the distinction between copying
and discussion, please
read this.
|
Course project
- Please see here for a list of project topics.
- The course project carries 25% marks.
- Each project will be done by a group of two students. If
you absolutely need more than two students in your group, please
contact the instructor.
- Each project will be based on one of a set of topics announced
in class.
-
After choosing a topic, you will finalize the
specific problem to be solved in consultation with the
instructor. This will require you to identify publicly
available tool(s) for solving the problem, and make minor
modification/tweaks to parts of the tool to help solve your
specific problem. The litmus test will be whether
your approach solves the problem in a manner
that can be scaled to large networks.
- A project submission includes a demo, a presentation and a report.
- In case a non-trivial problem is solved by a student (or
group of students), we keep open the possibility of developing
this further and attempting a research paper submission.
Project related deadllines:
| Registering groups with instructor |
Fri, Aug 29, 2025 |
| Project plan report submission |
Mon, Sep 29, 2025 |
| Project checkpoint meeting |
Thu, Oct 16, 2025 |
| Project presentations and demos |
Mon, Nov 24, 2025 (tentative) |
Practice problems, Quizes and Exams
| Exam/Quiz/Problem set | Posted on | Answers due by |
|---|
| In-class Quiz 1 with solutions | Aug 21, 2025 (3:15pm) | Aug 21, 2025 (3:30pm) |
| Quiz 1 with solutions | Sep 1, 2025 (8:30pm) | Sep 1, 2025 (9:30pm) |
| Mid-sem with solutions | Sep 19, 2025 (6:30pm) | Sep 19, 2025 (8:30pm) |
| Quiz 2 with solutions | Oct 17, 2025 (6:30pm) | Oct 17, 2025 (7:30pm) |
| In-class Quiz 2 with solutions | Oct 27, 2025 (9:45pm) | Oct 27, 2025 (10:30pm) |
Lectures and interactions
| Date | Topic | Resources |
|---|
| Jul 28 | Introduction to course and logistics; why
bother about formal methods in machine learning? Specifying properties of ML components |
Slides-1,
Slides-2 |
| Jul 31 | More on specifying properties of ML components; importance of abstraction in reasoning about large ML components |
Slides |
| Aug 4 | A brief introduction to abstract interpretation, as applied to neural network verification |
Same slides as above |
| Aug 7 | More on abstract interpretation; formulating verification problems as optimization problems, role of linear
approximations of non-linear activation functions. |
Paper: Sec 1, 2.1, 2.2 |
| Aug 11 | Linear relaxation based pertubation (LiRPA)
analysis, role of optimizable parameter α in fine-tuning linear
approximations, branch-and-bound algorithm to address
inaccuracies introduced by linear approximations |
Paper: Sec 2.3, Sec 3.1 |
| Aug 14 | Holder's inequality for bounding dual
norms, and its use in LiRPA; α-CROWN algorithm; incompleteness of
branch-and-bound with a simple example; tradeoff between
accuracy and efficiency for LP-based analysis and branch-and-bound
with LiRPA; need for
better ways to deal with splitting unstable neurons: towards
β-CROWN |
Slides on Holder's inequality
Paper: Sec 1, 2 |
| Aug 18 | β-CROWN approach for robustness
verification of neural networks in the presence of split neuron
constraints |
Paper: Sec 3.1, 3.3
Max-min inequality proof |
| Aug 21 | Quick summary of β-CROWN;
inter-relation of robustness, adversarial attacks and
explanations; basic idea behind abductive explanations of
neural network classifications; in-class evaluation |
Paper: Sec 1
Slides |
| Aug 25 | Working out an example of abductive explanation
generation step-by-step; algorithm for abductive explanation generation;
examples of abductive explanations on MNIST data set and image
classification network; understanding the relation between abductive
explanations and adversarial counterexamples/attacks, encoding neural
networks as MILP |
Paper: Sec
2,3,4, and 5 |
| Aug 28 | More on encoding neural networks as MILP,
big-M encoding in MILP; introduction to the Pareto-optimal
interpretation synthesis problem, recursive division of design
space to find Pareto-optimal interpretations |
Slides on big-M encoding
Paper: Sec 1, 2, 3A |
| Sep 1 | Pareto-optimal and locally Pareto-optimal
interpretation synthesis: formal problem statement, symbolic
encoding for reduction to weighted MaxSAT |
Paper: Sec 3A, 3B, Appendix A
Helper slides |
| Sep 4 | More on symbolic encoding for reduction to
weighted MaxSAT, recursive partitioning of design space and
related issues, encoding as MILP, formulating locally
Pareto-optimal synthesis as search+verification problem; brief
introduction to PAC learning and relevance to Pareto-optimal
interpretation synthesis |
Paper: Sec 3C, 4, 5 |
| Sep 8 | More on PAC learning essentials, and its
relevance to Pareto-optimal interpretation synthesis using
different accuracy and explainability measures in
interpretation synthesis -- relevant encodings; Contrastive and
abductive explanations revisited, illustration for decision
rule list, and for boosted tree ensembles.
|
Paper: Sec 1, 2
|
| Sep 11 | Relations between contrastive and
abductive explanations; modifications of explanations in the
presence of domain knowledge or rules; extraction of rules
from trustable datasets
|
Paper: Sec 2, 3, 4
|
| Sep 22 | Discussion on encoding of "at most k", "at least k" constraints
for sets of Boolean variables, Tseitin encoding, naive adder based encoding, Sinz
encoding, consistent and arc-consistent encodings
|
Slides by Ruben Martins: Slides 1-22
|
| Sep 25 | Decision sets, different metrics of
explainability for decision sets, optimal decision sets;
encoding of optimal decision set learning as
(weighted) MaxSAT problem
|
Paper: Sec 1, 2, 3, 4
|
| Sep 29 | Further observations about MaxSAT and MILP
encoding of optimal decision set learning, symmetric rules and handling them; safety in reinforcement learning: notions of shields and certificates
|
Paper: Sec 4.3, 5
|
| Oct 6 | Preemptive and post-posed shields: basic
modes of operation; basics of MDPs, reinforcement learning,
reactive controllers, safety property specification using
automata, two-player safety games
|
Paper: Sec 1, 2, 3
|
| Oct 9 | Abstracting MDP using a "safety" automaton;
justification for using non-deterministic as opposed to
probabilistic transitions; illustration through heated water-tank
inlet controller example; formulating the preemptive shielding
and post-posed shielding problems
|
Paper: Sec 3, 4, 5
|
| Oct 13 | Construction of game automaton,
identification of winning region and extraction of pre-emptive
and post-posed shields, correctness and minimal interference
of shields, convergence of learning in the presence of
shields; basic ideas of certificates for safety and liveness
properties in reinforcement learning
|
Paper-1: Sec 6, 7, 8
Paper-2: Sec 1, 2A
|
| Oct 16 |
More on safety, liveness and reach-while-avoid (RWA) properties,
discrete-time dynamical systems as a model for agent interacting
with environment; Lyapunov functions, Barrier functions, Lyapunov
Barrier functions as RWA certificates; neural RWA certificates,
Filtered RWA (FRWA) certificates; FRWA training, sampling and
verification
|
Paper: Sec 2, 4A, 4B
|
| Oct 23 | CEGIS loop for obtaining controller +
certificate, compositional RWA certificates: intuition,
algorithms, sampling, training, choosing intermediate goals
|
Paper: Sec 4C, 5
|
Oct 26
(part 1) | Metrics of fairness, Markov chains
as generators of events, randomized register monitors,
probabilistic specification expressions (PSE), formalization of
monitoring problem
|
Paper: Sec 1, 2, 3
|
Oct 26
(part 2) | Frequentist monitoring:
definition, core principle, division-free PSEs
|
Paper: Sec 4, 4.1
|
Oct 27
(part 1) | PSEs with division operator,
bounding memory with random reshuffling, algorithm for
implementing frequentist monitor
|
Paper: Sec 4.1, 4.2
|
Oct 27
(part 2) | Active monitoring of neural
networks to detect outliers, principal component analysis of
feature layer, bounding boxes of principal components for
training data, adaptation of monitor and re-training of
network; summary of course
|
Paper: Sec 1,2,3,4,5
|
|