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 上实施时可提供有效的结果，以推测最大化值的边界，并且可以随时停止，可用于推导形式化验证。