Doubly Non-Negative Relaxations for Deep Neural Networks

Neural network verification is critical for deploying AI in safety-critical systems like autonomous vehicles. Existing methods often rely on linear program (LP) or semidefinite program (SDP) relaxations. While LP methods are fast, they are often too conservative, leading to loose safety bounds. SDP methods are tighter but struggle with scalability. This paper addresses the need for a verification method that is both tight enough to provide meaningful safety guarantees and scalable enough for practical use.

The authors focus on the doubly non-negative (DNN) program, which is a tighter relaxation than standard SDPs because it incorporates element-wise non-negativity constraints. However, DNNs are typically intractable at scale. To solve this, the authors apply Burer-Monteiro (BM) factorization, which reduces the number of decision variables by factorizing the matrix variable into a low-rank form.

A major technical hurdle is that the additional non-negativity constraints in the DNN violate the Linear Independence Constraint Qualification (LICQ), making standard optimality certification methods inapplicable. The authors propose a novel eigenvalue maximization procedure that searches the space of non-unique dual multipliers to construct a valid certificate of global optimality.

The proposed method, termed (DNN)^2, consistently produces tighter bounds than standard SDP-based verifiers, often matching the exact solution obtained by computationally expensive mixed-integer linear programming (MILP) solvers. The authors demonstrate that their certification procedure successfully confirms global optimality in the vast majority of test cases. Furthermore, the (DNN)^2 approach exhibits significantly more favorable computational scaling compared to interior-point methods, which suffer from cubic growth in memory and time as network size increases.