Part III - Practice
using state-of-the-art toolboxes for neural network verification.

Updates 2025

For latest educational materials regarding neural network verification, you are suggested to take a look at the new course developed by Prof. Huan Zhang at UIUC. Checkout the slides at ECE598HZ: Advanced Topics in Machine Learning and Formal Methods. In particular, the following lectures will be helpful for understanding neural network verification problem settings and the representative linear bound propagation framework (CROWN) in the α,β-CROWN verifier.

Revisiting the SAT/SMT formulation in Lecture 3 - 4 may also be helpful for readers.

For a simple reference implementation of CROWN, please check out the Homework for ECE598HZ. Problem 3 comes with a complete and clean implementation of CROWN in its simplest form.

The content below is from the original AAAI 2022 tutorial, which may still be helpful but not updated anymore.

tl;dr: We first give a very brief overview of the tools used in the tutorial, including the motivations, features and design philosophy of the tools. Our tutorial will first cover the versatile PyTorch based auto_LiRPA library for incomplete verification and certified defense. The library allows easy handling of general neural networks, including ResNet, LSTM, and Transformer. Then, we introduce the usage of one of the state-of-the-art complete verification tools, ɑ,β-CROWN (alpha-beta-CROWN), which outperformed 11 other tools and won the first prize in VNN-COMP 2021.

Practical Incomplete Verification Tool: auto_LiRPA

Click here: Slides for Part III - Practice - auto_LiRPA (PDF)

Click here: Code demo for Part III - Practice - auto_LiRPA (Colab)

Practical Complete Verification Tool: ɑ,β-CROWN

Click here: Slides for Part III - Practice - ɑ,β-CROWN (PDF)

Click here: Code demo for Part III - Practice - ɑ,β-CROWN (Colab)

*****

A neural network verification tutorial presented by Huan Zhang, Kaidi Xu, Shiqi Wang and Cho-Jui Hsieh

☕ Pudhina theme by Knhash 🛠️