Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition

Understand

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.