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

Understand

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.