# Probabilistically Tightened Linear Relaxation-based Perturbation Analysis for Neural Network Verification

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 39 of its 63 references that are in the map.
- First posted on arXiv 7 Jul 2025.

## Builds on (most cited first, 30 of 39)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Towards Deep Learning Models Resistant to Adversarial Attacks](https://mlsanity.com/paper/1706.06083/) (2017)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Gaussian Error Linear Units (GELUs)](https://mlsanity.com/paper/1606.08415/) (2016)
- [Certified Adversarial Robustness via Randomized Smoothing](https://mlsanity.com/paper/1902.02918/) (2019)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Learning Complex Dexterous Manipulation with Deep Reinforcement Learning and Demonstrations](https://mlsanity.com/paper/1709.10087/) (2017)
- [An Introduction to Convolutional Neural Networks](https://mlsanity.com/paper/1511.08458/) (2015)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Towards Fast Computation of Certified Robustness for ReLU Networks](https://mlsanity.com/paper/1804.09699/) (2018)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Evaluating the Robustness of Neural Networks: An Extreme Value Theory Approach](https://mlsanity.com/paper/1801.10578/) (2018)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [An approach to reachability analysis for feed-forward ReLU neural networks](https://mlsanity.com/paper/1706.07351/) (2017)
- [General Cutting Planes for Bound-Propagation-Based Neural Network Verification](https://mlsanity.com/paper/2208.05740/) (2022)
- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [A Statistical Approach to Assessing Neural Network Robustness](https://mlsanity.com/paper/1811.07209/) (2018)
- [Robustness of Neural Networks: A Probabilistic and Practical Approach](https://mlsanity.com/paper/1902.05983/) (2019)
- [Verifying Learning-Based Robotic Navigation Systems](https://mlsanity.com/paper/2205.13536/) (2022)
- [Provably Bounding Neural Network Preimages](https://mlsanity.com/paper/2302.01404/) (2023)
- [CC-Cert: A Probabilistic Approach to Certify General Robustness of Neural Networks](https://mlsanity.com/paper/2109.10696/) (2021)
- [The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural Networks](https://mlsanity.com/paper/2301.07068/) (2023)
- [Enumerating Safe Regions in Deep Neural Networks with Provable Probabilistic Guarantees](https://mlsanity.com/paper/2308.09842/) (2023)
- [Make Sure You're Unsure: A Framework for Verifying Probabilistic Specifications](https://mlsanity.com/paper/2102.09479/) (2021)
- [Towards Hierarchical Task Decomposition using Deep Reinforcement Learning for Pick and Place Subtasks](https://mlsanity.com/paper/2102.04022/) (2021)
- [Provable Preimage Under-Approximation for Neural Networks (Full Version)](https://mlsanity.com/paper/2305.03686/) (2023)

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

- [Exact Verification of Graph Neural Networks with Incremental Constraint Solving](https://mlsanity.com/paper/2508.09320/) (2025)
- [A Survey on the Verification of Reinforcement Learning Policies](https://mlsanity.com/paper/2607.16210/) (2026)

## Abstract (arXiv)

We present Probabilistically Tightened Linear Relaxation-based Perturbation Analysis (textttPT-LiRPA), a novel framework that combines over-approximation techniques from LiRPA-based approaches with a sampling-based method to compute tight intermediate reachable sets. In detail, we show that with negligible computational overhead, textttPT-LiRPA exploiting the estimated reachable sets, significantly tightens the lower and upper linear bounds of a neural network's output, reducing the computational cost of formal verification tools while providing probabilistic guarantees on verification soundness. Extensive experiments on standard formal verification benchmarks, including the International Verification of Neural Networks Competition, show that our textttPT-LiRPA-based verifier improves robustness certificates, i.e., the certified lower bound of varepsilon perturbation tolerated by the models, by up to 3.31X and 2.26X compared to related work. Importantly, our probabilistic approach results in a valuable solution for challenging competition entries where state-of-the-art formal verification methods fail, allowing us to provide answers with high confidence (i.e., at least 99%).