# Make Sure You're Unsure: A Framework for Verifying Probabilistic Specifications

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

## Key facts

- Cited by 18 papers in the map (data through 14 Oct 2026).
- Builds on 23 of its 37 references that are in the map.
- First posted on arXiv 18 Feb 2021.

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

- [Deep Residual Learning for Image Recognition](https://mlsanity.com/paper/1512.03385/) (2015)
- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [Very Deep Convolutional Networks for Large-Scale Image Recognition](https://mlsanity.com/paper/1409.1556/) (2014)
- [Towards Deep Learning Models Resistant to Adversarial Attacks](https://mlsanity.com/paper/1706.06083/) (2017)
- [Dropout as a Bayesian Approximation: Representing Model Uncertainty in Deep Learning](https://mlsanity.com/paper/1506.02142/) (2015)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Square Attack: a query-efficient black-box adversarial attack via random search](https://mlsanity.com/paper/1912.00049/) (2019)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Why ReLU networks yield high-confidence predictions far away from the training data and how to mitigate the problem](https://mlsanity.com/paper/1812.05720/) (2018)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Semidefinite relaxations for certifying robustness to adversarial examples](https://mlsanity.com/paper/1811.01057/) (2018)
- [A Dual Approach to Scalable Verification of Deep Networks](https://mlsanity.com/paper/1803.06567/) (2018)
- [Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming](https://mlsanity.com/paper/2010.11645/) (2020)
- [Uncertainty Quantification with Statistical Guarantees in End-to-End Autonomous Driving Control](https://mlsanity.com/paper/1909.09884/) (2019)
- [Probabilistic Safety for Bayesian Neural Networks](https://mlsanity.com/paper/2004.10281/) (2020)
- [Statistical Guarantees for the Robustness of Bayesian Neural Networks](https://mlsanity.com/paper/1903.01980/) (2019)
- [Bayesian Inference with Certifiable Adversarial Robustness](https://mlsanity.com/paper/2102.05289/) (2021)
- [Robustness Certification of Generative Models](https://mlsanity.com/paper/2004.14756/) (2020)
- [Probabilistic Verification and Reachability Analysis of Neural Networks via Semidefinite Programming](https://mlsanity.com/paper/1910.04249/) (2019)
- [Verification of deep probabilistic models](https://mlsanity.com/paper/1812.02795/) (2018)
- [An efficient nonconvex reformulation of stagewise convex optimization problems](https://mlsanity.com/paper/2010.14322/) (2020)
- [Certifiably Adversarially Robust Detection of Out-of-Distribution Data](https://mlsanity.com/paper/2007.08473/) (2020)

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

- [Provably Bounding Neural Network Preimages](https://mlsanity.com/paper/2302.01404/) (2023)
- [Robust Explanation Constraints for Neural Networks](https://mlsanity.com/paper/2212.08507/) (2022)
- [Convex Bounds on the Softmax Function with Applications to Robustness Verification](https://mlsanity.com/paper/2303.01713/) (2023)
- [Provably Robust Detection of Out-of-distribution Data (almost) for free](https://mlsanity.com/paper/2106.04260/) (2021)
- [On the Robustness of Bayesian Neural Networks to Adversarial Attacks](https://mlsanity.com/paper/2207.06154/) (2022)
- [BNN-DP: Robustness Certification of Bayesian Neural Networks via Dynamic Programming](https://mlsanity.com/paper/2306.10742/) (2023)
- [Adversarial Robustness Certification for Bayesian Neural Networks](https://mlsanity.com/paper/2306.13614/) (2023)
- [Out-of-Distribution Data: An Acquaintance of Adversarial Examples -- A Survey](https://mlsanity.com/paper/2404.05219/) (2024)
- [Specifying and Testing k-Safety Properties for Machine-Learning Models](https://mlsanity.com/paper/2206.06054/) (2022)
- [Probabilistic Verification of ReLU Neural Networks via Characteristic Functions](https://mlsanity.com/paper/2212.01544/) (2022)
- [Diffusion Denoised Smoothing for Certified and Adversarial Robust Out-Of-Distribution Detection](https://mlsanity.com/paper/2303.14961/) (2023)
- [Probabilistic Reach-Avoid for Bayesian Neural Networks](https://mlsanity.com/paper/2310.01951/) (2023)
- [Tight Verification of Probabilistic Robustness in Bayesian Neural Networks](https://mlsanity.com/paper/2401.11627/) (2024)
- [Solving Probabilistic Verification Problems of Neural Networks using Branch and Bound](https://mlsanity.com/paper/2405.17556/) (2024)
- [Probabilistically Tightened Linear Relaxation-based Perturbation Analysis for Neural Network Verification](https://mlsanity.com/paper/2507.05405/) (2025)
- [BEAVER: An Efficient Deterministic LLM Verifier](https://mlsanity.com/paper/2512.05439/) (2025)
- [Last Layer Hamiltonian Monte Carlo](https://mlsanity.com/paper/2507.08905/) (2025)
- [Support is All You Need for Certified VAE Training](https://mlsanity.com/paper/2504.11831/) (2025)

## Abstract (arXiv)

Most real world applications require dealing with stochasticity like sensor noise or predictive uncertainty, where formal specifications of desired behavior are inherently probabilistic. Despite the promise of formal verification in ensuring the reliability of neural networks, progress in the direction of probabilistic specifications has been limited. In this direction, we first introduce a general formulation of probabilistic specifications for neural networks, which captures both probabilistic networks (e.g., Bayesian neural networks, MC-Dropout networks) and uncertain inputs (distributions over inputs arising from sensor noise or other perturbations). We then propose a general technique to verify such specifications by generalizing the notion of Lagrangian duality, replacing standard Lagrangian multipliers with "functional multipliers" that can be arbitrary functions of the activations at a given layer. We show that an optimal choice of functional multipliers leads to exact verification (i.e., sound and complete verification), and for specific forms of multipliers, we develop tractable practical verification algorithms. We empirically validate our algorithms by applying them to Bayesian Neural Networks (BNNs) and MC Dropout Networks, and certifying properties such as adversarial robustness and robust detection of out-of-distribution (OOD) data. On these tasks we are able to provide significantly stronger guarantees when compared to prior work -- for instance, for a VGG-64 MC-Dropout CNN trained on CIFAR-10, we improve the certified AUC (a verified lower bound on the true AUC) for robust OOD detection (on CIFAR-100) from 0% rightarrow 29%. Similarly, for a BNN trained on MNIST, we improve on the robust accuracy from 60.2% rightarrow 74.6%. Further, on a novel specification -- distributionally robust OOD detection -- we improve the certified AUC from 5% rightarrow 23%.