Distributionally Robust Safety Verification of Neural Networks via Worst-Case CVaR
This work addresses safety verification for neural networks in safety-critical applications, representing an incremental extension of prior methods.
The paper tackles the challenge of verifying neural network safety under input uncertainty by extending a quadratic-constraint and semidefinite-programming framework to incorporate worst-case Conditional Value-at-Risk over a moment-based ambiguity set, resulting in SDP-checkable conditions that account for tail risk and broaden input-uncertainty geometries.
Ensuring the safety of neural networks under input uncertainty is a fundamental challenge in safety-critical applications. This paper builds on and expands Fazlyab's quadratic-constraint (QC) and semidefinite-programming (SDP) framework for neural network verification to a distributionally robust and tail-risk-aware setting by integrating worst-case Conditional Value-at-Risk (WC-CVaR) over a moment-based ambiguity set with fixed mean and covariance. The resulting conditions remain SDP-checkable and explicitly account for tail risk. This integration broadens input-uncertainty geometry-covering ellipsoids, polytopes, and hyperplanes-and extends applicability to safety-critical domains where tail-event severity matters. Applications to closed-loop reachability of control systems and classification are demonstrated through numerical experiments, illustrating how the risk level $\varepsilon$ trades conservatism for tolerance to tail events-while preserving the computational structure of prior QC/SDP methods for neural network verification and robustness analysis.