Interior-Point Vanishing Problem in Semidefinite Relaxations for Neural Network Verification

TL;DR

This paper identifies a fundamental limitation called interior-point vanishing in SDP relaxations for neural network verification, especially in deep networks, and proposes solutions to improve feasibility and scalability.

Contribution

The paper reveals the interior-point vanishing problem in SDP relaxations for deep neural network verification and introduces five methods to enhance feasibility, enabling verification of deeper networks.

Findings

Successfully solved 88% of previously unsolvable problems

Revealed that traditional constraints can harm feasibility

Provided practical solutions to improve SDP scalability

Abstract

Semidefinite programming (SDP) relaxation has emerged as a promising approach for neural network verification, offering tighter bounds than other convex relaxation methods for deep neural networks (DNNs) with ReLU activations. However, we identify a critical limitation in the SDP relaxation when applied to deep networks: interior-point vanishing, which leads to the loss of strict feasibility -- a crucial condition for the numerical stability and optimality of SDP. Through rigorous theoretical and empirical analysis, we demonstrate that as the depth of DNNs increases, the strict feasibility is likely to be lost, creating a fundamental barrier to scaling SDP-based verification. To address the interior-point vanishing, we design and investigate five solutions to enhance the feasibility conditions of the verification problem. Our methods can successfully solve 88% of the problems that could not be solved by existing methods, accounting for 41% of the total. Our analysis also reveals that the valid constraints for the lower and upper bounds for each ReLU unit are traditionally inherited from prior work without solid reasons, but are actually not only unbeneficial but also even harmful to the problem's feasibility. This work provides valuable insights into the fundamental challenges of SDP-based DNN verification and offers practical solutions to improve its applicability to deeper neural networks, contributing to the development of more reliable and secure systems with DNNs.