$(\text{DNN})^2$: Doubly Non-Negative Relaxations for Deep Neural Networks

Hanna Jiamei Zhang; Alan Papalia; Michael Everett; David M. Rosen

cs.LGAug 25, 2026

$(\text{DNN})^2$ : Doubly Non-Negative Relaxations for Deep Neural Networks

Authors: Hanna Jiamei Zhang, Alan Papalia, Michael Everett, David M. Rosen

Organizations: Departments of Computer Science, Electrical and Computer Engineering, and Mathematics Northeastern University, Boston, MA. · Department of Naval Architecture and Marine Engineering, University of Michigan, Ann Arbor, MI.

Abstract

Existing linear program (LP) and semidefinite program (SDP) relaxations for rectified linear unit (ReLU) neural network (NN) verification yield overly-conservative safety guarantees due to significant relaxation gaps. While the completely positive program (CPP) formulation closes this gap, it is NP-hard to solve. Its cheapest tractable relaxation, the doubly non-negative program (DNN), retains critical constraints as an SDP, but one whose size exceeds the reach of interior-point methods at practical scale. While Burer-Monteiro (BM) factorization has been applied to make SDP-based verification scalable, no such result exists for the strictly tighter DNN formulation. A key obstacle is that additional non-negativity constraints in the DNN cause dual multipliers for optimality certification to be non-unique, making standard certification methods inapplicable. We propose a novel eigenvalue maximization procedure that searches the non-unique multiplier space for a valid certificate, i.e. a global optimality guarantee. Experiments demonstrate that our approach $(\text{DNN})^2$ produces bounds consistently tighter than the standard SDP method, often matching the exact solution, and that our certification procedure confirms global optimality when a valid certificate exists. These results are a key step toward providing tight, certifiable, and computationally scalable verification guarantees needed to deploy neural network controllers and perception modules in safety-critical autonomous systems.

Figures & tables

Fig. 1 : (top) A comparison of the tightness of various verification methods against the ground-truth MILP solution across 100 ReLUNNs . While the standard c-SDP [ 9 , 2 ] leaves significant relaxation gaps, our proposed rank-2 BM-factorized DNN,

(\text{DNN})^{2}

, consistently produces tighter bounds, frequently matching the exact MILP solution

95\%

of all verification instances. Our proposed optimality certification procedure (Eq. 10 ) reliably distinguishes between global and local optima, with the latter marked with

\mathbf{\APLstar}

. (bottom) Wall time computational performance comparison between the direct DNN (solved via interior-point methods, MOSEK ) and

(\text{DNN})^{2}

(solved as a non-linear program, KNITRO ) with increasing network size parameter

k

, using the Julia JuMP interface. As expected, while interior-point solve times grow rapidly (cubically) with problem size, our

(\text{DNN})^{2}

exhibits significantly more favorable linear scaling.

Panel of Figure 2 — Fig. 2 : Analysis of how verification accuracy degrades as NNs increase in height (top) and depth (bottom). The canonical c- SDP bounds (blue) become progressively looser as the network grows, making safety verification more difficult. In contrast, our $(\text{DNN})^{2}$ formulation (orange) remains highly tight to the MILP ground truth across all tested scales, demonstrating its robustness for larger, more complex network architectures. Our proposed certification procedure (Eq. 10 ) successfully identifies instances where $(\text{DNN})^{2}$ has reached a local rather than global optimum; these points are marked with $\mathbf{\APLstar}$ and are excluded from the box plots. The percentage of instances certified as globally optimal is annotated for each configuration.

Fig. 3 : Visualizing why the DNN relaxation is tighter than c- SDP . Let

z_{1}=\text{ReLU}\left(x_{1}+x_{2}\right)

and

z_{2}=\text{ReLU}\left(x_{1}-x_{2}\right)

. (left) The feasible set of each relaxation projected onto the post-activation variables

(z_{1},z_{2})

for fixed input

x_{1}=x_{2}=0.5

. (right) The same projection across all feasible inputs, under the objective

\max\;z_{1}+z_{2}

. Because the DNN formulation enforces additional element-wise non-negativity constraints not present in the SDP , it produces a strictly smaller feasible set (red) than the SDP (blue), leading to tighter outer NN bounds and more accurate safety guarantees.

Neural Network Verification

Neural network verification develops methods to prove whether networks satisfy properties such as robustness, safety, and bounded output behavior.

See all 121 papers

Certified Robustness via Sparse Second-Order Cone Relaxations
Oct 12, 2026Mohammadreza Maleki, Daniel Sadig, Rushendra Sidibomma +3Convex Relaxation Neural Network Verification
Toronto Metropolitan University · University of Minnesota Twin Cities · Johns Hopkins University +2
Neural Network Verification using Partial Multi-Neuron Relaxation
May 28, 2026Ido Shmuel, Guy KatzNeural Network Verification
The Hebrew University of Jerusalem, Jerusalem, Israel
Verifying Neural Networks with Reinforcement Learning
Sep 28, 2026Hai Duong, Thanh Le, ThanhVu NguyenNeural Network Verification Branch and Bound
Department of Computer Science George Mason University Fairfax, VA, USA · Unaffiliated Yokosuka, Japan

Oct 12, 2026J/K move · Enter open · S save

Certified Robustness via Sparse Second-Order Cone Relaxations

Mohammadreza Maleki, Daniel Sadig, Rushendra Sidibomma, Mahyar Fazlyab+2

Toronto Metropolitan University · University of Minnesota Twin Cities · Johns Hopkins University+2

Convex Relaxation Neural Network Verification Certified Robustness Constrained Optimization

Open paper AskPDF arXiv

Certified robustness is critical for deploying neural networks in safety-sensitive settings, but computing exact certificates typically requires solving nonconvex optimization problems. Practical verifiers use convex relaxations: linear programming (LP) relaxations are scalable but often too conservative, whereas semidefinite programming (SDP) relaxations can be substantially tighter but are computationally expensive. We introduce a hierarchy of second-order cone programming (SOCP) relaxations that provide stronger certificates than LP while avoiding the cost of global positive-semidefinite constraints. Our construction combines convex-hull relaxations of ReLU activations, selective McCormick lifting over certified variable bounds, and second-order cone constraints induced by 2-by-2 principal minors. Adding these constraints progressively yields a monotone hierarchy of increasingly tight bounds with a controllable computation-tightness trade-off. On fully connected and convolutional networks on MNIST and CIFAR-10, SOCP-based verification improves certified robust accuracy over LP-based verification and is competitive with alpha,beta-CROWN, while remaining orders of magnitude faster than SDP-based verification. These results position selective second-order constraints as a practical middle ground between scalable LP-based and tight SDP-based certification. Finally, we introduce class-optimized robust evaluation (CORE), which applies tighter relaxations only to target classes not certified by cheaper ones. On the fully connected MNIST benchmark, CORE variants match SDP-cert's certified robust accuracy while reducing average verification time by up to 86.30%.

Abstract

Neural Network Verification

Explore similar work

Certified Robustness via Sparse Second-Order Cone Relaxations

Neural Network Verification using Partial Multi-Neuron Relaxation

Verifying Neural Networks with Reinforcement Learning