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

## Abstract

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.

## 1 Introduction

Deep Neural Networks (DNNs) have achieved remarkable success across various domains, including image recognition [25], natural language processing [3], and autonomous systems [10].
However, their vulnerability against adversarial perturbations, known as adversarial attacks [41, 18], has raised critical concerns about their reliability and security [28] and spurred extensive research efforts to enhance the robustness of DNN models such as robustified training (e.g., adversarial training [32]) and certified defenses [48, 13].
Although these defense or mitigation methods have gained traction, they can so far only offer empirical or probabilistic guarantees and thus do not provide definitive guarantees about a model’s behavior under adversarial conditions. To address the limitation, DNN verification [22, 11, 23] has emerged as a critical area of research, aiming to ensure that DNN models behave reliably under all possible scenarios within assumed conditions, e.g., verifying whether a classification model maintains its predicted label for any input perturbation within a given norm ball.

Due to the high complexity of DNNs, complete (i.e., exact) verification methods [1, 4, 6, 16, 24, 30, 42] are often NP-hard and therefore too expensive in practice. Consequently, incomplete verification [19, 39, 47, 46] has gained attention, which is a method to verify a relaxed version of the complete DNN verification problem since a DNN is always verified if its relaxed verification problem is verified. Among the various approaches to relaxing the complete verification, semidefinite programming (SDP) relaxation [36, 5] has shown high performance for verifying DNNs with rectified linear unit (ReLU) activation units, as it is known to give the tightest relaxation among convex relaxation approaches [16]. The current state-of-the-art incomplete approaches [51, 46, 55] refine the solutions with branch-and-bound (BaB) strategies, e.g., exploring all combinations of positive and negative cases of each ReLU activation [9, 46]. While BaB brings performance improvements in practice, the quality of the initial solution obtained by the convex relaxation is still essential, as BaB is applied on top of it.

While SDP relaxation is recognized as a method that can give one of the tightest relaxations [12, 5], SDP-based verification methods are not commonly used in state-of-the-art verification methods [8]. Their high computational cost is often mentioned as a reason for this [28]. However, in this study, we identify a more fundamental reason that challenges the use of SDP in DNN verification: interior-point vanishing, a term we define to describe the phenomenon that SDP-based verification is unlikely to have feasible interior points (i.e., strict feasibility) when the depth of the DNN being verified increases.
Strict feasibility is a crucial condition that ensures numerical stability and optimality in SDP solutions [38]. The interior-point vanishing could be the actual reason hindering the development of the SDP-based approach in this area.

Contributions: This study is the first to identify the interior-point vanishing problem in SDP-based DNN verification and evaluate the impacts. Prior studies [5, 26] did not identify this problem because they did not evaluate models as deep as practical DNNs to observe the impact.
Through our theoretical and empirical analysis, we reveal that as the depth of a network grows, the likelihood of encountering strict feasibility issues increases, posing a significant limitation to the applicability of SDP-based verification methods in practical scenarios.
To address the challenges, we propose five newly designed approaches to enhance the feasibility conditions of the verification problem. These methods aim to mitigate numerical instability and improve the solvability of the SDP.
Our experimental results demonstrate that our methods can successfully solve 88% of the problems that could not be solved by existing methods, accounting for 41% of the total.
We further find that the valid constraints for the lower and upper bounds for each ReLU unit are traditionally inherited from prior work [5, 36] without solid reasons, but are actually not only unbeneficial but also harmful to the problem’s feasibility.

Notation:
Let $\mathbb{R}^{n}$ and $\mathcal{S}^{n}$ denote the $n$-dimensional Euclidean space and the space of $n\times n$ symmetric matrices, respectively.
We express a symmetric matrix $\bm{X}\in\mathcal{S}^{n}$ as $\bm{X}\succeq\bm{O}$ and $\bm{X}\succ\bm{0}$ if $\bm{X}$ is positive semidefinite and positive definite, respectively.
For a vector $\bm{x}\in\mathbb{R}^{n}$, its $i$-th element is denoted by $\lparen\bm{x}\rparen_{i}$.
For a matrix $\bm{X}\in\mathbb{R}^{m\times n}$, the $\lparen i,j\rparen$ element of $\bm{X}$ is denoted by $\lparen\bm{X}\rparen_{ij}$, and the $i$-th row of $\bm{X}$ is denoted by $\bm{X}\lparen i,\colon\rparen$.
The $\ell_{2}$ and $\ell_{\infty}$ norms of a vector $\bm{x}$ are denoted by $\lVert\bm{x}\rVert_{2}$ and $\lVert\bm{x}\rVert_{\infty}$, respectively, and the Frobenius norm of a matrix $\bm{X}$ is denoted by $\lVert\bm{X}\rVert_{F}=\sqrt{\mathrm{tr}\left\lparen\bm{X}^{\top}\bm{X}\right\rparen}$.
For two vectors $\bm{x},\bm{y}\in\mathbb{R}^{n}$, the Hadamard product, which is
element-wise multiplication, is denoted by $\bm{x}\odot\bm{y}$.
The map $\mathrm{diag}\left\lparen\cdot\right\rparen\colon\mathbb{R}^{n\times n}\to
\mathbb{R}^{n}$ represents the operator that arranges the diagonal elements of a matrix into a vector.
For a nonnegative integer $L$, we define $[L]\coloneqq\{0,1,\dots,L-1\}$.

## 2 Background

### 2.1 DNN Verification Problem

Consider a DNN model $\bm{f}\colon\mathbb{R}^{d}\rightarrow\mathbb{R}^{m}$ for $m$-class classification.
Let $\bar{\bm{x}}$ be an input instance and $i^{\star}$ be its prediction label provided by $\bm{f}$.
We define the DNN verification problem as the following decision problem:

###### Problem 2.1 (DNN Verification) .

Given a DNN model $\bm{f}\colon\mathbb{R}^{d}\rightarrow\mathbb{R}^{m}$, an input instance $\bar{\bm{x}}$ with the prediction label $i^{\star}$, and a perturbation radius $\rho>0$, determine whether for all $\bm{x}_{0}$ satisfying $\lVert\bm{x}_{0}-\bar{\bm{x}}\rVert_{\infty}\leq\rho$, the prediction label remains unchanged, i.e., $\mathop{\rm arg~{}max}\limits_{i=1,\dots,m}~{}\lparen\bm{f}\lparen\bm{x}_{0}
\rparen\rparen_{i}=i^{\star}$.

