Zonotope Domains for Lagrangian Neural Network Verification

TL;DR

This paper introduces a novel verification method combining zonotope abstract domains with Lagrangian decomposition, enabling efficient and tighter bounds for neural network outputs compared to existing techniques.

Contribution

It merges zonotope-based abstract domains with Lagrangian methods, decomposing deep network verification into manageable 2-layer subproblems with improved efficiency.

Findings

Provides tighter bounds than linear programming methods.

Achieves more efficient verification in terms of time.

Demonstrates effectiveness on deep neural networks.

Abstract

Neural network verification aims to provide provable bounds for the output of a neural network for a given input range. Notable prior works in this domain have either generated bounds using abstract domains, which preserve some dependency between intermediate neurons in the network; or framed verification as an optimization problem and solved a relaxation using Lagrangian methods. A key drawback of the latter technique is that each neuron is treated independently, thereby ignoring important neuron interactions. We provide an approach that merges these two threads and uses zonotopes within a Lagrangian decomposition. Crucially, we can decompose the problem of verifying a deep neural network into the verification of many 2-layer neural networks. While each of these problems is provably hard, we provide efficient relaxation methods that are amenable to efficient dual ascent procedures. Our technique yields bounds that improve upon both linear programming and Lagrangian-based verification techniques in both time and bound tightness.