Neural Network Verification with Branch-and-Bound for General Nonlinearities

Neural Network Verification with Branch-and-Bound for General Nonlinearities

31 May 2024 | Zhouxing Shi*1, Qirui Jin*2, Zico Kolter3, Suman Jana4, Cho-Jui Hsieh1, Huan Zhang5
This paper introduces GenBaB, a general framework for neural network (NN) verification using branch-and-bound (BaB) for nonlinearities in computational graphs. GenBaB addresses the limitations of existing BaB methods, which primarily focus on ReLU networks. The framework is designed to handle various nonlinearities, including Sigmoid, Tanh, Sine, and GeLU, as well as multi-dimensional nonlinear operations like multiplications in LSTMs and Vision Transformers. Key contributions include a new branching heuristic, Bound Propagation with Shortcuts (BBPS), which leverages linear bounds to efficiently estimate the potential improvement after branching, and an offline optimization procedure to determine nontrivial branching points. Experiments demonstrate the effectiveness of GenBaB on a wide range of NNs, showing significant improvements over existing methods, especially for models with stronger nonlinearities. GenBaB has been integrated into the latest version of α,β-CROWN, which won the 4th International Verification of Neural Networks Competition (VNN-COMP 2023).This paper introduces GenBaB, a general framework for neural network (NN) verification using branch-and-bound (BaB) for nonlinearities in computational graphs. GenBaB addresses the limitations of existing BaB methods, which primarily focus on ReLU networks. The framework is designed to handle various nonlinearities, including Sigmoid, Tanh, Sine, and GeLU, as well as multi-dimensional nonlinear operations like multiplications in LSTMs and Vision Transformers. Key contributions include a new branching heuristic, Bound Propagation with Shortcuts (BBPS), which leverages linear bounds to efficiently estimate the potential improvement after branching, and an offline optimization procedure to determine nontrivial branching points. Experiments demonstrate the effectiveness of GenBaB on a wide range of NNs, showing significant improvements over existing methods, especially for models with stronger nonlinearities. GenBaB has been integrated into the latest version of α,β-CROWN, which won the 4th International Verification of Neural Networks Competition (VNN-COMP 2023).
Reach us at info@study.space
[slides] Neural Network Verification with Branch-and-Bound for General Nonlinearities | StudySpace