PaperlayerView exact revision on arXiv

Source-linked AI summary

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

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

arXiv:2608.24743v1cs.LGcs.ROeess.SY

TL;DR

The paper addresses the lack of scalable, certifiable solutions for the tighter DNN relaxation in ReLU neural-network verification, whose certification is complicated by non-unique multipliers. It applies rank-2 BM factorization and an eigenvalue-maximization search for certificates, recovering globally optimal DNN solutions in 95% of verification queries on a small test network and 84–100% depending on network configuration. The results support BM-factorized DNN relaxations as a promising path toward scalable, tight verification.

  • Problem

    Existing SDPs can have relaxation gaps, while exact CPP verification is NP-hard and DNN instances exceed practical interior-point scale; DNN certification is further complicated by non-unique multipliers.

  • Method

    The paper uses rank-2 Burer–Monteiro factorization for DNN optimization and eigenvalue maximization to search valid multipliers for global optimality certificates.

  • Results

    The method recovers the exact global optimum in 95% of verification queries on a small test network, while globally optimal DNN bounds are recovered in 84–100% of queries depending on network configuration.

  • Takeaways & Limitations

    BM-factorized DNN relaxations provide a promising route to verification that is tighter than canonical SDP and can carry global optimality guarantees despite LICQ failure.

Abstract

from arXiv · show

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.

I. INTRODUCTION

Neural-network verification needs tighter bounds and scalable optimization because existing LP, SDP, and MILP approaches face relaxation gaps or computational barriers. The paper targets the DNN relaxation with BM factorization and develops certification despite non-unique multipliers.

  • Motivation: Safety-critical neural networks require verification because outer bounds on reachable outputs can establish whether outputs remain within safe limits.These bounds connect verification with reachability analysis for reach-avoid guarantees in learning-based control.
  • Limitations of Existing Methods: LP relaxations are scalable and sound but can leave verification inconclusive because linear outer bounds approximate ReLU complementarity constraints.Branch-and-bound can recover completeness but is exponential in the worst case.
  • Limitations of Existing Methods: Existing SDPs enforce some quadratic neuron relationships but omit verification-defining constraints, producing relaxation gaps.MILP methods can obtain exact bounds but become intractable for larger instances.
  • DNN Relaxation: The CPP formulation is exact, while its coarsest tractable 0-SOS relaxation, DNN, is tighter than existing SDP formulations and often exact on small networks.The CPP is intractable, motivating scalable approximations.
  • Scalability: Interior-point SDP methods scale as O(n^3) per iteration, motivating BM factorization for large-scale relaxations.BM factorization replaces the convex SDP with a nonconvex NLP whose local solutions require global-optimality certification.
  • Contributions: Rank-2 BM factorization makes DNN optimization scalable by replacing interior-point SDP solves with lower-dimensional NLP solves, yielding bounds tighter than c-SDP and often exact.This is the paper’s scalable optimization contribution.
  • Contributions: An eigenvalue maximization procedure searches valid multiplier families to construct global optimality certificates without LICQ.LICQ is generically violated for DNN, so multipliers are non-unique and a solver-returned set may fail to certify an actually global solution.
  • Results: The method recovers the exact global optimum in 95% of verification queries on the small test network, while its certificate correctly identifies the corresponding cases.The paper positions these results as a step toward practical NN verification.

II. PROBLEM FORMULATION AND PRELIMINARIES

The paper models feedforward ReLU verification as a nonconvex optimization problem over layered network variables, bounded inputs, and output safety constraints. Its optimum supplies the ground truth for evaluating relaxation tightness.

  • II. PROBLEM FORMULATION AND PRELIMINARIES: The formulation is restricted to feedforward ReLU networks because their piecewise-linear activations admit exact bilinear complementarity representations.These representations enable the conic reformulations developed later.
  • A. NN Verification as Optimization: An ℓ-layer network maps input z0,* to output zℓ,* through the composition f = fℓ ◦ fℓ−1 ◦ · · · ◦ f1.Each layer fi maps R^h_i−1 to R^h_i.
  • A. NN Verification as Optimization: Each hidden layer applies ReLU elementwise to an affine transformation, while the final layer does not apply ReLU.Weights, biases, hidden-variable dimensions, neuron variables, and preactivation values are explicitly parameterized.
  • A. NN Verification as Optimization: Positive/negative splitting variables λ+ and λ− replace the typical preactivation/post-activation parameterization.The split variables satisfy λ+, λ− ≥ 0.
  • A. NN Verification as Optimization: Safety verification requires outputs in Y for every input in a bounded polytopic set X.The sets are represented using half-space constraints X = {x | Ax ≤ a} and Y = {y | c^T y ≥ d}.
  • A. NN Verification as Optimization: Substituting the split variables into the verification QCQP produces a nonconvex nonlinear QCQP.The reformulation follows the cited feedforward ReLU verification model.
  • A. NN Verification as Optimization: The network is safe if and only if the QCQP optimum g⋆ satisfies g⋆ ≥ d.Relaxation bounds are tight to the extent that their optimal values approach this ground-truth value.

