Tight Semidefinite Relaxations for Verifying Robustness of Neural Networks

TL;DR

This work analyzes when DeepSDP, a semidefinite relaxation used for safety verification of neural networks, is tight with respect to the underlying QCQP formulations. By employing a two-stage decomposition and KKT arguments, the authors establish rank-1 solvability under three configurations: a single-neuron network, a single-layer network with an ellipsoidal input set, and a single-layer network with a rectangular input set. The results provide explicit tightness conditions, ensuring that DeepSDP yields exact solutions for these cases and enabling exact safety guarantees in these settings. The findings offer theoretical guarantees for precise robustness verification and point to directions for extending tightness via local quadratic constraints and broader QCQP classes, with practical implications for safety-critical NN applications.

Abstract

For verifying the safety of neural networks (NNs), Fazlyab et al. (2019) introduced a semidefinite programming (SDP) approach called DeepSDP. This formulation can be viewed as the dual of the SDP relaxation for a problem formulated as a quadratically constrained quadratic program (QCQP). While SDP relaxations of QCQPs generally provide approximate solutions with some gaps, this work focuses on tight SDP relaxations that provide exact solutions to the QCQP for single-layer NNs. Specifically, we analyze tightness conditions in three cases: (i) NNs with a single neuron, (ii) single-layer NNs with an ellipsoidal input set, and (iii) single-layer NNs with a rectangular input set. For NNs with a single neuron, we propose a condition that ensures the SDP admits a rank-1 solution to DeepSDP by transforming the QCQP into an equivalent two-stage problem leads to a solution collinear with a predetermined vector. For single-layer NNs with an ellipsoidal input set, the collinearity of solutions is proved via the Karush-Kuhn-Tucker condition in the two-stage problem. In case of single-layer NNs with a rectangular input set, we demonstrate that the tightness of DeepSDP can be reduced to the single-neuron NNs, case (i), if the weight matrix is a diagonal matrix.

Figures (3)

• Figure 1: Correspondence between QCQPs and DeepSDP for the tightness. The solid lines display the equivalent optimal value of the problems. The wavy lines illustrate the corresponding relationship between the two problems.
• Figure 2: $\left(\e^1\right)^{\operatorname{T}}\z = 0$ case. The feasible set $\FC$ is the set of points on the gray plane and to the right of the white plane.
• Figure 3: $0 < \left(\e^1\right)^{\operatorname{T}}\z < \|\z\|$ case. The feasible set $\FC$ is the set of points below the gray plane and above the white plane.

Theorems & Definitions (19)

• Lemma 2.1
• Definition 2.2
• Lemma 2.3
• proof
• Theorem 3.1
• Lemma 4.3
• proof
• Proposition 4.4
• proof
• Theorem 4.5