Enhancing Branch and Bound for Robustness Verification of Neural Networks via an Effective Branching Strategy

The existence of adversarial examples highlights the vulnerability of neural networks and brings much interest to the formal verification of neural network robustness. To improve the scalability of neural network verification while approaching completeness, researchers have adopted the branch-and-bound (BaB) framework. Better branching can reduce the number of branches to explore and plays an important role in BaB verification methods. In this paper, we propose a new branching strategy. It utilizes a low-cost metric to make splitting decisions and supports branching on ReLU activation functions. We conduct experiments on widely used benchmarks to evaluate its performance. Simulation results demonstrate that this branching strategy effectively improves the verification efficiency and is better than the state-of-the-art strategies in overall performance.