# Probabilistic Verification of ReLU Neural Networks via Characteristic Functions

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

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Builds on 19 of its 39 references that are in the map.
- First posted on arXiv 3 Dec 2022.

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

- [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)
- [Provable defenses against adversarial examples via the convex outer adversarial polytope](https://mlsanity.com/paper/1711.00851/) (2017)
- [State-of-the-art Speech Recognition With Sequence-to-Sequence Models](https://mlsanity.com/paper/1712.01769/) (2017)
- [Semidefinite relaxations for certifying robustness to adversarial examples](https://mlsanity.com/paper/1811.01057/) (2018)
- [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)
- [Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming](https://mlsanity.com/paper/2010.11645/) (2020)
- [Autonomous Drone Racing with Deep Reinforcement Learning](https://mlsanity.com/paper/2103.08624/) (2021)
- [Reachable Polyhedral Marching (RPM): A Safety Verification Algorithm for Robotic Systems with Deep Neural Network Components](https://mlsanity.com/paper/2011.11609/) (2020)
- [CC-Cert: A Probabilistic Approach to Certify General Robustness of Neural Networks](https://mlsanity.com/paper/2109.10696/) (2021)
- [Make Sure You're Unsure: A Framework for Verifying Probabilistic Specifications](https://mlsanity.com/paper/2102.09479/) (2021)
- [Probabilistic Verification and Reachability Analysis of Neural Networks via Semidefinite Programming](https://mlsanity.com/paper/1910.04249/) (2019)
- [A Unified View of SDP-based Neural Network Verification through Completely Positive Programming](https://mlsanity.com/paper/2203.03034/) (2022)
- [PROVEN: Certifying Robustness of Neural Networks with a Probabilistic Approach](https://mlsanity.com/paper/1812.08329/) (2018)
- [Verification of deep probabilistic models](https://mlsanity.com/paper/1812.02795/) (2018)
- [Data-Driven Certification of Neural Networks with Random Input Noise](https://mlsanity.com/paper/2010.01171/) (2020)

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

- [DC is all you need: describing ReLU from a signal processing standpoint](https://mlsanity.com/paper/2407.16556/) (2024)
- [SAVER: A Toolbox for Sampling-Based, Probabilistic Verification of Neural Networks](https://mlsanity.com/paper/2412.02940/) (2024)
- [Distributionally Robust Safety Verification of Neural Networks via Worst-Case CVaR](https://mlsanity.com/paper/2509.17413/) (2025)
- [BaB-prob: Branch and Bound with Preactivation Splitting for Probabilistic Verification of Neural Networks](https://mlsanity.com/paper/2509.25647/) (2025)
- [Probabilistic Verification of Neural Networks via Efficient Probabilistic Hull Generation](https://mlsanity.com/paper/2604.21556/) (2026)

## Abstract (arXiv)

Verifying the input-output relationships of a neural network so as to achieve some desired performance specification is a difficult, yet important, problem due to the growing ubiquity of neural nets in many engineering applications. We use ideas from probability theory in the frequency domain to provide probabilistic verification guarantees for ReLU neural networks. Specifically, we interpret a (deep) feedforward neural network as a discrete dynamical system over a finite horizon that shapes distributions of initial states, and use characteristic functions to propagate the distribution of the input data through the network. Using the inverse Fourier transform, we obtain the corresponding cumulative distribution function of the output set, which can be used to check if the network is performing as expected given any random point from the input set. The proposed approach does not require distributions to have well-defined moments or moment generating functions. We demonstrate our proposed approach on two examples, and compare its performance to related approaches.