Probabilistically Tightened Linear Relaxation-based Perturbation Analysis for Neural Network Verification

TL;DR

This paper introduces PT-LiRPA, a probabilistic framework that enhances neural network verification by tightening bounds with minimal computational overhead, leading to more robust certificates and success in challenging benchmarks.

Contribution

PT-LiRPA combines LiRPA-based over-approximation with sampling to produce tighter bounds and probabilistic guarantees, improving verification efficiency and robustness certification.

Findings

Achieves up to 3.31X improvement in robustness bounds.

Provides high-confidence verification answers with at least 99% confidence.

Successfully verifies challenging models where previous methods fail.

Abstract

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, i.e., the certified lower bound of $\varepsilon$ perturbation tolerated by the models, 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%).