Parametric Chordal Sparsity for SDP-based Neural Network Verification
Many future technologies rely on neural networks, but verifying the
correctness of their behavior remains a major challenge. It is known that
neural networks can be fragile in the presence of even small input
perturbations, yielding unpredictable outputs. The verification of neural
networks is therefore vital to their adoption, and a number of approaches have
been proposed in recent years. In this paper we focus on semidefinite
programming (SDP) based techniques for neural network verification, which are
particularly attractive because they can encode expressive behaviors while
ensuring a polynomial time decision. Our starting point is the DeepSDP
framework proposed by Fazlyab et al, which uses quadratic constraints to
abstract the verification problem into a large-scale SDP. When the size of the
neural network grows, however, solving this SDP quickly becomes intractable.
Our key observation is that by leveraging chordal sparsity and specific
parametrizations of DeepSDP, we can decompose the primary computational
bottleneck of DeepSDP -- a large linear matrix inequality (LMI) -- into an
equivalent collection of smaller LMIs. Our parametrization admits a tunable
parameter, allowing us to trade-off efficiency and accuracy in the verification
procedure. We call our formulation Chordal-DeepSDP, and provide experimental
evaluation to show that it can: (1) effectively increase accuracy with the
tunable parameter and (2) outperform DeepSDP on deeper networks.