# Probabilistic Verification and Reachability Analysis of Neural Networks via Semidefinite Programming

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

## Key facts

- Cited by 15 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 9 Oct 2019.

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

- [Make Sure You're Unsure: A Framework for Verifying Probabilistic Specifications](https://mlsanity.com/paper/2102.09479/) (2021)
- [Neural Network Verification in Control](https://mlsanity.com/paper/2110.01388/) (2021)
- [Distributionally Robust Statistical Verification with Imprecise Neural Networks](https://mlsanity.com/paper/2308.14815/) (2023)
- [Probabilistic Verification of ReLU Neural Networks via Characteristic Functions](https://mlsanity.com/paper/2212.01544/) (2022)
- [Automated Controller Calibration by Kalman Filtering](https://mlsanity.com/paper/2111.10832/) (2021)
- [Characterizing Data Point Vulnerability via Average-Case Robustness](https://mlsanity.com/paper/2307.13885/) (2023)
- [A Survey of Neural Network Robustness Assessment in Image Recognition](https://mlsanity.com/paper/2404.08285/) (2024)
- [Formal Verification of Stochastic Systems with ReLU Neural Network Controllers](https://mlsanity.com/paper/2103.05142/) (2021)
- [An Overview and Prospective Outlook on Robust Training and Certification of Machine Learning Models](https://mlsanity.com/paper/2208.07464/) (2022)
- [Tightening Robustness Verification of MaxPool-based Neural Networks via Minimizing the Over-Approximation Zone](https://mlsanity.com/paper/2211.09810/) (2022)
- [Adversarial Examples in Environment Perception for Automated Driving (Review)](https://mlsanity.com/paper/2504.08414/) (2025)
- [Performance Bounds for Neural Network Estimators: Applications in Fault Detection](https://mlsanity.com/paper/2103.12141/) (2021)
- [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)
- [Scalable Digital Compute-in-Memory Ising Machines for Robustness Verification of Binary Neural Networks](https://mlsanity.com/paper/2603.05677/) (2026)

## Abstract (arXiv)

Quantifying the robustness of neural networks or verifying their safety properties against input uncertainties or adversarial attacks have become an important research area in learning-enabled systems. Most results concentrate around the worst-case scenario where the input of the neural network is perturbed within a norm-bounded uncertainty set. In this paper, we consider a probabilistic setting in which the uncertainty is random with known first two moments. In this context, we discuss two relevant problems: (i) probabilistic safety verification, in which the goal is to find an upper bound on the probability of violating a safety specification; and (ii) confidence ellipsoid estimation, in which given a confidence ellipsoid for the input of the neural network, our goal is to compute a confidence ellipsoid for the output. Due to the presence of nonlinear activation functions, these two problems are very difficult to solve exactly. To simplify the analysis, our main idea is to abstract the nonlinear activation functions by a combination of affine and quadratic constraints they impose on their input-output pairs. We then show that the safety of the abstracted network, which is sufficient for the safety of the original network, can be analyzed using semidefinite programming. We illustrate the performance of our approach with numerical experiments.