Marta Kwiatkowska

[intermediate/advanced] Probabilistic Verification for Neural Networks

Summary

This course will provide an overview of formal verification for neural networks, which can be used to certify that the networks are robust to adversarial perturbations. Most methods focus on lower or upper bounding the image, i.e. the set of outputs of the network, which may result in loose bounds. Instead, we focus on verifying the preimage, i.e. the set of inputs satisfying a given output property. The lectures will present a general framework based on linear relaxations for preimage abstraction that produces under- and over-approximations of any polyhedral output set, and demonstrate use cases of certification of controller reachability and patch attacks on neural networks. Finally, a probabilistic variant of neural networks, called Bayesian neural networks, will be introduced. Bayesian neural networks return a probability distribution on outputs, and their verification draws on bound propagation and involves bounding the posterior probability.

Syllabus

References

Pre-requisites

Short bio

Marta Kwiatkowska is a Professor of Computing Systems and Fellow at Trinity College, University of Oxford. Her area of expertise lies in probabilistic and quantitative verification techniques and the synthesis of correct-by-construction systems from quantitative specifications. She led the development of the probabilistic model checker PRISM, which has been used to model and verify numerous case studies across a variety of application domains. Recently, she has been focusing on safety and trust in Artificial Intelligence, with an emphasis on safety and robustness guarantees for machine learning. Marta has been the recipient of two ERC Advanced Grants and an honorary doctorate from KTH Institute of Technology, and was the first female winner of the Royal Society Milner Medal. She is a Fellow of the ACM, a Member of Academia Europea, and a Fellow of the Royal Society.