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

TL;DR

The paper introduces GenBaB, a versatile branch-and-bound framework for verifying neural networks with general nonlinearities, extending beyond piecewise linear activations to complex nonlinear functions and computation graphs.

Contribution

Develops a general branch-and-bound framework, GenBaB, for neural network verification with arbitrary nonlinearities, including new heuristics and pre-optimized branching points.

Findings

Effective verification of diverse nonlinear activation functions.

Applicable to complex neural architectures like LSTMs and Transformers.

Part of the winning entries in recent neural network verification competitions.

Abstract

Branch-and-bound (BaB) is among the most effective techniques for neural network (NN) verification. However, existing works on BaB for NN verification have mostly focused on NNs with piecewise linear activations, especially ReLU networks. In this paper, we develop a general framework, named GenBaB, to conduct BaB on general nonlinearities to verify NNs with general architectures, based on linear bound propagation for NN verification. To decide which neuron to branch, we design a new branching heuristic which leverages linear bounds as shortcuts to efficiently estimate the potential improvement after branching. To decide nontrivial branching points for general nonlinear functions, we propose to pre-optimize branching points, which can be efficiently leveraged during verification with a lookup table. We demonstrate the effectiveness of our GenBaB on verifying a wide range of NNs, including NNs with activation functions such as Sigmoid, Tanh, Sine and GeLU, as well as NNs involving multi-dimensional nonlinear operations such as multiplications in LSTMs and Vision Transformers. Our framework also allows the verification of general nonlinear computation graphs and enables verification applications beyond simple NNs, particularly for AC Optimal Power Flow (ACOPF). GenBaB is part of the latest $\alpha$,$\beta$-CROWN, the winner of the 4th and the 5th International Verification of Neural Networks Competition (VNN-COMP 2023 and 2024). Code for reproducing the experiments is available at https://github.com/shizhouxing/GenBaB.