Part II - Algorithms

a quick overview under the optimization perspective, with a focus on linear relaxation based methods.

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.

• Lecture 5: Basic formulation
• Lecture 6: Integer programming and linear programming formulations
• Lecture 7: CROWN bound propagation algorithm, illustrated with examples
• Lecture 8: Branch and bound algorithms (beta-CROWN)
• Lecture 9: Bound propagation on general computational graphs
• Lecture 10: Certified training and other misc topics

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.

Click here: Slides for Part II - Algorithms (PDF)

tl;dr: We first focus on efficient incomplete verifiers that rely on relaxing the nonconvex activation functions in neural networks into convex domains, such as CROWN and DeepPoly. Then, we briefly discuss how to further tighten the bounds from incomplete verifiers through optimization (α-CROWN). Then, we focus on complete verifiers with a specific focus on the recent research trend of branch-and-bound (BaB) based verifiers such as (β-CROWN) relying on rapid and GPU-accelerated incomplete verifiers for each bounding step.