Talk Title: Unboxing the Black-box: A Quest for Scalable and Powerful Neural Network Verifiers

Abstract: 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 under slightly altered inputs. When applying neural networks to mission-critical systems such as autonomous driving and aircraft control, it is often desirable to formally verify that a neural network satisfies given properties such as safety and robustness. Unfortunately, the complexity of neural networks has made the task of formally verifying their properties very challenging. To tackle this challenge, I first propose an efficient perturbation analysis algorithm based on linear relaxations of neural networks, which produces guaranteed output bounds given bounded input perturbations. The algorithm propagates linear inequalities through the network efficiently, analogous to the forward and backward propagation, and can be applied to arbitrary network architectures. To reduce relaxation error, I develop an efficient optimization procedure that can tighten linear relaxations rapidly on machine learning accelerators such as GPUs. This allows us to build a verifier which scales to much larger networks compared to existing linear programming based ones while producing tighter results. Lastly, I discuss how to further empower the verifier with branch and bound by incorporating the additional branching constraints into the bound propagation procedure. The combination of these advanced neural network verification techniques leads to α,β-CROWN, a scalable and powerful neural network verifier that is up to 2 to 3 orders of magnitudes faster than traditional CPU based neural network verifier and won the 2nd International Verification of Neural Networks Competition (VNN-COMP’21) with the highest total score over a set of 9 benchmarks.