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

arXiv: https://arxiv.org/abs/2412.02940 · HTML: https://mlsanity.com/paper/2412.02940/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 14 of its 39 references that are in the map.
- First posted on arXiv 4 Dec 2024.

## Builds on (most cited first, 14 of 14)

- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [Universal adversarial perturbations](https://mlsanity.com/paper/1610.08401/) (2016)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [One pixel attack for fooling deep neural networks](https://mlsanity.com/paper/1710.08864/) (2017)
- [An approach to reachability analysis for feed-forward ReLU neural networks](https://mlsanity.com/paper/1706.07351/) (2017)
- [Safety Verification and Robustness Analysis of Neural Networks via Quadratic Constraints and Semidefinite Programming](https://mlsanity.com/paper/1903.01287/) (2019)
- [Maximum Resilience of Artificial Neural Networks](https://mlsanity.com/paper/1705.01040/) (2017)
- [Neural Lander: Stable Drone Landing Control using Learned Dynamics](https://mlsanity.com/paper/1811.08027/) (2018)
- [Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming](https://mlsanity.com/paper/2010.11645/) (2020)
- [CC-Cert: A Probabilistic Approach to Certify General Robustness of Neural Networks](https://mlsanity.com/paper/2109.10696/) (2021)
- [A Unified View of SDP-based Neural Network Verification through Completely Positive Programming](https://mlsanity.com/paper/2203.03034/) (2022)
- [Probabilistic Verification of ReLU Neural Networks via Characteristic Functions](https://mlsanity.com/paper/2212.01544/) (2022)
- [Solving Probabilistic Verification Problems of Neural Networks using Branch and Bound](https://mlsanity.com/paper/2405.17556/) (2024)
- [Is Ordered Weighted ℓ1 Regularized Regression Robust to Adversarial Perturbation? A Case Study on OSCAR](https://mlsanity.com/paper/1809.08706/) (2018)

## Built on by (most cited first, 2 of 2)

- [GenCtrl -- A Formal Controllability Toolkit for Generative Models](https://mlsanity.com/paper/2601.05637/) (2026)
- [BaB-prob: Branch and Bound with Preactivation Splitting for Probabilistic Verification of Neural Networks](https://mlsanity.com/paper/2509.25647/) (2025)

## Abstract (arXiv)

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.