  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.