B. Generalized Cone Programs

Generalized cone programs express the relevant relaxations as convex optimization over affine constraints and a selected matrix cone. The cone determines the tradeoff between tractability and tightness.

  • B. Generalized Cone Programs: A generalized cone program minimizes a linear objective over the intersection of an affine subspace and a convex cone K_n.This framework unifies SDPs, DNNs, and CPPs.
  • B. Generalized Cone Programs: The generalized formulation uses a symmetric matrix variable Z, a convex objective f, and linear operators A and B for its constraints.The operators are defined through matrix inner products.
  • B. Generalized Cone Programs: The completely positive cone consists of matrices admitting a factorization with entrywise nonnegative factors.This cone is denoted C_n^* in the paper’s notation.
  • B. Generalized Cone Programs: Direct membership testing in the completely positive cone is NP-hard, motivating tractable outer approximations.The DNN cone is one such approximation.
  • B. Generalized Cone Programs: The DNN cone is the intersection of the positive semidefinite and entrywise nonnegative matrix cones.It provides a tractable alternative to direct optimization over the completely positive cone.

C. Conic Reformulations of Neural Network Verification

The paper presents canonical SDP, exact CPP, and tractable DNN conic reformulations of the neural-network verification QCQP. They share a generalized cone-program structure while differing in construction and relaxation gaps.

  • C. Conic Reformulations of Neural Network Verification: The paper introduces three conic reformulations: canonical SDP, exact CPP, and tractable DNN relaxations.Each uses the common generalized cone-program form to expose relationships among the formulations.
  • C. Conic Reformulations of Neural Network Verification: Because the objective and constraints are quadratic, the QCQP can be expressed using an objective matrix Q, constraint matrices, vectors, and a factor matrix X.Replacing XX^T with a symmetric PSD matrix variable Z yields convex relaxations over selected cones.

Q, XXT

Convex relaxations replace the low-rank outer product XX^T with a symmetric matrix constrained to a cone, trading tightness against tractability. The DNN retains verification-defining constraints and is tighter than the canonical SDP, but CPP optimization remains intractable.

  • Shor’s relaxation replaces XX^T with a generic symmetric PSD matrix Z, producing the canonical SDP relaxation.This increases the decision-variable dimension from X ∈ R^(n×r) to Z ∈ S^n.
  • SDP decision variables scale quadratically with network size, creating memory constraints that also limit the DNN.An ablation found relative errors ranging from 10^2 to 10^4 when a critical non-negativity constraint was omitted.
  • The CPP gives an exact zero-gap formulation, but membership testing in its copositive cone is NP-hard and co-NP-complete for the dual.Its intractability is concentrated in the cone constraint rather than combinatorial branching.
  • The SOS hierarchy supplies tractable SDP outer approximations, with progressively tighter approximations at greater computational cost.The coarsest 0-SOS level yields the DNN relaxation.
  • The DNN retains all verification-defining constraints and is tighter than the canonical SDP while remaining expressible as an SDP of the CPP’s size.It is described as the tightest same-size SDP relaxation without the additional variables and constraints of higher SOS levels.

D. Scalably Solving SDPs via Burer–Monteiro Factorization

Burer–Monteiro factorization makes large SDP relaxations more manageable by parameterizing the PSD matrix as a low-rank outer product. This reduces the optimization dimension but produces a nonconvex NLP.

  • BM factorization replaces the matrix variable Z with an assumed low-rank factorization Z = YY^T, where r ≤ p ≪ n.The factor Y ∈ R^(n×p) enforces positive semidefiniteness by construction.
  • The BM formulation reduces the number of decision variables from n^2 to np while retaining the original linear equality and inequality constraints in YY^T.Its objective is g(YY^T), subject to A(YY^T)=b and B(YY^T)≤u.

E. Global Optimality Certification and the Role of the LICQ

BM optimization is nonconvex, so stationary points require certification as global minimizers of the original SDP. Rank continuation and certificate construction provide a route to distinguish certifiable solutions from suboptimal ones, but prior methods rely on LICQ.

  • The BM-factorized problem is a nonconvex NLP that can admit suboptimal local minima, motivating rank-increasing search for global optima.The RS framework incrementally increases the factor rank to smooth the optimization landscape and escape suboptimal points.
  • RS locally optimizes to a KKT point, constructs a certificate matrix S, and either certifies Z=Y⋆Y⋆^T when S⪰0 or increases the rank.This procedure checks whether a stationary BM solution corresponds to an SDP solution.
  • Prior certification methods rely on LICQ to guarantee unique Lagrange multipliers and enable direct certificate construction.For canonical SDP verification, LICQ can follow from the nonzero preactivation condition.

III. CERTIFIABLY AND SCALABLY SOLVING DNNS

