Adaptive Branch-and-Bound Tree Exploration for Neural Network Verification

TL;DR

This work addresses the inefficiency of naive Branch-and-Bound (BaB) in neural network verification by introducing ABONN, an adaptive BaB framework that uses Monte-Carlo tree search guided by counterexample potentiality to prioritize sub-problems likely to yield counterexamples. Counterexample potentiality blends sub-problem depth with the approximated verifier output to steer exploration and enable early termination when a counterexample is found. ABONN achieves substantial speedups over baselines like BaB-baseline and $\alpha\beta$-Crown on MNIST and CIFAR-10 benchmarks, particularly for complex models, and analyzes the impact of hyperparameters, notably $\lambda$ and $c$, on performance. By integrating adaptive tree exploration with existing ReLU-branching heuristics, ABONN offers a practical, scalable approach to rigorous neural network verification with improved efficiency and robust results.

Abstract

Formal verification is a rigorous approach that can provably ensure the quality of neural networks, and to date, Branch and Bound (BaB) is the state-of-the-art that performs verification by splitting the problem as needed and applying off-the-shelf verifiers to sub-problems for improved performance. However, existing BaB may not be efficient, due to its naive way of exploring the space of sub-problems that ignores the \emph{importance} of different sub-problems. To bridge this gap, we first introduce a notion of ``importance'' that reflects how likely a counterexample can be found with a sub-problem, and then we devise a novel verification approach, called ABONN, that explores the sub-problem space of BaB adaptively, in a Monte-Carlo tree search (MCTS) style. The exploration is guided by the ``importance'' of different sub-problems, so it favors the sub-problems that are more likely to find counterexamples. As soon as it finds a counterexample, it can immediately terminate; even though it cannot find, after visiting all the sub-problems, it can still manage to verify the problem. We evaluate ABONN with 552 verification problems from commonly-used datasets and neural network models, and compare it with the state-of-the-art verifiers as baseline approaches. Experimental evaluation shows that ABONN demonstrates speedups of up to $15.2\times$ on MNIST and $24.7\times$ on CIFAR-10. We further study the influences of hyperparameters to the performance of ABONN, and the effectiveness of our adaptive tree exploration.

Figures (6)

• Figure 1: Neural network verification problem and a solution via branch and bound (BaB).
• Figure 2: $\mathsf{ABONN}$'s process for solving the problem.
• Figure 3: The distribution of the sizes of the BaB trees used in our experiments
• Figure 4: RQ1 -- Comparison of $\mathsf{ABONN}$ over BaB-baseline in time costs and speedup. Each blue dot stands for a problem.
• Figure 5: RQ2 -- Impact of hyperparameter selection across different $\lambda$ and $c$. A darker cell implies a better performance.

Theorems & Definitions (1)

• Definition 1: Counterexample potentiality