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

TL;DR

PT-LiRPA introduces a probabilistic tightening of LiRPA by combining sampling-based estimation of intermediate reachable sets with classical linear relaxations to yield significantly tighter output bounds for neural network verification. Leveraging Wilks’ tolerance limits and extreme value theory, the framework provides probabilistic guarantees on bound accuracy while maintaining soundness for all inputs in the perturbation region with a controllable confidence level. Empirically, PT-LiRPA improves robustness certificates by up to $3.31\times$ (compared to probabilistic baselines) and up to $3.62\times$ (vs worst-case methods), and proves valuable on challenging VNN-COMP instances where purely formal methods struggle, with negligible computational overhead thanks to GPU-accelerated sampling. This work positions probabilistic verification as a practical complement to provable methods, offering tighter safety insights for difficult instances and enabling more informative risk assessments in neural-network safety-critical applications.

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%).

Figures (10)

• Figure 1: Linear relaxation for ReLU($z^{(i)}_j$)
• Figure 2: Toy DNN used in this example. Intervals reported in green are the exact output reachable set computed via MIP, in black are the ones of IBP, and finally, in purple, the results for CROWN considering the input $[[-2,2], [-1,3]]$.
• Figure 3: Alternative representation of toy DNN of Figure \ref{['fig:toyDNN']}.
• Figure 4: Illustrative representation in 3D of Theorem 3.5.
• Figure 5: Toy DNN used in this example. Intervals reported in green are the exact output reachable set computed via MIP, in black are the results of the IBP, and in purple the CROWN ones considering the input $[[-2,2], [-1,3]]$. In red are the reachable sets computed using a naive sampling-based approach of $n=10k$ samples. Finally, in blue, the ones computed using a naive sampling-based approach combined with the EVT error estimation.

Theorems & Definitions (13)

• Definition 2.1: Robustness verification problem
• Definition 2.2: Reachable set
• Lemma 3.1: Probabilistically tightened reachable sets
• Proposition 3.2
• Lemma 3.3: ReLU Layer Relaxation using PT-LiRPA
• proof
• Theorem 3.4: PT-LiRPA weak probabilistic guarantees
• proof
• Theorem 3.5: Worst-case excess bound
• proof