The paper combines BM factorization with a certification procedure tailored to the DNN’s non-unique multipliers. It searches the feasible multiplier space for a certificate proving global optimality of a BM-DNN solution.

  • BM-DNN adds element-wise non-negativity constraints (YY^T)_ij ≥ 0 to the BM formulation of the DNN.These constraints distinguish BM-DNN from the basic BM factorization of a PSD relaxation.
  • If a first-order stationary point has KKT multipliers yielding S⪰0, then Z⋆=Y⋆Y⋆^T is a global minimizer of the DNN.The certificate requires existence of suitable multipliers rather than uniqueness.
  • Under LICQ, multipliers are unique and S̸⪰0 definitively proves non-optimality, but these conclusions do not hold directly when LICQ fails.DNN non-negativity constraints can be simultaneously active, violating LICQ and creating multiple valid multiplier sets.
  • The proposed approach searches the non-unique feasible multiplier space for a multiplier satisfying S⪰0, thereby certifying global optimality when found.This procedure is designed to solve DNN relaxations scalably while retaining global optimality guarantees.

B. Search for Optimality Certificate

The certificate search maximizes the minimum eigenvalue of a certificate matrix over feasible BM-DNN multipliers, addressing multiplier non-uniqueness without LICQ. A nonnegative optimum certifies global optimality, while a negative optimum rules it out under a suitable constraint qualification.

  • Certificate search: The procedure maximizes the certificate matrix’s minimum eigenvalue over multipliers satisfying BM-DNN KKT conditions.The constraints enforce stationarity, complementary slackness, and dual feasibility.
  • Certification conditions: If the optimal value satisfies θ⋆min ≥ 0, a feasible multiplier produces S ⪰ 0 and certifies the BM solution globally optimal.The certificate applies to the stationary point returned by the NLP solver.
  • Certification conditions: If θ⋆min < 0 and the DNN satisfies a suitable constraint qualification, the lifted BM point is not optimal for the DNN.For convex problems, KKT necessity and sufficiency make the absence of valid multipliers conclusive.
  • Numerical implementation: Finite solver tolerances require relaxing stationarity and complementary-slackness constraints with ℓ1-norm bounds derived from NLP multiplier residuals.Other norms could interact differently with the chosen solver.
  • Certificate search: An epigraph variable θmin converts the nonsmooth eigenvalue objective into an SDP constraint, S(µ) − θmin I ⪰ 0.This yields the numerically robust formulation in Eq. 10.
  • Numerical implementation: The certificate SDP is used for validation rather than intrinsic runtime, because any feasible µ with S ⪰ 0 suffices and early termination is allowed.Scaling this search remains future work.

IV. EXPERIMENTAL RESULTS AND DISCUSSION

Experiments evaluate rank-2 BM factorization of the DNN relaxation on generated feedforward ReLU networks. The method generally preserves DNN tightness, frequently recovers global optima, and exposes a small certification failure rate caused by certificate-solver timeouts.

  • Experimental setup: The experiments use rank-2 BM factorization, denoted (DNN)2, to study DNN tightness and global-optimality certification.The evaluation restricts attention to generated FF ReLU networks to isolate relaxation tightness and BM factorization.
  • Global optimality and tightness: 95% of verification queries on the small test network recover the exact global optimum of the DNN relaxation.Certificate (10) correctly identifies each such case.
  • Scaling experiments: For larger and deeper networks, c-SDP bounds become progressively looser, whereas (DNN)2 remains within 10^-4 of MILP ground truth in the majority of instances.The comparison varies network height and depth over 100 random instances per configuration.
  • Certification limitations: 0.075% of queries match MILP to numerical precision but lack certificate confirmation because the interior-point solver for Eq. 10 times out.This is attributed to the certificate solver rather than the DNN formulation.
  • Global optimality and tightness: The DNN relaxation is exact in all but 2 instances, while (DNN)2 recovers the globally optimal DNN bound in 84–100% of queries across configurations.The reported range depends on network configuration.
  • Why DNN is tighter: The feasible-set analysis shows that DNN’s additional element-wise non-negativity constraints produce a strictly smaller feasible region than c-SDP.The smaller region explains the tighter outer bounds shown in the comparison.

B. Computational Scalability of BM-DNN over DNN

BM factorization improves the computational scaling of DNN optimization as network size grows, despite NLP overhead on small instances. The experiments illustrate why direct interior-point DNN solves become impractical at larger dimensions.

  • Computational scaling: Direct DNN solve times grow rapidly with network size, while the BM-factored (DNN)2 form has more favorable scaling.The comparison uses architecture [k, k·1k, k] with increasing k.
  • Computational scaling: For small instances, (DNN)2 is slower than direct DNN because of NLP solver overhead.The scaling trends diverge rapidly as k increases.
  • Computational scaling: Interior-point costs grow cubically in matrix dimension, whereas the BM variable count grows only linearly.This difference drives the widening computational gap with network size.
  • Computational scaling: The direct SDP solve at k = 11 fails because of memory exhaustion, illustrating the practical scalability limit of the matrix formulation.The BM-factored form avoids the same observed failure in the reported scaling comparison.
  • Implication: The BM-factorized DNN combines tighter-than-c-SDP bounds with a scalable optimization route toward neural-network verification.The paper presents this combination as a promising path for tight, scalable verification.
Loading 2608.24743v1…