Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition

by   Alessandro De Palma, et al.

We improve the scalability of Branch and Bound (BaB) algorithms for formally proving input-output properties of neural networks. First, we propose novel bounding algorithms based on Lagrangian Decomposition. Previous works have used off-the-shelf solvers to solve relaxations at each node of the BaB tree, or constructed weaker relaxations that can be solved efficiently, but lead to unnecessarily weak bounds. Our formulation restricts the optimization to a subspace of the dual domain that is guaranteed to contain the optimum, resulting in accelerated convergence. Furthermore, it allows for a massively parallel implementation, which is amenable to GPU acceleration via modern deep learning frameworks. Second, we present a novel activation-based branching strategy. By coupling an inexpensive heuristic with fast dual bounding, our branching scheme greatly reduces the size of the BaB tree compared to previous heuristic methods. Moreover, it performs competitively with a recent strategy based on learning algorithms, without its large offline training cost. Finally, we design a BaB framework, named Branch and Dual Network Bound (BaDNB), based on our novel bounding and branching algorithms. We show that BaDNB outperforms previous complete verification systems by a large margin, cutting average verification times by factors up to 50 on adversarial robustness properties.


page 1

page 2

page 3

page 4


Lagrangian Decomposition for Neural Network Verification

A fundamental component of neural network verification is the computatio...

Zonotope Domains for Lagrangian Neural Network Verification

Neural network verification aims to provide provable bounds for the outp...

RLT2-based Parallel Algorithms for Solving Large Quadratic Assignment Problems on Graphics Processing Unit Clusters

This paper discusses efficient parallel algorithms for obtaining strong ...

Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound

State-of-the-art neural network verifiers are fundamentally based on one...

Scaling the Convex Barrier with Active Sets

Tight and efficient neural network bounding is of critical importance fo...

IBP Regularization for Verified Adversarial Robustness via Branch-and-Bound

Recent works have tried to increase the verifiability of adversarially t...

Neural Network Branching for Neural Network Verification

Formal verification of neural networks is essential for their deployment...

Please sign up or login with your details

Forgot password? Click here to reset