二重非負緩和による深層ニューラルネットワークの検証
$(\text{DNN})^2$: Doubly Non-Negative Relaxations for Deep Neural Networks
ReLUニューラルネットワークの検証において、完全正値計画法の緩和である二重非負計画法を大規模に解く手法を提案し、既存のSDP緩和より厳しい境界を計算できることを示した。
著者: Hanna Jiamei Zhang, Alan Papalia, Michael Everett, David M. Rosen
分類: cs.LG, cs.RO, eess.SY
原文アブストラクト
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.