SAVER: A Toolbox for Sampling-Based, Probabilistic Verification of Neural Networks

TL;DR

SAVER addresses the challenge of probabilistic verification for neural networks under input uncertainty by introducing a sampling-based toolbox that estimates the likelihood of outputs lying in a target set using empirical CDFs and guarantees from the Dvoretzky-Kiefer-Wolfowitz inequality and scenario optimization. It encodes specifications with signed distance functions (SDFs), enabling straightforward set enlargement or reduction via a level-set parameter $\theta$ to satisfy a user-defined probability $1-\Delta$. The paper formalizes the problem, derives sample-complexity bounds, and demonstrates three applications (feedforward networks, image classifiers, and TaxiNet) to illustrate how to compute required samples and perform probabilistic satisfaction checks or adjustments. Overall, SAVER offers a practical, extensible framework for probabilistic NN verification with quantifiable confidence, suitable for safety-critical domains. The key contribution is a unified, SDF-based, data-driven verification workflow that yields both probabilistic guarantees and actionable set-tuning to meet specified reliability levels.

Abstract

We present a neural network verification toolbox to 1) assess the probability of satisfaction of a constraint, and 2) synthesize a set expansion factor to achieve the probability of satisfaction. Specifically, the tool box establishes with a user-specified level of confidence whether the output of the neural network for a given input distribution is likely to be contained within a given set. Should the tool determine that the given set cannot satisfy the likelihood constraint, the tool also implements an approach outlined in this paper to alter the constraint set to ensure that the user-defined satisfaction probability is achieved. The toolbox is comprised of sampling-based approaches which exploit the properties of signed distance function to define set containment.

Figures (8)

• Figure 1: We consider neural nets with probabilistic inputs, and seek to identify the likelihood that the output distribution falls within a set $C$ with at least some probability $1-\Delta$ (Problem \ref{['prob:NNProbVerification']}), and if necessary, to identify the smallest enlargement of the set $C$, by a distance $\theta$, in order to satisfy the same probability (Problem \ref{['prob:setEnlargment']}).
• Figure 2: Flowchart depicting SAVER toolbox elements.
• Figure 3: A subset set $C$ (left) of a vector space $\mathcal{X}$ and the graph of its SDF $g_C$ (right). A point $p$ positioned at a signed distance $\theta^*$ away from $C$ lies on the border of the enlarged set $C^* = \{x:\ g_C(x) = \theta^*\}$, which is the projection of the graph section $\{(x,\theta^*):(g_C(x) = \theta^*)\}$ onto $\mathcal{X}$. Here $\theta^* > 0$, resulting in an enlargement; if $\theta^*$ were negative, the new set would be a reduction.
• Figure 4: We propagate a standard Cauchy distribution at the input through a feedforward neural network with ReLU activation functions and determine whether the output resides within the set $C$ (in red) with probability greater than $1-\Delta$.
• Figure 5: Samples of the output of the neural network are superimposed on the set specification \ref{['eq:ffNNSetSpecification']}. Through both DKW and scenario optimization approaches, we achieve probabilistic satisfaction of the specification with probability greater than 99%. To reduce the set's conservatism, we revise the specification using DKW (yellow) and scenario (green) approaches to solve Problem \ref{['prob:setEnlargment']} while ensuring 99.9% specification satisfaction.

Theorems & Definitions (2)

• Remark 1
• Definition 1