Scaling the Convex Barrier with Active Sets. (arXiv:2101.05844v1 [cs.LG])

Tight and efficient neural network bounding is of critical importance for the
scaling of neural network verification systems. A number of efficient
specialised dual solvers for neural network bounds have been presented
recently, but they are often too loose to verify more challenging properties.
This lack of tightness is linked to the weakness of the employed relaxation,
which is usually a linear program of size linear in the number of neurons.
While a tighter linear relaxation for piecewise linear activations exists, it
comes at the cost of exponentially many constraints and thus currently lacks an
efficient customised solver. We alleviate this deficiency via a novel dual
algorithm that realises the full potential of the new relaxation by operating
on a small active set of dual variables. Our method recovers the strengths of
the new relaxation in the dual space: tightness and a linear separation oracle.
At the same time, it shares the benefits of previous dual approaches for weaker
relaxations: massive parallelism, GPU implementation, low cost per iteration
and valid bounds at any time. As a consequence, we obtain better bounds than
off-the-shelf solvers in only a fraction of their running time and recover the
speed-accuracy trade-offs of looser dual solvers if the computational budget is
small. We demonstrate that this results in significant formal verification
speed-ups.