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.

本篇论文提出了基于 Lagrangian Decomposition 的 bounding 算法和一种新的基于 activation 的 branching 策略。这些新方法应用于 BaDNB 框架中，比以前的完整验证系统具有更快的效率和更高的可扩展性。

通过 Lagrangian 分解改进的神经网络验证分支定界算法

Improved Branch and Bound for Neural Network Verification via Lagrangian  Decomposition

A fundamental component of neural network verification is the computation of
bounds on the values their outputs can take. Previous methods have either used
off-the-shelf solvers, discarding the problem structure, or relaxed the problem
even further, making the bounds unnecessarily loose. We propose a novel
approach based on Lagrangian Decomposition. Our formulation admits an efficient
supergradient ascent algorithm, as well as an improved proximal algorithm. Both
the algorithms offer three advantages: (i) they yield bounds that are provably
at least as tight as previous dual algorithms relying on Lagrangian
relaxations; (ii) they are based on operations analogous to forward/backward
pass of neural networks layers and are therefore easily parallelizable,
amenable to GPU implementation and able to take advantage of the convolutional
structure of problems; and (iii) they allow for anytime stopping while still
providing valid bounds. Empirically, we show that we obtain bounds comparable
with off-the-shelf solvers in a fraction of their running time, and obtain
tighter bounds in the same time as previous dual algorithms. This results in an
overall speed-up when employing the bounds for formal verification. Code for
our algorithms is available at
this https URL

通过 Lagrangian 分解，提出了一种新的神经网络验证方法，其在 GPU 上实施时可提供有效的结果，以推测最大化值的边界，并且可以随时停止，可用于推导形式化验证。