A Dual Approach to Scalable Verification of Deep Networks

TL;DR

The paper tackles scalable, formal verification of neural networks with arbitrary activation functions by formulating verification as a constrained optimization and deriving a Lagrangian dual that provides upper bounds on worst-case specification violations. The approach exploits layer-wise separability, reducing subproblems to simple, low-dimensional optimizations per neuron and per layer, and combines them into a global dual via subgradient methods. This anytime framework yields valid bounds without requiring complete convergence, with potential tightness guarantees under certain assumptions. The method enables provable robustness guarantees for networks in broader settings and larger architectures than prior piecewise-linear-only approaches.

Abstract

This paper addresses the problem of formally verifying desirable properties of neural networks, i.e., obtaining provable guarantees that neural networks satisfy specifications relating their inputs and outputs (robustness to bounded norm adversarial perturbations, for example). Most previous work on this topic was limited in its applicability by the size of the network, network architecture and the complexity of properties to be verified. In contrast, our framework applies to a general class of activation functions and specifications on neural network inputs and outputs. We formulate verification as an optimization problem (seeking to find the largest violation of the specification) and solve a Lagrangian relaxation of the optimization problem to obtain an upper bound on the worst case violation of the specification being verified. Our approach is anytime i.e. it can be stopped at any time and a valid bound on the maximum violation can be obtained. We develop specialized verification algorithms with provable tightness guarantees under special assumptions and demonstrate the practical significance of our general verification approach on a variety of verification tasks.