这篇论文提出了一种新的方法，可以更精确地验证深度神经网络的安全性能，对于安全关键的自驾驶系统具有重要意义。
针对ReLU神经网络的线性规划（LP）和半定规划（SDP）松弛，由于显著的松弛间隙，导致过于保守的安全保证。虽然完全正规划（CPP）公式关闭了这一差距，但其最经济的可处理松弛——双重非负规划（DNN）保留了关键的约束，但其规模超出了实际规模的内点方法的范围。我们提出了一种新的特征值最大化程序，在非唯一乘子空间中搜索有效的证书，即全局最优保证。实验表明，我们的方法$( ext{DNN})^2$产生的界限始终比标准SDP方法更紧，通常与精确解相匹配，并且当存在有效证书时，我们的认证程序确认了全局最优性。这些结果是提供紧、可验证和计算可扩展的验证保证的关键步骤，这些保证对于在安全关键的自驾驶系统中部署神经网络控制器和感知模块至关重要。
$(\text{DNN})^2$: Doubly Non-Negative Relaxations for Deep Neural Networks
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.