This problem determines whether the prediction label of the input $\bar{\bm{x}}$ can be changed to another label $i\neq i^{\star}$ by perturbing the input within the radius $\rho>0$. If [2.1](https://arxiv.org/html/2506.10269v1#S2.Thmtheorem1) is true, the prediction label cannot change to another label $i\neq i^{\star}$ by perturbing the original input $\bar{\bm{x}}$ within the radius $\rho$, meaning the DNN model $\bm{f}$ is *robust* for $\bar{\bm{x}}$ with a perturbation radius $\rho$.
In this work, we focus on $L$-layer feed-forward DNN $\bm{f}\colon\mathbb{R}^{d}\to\mathbb{R}^{m}$. For an input $\bar{\bm{x}}$, its output is defined as $\bm{f}\lparen\bar{\bm{x}}\rparen\coloneqq\bm{W}_{L}\bm{x}_{L}+\bm{b}_{L}$, where $\bm{x}_{i+1}=\mathrm{ReLU}\left\lparen\bm{W}_{i}\bm{x}_{i}+\bm{b}_{i}\right\rparen$ for $i\in[L]$, and $\bm{x}_{0}=\bar{\bm{x}}$, where $\bm{W}_{i}\in\mathbb{R}^{n_{i+1}\times n_{i}}$ and $\bm{b}_{i}\in\mathbb{R}^{n_{i+1}}$ are the weight matrix and bias vector of the $i$-th layer, respectively.
$\mathrm{ReLU}\left\lparen\cdot\right\rparen$ is a map that applies the ReLU function to each element of a vector. The predicted label for an input $\bar{\bm{x}}$ is determined as $i^{\star}=\mathop{\rm arg~{}max}\limits_{i=1,\dots,m}~{}\lparen\bm{f}\lparen
\bar{\bm{x}}\rparen\rparen_{i}$.

For a DNN with ReLU activation, [2.1](https://arxiv.org/html/2506.10269v1#S2.Thmtheorem1) can be equivalent to solve the following optimization problem:

$$ $\displaystyle\gamma^{\star}\coloneqq\min_{\{\bm{x}_{i}\}}$ $\displaystyle\quad\bm{c}^{\top}\bm{x}_{L}+c_{0}$ (1a) $\displaystyle\mathrm{s.t.}$ $\displaystyle\quad\bm{x}_{i+1}=\operatorname{ReLU}\lparen\bm{W}_{i}\bm{x}_{i}+ \bm{b}_{i}\rparen$ $\displaystyle\quad\lparen i\in[L]\rparen,$ (1b) $\displaystyle\quad\lVert\bm{x}_{0}-\bar{\bm{x}}\rVert_{\infty}\leq\rho,$ (1c) $\displaystyle\quad\bm{l}_{i+1}\leq\bm{x}_{i+1}\leq\bm{u}_{i+1}$ $\displaystyle\quad\lparen i\in[L]\rparen,$ (1d) $$

where $\bm{c}\coloneq\lparen\bm{W}_{L}\lparen i^{\star},\colon\rparen-\bm{W}_{L}
\lparen i,\colon\rparen\rparen^{\top}$ and $c_{0}\coloneq\lparen\bm{b}_{L}\rparen_{i^{\star}}-\lparen\bm{b}_{L}\rparen_{i}$.
The vectors $\bm{l}_{i+1}$ and $\bm{u}_{i+1}$ represent the lower and upper bounds after activation, respectively. We obtained the lower and upper bounds using a boundary propagation method [45, 19].
[2.1](https://arxiv.org/html/2506.10269v1#S2.Thmtheorem1) is true if and only if the optimal value $\gamma^{\star}$ is positive.
However, due to the constraint ([1b](https://arxiv.org/html/2506.10269v1#S2.E1.2)), this optimization problem is nonconvex and thus generally hard to solve in a practical time.

Instead of directly solving this complete verification problem, we can relax it to an incomplete convex relaxation problem by outer-approximating the feasible region of the problem ([1](https://arxiv.org/html/2506.10269v1#S2.E1)) with a convex set $\mathcal{D}$:

$$ $\displaystyle\gamma_{\mathcal{D}}\coloneqq\min_{\{\bm{x}_{i}\}}$ $\displaystyle\quad\bm{c}^{\top}\bm{x}_{L}+c_{0}$ $\displaystyle\mathrm{s.t.}$ $\displaystyle\quad\lparen\bm{x}_{0},\bm{x}_{1},\ldots,\bm{x}_{L}\rparen\in \mathcal{D},$ $$

where $\gamma^{\star}\geq\gamma_{\mathcal{D}}$ holds.
When $\gamma_{\mathcal{D}}>0$, the answer to [2.1](https://arxiv.org/html/2506.10269v1#S2.Thmtheorem1) is true; Otherwise (i.e., when $\gamma^{\star}>0\geq\gamma_{\mathcal{D}}$), the verification is undetermined.

###### Problem 2.1 (DNN Verification) .

### 2.2 Semidefinite Relaxation

SDP relaxation [36, 5, 12] is one of the outer-approximation methods for the nonconvex optimization problem ([1](https://arxiv.org/html/2506.10269v1#S2.E1)), and recognized as a method that can give one of the tightest relaxations. Starting from the problem ([1](https://arxiv.org/html/2506.10269v1#S2.E1)), we can obtain the SDP-relaxed problem as the following procedure: First, we convert the problem ([1](https://arxiv.org/html/2506.10269v1#S2.E1)) into an equivalent quadratically constrained quadratic program (QCQP). The ReLU constraints ([1b](https://arxiv.org/html/2506.10269v1#S2.E1.2)) can be equivalently replaced with the following linear and quadratic constraints:

$$ $\displaystyle\bm{x}_{i+1}\geq\bm{0}$ $\displaystyle\quad\lparen i\in[L]\rparen,$ (2a) $\displaystyle\bm{x}_{i+1}\geq\bm{W}_{i}\bm{x}_{i}+\bm{b}_{i}$ $\displaystyle\quad\lparen i\in[L]\rparen,$ (2b) $\displaystyle\bm{x}_{i+1}\odot\lparen\bm{x}_{i+1}-\bm{W}_{i}\bm{x}_{i}-\bm{b}_ {i}\rparen=0$ $\displaystyle\quad\lparen i\in[L]\rparen.$ (2c) $$

The input and activation constraints ([1c](https://arxiv.org/html/2506.10269v1#S2.E1.3)) and ([1d](https://arxiv.org/html/2506.10269v1#S2.E1.4)) can be also replaced with the following quadratic ones:

$$ $\bm{x}_{i}\odot\bm{x}_{i}-\lparen\bm{l}_{i}+\bm{u}_{i}\rparen\odot\bm{x}_{i}+ \bm{l}_{i}\odot\bm{u}_{i}\leq 0\quad\lparen i\in[L+1]\rparen.$ (3) $$

We note that $i=0$ corresponds to the input layer. [Eq. 3](https://arxiv.org/html/2506.10269v1#S2.E3) for $i=0$ describes the perturbation bound on the input $\bar{\bm{x}}$, i.e., $\bm{l}_{0}=\bar{\bm{x}}-\rho\bm{1}_{n_{0}}$ and $\bm{u}_{0}=\bar{\bm{x}}+\rho\bm{1}_{n_{0}}$ for the input layer, [Eq. 3](https://arxiv.org/html/2506.10269v1#S2.E3) with $L=0$ is equivalent to the input constraint ([1c](https://arxiv.org/html/2506.10269v1#S2.E1.3)). As [Eqs. 2](https://arxiv.org/html/2506.10269v1#S2.E2) and [3](https://arxiv.org/html/2506.10269v1#S2.E3) are quadratic, the problem ([1](https://arxiv.org/html/2506.10269v1#S2.E1)) can be converted to the following QCQP:

$$ $\gamma^{*}\coloneqq\min\{\bm{c}^{\top}\bm{x}_{L}+\bm{c}_{0}\mid\text{\lx@cref{ creftypepluralcap~refnum}{eq:relu_qcqp} and~\lx@cref{refnum}{eq:qcqp}}\}.$ (4) $$

Finally, we can derive an SDP relaxation of the QCQP problem ([4](https://arxiv.org/html/2506.10269v1#S2.E4)) by polynomial lifting [34, 27].
We introduce a vector $\bm{v}=\lparen 1,\bm{x}_{0}^{\top},\bm{x}_{1}^{\top},\dots,\bm{x}_{L}^{\top}
\rparen^{\top}\in\mathbb{R}^{1+\sum_{i=0}^{L}n_{i}}$ and a symmetric matrix variable $\bm{P}=\bm{v}\bm{v}^{\top}\in\mathcal{S}^{1+\sum_{i=0}^{L}n_{i}}$.
With $\bm{v}$ and $\bm{P}$, the problem ([4](https://arxiv.org/html/2506.10269v1#S2.E4)) can be equivalently reformulated as an SDP with a rank constraint: $\mathrm{rank}\left\lparen\bm{P}\right\rparen=1$.
By removing the rank constraint, we can obtain an SDP relaxation of the problem ([4](https://arxiv.org/html/2506.10269v1#S2.E4)) as follows:

$$ $\displaystyle\min_{\bm{P}}$ $\displaystyle\quad\bm{c}^{\top}\bm{P}[\bm{x}_{L}]+c_{0}$ (5a) $\displaystyle\mathrm{s.t.}$ $\displaystyle\quad\bm{P}[\bm{x}_{i+1}]\geq\bm{0}$ $\displaystyle\quad\lparen i\in[L]\rparen,$ (5b) $\displaystyle\quad\bm{P}[\bm{x}_{i+1}]\geq\bm{W}_{i}\bm{P}[\bm{x}_{i}]+\bm{b}_ {i},$ $\displaystyle\quad\lparen i\in[L]\rparen,$ (5c) $\displaystyle\quad\mathrm{diag}\left\lparen\bm{P}[\bm{x}_{i+1}\bm{x}_{i+1}^{ \top}]-\bm{W}_{i}\bm{P}[\bm{x}_{i}\bm{x}_{i+1}^{\top}]\right\rparen-\bm{b}_{i} \odot\bm{P}[\bm{x}_{i+1}]=\bm{0}$ $\displaystyle\quad\lparen i\in[L]\rparen,$ (5d) $\displaystyle\quad\mathrm{diag}\left\lparen\bm{P}\left[\bm{x}_{i}\bm{x}_{i}^{ \top}\right]\right\rparen-\lparen\bm{l}_{i}+\bm{u}_{i}\rparen\odot\bm{P}[\bm{x }_{i}]+\bm{l}_{i}\odot\bm{u}_{i}\leq\bm{0}$ $\displaystyle\quad\lparen i\in[L]\rparen,$ (5e) $\displaystyle\quad\bm{P}\left[1\right]=1,~{}\bm{P}\succeq\bm{O},$ (5f) $$

where we use the same indexings $\bm{P}[\cdot]$ as in [36].
The constraints ([2](https://arxiv.org/html/2506.10269v1#S2.E2)) and ([3](https://arxiv.org/html/2506.10269v1#S2.E3)) are reformulated as linear constraints in [Eqs. 5b](https://arxiv.org/html/2506.10269v1#S2.E5.2), [5c](https://arxiv.org/html/2506.10269v1#S2.E5.3), [5d](https://arxiv.org/html/2506.10269v1#S2.E5.4) and [5e](https://arxiv.org/html/2506.10269v1#S2.E5.5).
Note also that the constraints in [Eq. 5f](https://arxiv.org/html/2506.10269v1#S2.E5.6) are valid constraints when $\bm{P}=\bm{v}\bm{v}^{\top}$.

#### 2.2.1 Preprocessing to Remove Inactive Neurons

We always apply a popular preprocessing to remove identified inactive neurons with the upper bound $u_{ij}=0$ before solving the problem ([4](https://arxiv.org/html/2506.10269v1#S2.E4)) throughout this paper. We follow the same preprocessing methodology used in prior work [5] and use the $\alpha$-CROWN [51] to obtain the upper and lower bounds.
However, we emphasize that it is generally impossible to identify and remove all inactive neurons before solving DNN verification. This preprocessing identifies inactive neurons with lightweight verification methods, such as $\alpha$-CROWN [51]. However, these methods are still incomplete verification techniques, i.e., they cannot identify all inactive neurons. We can identify all inactive neurons if we apply complete verification, such as MIP-based verification, but this is almost equivalent to solving the original problem and is generally impractical.

## 3 Interior-Point Vanishing

We investigate the impact of the interior-point vanishing on the numerical stability and optimality of the SDP relaxation problem ([5](https://arxiv.org/html/2506.10269v1#S2.E5)).
We define interior-point vanishing to describe the phenomenon of SDP-based verification’s inability to have feasible interior points (i.e., strict feasibility) when the depth of the DNN being verified increases. We first introduce the critical role of strict feasibility when solving SDP problems and then conduct an empirical and theoretical impact analysis on the SDP relaxation problem.

### 3.1 Strict Feasibility and Slater’s Condition

We first introduce the strict feasibility and Slater’s condition, which are essential for the strong duality theorem in SDP problems.
We start this discussion from the standard form of the SDP problem.
Let $\mathcal{S}^{n}$ be the set of $n\times n$ real-valued symmetric matrices.
Then, the standard form of the primal SDP problem is given as follows:

$$ $\displaystyle\min_{\bm{X}}$ $\displaystyle\quad\mathrm{tr}\left\lparen\bm{C}\bm{X}\right\rparen$ (6a) $\displaystyle\mathrm{s.t.}$ $\displaystyle\quad\mathrm{tr}\left\lparen\bm{A}_{j}\bm{X}\right\rparen=b_{j}~{ }(j=1,\ldots,m),$ (6b) $\displaystyle\quad\bm{X}\succeq\bm{O},$ (6c) $$

where the variable is $\bm{X}\in\mathcal{S}^{n}$, and $\bm{A}_{j}\in\mathcal{S}^{n}$, $b_{j}\in\mathbb{R}~{}(j=1.\dots,m)$, and $\bm{C}\in\mathcal{S}^{n}$ are given parameters.

When the SDP problem ([6](https://arxiv.org/html/2506.10269v1#S3.E6)) has a feasible solution with $\bm{X}\succ\bm{O}$, we say that the problem is strictly feasible, and such a feasible solution $\bm{X}$ is called a strictly feasible solution or an interior feasible solution.
Strict feasibility is crucial when solving SDP problems, since Slater’s condition, a sufficient condition for strong duality, requires strict feasibility [31].

###### Theorem 3.1 (Strong Duality) .

If the primal problem ([6](https://arxiv.org/html/2506.10269v1#S3.E6)) and its dual are both strictly feasible, then both have bounded optimal solutions
and have the same optimal value.

To determine whether the current solution is optimal, the primal-dual interior-point method requires the gap between the objective functions of the primal and dual problems to be sufficiently close to zero.
However, when the strong duality does not hold, such a gap is not necessarily zero for optimal solutions, and thus, the primal-dual interior-point method may fail to determine the optimality of the current solution.
In addition, [38] reports that the lack of strong duality causes serious numerical instability and gives wrong optimal values and solutions when the problem is not strictly feasible. This numerical instability is critical for interior-point methods and can be even more severe for first-order methods [7, 40, 14], as the latter cannot exploit second-order Hessian information during optimization. We further discuss this in [Section 6.1](https://arxiv.org/html/2506.10269v1#S6.SS1).

To identify the strict feasibility of the SDP problem ([6](https://arxiv.org/html/2506.10269v1#S3.E6)), we design the following verification problem:

###### Proposition 3.2 (Verification of Strict Feasibility) .

Consider the following problem:

$$ $\displaystyle\max_{\bm{X},\lambda}\quad$ $\displaystyle\lambda$ (7a) $\displaystyle\mathrm{s.t.}\quad$ $\displaystyle\mathrm{tr}\left\lparen\bm{A}_{j}\cdot\lparen\bm{X}+\lambda\bm{I} \rparen\right\rparen=b_{j}~{}(j=1,\dots,m)$ (7b) $\displaystyle\bm{X}\succeq\bm{O},$ (7c) $$

where $\bm{I}$ is the identity matrix and $\lambda\in\mathbb{R}$ is an auxiliary variable. The original SDP problem ([6](https://arxiv.org/html/2506.10269v1#S3.E6)) is strictly feasible if and only if the optimal value of the problem ([7](https://arxiv.org/html/2506.10269v1#S3.E7)) is positive.

###### Proof.

See [Section A.1](https://arxiv.org/html/2506.10269v1#A1.SS1).
∎

We note that the SDP-based relaxation problem ([5](https://arxiv.org/html/2506.10269v1#S2.E5)) can be equivalently expressed in the standard form ([6](https://arxiv.org/html/2506.10269v1#S3.E6)) since the problem ([6](https://arxiv.org/html/2506.10269v1#S3.E6)) is a standard form of SDP problems.
Therefore, we can check the strict feasibility of the problem ([5](https://arxiv.org/html/2506.10269v1#S2.E5)) by solving its corresponding problem ([7](https://arxiv.org/html/2506.10269v1#S3.E7)). [Appendix B](https://arxiv.org/html/2506.10269v1#A2) describes the standard SDP form of [Proposition 3.2](https://arxiv.org/html/2506.10269v1#S3.Thmtheorem2).

###### Theorem 3.1 (Strong Duality) .

###### Proposition 3.2 (Verification of Strict Feasibility) .

###### Proof.

### 3.2 Empirical Analysis

We empirically investigate the impact of the interior-point vanishing problem using the strict feasibility verification problem ([7](https://arxiv.org/html/2506.10269v1#S3.E7)) and demonstrate that the interior-point vanishing becomes more severe as the number of layers $L$ increases.

Experimental Setup:
We investigated how frequently the interior-point vanishing problem arises in the problem ([5](https://arxiv.org/html/2506.10269v1#S2.E5)) and how it depends on the number of layers in NN models by solving the problem ([7](https://arxiv.org/html/2506.10269v1#S3.E7)).
In this experiment, we used two datasets: MNIST [15] and Fashion-MNIST [50], and trained fully connected ReLU networks with cross-entropy loss and AdaDelta optimizer [54].
For ReLU networks, we set the number of layers $L$ from 2 to 16 and the number of neurons in each layer to 20.

To construct the problem instances for the problem ([7](https://arxiv.org/html/2506.10269v1#S3.E7)), we selected ten images from each dataset and downsampled them to $5\ {\rm pixel}\times 5\ {\rm pixel}$ to reduce the computational load, which is caused by high-precision computation.
For the instance $\bar{\bm{x}}$ for verification, we selected the first ten images from each dataset and compressed them to $5\ {\rm pixel}\times 5\ {\rm pixel}$.
For each instance, we computed the upper and lower bounds $\lparen\bm{l}_{i},\bm{u}_{i}\rparen$ of each layer by the $\alpha$-CROWN [51]. We removed all inactivate neurons with $u_{ij}=0$, similar to prior work [5]. We then solved the corresponding strict feasibility verification problem ([7](https://arxiv.org/html/2506.10269v1#S3.E7)) by using the SDPA-GMP [33].
Note that the SDPA-GMP solver employs multi-precision arithmetic in a primal-dual interior point method, making it more reliable than standard double-precision arithmetic for ill-conditioned SDP problem instances. We used the hexadecuple precision (512 bits).

Results and Analysis:
LABEL:tbl:min_eign summarizes the results for each $L$.
For each dataset, we constructed five distinct models with different random seeds, yielding a total of 50 problem instances per dataset (10 images times 5 models).
The column Solved (%) in LABEL:tbl:min_eign shows the fraction of instances that SDPA-GMP successfully terminated its computation with an optimality guarantee, and the column *Avg. Obj.* represents the average of the optimal values across the solved instances.
From Table LABEL:tbl:min_eign, we observe that for both MNIST and Fashion-MNIST, SDPA-GMP consistently terminated its computation for most instances when the DNN depth was less than 10.
However, as $L$ increased, the Solved (%) decreased, and when $L=16$, SDPA-GMP failed to finish the computation for all instances in both datasets.
Furthermore, when $L\geq 10$, *Avg. Obj.* was sufficiently close to zero regardless of the datasets, indicating that the SDP-based verification problem ([5](https://arxiv.org/html/2506.10269v1#S2.E5)) did not have strictly feasible solutions.
This lack of strict feasibility appears to be a major factor causing SDPA-GMP to fail.
Overall, these results highlight that the interior-point vanishing problem is likely to occur in the SDP-based DNN verification when $L$ is large.

Interior-Point Vanishing in Benchmark Networks:
To further validate our findings, we also evaluated networks commonly used in prior verification research [37, 12], including models trained with different robustification techniques such as dual formulation training, adversarial training, and standard training. Our experiments on these networks (ranging from 2 to 9 layers with 100 neurons per layer) consistently showed interior-point vanishing across all training methodologies, with minimum eigenvalues at or near zero. This confirms that the phenomenon is an inherent property of the SDP relaxation rather than a training artifact, and affects practical networks used in the verification works. Detailed results are in [Appendix D](https://arxiv.org/html/2506.10269v1#A4).

**Table 1: Impact of the interior-point vanishing problem on the different layer depths. The gray rows indicate that the interior-point vanishing almost always happens as the minimum eigenvalues are almost zero, and even negative due to numerical errors.**
| $L$ | MNIST | Fashion-MNIST |  |  |
| --- | --- | --- | --- | --- |
|  | Solved (%) | Avg. Obj. | Solved (%) | Avg. Obj. |
| 2 | 98% | 2.13$\pm$1.93E-05 | 100% | 5.79$\pm$5.76E-05 |
| 4 | 98% | 1.72$\pm$1.45E-06 | 100% | 4.93$\pm$5.73E-06 |
| 6 | 98% | 8.06$\pm$5.38E-08 | 98% | 1.56$\pm$1.12E-07 |
| 8 | 98% | 3.52$\pm$3.47E-09 | 94% | 4.98$\pm$5.88E-09 |
| 10 | 18% | $-$4.09$\pm$1.70E-10 | 26% | $-$2.57$\pm$3.11E-10 |
| 12 | 2% | $-$8.31$\pm$2.96E-10 | 4% | $-$6.90$\pm$2.62E-10 |
| 16 | 0% | $-$1.20$\pm$8.24E-09 | 0% | $-$9.35$\pm$3.47E-10 |

#### 3.2.1 Constraints Related to Interior-Point Vanishing Problem

To identify the constraints causing the interior-point-vanishing problem, we analyze which constraint in ([5](https://arxiv.org/html/2506.10269v1#S2.E5)) is significant in the problem’s feasibility by removing the constraints one by one. We find that the ReLU equality constraint ([5d](https://arxiv.org/html/2506.10269v1#S2.E5.4)) and the upper bound $u_{i}$ in [Eq. 5e](https://arxiv.org/html/2506.10269v1#S2.E5.5) have high sensitivity to the problem feasibility. Details are in [Appendix C](https://arxiv.org/html/2506.10269v1#A3). We will explore the relaxation methods on these constraints in [Section 4](https://arxiv.org/html/2506.10269v1#S4).

### 3.3 Theoretical Analysis

We explore the theoretical reasoning behind why the interior-point vanishing problem happens when the depth of DNN increases by examining the structures of the problem ([5](https://arxiv.org/html/2506.10269v1#S2.E5)).

#### 3.3.1 Existence of Inactive Neurons

We first demonstrate that interior-point vanishing occurs—that is, problem ([5](https://arxiv.org/html/2506.10269v1#S2.E5)) lacks strictly feasible solutions—when the DNN contains inactive neurons whose outputs are always zero. The following proposition states that a positive semidefinite matrix $\bm{P}\succeq\bm{O}$ is not positive definite if it has a diagonal element $\lparen\bm{P}\rparen_{ii}=0$.

###### Proposition 3.3 .

For a positive semidefinite matrix $\bm{P}\succeq\bm{O}$, if there exists a diagonal element $\lparen\bm{P}\rparen_{ii}=0$, $\lambda_{\min}\lparen\bm{P}\rparen=0$, that is $\bm{P}$ is not positive definite.

###### Proof.

See [20], for example.
∎

According to [Proposition 3.3](https://arxiv.org/html/2506.10269v1#S3.Thmtheorem3), the minimum eigenvalue of feasible $\bm{P}$ will always be zero if some diagonal elements of the matrix variable $\bm{P}$ in the problem ([5](https://arxiv.org/html/2506.10269v1#S2.E5)) are forced to be zero. In this case, the problem ([5](https://arxiv.org/html/2506.10269v1#S2.E5)) does not have any strictly feasible solutions.
We explore a situation in which this issue arises within problem ([5](https://arxiv.org/html/2506.10269v1#S2.E5)).
Let us consider a situation where an entry of the upper bound vector $\bm{u}_{i}$ is zero for the $i$-th layer, which means that the corresponding neuron is always inactive for all $\bm{x}_{0}\in\{\bm{x}\mid\|\bm{x}-\bar{\bm{x}}\|_{\infty}\leq\rho\}$.
Let $j$ be the corresponding index of the neuron of the $i$-th layer
with $\lparen\bm{u}_{i}\rparen_{j}=0$.
In this case, its corresponding lower bound $\lparen\bm{l}_{i}\rparen_{j}\leq 0$, and from the constraint ([5e](https://arxiv.org/html/2506.10269v1#S2.E5.5)) for the $j$-th neuron of the $i$-th layer, we have

$$ $\lparen\bm{P}[\bm{x}_{i}\bm{x}_{i}^{\top}]\rparen_{jj}\leq\left\lparen\lparen \bm{l}_{i}+\bm{u}_{i}\rparen\odot\bm{P}[\bm{x}_{i}]+\bm{l}_{i}\odot\bm{u}_{i} \right\rparen_{j}\leq 0.$ $$

Along with the semidefinite constraint $\bm{P}\succeq\bm{O}$ and the constraint ([5e](https://arxiv.org/html/2506.10269v1#S2.E5.5)), we have $\lparen\bm{P}[\bm{x}_{i}\bm{x}_{i}^{\top}]\rparen_{jj}=0$.
This implies that for all feasible $\bm{P}$ for the problem ([5](https://arxiv.org/html/2506.10269v1#S2.E5)), its minimum eigenvalue is zero.
Consequently, we see that if there are neurons that are always inactive for all input $\bm{x}_{0}\in\{\bm{x}\mid\lVert\bm{x}-\bar{\bm{x}}\rVert_{\infty}\leq\rho\}$, the problem ([5](https://arxiv.org/html/2506.10269v1#S2.E5)) does not have any strictly feasible solutions.
As discussed in [Section 2.2.1](https://arxiv.org/html/2506.10269v1#S2.SS2.SSS1), we cannot identify and remove all inactive neurons before solving DNN verification. Since even a single inactive neuron can cause interior-point vanishing, this indicates that there is no trivial method to address the interior-point vanishing problem.

###### Proposition 3.3 .

###### Proof.

#### 3.3.2 Minimum Eigenvalue Bound

We examine the minimum eigenvalue of feasible $\bm{P}$ to the problem ([5](https://arxiv.org/html/2506.10269v1#S2.E5)) and show that the norm of the weight matrix of each layer is crucial for the strict feasibility of the problem ([5](https://arxiv.org/html/2506.10269v1#S2.E5)).
For notational simplicity, let us define a constant matrix horizontally concatenating $\bm{b}_{i}$ and $\bm{W}_{i}$ as
$\widetilde{\bm{W}}_{i}=\lparen\bm{b}_{i}~{}\bm{W}_{i}\rparen~{}\lparen i\in[L]\rparen$.

First, we show that the trace of $\bm{P}[\bm{x}_{i}\bm{x}_{i}^{\top}]$ for each $i\in[L]$ is bounded by a nonnegative constant.
We formally express this in the following lemma:

###### Lemma 3.4 (Trace Bound Propagation) .

Let $T_{0}\coloneqq\lparen\lVert\bar{\bm{x}}\rVert_{2}+\rho\sqrt{n_{0}}\rparen^{2}\geq
0$.
For each $i\in[L-1]$, recursively define

$$ $T_{i+1}\coloneqq(1+T_{i})\cdot\lVert\widetilde{\bm{W}}_{i}\rVert_{F}^{2}\quad \lparen i\in[L-1]\rparen.$ $$

Then, for any feasible solution $\bm{P}\succeq\bm{O}$ to the problem ([5](https://arxiv.org/html/2506.10269v1#S2.E5)), the following inequality holds:

$$ $\mathrm{tr}\left\lparen\bm{P}[\bm{x}_{i}\bm{x}_{i}^{\top}]\right\rparen\leq T_ {i}\quad\lparen i\in[L]\rparen.$ (8) $$

###### Proof.

See Appendix [3.4](https://arxiv.org/html/2506.10269v1#S3.Thmtheorem4).
∎

While [Lemma 3.4](https://arxiv.org/html/2506.10269v1#S3.Thmtheorem4) focuses on bounding $\mathrm{tr}\left\lparen\bm{P}[\bm{x}_{i}\bm{x}_{i}^{\top}]\right\rparen$ for each $i\in[L]$, we can also derive individual upper bounds for each diagonal element of feasible $\bm{P}$ for the problem ([5](https://arxiv.org/html/2506.10269v1#S2.E5)) in a similar manner.

###### Lemma 3.5 (Element-wise Bound Propagation) .

Let $T_{i}$ be the constant defined in [Lemma 3.4](https://arxiv.org/html/2506.10269v1#S3.Thmtheorem4).
Then, for each $i\in[L]$, the $j$-th diagonal element of $\lparen\bm{P}[\bm{x}_{i}\bm{x}_{i}^{\top}]\rparen_{jj}$ is bounded as

$$ $\lparen\bm{P}[\bm{x}_{i+1}\bm{x}_{i+1}^{\top}]\rparen_{jj}\leq\lparen 1+T_{i} \rparen\cdot\lVert\bm{\widetilde{W}}_{i}\lparen j,\colon\rparen\rVert_{2}^{2},$ $$

where $\bm{\widetilde{W}}_{i}\lparen j,\colon\rparen$ is the $j$-th row vector of $\bm{\widetilde{W}}_{i}$.

We can show [Lemma 3.5](https://arxiv.org/html/2506.10269v1#S3.Thmtheorem5) in the same way as [Lemma 3.4](https://arxiv.org/html/2506.10269v1#S3.Thmtheorem4) by focusing on the $j$-th diagonal element of $\bm{P}[\bm{x}_{i}\bm{x}_{i}^{\top}]$, and we omit the proof here.

From [Lemma 3.5](https://arxiv.org/html/2506.10269v1#S3.Thmtheorem5) and the fact that $\lambda_{\min}\lparen\bm{P}\rparen\leq\min_{j}\lparen\bm{P}\rparen_{jj}$ for $\bm{P}\succeq\bm{O}$, we finally provide an upper bound of the minimum eigenvalue of feasible $\bm{P}\succeq\bm{O}$ to the problem ([5](https://arxiv.org/html/2506.10269v1#S2.E5)).

###### Theorem 3.6 (Minimum Eigenvalue Bound) .

Let $T_{i}$ be the constant defined in [Lemma 3.4](https://arxiv.org/html/2506.10269v1#S3.Thmtheorem4).
Then, for all feasible solutions $\bm{P}$ to the problem ([5](https://arxiv.org/html/2506.10269v1#S2.E5)), it follows that

$$ $\lambda_{\min}\lparen\bm{P}\rparen\leq\min_{i\in[L]}\left\{\min_{j=1,\dots,n_{ i}}\left\{\lparen 1+T_{i}\rparen\cdot\lVert\bm{\widetilde{W}}_{i}\lparen j, \colon\rparen\rVert_{2}^{2}\right\}\right\}.$ $$

[Theorem 3.6](https://arxiv.org/html/2506.10269v1#S3.Thmtheorem6) highlights that the minimum norm of the extended row vector $\bm{\widetilde{W}}_{i}\lparen j,\colon\rparen$ plays a crucial role in controlling the possible minimum eigenvalue of feasible $\bm{P}$ to the problem ([5](https://arxiv.org/html/2506.10269v1#S2.E5)).
Specifically, [Theorem 3.6](https://arxiv.org/html/2506.10269v1#S3.Thmtheorem6) indicates that when there exists a single neuron $j$ in some layer $i\in[L]$ with a small $\lVert\bm{\widetilde{W}}_{i}\lparen j,\colon\rparen\rVert_{2}$, the minimum eigenvalue of any feasible $\bm{P}$ is constrained to be close to zero.
*Consequently, the presence of even a single such neuron can trigger the interior-point vanishing problem in SDP-based DNN verification.*

Figure: Figure 1: Relaxed area of our LeakySDP by Leaky ReLU function.

###### Lemma 3.4 (Trace Bound Propagation) .

###### Proof.

###### Lemma 3.5 (Element-wise Bound Propagation) .

###### Theorem 3.6 (Minimum Eigenvalue Bound) .

## 4 Methodology

To address the interior-point vanishing problem, we designed five methods to relax the constraints to obtain more feasible interior points. Based on the observations found in [Section 3](https://arxiv.org/html/2506.10269v1#S3), we mainly explore the further relaxations regarding the ReLU equality constraint ([5d](https://arxiv.org/html/2506.10269v1#S2.E5.4)) and the upper bound $\bm{u}_{i}$ in [Eq. 5e](https://arxiv.org/html/2506.10269v1#S2.E5.5).

### 4.1 Relaxation of Equality Constraints: ε 𝜀 \varepsilon italic_ε -SDP

We first simply relax the ReLU equality constraint ([5d](https://arxiv.org/html/2506.10269v1#S2.E5.4)) by allowing a tolerance $\varepsilon\geq 0$ as follows:

$$ $\displaystyle\min_{\bm{P}}{}$ $\displaystyle\quad\bm{c}^{\top}\bm{P}[\bm{x}_{L}]+c_{0}$ $\displaystyle\mathrm{s.t.}{}$ Eqs. 5b , 5c , 5e and 5f , and $\displaystyle\quad-\varepsilon\cdot\bm{1}_{n_{i}}\leq\mathrm{diag}\left\lparen \bm{P}[\bm{x}_{i+1}\bm{x}_{i+1}^{\top}]-\bm{W}_{i}\bm{P}[\bm{x}_{i}\bm{x}_{i+1 }^{\top}]\right\rparen-\bm{b}_{i}\odot\bm{P}[\bm{x}_{i+1}]\leq\varepsilon\cdot \bm{1}_{n_{i}}$ $\displaystyle\quad\lparen i\in[L]\rparen.$ $$

We call this new relaxed incomplete verification $\varepsilon$-SDP. This relaxation is simple but straightforwardly relaxes the ReLU equality constraint.

### 4.2 SDP Relaxation with Leaky ReLU: LeakySDP

We also relax the ReLU constraint ([5d](https://arxiv.org/html/2506.10269v1#S2.E5.4)) with the Leaky ReLU function, which is defined as:

$$ $\mathrm{LeakyReLU}\left\lparen x\right\rparen=\begin{cases}x&\lparen x\geq 0 \rparen,\\ \alpha\cdot x&\lparen x<0\rparen,\end{cases}$ $$

where $\alpha\in(0,1)$ is a small positive constant. Similar to the ReLU, we can describe the Leaky ReLU with linear constraints on $\bm{P}$.

Since the DNN to be verified uses the ReLU, we relax the ReLU activation with the Leaky ReLU as illustrated in [Figure 1](https://arxiv.org/html/2506.10269v1#S3.F1). We allow the verification problem to take the value in the area between the Leaky ReLU and the x-axis when $x\geq 0$. As it still contains the ReLU function part, this operation relaxes the original problem.
Formally, the constraints ([5b](https://arxiv.org/html/2506.10269v1#S2.E5.2)), ([5c](https://arxiv.org/html/2506.10269v1#S2.E5.3)), and
([5d](https://arxiv.org/html/2506.10269v1#S2.E5.4)) are replaced with the inequalities and equality constraints associated with the Leaky ReLU function as follows:

$$ $\displaystyle\min_{\bm{P}}{}$ $\displaystyle\quad\bm{c}^{\top}\bm{P}[\bm{x}_{L}]+c_{0}$ $\displaystyle\mathrm{s.t.}{}$ Eqs. ( 5e ), ( 5f ), and $\displaystyle\quad\bm{P}[\bm{x}_{i+1}]\geq\alpha\left\lparen\bm{W}_{i}\bm{P}[ \bm{x}_{i}]+\bm{b}_{i}\right\rparen$ $\displaystyle\quad\lparen i\in[L]\rparen,$ $\displaystyle\quad\bm{P}[\bm{x}_{i+1}]\geq\bm{W}_{i}\bm{P}[\bm{x}_{i}]+\bm{b}_ {i}$ $\displaystyle\quad\lparen i\in[L]\rparen,$ $\displaystyle\quad\operatorname{diag}\left\lparen\bm{P}[\bm{x}_{i+1}\bm{x}_{i+ 1}^{\top}]-\bm{W}_{i}\,\bm{P}[\bm{x}_{i}\bm{x}_{i+1}^{\top}]\right\rparen-\bm{ b}_{i}\odot\bm{P}[\bm{x}_{i+1}]\leq\bm{0}$ $\displaystyle\quad\lparen i\in[L]\rparen.$ $$

We refer to this formulation as LeakySDP.

### 4.3 Diagonal Scaling: D-Scale

We adopt a common approach to solve an ill-conditioned SDP, called scaling [49], which aims to improve the condition number of the matrices involved in SDP to reduce sensitivity to numerical errors. As finding the optimal scaling is almost the same as solving the original SDP, several heuristic approaches have been designed.
Diagonal scaling [17] is one of the most commonly used scaling methods due to its low computational overheads. Specifically, the diagonal scaling can be written as follows:

###### Proposition 4.1 .

Let $\bm{D}\succ\bm{O}$ be a diagonal matrix.
Then, the standard primal SDP ([6](https://arxiv.org/html/2506.10269v1#S3.E6)) can be equivalently transformed as follows:

$$ $\displaystyle\min_{\bm{X}}$ $\displaystyle\quad\mathrm{tr}\left\lparen\lparen\bm{D}\bm{C}\bm{D}\rparen\cdot \lparen\bm{D}^{-1}\bm{X}\bm{D}^{-1}\rparen\right\rparen$ $\displaystyle\mathrm{s.t.}$ $\displaystyle\quad\mathrm{tr}\left\lparen\lparen\bm{D}\bm{A}_{j}\bm{D}\rparen \cdot\lparen\bm{D}^{-1}\bm{X}\bm{D}^{-1}\rparen\right\rparen=b_{j}\quad(j=1, \ldots,m),$ $\displaystyle\quad\bm{D}^{-1}\bm{X}\bm{D}^{-1}\succeq\bm{O}.$ $$

As a scaling diagonal matrix, we use $\bm{D}$ whose diagonal elements $\mathrm{diag}\left\lparen\bm{D}\right\rparen=\lparen 1,\bm{u}_{1}^{\top},\bm{u
}_{2}^{\top},\ldots,\bm{u}_{L}^{\top}\rparen^{\top}$. We note that division by zero does not occur since we remove neurons with $u_{ij}\leq 0$ in the preprocessing as discussed in [Section 2.2.1](https://arxiv.org/html/2506.10269v1#S2.SS2.SSS1).

###### Proposition 4.1 .

### 4.4 Neural Network Weight Scaling: W-Scale

We further design a new scaling method by leveraging the findings in [Theorem 3.6](https://arxiv.org/html/2506.10269v1#S3.Thmtheorem6), which shows that the minimum eigenvalue of any feasible solution $\bm{P}$ to the SDP relaxation is constrained by the smallest norm of the extended row vector $\widetilde{\bm{W}}_{i}\lparen j,\colon\rparen$.
Since a neuron $j$ in some layer $i$ has a particularly small norm $\|\widetilde{\bm{W}}_{i}(j,\colon)\|_{2}$ triggers the interior-point vanishing problem, we rescale the parameters in each layer to avoid excessively small row norms.
Let $\check{w}_{i}=\min_{j=1,\dots,n_{i}}\|\widetilde{\bm{W}}_{i}(j,\colon)\|_{2}$ be the minimum $L_{2}$ norm of the row vectors of $\widetilde{\bm{W}}_{i}$.
According to $\check{w}_{i}$, we scale the weight matrix $\widetilde{\bm{W}}_{i}$ of intermediate layers $i\in[L-1]$ as $\widetilde{\bm{W}}^{\prime}_{i}\coloneqq\widetilde{\bm{W}}_{i}/\check{w}_{i}~{
}\lparen i\in[L-1]\rparen,$
and for the final layer as
$\widetilde{\bm{W}}^{\prime}_{L}\coloneqq\widetilde{\bm{W}}_{L}\cdot\prod_{i=0}
^{L-1}\check{w}_{i}.$
Note that this scaling makes the final output given by the scaled network the same as the original one.
We refer to this approach as *W-Scale*.

**Table 2: Comparison of success rates for SDP verification problems solved by our five proposed methods and two prior methods.**
| $L$ | Proposed Methods | Prior Methods |  |  |  |  |  |
| --- | --- | --- | --- | --- | --- | --- | --- |
|  | $\varepsilon$-SDP | LeakySDP | B-Remove | D-Scale | W-Scale | LayerSDP | SDP-IP |
| 2 | 100% | 100% | 100% | 100% | 100% | 100% | 100% |
| 4 | 100% | 100% | 100% | 100% | 100% | 100% | 100% |
| 6 | 100% | 98% | 100% | 100% | 100% | 100% | 100% |
| 8 | 100% | 82% | 100% | 88% | 88% | 82% | 98% |
| 10 | 100% | 4% | 100% | 8% | 8% | 2% | 14% |
| 12 | 78% | 0% | 100% | 0% | 0% | 0% | 0% |
| 16 | 24% | 0% | 66% | 0% | 0% | 0% | 0% |

Figure: Figure 2: Average gap between the optimal objective values of our methods and the LayerSDP’s optimal. The numbers above each bars are $\varepsilon$ for $\varepsilon$-SDP and $\alpha$ for LeakySDP.
Refer to caption: x1.png

### 4.5 Removal of Bound Constraints: B-Remove

To relax the upper bound constraints highly related to the interior-point vanishing, we simply remove the constraints from the intermediate layers since the SDP relaxation of ReLU does not require such bounds as shown in [Section 2.2](https://arxiv.org/html/2506.10269v1#S2.SS2) and Appendix [C](https://arxiv.org/html/2506.10269v1#A3). The bounds are introduced as valid constraints, which typically help higher converging in many applications. We refer to this approach as *B-Remove*.

## 5 Evaluation

We evaluate our five methods designed in [Section 4](https://arxiv.org/html/2506.10269v1#S4), regarding the capability to address the interior-point vanishing problem and the relaxation quality.

### 5.1 Experimental Setup

We trained 35 fully connected DNN models on the MNIST dataset:
We set the number of layers $L\in\{2,4,\dots,16\}$ and tried 5 different seeds for each $L$.
The number of neurons in each layer was fixed to $n_{i}=20~{}\lparen i=1,\dots,L\rparen$.
We use the original resolution, i.e., $28\ {\rm pixel}\times 28\ {\rm pixel}$, and use the normal version of SDPA [53], not the high-precision SDPA-GMP as used in [Section 3](https://arxiv.org/html/2506.10269v1#S3), to handle the original image size. SDPA may introduce worse numerical stability, but this can allow us to conduct larger-scale experiments and more clearly observe the improved numerical stability from our designed methods. We discuss the choice of SDP solver in [Section 6.3](https://arxiv.org/html/2506.10269v1#S6.SS3).
We judge that an SDP problem is successfully solved if the primal-dual objective gap is lower than $10^{-6}$.
We randomly selected 10 images from MNIST and randomly chose targets for the labels.
We compare our proposed methods, denoted as $\varepsilon$-SDP (with parameter $\varepsilon=0.01$) and LeakySDP (with parameter $\alpha=0.01$), against prior SDP-based verification methods: SDP-IP [36], the original SDP-based verification method, and LayerSDP [5], an improved SDP-based verification method that utilizes the sparse structure in the layer-wise structure of DNN and the constraints used in the LP-based verification [16].

### 5.2 Evaluation on Interior-Point Vanishing

We evaluate whether our methods can effectively address the interior-point vanishing problem.
[Table 2](https://arxiv.org/html/2506.10269v1#S4.T2) shows the success rates for SDP verification problems solved by our five proposed methods and two existing methods.
As shown, the existing methods (LayerSDP and SDP-IP) suffer from this problem starting at $L=8$, and fail almost entirely at $L=10$, as discussed in [Section 3.2](https://arxiv.org/html/2506.10269v1#S3.SS2).

In contrast, our $\varepsilon$-SDP and B-Remove show substantial improvements.
These two methods directly address the constraints we identified as a potential source of the interior-point vanishing problem in [Section 3.3](https://arxiv.org/html/2506.10269v1#S3.SS3) and [Appendix C](https://arxiv.org/html/2506.10269v1#A3).
Notably, B-Remove achieves a surprisingly large improvement despite its simplicity—just removing upper and lower bounds.
We further discuss this result in [Section 6.1](https://arxiv.org/html/2506.10269v1#S6.SS1).

The other three methods (LeakySDP, D-Scale, and W-Scale), however, do not significantly improve the success rate.
For LeakySDP, it can be noted that while it relaxes the part where the input of the ReLU activation function is non-positive in the negative direction, it has little effect on the positive part.
Due to this property, the effectiveness of the method is limited when positive activations are dominant.
In addition, nodes with small absolute values may contribute significantly to the primal-dual gap, but applying Leaky-ReLU to such nodes results in only minor changes, limiting the method’s impact.
D-Scale and W-Scale aimed to improve the ill-condition of the SDP by scaling, which is commonly used to improve the convergence of SDP.
However, our experiments suggest that such generic approaches were not effective for addressing the interior-point vanishing problem.

### 5.3 Evaluation on Relaxation Quality

We then evaluate the relaxation quality of our methods.
Since all our proposed methods relaxed the problem more than SDP-IP and LayerSDP, our methods generally have less verification power than these existing methods, as long as the existing methods can solve the problem.
To quantify the verification power losses, we calculate the gap between the optimal objective values obtained by our methods and LayerSDP, which has a tighter or at least eaqual relaxation than SDP-IP.
A small objective gap implies that although our methods yield looser relaxations, they still maintain comparable verification power to LayerSDP.

[Figure 2](https://arxiv.org/html/2506.10269v1#S4.F2) shows the average gap between the optimal objective function values of our methods and the LayerSDP’s ones.
The average is only calculated over the instances for which all methods converge to their optimal. $\varepsilon$-SDP shows relatively high verification power loss since it directly relaxes the ReLU constraints, although $\varepsilon$-SDP can mitigate the interior-point vanishing problem as in [Section 5.2](https://arxiv.org/html/2506.10269v1#S5.SS2). LeakySDP does not have significant power losses. Considering LeakySDP shows almost similar performance to LayerSDP in [Section 5.2](https://arxiv.org/html/2506.10269v1#S5.SS2), the relaxation in the negative area does not look effective. In contrast, B-Remove does not cause a major verification power loss. This is because the SDP relaxation of ReLU does not require the upper and lower bounds other than for the input layer as shown in [Eq. 3](https://arxiv.org/html/2506.10269v1#S2.E3), i.e., $\bm{l}_{i}$ and $\bm{u}_{i}$ for $i>0$. The lower and upper bounds of the input layer describe the attacker’s norm budget $\rho$ in [2.1](https://arxiv.org/html/2506.10269v1#S2.Thmtheorem1), not used to relax ReLU. Nevertheless, prior approaches adopt each layer’s upper and lower bounds by following the same custom in the traditional LP-based verification [16]. We further discuss this in [Section 6.1](https://arxiv.org/html/2506.10269v1#S6.SS1).

## 6 Discussion

### 6.1 Backfire of Layer Bounds

We find that the upper and lower bounds of each layer, i.e., $\bm{l}_{i}$ and $\bm{u}_{i}$ for $i>0$ even amplify the interior-point vanishing problem ([Section 5.2](https://arxiv.org/html/2506.10269v1#S5.SS2)) even though they does not have a major impact on improving the relaxation quality ([Section 5.3](https://arxiv.org/html/2506.10269v1#S5.SS3)). For the SDP-based DNN verification, the upper and lower bounds are not mandatory to formulate the problem. Nevertheless, prior approaches adopt them because the SDP formulation is extended from the traditional LP-based verification [16], which requires the bounds to form the triangle area consisting of the three points at the origin, lower bound, and upper bound, to relax the ReLU function. Generally, more valid linear constraints are considered to be beneficial in improving the verification quality, e.g., LayerSDP introduces constraints inspired by the triangle area in the LP-based verification. However, this assumption does not always hold for SDP. Unnecessary valid constraints may remove the feasible interior points and lead to numerical instability. The increase in the number of linear constraints also introduces additional computational costs. Even if it works for a toy shallow model, we recommend validating the effectiveness on the deeper model at least with 10 layers, ideally more than 20 layers.

### 6.2 Applicability of Non-Interior-Point Methods

We predominantly used the interior-point method, more specifically, the primal-dual interior-point path-following method, to solve the SDP problems in this study. While prior work [14] demonstrates that their first-order method outperforms interior-point methods in DNN verification, we cannot employ first-order methods [7, 40, 14] for our research as they cannot provide theoretical guarantees of optimality. Since first-order methods depend on heuristic stopping criteria and step size adjustments, we cannot conclusively determine the existence of interior-point vanishing, even if the first-order methods say they converge to some solutions. Furthermore, the interior-point methods have generally higher numerical stability and accuracy compared to the first-order methods, as the interior-point method can utilize second-order Hessian information [29, 43], and thus the first-order methods should suffer from the lack of feasible interior points more significantly. We note that the numerical instability introduced by the lack of feasible interior points is not a specific problem in the interior-point method, but a more fundamental issue in the SDP problem itself. As our research primarily aims to identify and diagnose the interior-point vanishing problem in SDP-based DNN verification rather than directly developing a practical method, we only used the interior-point method.

### 6.3 Choice of SDP Solver

We use SDPA [52] and its high-precision version SDPA-GMP [33] with multiple-precision arithmetic. The main reason for the choice is the availability of multiple-precision arithmetic. We also tried MOSEK [2] solver, but we finally decided not to use MOSEK due to our specific needs. MOSEK has a parameter, intpntCoTolNearRel, which allows for violating the constraint at a certain level. We observed a case where the equality constraints were not satisfied to the order of 10e-6. Furthermore, MOSEK’s parameter semidefiniteTolApprox allows for violations of the semidefinite constraint, potentially permitting negative eigenvalues. In contrast, we confirmed that SDPA and SDPA-GMP strictly enforce semidefinite constraints based on their open-source implementations. Since MOSEK is closed-source, we could not diagnose these issues by ourselves, which ultimately led us to choose not to use MOSEK for this study.

### 6.4 Applicability of Facial Reduction

This study identifies the interior-point vanishing problem, describing the fact that the SDP-based DNN verification suffers from a lack of feasible interior points (i.e., strict feasibility) when the depth of the DNN increases. Meanwhile, the numerical instability caused by the lack of strict feasibility is a well-known problem in the SDP area [31, 38]. One of the most fundamental approaches to addressing the issue is facial reduction [35, 21], which aims to reduce the size of the original SDP problem, ultimately transforming it into another equivalent problem with a lower dimension where strictly feasible solutions are available. Facial reduction can be iteratively applied until a feasible interior point exists [44]. However, facial reduction techniques do not always guarantee the achievement of a problem with strict feasibility. Furthermore, applying facial reduction itself requires iteratively solving SDP problems. This procedure may even introduce another numerical instability. As facial reduction is unlikely to yield a practical level,
we did not explore it in this research. Practical facial reduction techniques specializing in the DNN verification problem structure can be a potential future research.

## 7 Conclusion

In this study, we discover a fundamental challenge in the convergence of SDP-based DNN verifiers, interior-point vanishing, and we are the first to evaluate the impact of strict feasibility on SDP-based DNN verification against the DNN models with practical depth, which is not covered by prior work. We conduct a theoretical and empirical analysis of the interior-point vanishing and find the potential root causes of the problem.
We newly designed five approaches to improve the feasibility of SDP-based verification problems and demonstrate that our methods can successfully solve 88% of the problems that could not be solved by existing methods, accounting for 41% of the total.
We further find 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 not beneficial but also even harmful to the problem’s feasibility. This work provides valuable insights into the fundamental challenges of SDP-based DNN verification, contributing to the development of more reliable and secure systems with DNNs.

## References

- [1]
Ross Anderson, Joey Huchette, Will Ma, Christian Tjandraatmadja, and Juan Pablo Vielma.
Strong Mixed-Integer Programming Formulations for Trained Neural Networks.
Mathematical Programming, 183(1):3–39, 2020.
- [2]
MOSEK ApS.
MOSEK Fusion API for Python 11.0.4, 2025.
- [3]
Dzmitry Bahdanau.
Neural Machine Translation by Jointly Learning to Align and Translate.
arXiv Preprint arXiv:1409.0473, 2014.
- [4]
Osbert Bastani, Yani Ioannou, Leonidas Lampropoulos, Dimitrios Vytiniotis, Aditya Nori, and Antonio Criminisi.
Measuring Neural Net Robustness With Constraints.
Advances in Neural Information Processing Systems, 29, 2016.
- [5]
Ben Batten, Panagiotis Kouvaros, Alessio Lomuscio, and Yang Zheng.
Efficient Neural Network Verification via Layer-Based Semidefinite Relaxations and Linear Cuts.
In Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, pages 2184–2190, 2021.
- [6]
Elena Botoeva, Panagiotis Kouvaros, Jan Kronqvist, Alessio Lomuscio, and Ruth Misener.
Efficient Verification of ReLU-Based Neural Networks via Dependency Analysis.
In Proceedings of the AAAI Conference on Artificial Intelligence, pages 3291–3299, 2020.
- [7]
Stephen Boyd, Neal Parikh, Eric Chu, Borja Peleato, Jonathan Eckstein, et al.
Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers.
Foundations and Trends® in Machine Learning, 3(1):1–122, 2011.
- [8]
Christopher Brix, Stanley Bak, Taylor T Johnson, and Haoze Wu.
The Fifth International Verification of Neural Networks Competition (VNN-COMP 2024): Summary and Results.
arXiv Preprint arXiv:2412.19985, 2024.
- [9]
Rudy R Bunel, Ilker Turkaslan, Philip Torr, Pushmeet Kohli, and Pawan K Mudigonda.
A Unified View of Piecewise Linear Neural Network Verification.
Advances in Neural Information Processing Systems, 31, 2018.
- [10]
Li Chen, Penghao Wu, Kashyap Chitta, Bernhard Jaeger, Andreas Geiger, and Hongyang Li.
End-to-End Autonomous Driving: Challenges and Frontiers.
IEEE Transactions on Pattern Analysis and Machine Intelligence, 2024.
- [11]
Chih-Hong Cheng, Georg N”uhrenberg, and Harald Ruess.
Maximum Resilience of Artificial Neural Networks.
In Automated Technology for Verification and Analysis: 15th International Symposium, ATVA 2017, Pune, India, October 3–6, 2017, Proceedings 15, pages 251–268. Springer, 2017.
- [12]
Hong-Ming Chiu and Richard Y Zhang.
Tight Certification of Adversarially Trained Neural Networks via Nonconvex Low-Rank Semidefinite Relaxations.
In International Conference on Machine Learning, pages 5631–5660. PMLR, 2023.
- [13]
Jeremy Cohen, Elan Rosenfeld, and Zico Kolter.
Certified Adversarial Robustness via Randomized Smoothing.
In Proceedings of the 36th International Conference on Machine Learning, pages 1310–1320. PMLR, 2019.
- [14]
Sumanth Dathathri, Krishnamurthy Dvijotham, Alexey Kurakin, Aditi Raghunathan, Jonathan Uesato, Rudy R Bunel, Shreya Shankar, Jacob Steinhardt, Ian Goodfellow, Percy S Liang, et al.
Enabling Certification of Verification-Agnostic Networks via Memory-Efficient Semidefinite Programming.
Advances in Neural Information Processing Systems, 33:5318–5331, 2020.
- [15]
Li Deng.
The MNIST Database of Handwritten Digit Images for Machine Learning Research.
IEEE Signal Processing Magazine, 29(6):141–142, 2012.
- [16]
Ruediger Ehlers.
Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks.
In Automated Technology for Verification and Analysis: 15th International Symposium, ATVA 2017, Pune, India, October 3–6, 2017, Proceedings 15, pages 269–286. Springer, 2017.
- [17]
Wenzhi Gao, Zhaonan Qu, Madeleine Udell, and Yinyu Ye.
Scalable Approximate Optimal Diagonal Preconditioning.
arXiv preprint arXiv:2312.15594, 2023.
- [18]
Ian J Goodfellow, Jonathon Shlens, and Christian Szegedy.
Explaining and Harnessing Adversarial Examples.
arXiv Preprint arXiv:1412.6572, 2014.
- [19]
Patrick Henriksen and Alessio Lomuscio.
Efficient Neural Network Verification via Adaptive Refinement and Adversarial Search.
In Proceedings of the 24th European Conference on Artificial Intelligence, pages 2513–2520. IOS Press, 2020.
- [20]
Roger A Horn and Charles R Johnson.
Matrix Analysis.
Cambridge University Press, Cambridge, England, 2 edition, Oct 2012.
- [21]
Hao Hu, Renata Sotirov, and Henry Wolkowicz.
Facial Reduction for Symmetry Reduced Semidefinite and Doubly Nonnegative Programs.
Mathematical Programming, 200(1):475–529, 2023.
- [22]
Xiaowei Huang, Marta Kwiatkowska, Sen Wang, and Min Wu.
Safety Verification of Deep Neural Networks.
In Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I 30, pages 3–29. Springer, 2017.
- [23]
Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel J Kochenderfer.
Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks.
In Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I 30, pages 97–117. Springer, 2017.
- [24]
Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel J Kochenderfer.
Reluplex: A Calculus for Reasoning About Deep Neural Networks.
Formal Methods in System Design, 60(1):87–116, 2022.
- [25]
Alex Krizhevsky, Ilya Sutskever, and Geoffrey E Hinton.
ImageNet Classification With Deep Convolutional Neural Networks.
Advances in Neural Information Processing Systems, 25, 2012.
- [26]
Jianglin Lan, Benedikt Brückner, and Alessio Lomuscio.
A Semidefinite Relaxation Based Branch-and-Bound Method for Tight Neural Network Verification.
In Proceedings of the AAAI Conference on Artificial Intelligence, pages 14946–14954, 2023.
- [27]
Jean Bernard Lasserre.
Moments, Positive Polynomials and Their Applications, volume 1.
World Scientific, 2009.
- [28]
Linyi Li, Tao Xie, and Bo Li.
SoK: Certified Robustness for Deep Neural Networks.
In IEEE Symposium on Security and Privacy (SP), pages 1289–1310. IEEE, 2023.
- [29]
Tianyi Lin, Shiqian Ma, Yinyu Ye, and Shuzhong Zhang.
An ADMM-Based Interior-Point Method for Large-Scale Linear Programming.
Optimization Methods and Software, 36(2-3):389–424, 2021.
- [30]
Alessio Lomuscio and Lalit Maganti.
An Approach to Reachability Analysis for Feed-Forward ReLU Neural Networks.
arXiv Preprint arXiv:1706.07351, 2017.
- [31]
Bruno F Lourenço, Masakazu Muramatsu, and Takashi Tsuchiya.
A Structural Geometrical Analysis of Weakly Infeasible SDPs.
Journal of the Operations Research Society of Japan, 59(3):241–257, 2016.
- [32]
Aleksander Madry, Aleksandar Makelov, Ludwig Schmidt, Dimitris Tsipras, and Adrian Vladu.
Towards Deep Learning Models Resistant to Adversarial Attacks.
International Conference on Learning Representations, 2018.
- [33]
Maho Nakata.
A Numerical Evaluation of Highly Accurate Multiple-Precision Arithmetic Version of Semidefinite Programming Solver: SDPA-GMP, -QD and -DD.
In IEEE International Symposium on Computer-Aided Control System Design, pages 29–34, 2010.
- [34]
Pablo A Parrilo.
Structured Semidefinite Programs and Semialgebraic Geometry Methods in Robustness and Optimization.
California Institute of Technology, 2000.
- [35]
Frank Permenter and Pablo Parrilo.
Partial Facial Reduction: Simplified, Equivalent SDPs via Approximations of the PSD Cone.
Mathematical Programming, 171:1–54, 2018.
- [36]
Aditi Raghunathan, Jacob Steinhardt, and Percy S Liang.
Semidefinite Relaxations for Certifying Robustness to Adversarial Examples.
Advances in Neural Information Processing Systems, 31, 2018.
- [37]
Hadi Salman, Greg Yang, Huan Zhang, Cho-Jui Hsieh, and Pengchuan Zhang.
A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks.
Advances in Neural Information Processing Systems, 32, 2019.
- [38]
Yoshiyuki Sekiguchi and Hayato Waki.
Perturbation Analysis of Singular Semidefinite Programs and Its Applications to Control Problems.
Journal of Optimization Theory and Applications, 188:52–72, 2021.
- [39]
Gagandeep Singh, Timon Gehr, Markus P”uschel, and Martin Vechev.
An Abstract Domain for Certifying Neural Networks.
Proceedings of the ACM on Programming Languages, 3(POPL):1–30, 2019.
- [40]
Defeng Sun, Kim-Chuan Toh, Yancheng Yuan, and Xin-Yuan Zhao.
SDPNAL+: A MATLAB Software for Semidefinite Programming With Bound Constraints (Version 1.0).
Optimization Methods and Software, 35(1):87–115, 2020.
- [41]
Christian Szegedy, Wojciech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian Goodfellow, and Rob Fergus.
Intriguing Properties of Neural Networks.
In International Conference on Learning Representations, 2014.
- [42]
Vincent Tjeng, Kai Xiao, and Russ Tedrake.
Evaluating Robustness of Neural Networks With Mixed Integer Programming.
arXiv Preprint arXiv:1711.07356, 2017.
- [43]
Stephen Tu and Jingyan Wang.
Practical First-Order Methods for Large-Scale Semidefinite Programming.
Technical Report, University of California, Berkeley, 2014.
- [44]
Hayato Waki and Masakazu Muramatsu.
Facial Reduction Algorithms for Conic Optimization Problems.
Journal of Optimization Theory and Applications, 158:188–215, 2013.
- [45]
Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana.
Efficient Formal Safety Analysis of Neural Networks.
Advances in Neural Information Processing Systems, 31, 2018.
- [46]
Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter.
Beta-CROWN: Efficient Bound Propagation With Per-Neuron Split Constraints for Neural Network Robustness Verification.
Advances in Neural Information Processing Systems, 34:29909–29921, 2021.
- [47]
Lily Weng, Huan Zhang, Hongge Chen, Zhao Song, Cho-Jui Hsieh, Luca Daniel, Duane Boning, and Inderjit Dhillon.
Towards Fast Computation of Certified Robustness for ReLU Networks.
In International Conference on Machine Learning, pages 5276–5285. PMLR, 2018.
- [48]
Eric Wong and Zico Kolter.
Provable Defenses Against Adversarial Examples via the Convex Outer Adversarial Polytope.
In International Conference on Machine Learning, pages 5286–5295. PMLR, 2018.
- [49]
Stephen J Wright.
Numerical Optimization, 2006.
- [50]
Han Xiao, Kashif Rasul, and Roland Vollgraf.
Fashion-MNIST: A Novel Image Dataset for Benchmarking Machine Learning Algorithms.
arXiv Preprint arXiv:1708.07747, 2017.
- [51]
Kaidi Xu, Huan Zhang, Shiqi Wang, Yihan Wang, Suman Jana, Xue Lin, and Cho-Jui Hsieh.
Fast and Complete: Enabling Complete Neural Network Verification With Rapid and Massively Parallel Incomplete Verifiers.
International Conference on Learning Representations, 2022.
- [52]
Makoto Yamashita, Katsuki Fujisawa, Mituhiro Fukuda, Kazuhiro Kobayashi, Kazuhide Nakata, and Maho Nakata.
Latest Developments in the SDPA Family for Solving Large-Scale SDPs.
Handbook on Semidefinite, Conic and Polynomial Optimization, pages 687–713, 2012.
- [53]
Makoto Yamashita, Katsuki Fujisawa, Kazuhide Nakata, Maho Nakata, Mituhiro Fukuda, Kazuhiro Kobayashi, and Kazushige Goto.
A High-Performance Software Package for Semidefinite Programs: SDPA 7.
Handbook on Semidefinite, Conic and Polynomial Optimization, 2010.
- [54]
Matthew D Zeiler.
ADADELTA: an Adaptive Learning Rate Method.
arXiv preprint arXiv:1212.5701, 2012.
- [55]
Duo Zhou, Christopher Brix, Grani A Hanasusanto, and Huan Zhang.
Scalable Neural Network Verification With Branch-and-Bound Inferred Cutting Planes.
Advances in Neural Information Processing Systems, 2024.

## Appendix

## Appendix A Detailed Proofs

### A.1 Proof of Proposition 3.2

###### Proof.

Let $(\bm{X}^{*},\lambda^{*})$ be an optimal solution to the problem ([7](https://arxiv.org/html/2506.10269v1#S3.E7)).
Suppose that $\lambda^{*}>0$, we have $\bm{X}^{*}+\lambda^{*}\bm{I}\succ\bm{O}$.
Also, $\bm{X}^{*}+\lambda^{*}\bm{I}$ is a feasible solution to the problem ([6](https://arxiv.org/html/2506.10269v1#S3.E6)), which means the original problem is strictly feasible.

On the other hand, suppose that the original problem has a strictly feasible solution $\bm{X}^{\prime}\succ\bm{O}$.
Since $\bm{X}^{\prime}\succ\bm{O}$, we have $\bar{\lambda}=\lambda_{\min}(\bm{X}^{\prime})>0$.
By construction, $\bar{\bm{X}}=\bm{X}^{\prime}-\bar{\lambda}\bm{I}\succeq\bm{O}$ since all eigenvalues of $\bar{\bm{X}}$ remain nonnegative.
Then, since we have $\mathrm{tr}\left\lparen\bm{A}_{j}\lparen\bar{\bm{X}}+\bar{\lambda}\bm{I}
\rparen\right\rparen=\mathrm{tr}\left\lparen\bm{A}_{j}\bm{X}^{\prime}\right
\rparen=b_{j}~{}(j=1,\dots,m)$ and $\bar{\bm{X}}\succeq\bm{O}$,
$\lparen\bar{\bm{X}},\bar{\lambda}\rparen$ is a feasible solution to the problem ([7](https://arxiv.org/html/2506.10269v1#S3.E7)), and its objective value is $\lambda_{\min}\lparen\bm{X}^{\prime}\rparen>0$.
Thus, we see that the optimal value of the problem ([7](https://arxiv.org/html/2506.10269v1#S3.E7)) is positive, which completes the proof.
∎

###### Proof.

### A.2 Proof of Lemma 3.4

###### Proof.

We prove this by induction for $i\in[L]$.
Let us consider the initial case $i=0$.
Since $\bm{P}\succeq\bm{O}$, we have

$$ $\begin{pmatrix}1&\bm{P}[\bm{x}_{0}^{\top}]\\ \bm{P}[\bm{x}_{0}]&\bm{P}[\bm{x}_{0}\bm{x}_{0}^{\top}]\end{pmatrix}\succeq\bm{ O},$ $$

which implies

$$ $\lVert\bm{P}[\bm{x}_{0}]\rVert^{2}_{2}\leq\mathrm{tr}\left\lparen\bm{P}[\bm{x} _{0}\bm{x}_{0}^{\top}]\right\rparen.$ $$

Recalling $\bm{l}_{0}=\bar{\bm{x}}-\varepsilon\bm{1}$ and $\bm{u}_{0}=\bar{\bm{x}}+\varepsilon\bm{1}$, from the constraint ([5e](https://arxiv.org/html/2506.10269v1#S2.E5.5)), we have

$$ $\displaystyle\mathrm{tr}\left\lparen\bm{P}[\bm{x}_{0}\bm{x}_{0}^{\top}]\right\rparen$ $\displaystyle=\lparen\bm{l}_{0}+\bm{u}_{0}\rparen^{\top}\bm{P}[\bm{x}_{0}]-\bm {l}_{0}^{\top}\bm{u}_{0}$ $\displaystyle\leq 2\lVert\bar{\bm{x}}\rVert_{2}\lVert\bm{P}[\bm{x}_{0}]\rVert_ {2}-\lVert\bar{\bm{x}}\rVert_{2}^{2}+\varepsilon^{2}\cdot n_{0}$ $\displaystyle\leq 2\lVert\bar{\bm{x}}\rVert_{2}\sqrt{\mathrm{tr}\left\lparen \bm{P}[\bm{x}_{0}\bm{x}_{0}^{\top}]\right\rparen}-\lVert\bar{\bm{x}}\rVert_{2} ^{2}+\varepsilon^{2}\cdot n_{0}.$ $$

Rearranging the above inequality gives

$$ $\left\lparen\sqrt{\mathrm{tr}\left\lparen\bm{P}[\bm{x}_{0}\bm{x}_{0}^{\top}] \right\rparen}-\lVert\bar{\bm{x}}\rVert_{2}\right\rparen^{2}\leq\varepsilon^{2 }\cdot n_{0}.$ $$

Thus, by taking the square root of both sides, we obtain

$$ $\mathrm{tr}\left\lparen\bm{P}[\bm{x}_{0}\bm{x}_{0}^{\top}]\right\rparen\leq \lparen\lVert\bar{\bm{x}}\rVert_{2}+\varepsilon\sqrt{n_{0}}\rparen^{2}=T_{0},$ $$

which ensures that [Eq. 8](https://arxiv.org/html/2506.10269v1#S3.E8) holds for $i=0$.

Next, let $i\in[L-1]$, and assuming that [Eq. 8](https://arxiv.org/html/2506.10269v1#S3.E8) holds for all indices up to and including $i$, we show that it also holds for $i+1$.
Let $\bm{P}\succeq\bm{O}$ be any feasible solution for the problem ([5](https://arxiv.org/html/2506.10269v1#S2.E5)).
Then, the following $3\times 3$ principal submatrix is positive semidefinite:

$$ $\begin{pmatrix}1&\bm{P}[\bm{x}_{i}^{\top}]&\bm{P}[\bm{x}_{i+1}^{\top}]\\ \bm{P}[\bm{x}_{i}]&\bm{P}[\bm{x}_{i}\bm{x}_{i}^{\top}]&\bm{P}[\bm{x}_{i}\bm{x} _{i+1}^{\top}]\\ \bm{P}[\bm{x}_{i+1}]&\bm{P}[\bm{x}_{i+1}\bm{x}_{i}^{\top}]&\bm{P}[\bm{x}_{i+1} \bm{x}_{i+1}^{\top}]\end{pmatrix}\succeq\bm{O}.$ (9) $$

From the induction hypothesis, we have $\mathrm{tr}\left\lparen\bm{P}[\bm{x}_{i}\bm{x}_{i}^{\top}]\right\rparen\leq T_
{i}$, which implies $\lambda_{\max}\lparen\bm{P}[\bm{x}_{i}\bm{x}_{i}^{\top}]\rparen\leq T_{i}$.
Thus, by replacing the first $2\times 2$ principal submatrix in the left-hand side of ([9](https://arxiv.org/html/2506.10269v1#A1.E9)) with $\lparen 1+T_{i}\rparen\bm{I}$, we obtain

$$ $\left\lparen\begin{array}[]{cc|c}&&\bm{P}[\bm{x}_{i+1}^{\top}]\\ \lx@intercol\hfil\smash{\raisebox{6.0pt}{$(1+T_{i})\bm{I}$}}\hfil\lx@intercol \vrule\lx@intercol&\bm{P}[\bm{x}_{i}\bm{x}_{i+1}^{\top}]\\ \hline\cr\bm{P}[\bm{x}_{i+1}]&\bm{P}[\bm{x}_{i+1}\bm{x}_{i}^{\top}]&\bm{P}[\bm {x}_{i+1}\bm{x}_{i+1}^{\top}]\end{array}\right\rparen\succeq\bm{O}.$ (10) $$

Let us define the concatenated matrix as

$$ $\bm{\widetilde{P}}_{i+1}=\begin{pmatrix}\bm{P}[\bm{x}_{i+1}^{\top}]\\ \bm{P}[\bm{x}_{i}\bm{x}_{i+1}^{\top}]\end{pmatrix}.$ $$

By taking the Schur complement of $\lparen 1+T_{i}\rparen\bm{I}$ of the left-hand side in [Eq. 10](https://arxiv.org/html/2506.10269v1#A1.E10), we have

$$ $\bm{P}[\bm{x}_{i+1}\bm{x}_{i+1}^{\top}]-\frac{1}{1+T_{i}}\bm{\widetilde{P}}_{i +1}\bm{\widetilde{P}}_{i+1}^{\top}\succeq\bm{O},$ $$

which implies

$$ $\mathrm{tr}\left\lparen\bm{P}[\bm{x}_{i+1}\bm{x}_{i+1}^{\top}]\right\rparen \geq\frac{1}{1+T_{i}}\lVert\bm{\widetilde{P}}_{i+1}\rVert_{F}^{2}.$ (11) $$

On the other hand, from the constraint ([5d](https://arxiv.org/html/2506.10269v1#S2.E5.4)) and the definitions of $\bm{\widetilde{P}}_{i+1}$ and $\bm{\widetilde{W}}_{i}$, we have

$$ $\displaystyle\mathrm{tr}\left\lparen\bm{P}[\bm{x}_{i+1}\bm{x}_{i+1}^{\top}]\right\rparen$ $\displaystyle=\mathrm{tr}\left\lparen\bm{\widetilde{W}}_{i}\bm{\widetilde{P}}_ {i+1}\right\rparen$ $\displaystyle\leq\lVert\bm{\widetilde{W}}_{i}\rVert_{F}\lVert\bm{\widetilde{P} }_{i+1}\rVert_{F}.$ (12) $$

Combining ([11](https://arxiv.org/html/2506.10269v1#A1.E11)) and ([12](https://arxiv.org/html/2506.10269v1#A1.E12)), we derive

$$ $\lVert\bm{\widetilde{P}}_{i+1}\rVert_{F}\leq(1+T_{i})\lVert\bm{\widetilde{W}}_ {i}\rVert_{F},$ $$

which leads to

$$ $\mathrm{tr}\left\lparen\bm{P}[\bm{x}_{i+1}\bm{x}_{i+1}^{\top}]\right\rparen \leq(1+T_{i})\lVert\bm{\widetilde{W}}_{i}\rVert_{F}^{2},$ $$

which ensures that [Eq. 8](https://arxiv.org/html/2506.10269v1#S3.E8) holds for $i+1$ and completes the proof.
∎

###### Proof.

## Appendix B Conversion Proposition 3.2 into Standard SDP Form

We introduce nonnegative variables $\lambda_{1},\lambda_{2}\geq 0$ and decompose

$$ $\lambda\;=\;\lambda_{1}\;-\;\lambda_{2}.$ $$

Using this decomposition, the objective function becomes one of maximizing
$\lambda_{1}-\lambda_{2}$. We then gather the variable matrices into the following block-diagonal matrix:

$$ $\widetilde{\bm{X}}\;=\;\begin{pmatrix}\bm{X}&0&0\\ 0&\lambda_{1}&0\\ 0&0&\lambda_{2}\end{pmatrix}\quad(\widetilde{\bm{X}}\succeq\bm{O}),$ $$

thereby simultaneously representing
$\bm{X}\succeq\bm{O},\ \lambda_{1}\geq 0,\ \lambda_{2}\geq 0.$

Next, to express the objective function $\lambda_{1}-\lambda_{2}$, we can define the matrix
$\widetilde{\bm{C}}$ as follows:

$$ $\widetilde{\bm{C}}\;=\;\begin{pmatrix}0&0&0\\ 0&1&0\\ 0&0&-1\end{pmatrix}\quad\Longrightarrow\quad\mathrm{tr}\left\lparen\widetilde{ \bm{C}}\widetilde{\bm{X}}\right\rparen\;=\;\lambda_{1}\;-\;\lambda_{2}.$ $$

Meanwhile, each constraint

$$ $\mathrm{tr}\left\lparen\bm{A}_{j}\cdot\lparen\bm{X}+\lparen\lambda_{1}-\lambda _{2}\rparen\bm{I}\rparen\right\rparen\;=\;b_{j}$ $$

can be written as

$$ $\mathrm{tr}\left\lparen\bm{A}_{j}\bm{X}\right\rparen\;+\;\lparen\lambda_{1}- \lambda_{2}\rparen\,\mathrm{tr}\left\lparen\bm{A}_{j}\bm{I}\right\rparen\;=\;b _{j},$ $$

where $\lparen\bm{A}_{j}\bm{I}\rparen=\mathrm{tr}\left\lparen\bm{A}_{j}\right\rparen$ is a constant.
Defining

$$ $\widetilde{\bm{A}}_{j}=\begin{pmatrix}\bm{A}_{j}&0&0\\ 0&\mathrm{tr}\left\lparen\bm{A}_{j}\right\rparen&0\\ 0&0&-\,\mathrm{tr}\left\lparen\bm{A}_{j}\right\rparen\end{pmatrix}\quad \Longrightarrow\quad\mathrm{tr}\left\lparen\widetilde{\bm{A}}_{j}\widetilde{ \bm{X}}\right\rparen=b_{j},$ $$

we see that the original problem can be rewritten in the standard SDP form with
the matrix variable $\widetilde{\bm{X}}\succeq\bm{O}$, as

$$ $\displaystyle\max_{\widetilde{\bm{X}}}\quad$ $\displaystyle\mathrm{tr}\left\lparen\widetilde{\bm{C}}\widetilde{\bm{X}}\right\rparen\quad$ s.t. $\displaystyle\mathrm{tr}\left\lparen\widetilde{\bm{A}}_{j}\widetilde{\bm{X}} \right\rparen=b_{j},\quad\lparen j=1,\dots,m\rparen,$ $\displaystyle\widetilde{\bm{X}}\succeq\bm{O}.$ $$

**Table 3: Average of the optimal values across the solved instances for the different layer sizes for Problem A and B.**
| $L$ | Problem A | Problem B |
| --- | --- | --- |
| 2 | 7.17$\pm$7.24E-05 | 4.93$\pm$1.13E-05 |
| 4 | 5.53$\pm$5.31E-06 | 3.86$\pm$1.26E-06 |
| 6 | 1.55$\pm$1.57E-07 | 1.92$\pm$7.52E-07 |
| 8 | 3.75$\pm$3.69E-09 | 1.56$\pm$1.12E-08 |
| 10 | 9.93$\pm$8.48E-11 | 8.55$\pm$9.09E-10 |
| 12 | 8.88$\pm$6.14E-13 | $-$4.05$\pm$3.53E-10 |
| 16 | 6.38$\pm$7.81E-16 | $-$1.07$\pm$0.73E-09 |

## Appendix C Empirical Analysis of Constraint Impacts on the Interior-Point Vanishing

To identify the constraints causing the interior-point-vanishing problem, we just directly relaxed the MEM problem ([7](https://arxiv.org/html/2506.10269v1#S3.E7)) by removing each constraint.
We consider the following two problems:

##### Problem A: Removal of equality constraints related to ReLU

$$ $\displaystyle\min_{\bm{P}}$ $\displaystyle\quad\bm{c}^{\top}\bm{P}[\bm{x}_{L}]+c_{0}$ s.t. $\displaystyle\quad\bm{P}[\bm{x}_{i+1}]\geq\bm{0}$ $\displaystyle\quad\lparen i\in[L]\rparen,$ $\displaystyle\quad\bm{P}[\bm{x}_{i+1}]\geq\bm{W}_{i}\bm{P}[\bm{x}_{i}]+\bm{b}_ {i}$ $\displaystyle\quad\lparen i\in[L]\rparen,$ $\displaystyle\quad\mathrm{diag}\left\lparen\bm{P}[\bm{x}_{i}\bm{x}_{i}^{\top}] \right\rparen-\lparen\bm{l}_{i}+\bm{u}_{i}\rparen\odot\bm{P}[\bm{x}_{i}]+\bm{l }_{i}\odot\bm{u}_{i}\leq\bm{0}$ $\displaystyle\quad\lparen i\in[L]\rparen,$ $\displaystyle\quad\bm{P}[1]=1,~{}\bm{P}\succeq\bm{O}.$ $$

##### Problem B: Applying upper and lower bound constraints only to the input layer

$$ $\displaystyle\min_{\bm{P}}$ $\displaystyle\quad\bm{c}^{\top}\bm{P}[\bm{x}_{L}]+c_{0}$ s.t. $\displaystyle\quad\bm{P}[\bm{x}_{i+1}]\geq\bm{0}$ $\displaystyle\quad\lparen i\in[L]\rparen,$ $\displaystyle\quad\bm{P}[\bm{x}_{i+1}]\geq\bm{W}_{i}\bm{P}[\bm{x}_{i}]+\bm{b}_ {i}$ $\displaystyle\quad\lparen i\in[L]\rparen,$ $\displaystyle\quad\mathrm{diag}\left\lparen\bm{P}[\bm{x}_{i+1}\bm{x}_{i+1}^{ \top}]-\bm{W}_{i}\bm{P}[\bm{x}_{i}\bm{x}_{i+1}^{\top}]\right\rparen-\bm{b}_{i} \odot\bm{P}[\bm{x}_{i+1}]=\bm{0}$ $\displaystyle\quad\lparen i\in[L]\rparen,$ $\displaystyle\quad\mathrm{diag}\left\lparen\bm{P}[\bm{x}_{0}\bm{x}_{0}^{\top}] \right\rparen-\lparen\bm{l}_{0}+\bm{u}_{0}\rparen\odot\bm{P}[\bm{x}_{0}]+\bm{l }_{0}\odot\bm{u}_{0}\leq\bm{0},$ $\displaystyle\quad\bm{P}[1]=1,~{}\bm{P}\succeq\bm{O}.$ $$

###### Proposition C.1 .

The feasible region of Problem A is bounded.

###### Proof.

As in the proof of [Lemma 3.4](https://arxiv.org/html/2506.10269v1#S3.Thmtheorem4), for each $i\in[L]$, we have

$$ $\mathrm{tr}\left\lparen\bm{P}[\bm{x}_{i}\bm{x}_{i}^{\top}]\right\rparen\leq \lVert\bm{l}_{i}+\bm{u}_{i}\rVert_{2}\sqrt{\mathrm{tr}\left\lparen P[\bm{x}_{i }\bm{x}_{i}^{\top}]\right\rparen}-\bm{l}_{i}^{\top}\bm{u}_{i},$ $$

which implies

$$ $\mathrm{tr}\left\lparen\bm{P}[\bm{x}_{i}\bm{x}_{i}^{\top}]\right\rparen\leq \frac{\lVert\bm{u}_{i}\rVert^{2}+\lVert\bm{l}_{i}\rVert^{2}}{2}\quad(i\in[L]).$ $$

Thus, for any feasible solution $\bm{P}\succeq\bm{O}$ to Problem A, we have

$$ $\displaystyle\lambda_{\max}\lparen\bm{P}\rparen$ $\displaystyle\leq\mathrm{tr}\left\lparen\bm{P}\right\rparen\leq\frac{1}{2}\sum _{i\in[L]}\lparen\lVert\bm{u}_{i}\rVert^{2}+\lVert\bm{l}_{i}\rVert^{2}\rparen,$ $$

which ensures that the feasible region of Problem A is bounded.
∎

###### Proposition C.2 .

The feasible region of Problem B is bounded.

###### Proof.

Since the proof of [Lemma 3.4](https://arxiv.org/html/2506.10269v1#S3.Thmtheorem4) only relies on $\bm{l}_{0}$ and $\bm{u}_{0}$, and
$\bm{l}_{i}$ and $\bm{u}_{i}$ for $i\geq 1$ are not used, [Eq. 8](https://arxiv.org/html/2506.10269v1#S3.E8) also holds for feasible solutions to Problem B.
Thus, we have that any feasible solution $\bm{P}\succeq\bm{O}$ to Problem B satisfies

$$ $\displaystyle\lambda_{\max}\lparen\bm{P}\rparen$ $\displaystyle\leq\mathrm{tr}\left\lparen\bm{P}\right\rparen\leq\sum_{i\in[L]}T _{i},$ $$

which completes the proof.
∎

We check the strict feasibility of the instances of Problems A and B
by solving the associated problems ([7](https://arxiv.org/html/2506.10269v1#S3.E7)).
We use the same experimental setup as in [Section 3.2](https://arxiv.org/html/2506.10269v1#S3.SS2).
[Table 3](https://arxiv.org/html/2506.10269v1#A2.T3) lists the average of the optimal values across the solved instances (*Avg. Obj.*). As shown, for Problem A, the optimal values were always small regardless of the number of layers.
For Problem B, while the average of their optimal values tended to decrease as the number of layers increased, their values were larger than those of Problem A, especially for $L=8,10$.
The results suggest that when a primal-dual gap occurs, relaxation of the upper bound $\bm{u}_{i}$ or relaxation of the ReLU equality constraint ([5d](https://arxiv.org/html/2506.10269v1#S2.E5.4)) may be effective.

###### Proposition C.1 .

###### Proof.

###### Proposition C.2 .

###### Proof.

## Appendix D Validation on Networks from Prior Works

We conduct experiments to demonstrate that the interior-point vanishing problem also occurs in DNN models commonly used in prior neural network verification research.

Experimental Setup:
We evaluated four networks from prior works [37, 12], ranging from 2-layer to 9-layer architectures with 100 neurons per layer. These networks include models trained with different robustification techniques: LPD-MNIST trained using dual formulation training, NOR-MNIST with standard training without robustification, ADV-MNIST as an adversarially trained network, and mnist_MLP_9_100_ADV as a deep adversarially trained network with 9 layers. We applied the same experimental methodology as described in [Section 3.2](https://arxiv.org/html/2506.10269v1#S3.SS2), solving the strict feasibility verification problem ([5](https://arxiv.org/html/2506.10269v1#S2.E5)) for each model. Due to computational constraints with larger networks, we employed the standard SDPA solver rather than SDPA-GMP (multi-precision arithmetic). For each network, we solved a single verification instance to assess the presence of interior-point vanishing.

Results:
The results in [Table 4](https://arxiv.org/html/2506.10269v1#A4.T4) demonstrate that interior-point vanishing occurs across networks used in prior verification research. All tested networks exhibit minimum eigenvalues at or near zero, indicating loss of strict feasibility regardless of the training methodology employed. This universal occurrence suggests that the phenomenon affects networks trained with different robustification techniques, including dual formulation and adversarial training, as well as standard training, indicating it is an inherent property of the SDP relaxation rather than a training artifact.
The interior-point vanishing problem becomes more severe with increased network depth, as evidenced by the 9-layer network showing a more negative minimum eigenvalue ($-1.80\times 10^{-4}$) compared to the 2-layer networks. This observation confirms our theoretical analysis that deeper networks exacerbate interior-point vanishing.

**Table 4: Interior-point vanishing in networks from prior verification works**
| Model | # Layers | # Neurons/Layer | Training Method | Objective |
| --- | --- | --- | --- | --- |
| LPD-MNIST [37, 12] | 2 | 100 | Dual formulation | $1.14\times 10^{-4}$ |
| NOR-MNIST [37, 12] | 2 | 100 | - | $5.29\times 10^{-5}$ |
| ADV-MNIST [37, 12] | 2 | 100 | Adversarial Training | $-1.26\times 10^{-5}$ |
| mnist_MLP_9_100_ADV [37] | 9 | 100 | Adversarial Training | $-1.80\times 10^{-4}$ |

## Peer Reviews

confidence: 4
contribution: 3
initial_rating: 6
presentation: 3
questions: 1. Your analysis is specific to ReLU networks. Do you believe the interior-point vanishing problem is an issue for SDP relaxations of networks with other activation functions (e.g., sigmoid, tanh)? Would your solutions, particularly $\varepsilon$-SDP and LeakySDP, be easily adaptable?
2. For networks with more layers, do $\varepsilon$-SDP and B-Remove still maintain feasibility? If not, is there a threshold beyond which interior-point vanishing reoccurs, and can you theoretically predict this threshold?
soundness: 3
strengths: - The paper is the first to define and analyze interior-point vanishing in DNN verification, moving beyond incremental improvements to address a foundational limitation. The theoretical link between inactive neurons/weight norms and SDP feasibility is novel and rigorously proven.
- The use of high-precision solvers (SDPA-GMP), controlled depth experiments, and benchmark network validation ensures results are reliable and generalizable. The 88% success rate on unsolvable instances is a concrete, impactful outcome.
- The methods are lightweight and compatible with existing SDP solvers (SDPA, SDPA-GMP), requiring no specialized hardware. B-Remove, in particular, is easy to implement (removing constraints) and delivers significant gains.
- The evaluation is holistic, diagnosing the problem and evaluating solutions on both feasibility and quality metrics.
summary: This paper addresses a critical limitation of semidefinite programming (SDP) relaxation, which is a state-of-the-art convex relaxation method for verifying deep neural networks (DNNs) with ReLU activations, by identifying and resolving the interior-point vanishing problem. SDP relaxation is widely recognized for providing tighter bounds than other convex methods (e.g., linear programming) in DNN verification, but its scalability to deep networks has remained elusive, traditionally attributed to high computational cost.

In my view, there are four core contributions:
1. The paper rigorously demonstrates that as network depth increases, the SDP's feasible set likely lacks interior points, rendering standard interior-point methods numerically unstable and often failing to converge.
2. The paper offers both theoretical proofs and extensive empirical evidence using high-precision solvers to validate the phenomenon's prevalence. They trace interior-point vanishing to two root causes: (a) unidentifiable inactive neurons forcing diagonal entries of the SDP matrix to zero, and b. small row norms of the extended weight matrix constraining the SDP matrix’s minimum eigenvalue to near zero.
3. The paper proposes five distinct methods to restore strict feasibility: (a) $\varepsilon$-SDP (tolerating small violations of ReLU equality constraints), (b) LeakySDP (replacing ReLU with Leaky ReLU), (c) B-Remove (removing unnecessary intermediate-layer bound constraints), (d) D-Scale (diagonal scaling to improve numerical conditioning), and (e) W-Scale (weight scaling to enlarge small row norms).

The paper still falls short in terms of scalability. However, such a limitation is inherent to the verification tasks for neural networks.
weaknesses: - The paper only evaluates fully connected ReLU networks. Convolutional Neural Networks or transformers have distinct weight structures that may alter interior-point vanishing dynamics. Extending validation to CNNs would strengthen generalizability.
- The paper’s maximum depth is 16 layers. For modern deep networks, it remains unclear if the proposed methods (especially $\varepsilon$-SDP and B-Remove) can maintain feasibility. Evaluating 20–30-layer networks would better assess scalability.
- LeakySDP, D-Scale, and W-Scale show minimal gains but lack detailed failure analysis. For example, why does LeakySDP underperform?

---

confidence: 5
contribution: 1
initial_rating: 2
presentation: 2
questions: - Rather than showing the average objective and the percentage of solved problems (for instance, in Table 1), I think it would be more informative to report the share of problems for which the objective was negative (i.e., strict feasibility was lacking).
- When you evaluate robustly-trained networks from previous work, the average objective is not negative for all networks. Why do you claim that this "consistently" shows interior-point vanishing?
- I am a bit confused by the claim that inactive neurons will lead to interior-point vanishing. It seems to me that for this to happen, $u_i$, which is a known pre-computed pre-activation bound, should be non-positive. But if this is the case, then such inactive neuron can and should be removed, as you also state. You elaborate that some neurons may be inactive but the loose pre-activation bounds may not spot it. But isn't the lack of strict feasibility linked to the employed numerical $u_i$ value, rather than the "true" inactivity?
soundness: 2
strengths: The main strength of the work is its novelty: the problem of strict feasibility was not identified before in the SDP-based neural network verification literature. The authors also propose a simple solution (B-remove) that successfully addresses the problem without any significant gap in optimal objective value.
summary: The submission identifies a problem within SDP-based algorithms for incomplete neural network verification.
Specifically, the lack of strict feasibility, which the authors call "interior-point vanishing", which prevents some SDP solvers (based on primal-dual interior-point methods) from converging to the optimal solution, and causes numerical instabilities in the others.
The authors first demonstrate that the strict feasibility does not hold on a series of networks, then propose a series of remedies, whose efficacy is empirically investigates on small toy networks.
weaknesses: The main weakness of the work lies in the specificity of its subject and on its potential impact. Indeed, the experiments only focus on the impact of strict feasibility in isolation, without ever considering whether this is any useful in practice towards obtaining an effective neural network verifier. Given the venue, this alone places the work markedly below the acceptance threshold, I believe.

More in detail:
- Some of the motivational text makes exaggerated claims. Lines 67-68: *The interior-point vanishing could be the actual reason hindering the development of the SDP-based approach in this area*. The main reason is their lack of scalability. By the time an SDP solver returns a bound, branch-and-bound based on LP relaxations will have returned a significantly tighter one. 
- In order to show the impact of the method, the authors should show that, once the strict feasibility problem is fixed, SDP-based branch-and-bound attains significantly better trade-offs between the accuracy of the bounds and the time to compute them. This is virtually the only metric in the area.
- The authors exclude first-order methods from their study because they cannot check optimality. However, given the claim that strict feasibility is important there too because of numerical stability, it is extremely important to check whether this has any practical impact.
- I think it would be quite important to evaluate the impact of the mitigation strategies on networks from previous works too (currently, those experiments are only carried out on networks trained by the authors, which are much narrower and much deeper than those used in the literature).

---

confidence: 3
contribution: 3
initial_rating: 4
presentation: 2
questions: ## Questions

1. In line 317, shouldn't you use  $(\textbf{P}[x_ix_i^\top])_{jj}$?
2. Is it reasonable to use W-Scale approach if the smallest norm is close to zero? Wouldn't dividing by $\check{w}_i$ induce more instability?
3. Your approach demonstrates that bound constraints are sometimes harmful for deeper networks? Is it true for all types of redundant constraints which are commonly used to increase tightness of SDP relaxations?
4. You only presented results with $\epsilon=\alpha=0.01$. What is the sensitivity of the interior-point vanishing with respect to $\epsilon$ and $\alpha$?
5. At fixed depth, do you observe similar results for different network widths?
soundness: 2
strengths: The paper studies a relevant question from a novel perspective, namely strict feasibility as the real cause of SDP verification failures. It offers practical and simple fixes that restore solver stability at depth with modest loss in tightness. It also clarifies which constraints actually harm feasibility.
summary: The paper studies why SDP-based verifiers for ReLU networks often lose strict feasibility (no interior point) as depth increases. It formalizes a simple diagnostic feasibility problem, analyzes structural causes (inactive neurons,  tiny per-row weight norms), and evaluates five practical strategies for alleviating this issue: $\epsilon$-SDP (soften ReLU equalities), LeakySDP, diagonal scaling (D-Scale), weight scaling (W-Scale), and removing intermediate bound constraints (B-Remove). Experiments over 50 instances per setting (10 inputs × 5 training seeds) show strict-feasibility margins shrink with depth, but $\epsilon$-SDP and especially B-Remove substantially improve solver success with modest loss in tightness.
weaknesses: The writing and presentation require substantial revision. While the experiments illustrate interior-point vanishing, they do not clearly demonstrate that the proposed fixes translate into more verified instances in practice. The theoretical analysis would be more impactful if some insights were included on, for example, how to train neural networks in a way that mitigates the vanishing problem and thereby facilitates SDP verification subsequently.

### Major points

- Writing is informal or imprecise (draft style) at times, with many typos. Some examples include: line 067 (using *actual*), line 101 (problem is *true*), line 117 (boundary propagation method..), line 234 (that SDPA-GMP successfully terminated its computation), line 963 (more negative eigenvalue), line 311 (Appendix 3.4), line 397-399, line 407 (which typically help higher converging), line 356 (when $x>0$), line 471-473, etc. Many repetitions are present. For example: repeating *we first introduce*, then Proposition 3.1 (that misses some connection words), just repeats the sentence above, etc. Figures and tables are not well placed, making the reading difficult, e.g., Figure 1 is referenced almost 2 pages after being introduced, Table 3 is misplaced, etc.

- The experimental section is limited: while it illustrates the phenomenon, the comparisons are not exhaustive. In particular, no baselines that tighten SDP bounds via linear reformulations and quadratic constraints, or compute SDP-based upper bounds on Lipschitz constants, are included. Several experiments are also "underpowered"; for example, Table~4 draws conclusions from a single verification instance (one image).

### Minor points

- Why is problem (7) referred to as *MEM* on Line 785?
- Line 851 - you meant associated problem (7) for each model?
- Notation $a\pm b \operatorname{E}-k$ could be clarified to avoid ambiguity, i.e, whether the exponent applies to both $a$ and $b$ or $b$ only.
- Clarify whether success rate (Table 2) means that vanishing problem is solved or whether the instance robustness was verified.

---

confidence: 4
contribution: 2
initial_rating: 4
presentation: 3
questions: - Could the authors provide verification times and success rates for their experiments?
- Could the authors comment on the scalability of their methods?
soundness: 3
strengths: - The identification of the issue of interior-point vanishing in SDP-based neural network verification is a novel and relevant contribution to SDP-based verification. As far as I'm aware, this is the first time this problem is identified.
- The authors propose multiple approaches for eliminating the interior-point vanishing problem. The experimental evaluation shows that they are effective at alleviating the problem and enable a higher number of verification queries to be solved in the majority of cases.
- The theoretical analysis in the problem seems sound and effectively supports the authors' argumentation
summary: This work analyses issues that arise when Neural Network Verification problems are solved with the help of Semidefinite Programming solvers based on interior point methods. The effectiveness of the off-the-shelf interior point solvers that are used in SDP-based verification relies on Slater's condition, but the authors find that the condition may not actually hold for neural network verification problems. When this occurs, it leads to various numerical issues for the solvers. As a consequence, the duality gap at optimality may be nonzero which would also be an issue for other (non-interior-point) solvers. The work identifies the constraints which are responsible for the interior point vanishing and the authors suggest a number of different ways of dealing with the issue. The methods put forward by the authors are backed by a theoretical underpinning but are also empirically evaluated through benchmarks which compare previously introduced SDP-based verifiers to the methods proposed by the authors. These experiments demonstrate that the proposed methods effectively resolve the issues.
weaknesses: - In Appendix E the authors explain why they do not consider first-order methods in their analysis. While I do understand the issues that are mentioned, I would still argue that not being able to analyse whether the interior-point vanishing problem affects the faster first-order methods which often outperform interior-point solvers is a weakness of the work. The authors' argumentation sidesteps the most critical question of whether interior-point vanishing actually matters to the state-of-the-art first-order method solvers. The paper claims that the problem would be "even more severe" for those but provides no evidence to support these claims.
- The evaluation in the paper is based on the "success rate", i.e. whether the solver converged, and the objective gaps. However, the paper completely omits other metrics which are normally reported by neural network verification papers. The goal of verification is to either prove or disprove a robustness property at hand as quickly as possible. Besides analysing the convergence of the algorithm, the authors should therefore also compare
  - the time required to solve the verification problems. This would enable an assessment of whether the different methods put forward by the authors make the problems more computationally expensive to solve. It would also make it possible to assess the scaling of the algorithms as the network depth grows.
  - the success rate of the different verification methods. The authors analyse the objective value gaps in Figure 2, but it would be helpful to see the impacts of the gaps on the verification success rate.
- The analysis focuses too much on the convergence of the algorithms rather than the success rate of verification. Even if a solver does not converge, it might be able to provide a dual bound that is sufficient for proving the robustness of a given sample (and the failure to converge would therefore not matter). This should be discussed in the paper and additional metrics (such as the success rate mentioned above) should be reported to assess the relevance of this point.
- There is no comparison of the methods proposed by the authors with other state-of-the-art neural network verification tools. Besides this, the networks that the authors conduct their experiments on are small toy networks and do not conduct any experiments on popular benchmarks such as those from recent Verification of Neural Networks (VNNCOMP) competitions. This makes it difficult to assess the relevance of the work for verifying neural networks in practice which would normally be much larger than those evaluated by the authors. SDP-based verification seems to have been surpassed by various branch-and-bound schemes which employ looser relaxations but operate on subproblems that are much easier to solve. I doubt that this work would contribute to SDP methods being able to rival such methods (such as GCP-CROWN) and its practical relevance is therefore limited. Appendix D shows that the interior-point vanishing problem does occur in networks from prior verification works, but the authors do not provide any evidence that their proposed methods help solve the issues on these larger networks.


Decision: Reject