Probabilistically Tightened Linear Relaxation-based Perturbation Analysis for Neural Network Verification
This work addresses the challenge of efficiently verifying neural network robustness for safety-critical applications, offering a novel probabilistic approach that advances the field beyond deterministic methods.
The paper tackles the problem of neural network verification by introducing PT-LiRPA, a framework that combines over-approximation with sampling to tighten output bounds, resulting in up to 3.31X improvement in robustness certificates and enabling verification in cases where state-of-the-art methods fail with at least 99% confidence.
We present $\textbf{P}$robabilistically $\textbf{T}$ightened $\textbf{Li}$near $\textbf{R}$elaxation-based $\textbf{P}$erturbation $\textbf{A}$nalysis ($\texttt{PT-LiRPA}$), a novel framework that combines over-approximation techniques from LiRPA-based approaches with a sampling-based method to compute tight intermediate reachable sets. In detail, we show that with negligible computational overhead, $\texttt{PT-LiRPA}$ exploiting the estimated reachable sets, significantly tightens the lower and upper linear bounds of a neural network's output, reducing the computational cost of formal verification tools while providing probabilistic guarantees on verification soundness. Extensive experiments on standard formal verification benchmarks, including the International Verification of Neural Networks Competition, show that our $\texttt{PT-LiRPA}$-based verifier improves robustness certificates by up to 3.31X and 2.26X compared to related work. Importantly, our probabilistic approach results in a valuable solution for challenging competition entries where state-of-the-art formal verification methods fail, allowing us to provide answers with high confidence (i.e., at least 99%).