(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.
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 (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, (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 \APLstar . (bottom) Wall time computational performance comparison between the direct DNN (solved via interior-point methods, MOSEK ) and (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 (DNN)2 exhibits significantly more favorable linear scaling.
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 (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 (DNN)2 has reached a local rather than global optimum; these points are marked with \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 z1=ReLU(x1+x2) and z2=ReLU(x1−x2) . (left) The feasible set of each relaxation projected onto the post-activation variables (z1,z2) for fixed input x1=x2=0.5 . (right) The same projection across all feasible inputs, under the objective maxz1+z2 . 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.
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%.
Mohammadreza Maleki, Daniel Sadig, Rushendra Sidibomma +3
Toronto Metropolitan University · University of Minnesota Twin Cities · Johns Hopkins University +2
The increasing integration of deep neural networks in critical systems has spawned a theoretical and practical interest in formally guaranteeing safety properties about their behavior. To achieve this, contemporary verification algorithms rely on computing linear relaxations for a network's non-linear activation functions. Existing approaches for linear relaxations typically fall into one of two categories: single-neuron relaxation, in which each activation neuron is bounded in terms of its sources; and multi-neuron relaxation, in which linear bounds involving multiple activation neurons and their sources are calculated. However, existing methods might fail to balance tightness and scalability, as single-neuron bounds might not derive sufficiently tight bounds necessary for verification to complete, whereas generating multi-neuron relaxation for all activation neurons is computationally expensive. In this paper, we present a middle-ground approach featuring partial multi-neuron relaxation, in which we generate multi-neuron bounds for only a small, heuristically selected subset of neurons. To achieve this, we build upon existing branching heuristics for selecting neurons and for optimizing bounding hyper-planes for multi-neuron bounds. We integrated our proposed method within the Marabou verifier, and obtained favorable results in comparison to existing bound tightening methods. Our experiments showcase the potential of our technique for neural network verification.
Ido Shmuel, Guy Katz
The Hebrew University of Jerusalem, Jerusalem, Israel
Formal verification can play a key role in ensuring the reliability of Deep Neural Networks (DNNs) deployed in safety-critical systems. Modern DNN verifiers employ a branch-and-bound framework, which alternates between branching (splitting into smaller subproblems) and bounding (pruning subproblems) to efficiently explore the verification space. However, existing branching heuristics make greedy decisions based on static scoring functions. They do not anticipate long-term efficiency or leverage the growing availability of verification data to improve performance. This work introduces RSB, a reinforcement learning framework that learns to refine baseline branching heuristics. It trains an actor-critic architecture to maximize cumulative future rewards rather than immediate scores. The actor generates attention weights from observations of raw neuron features and learned graph embeddings, which rescale baseline heuristic scores to guide neuron branching. Evaluation on 600 challenging instances demonstrates that RSB consistently outperforms state-of-the-art branching heuristics, solving 11% more instances while reducing branch exploration by 50%.
Hai Duong, Thanh Le, ThanhVu Nguyen
Department of Computer Science George Mason University Fairfax, VA, USA · Unaffiliated Yokosuka, Japan