Neural networks have become a crucial element in modern artificial intelligence. However, they are often black-boxes and can behave unexpectedly and produce surprisingly wrong results, such as adversarial examples. In this tutorial, we introduce the neural network verification problem, which aims to formally guarantee properties of neural networks such as robustness, safety, and correctness. Our tutorial covers the theoretical foundations of the verification problem and an introduction to state-of-the-art algorithms. Furthermore, we will give a hands-on coding tutorial for user-friendly neural network verification toolboxes, allowing practitioners to easily apply formal verification techniques to their customized applications.
In the first half of the tutorial, we introduce Mathematical Backgrounds and Algorithms for neural network verification, including problem formulation, incomplete verification algorithms (with a focus on state-of-the-art bound propagation based algorithms such as CROWN), complete verification algorithms (e.g., integer programming formulation and branch and bound based methods). The second half is a Hands-on Tutorial with interactive coding examples to help the participants understand the verification problem and apply state-of-the-art neural network verification tools to their own applications. Coding examples include adversarial robustness verification problem on a CIFAR-10 classifier and a certified adversarial defense for a natural language model (LSTM/Transformer). Finally, we demonstrate how to use the state-of-the-art and award-winning complete neural network verifier α,β-CROWN (also written as alpha-beta-CROWN).
The slides for each part of the tutorial are provided below:
Here are some relevant pre-recorded videos on neural network verification by the tutorial organizers.