# Scalable Quantitative Verification For Deep Neural Networks

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

## Key facts

- Cited by 31 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 17 Feb 2020.

## Built on by (most cited first, 30 of 31)

- [BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networks](https://mlsanity.com/paper/2103.07224/) (2021)
- [NLP Verification: Towards a General Methodology for Certifying Robustness](https://mlsanity.com/paper/2403.10144/) (2024)
- [Provable Preimage Under-Approximation for Neural Networks (Full Version)](https://mlsanity.com/paper/2305.03686/) (2023)
- [Towards Practical Robustness Analysis for DNNs based on PAC-Model Learning](https://mlsanity.com/paper/2101.10102/) (2021)
- [QVIP: An ILP-based Formal Verification Approach for Quantized Neural Networks](https://mlsanity.com/paper/2212.11138/) (2022)
- [Certifying Counterfactual Bias in LLMs](https://mlsanity.com/paper/2405.18780/) (2024)
- [QEBVerif: Quantization Error Bound Verification of Neural Networks](https://mlsanity.com/paper/2212.02781/) (2022)
- [Provably Tightest Linear Approximation for Robustness Verification of Sigmoid-like Neural Networks](https://mlsanity.com/paper/2208.09872/) (2022)
- [TrajPAC: Towards Robustness Verification of Pedestrian Trajectory Prediction Models](https://mlsanity.com/paper/2308.05985/) (2023)
- [PREMAP: A Unifying PREiMage APproximation Framework for Neural Networks](https://mlsanity.com/paper/2408.09262/) (2024)
- [Requirements Engineering for Machine Learning: A Review and Reflection](https://mlsanity.com/paper/2210.00859/) (2022)
- [ANTONIO: Towards a Systematic Method of Generating NLP Benchmarks for Verification](https://mlsanity.com/paper/2305.04003/) (2023)
- [When to Trust AI: Advances and Challenges for Certification of Neural Networks](https://mlsanity.com/paper/2309.11196/) (2023)
- [Probabilistic Robustness in Deep Learning: A Concise yet Comprehensive Guide](https://mlsanity.com/paper/2502.14833/) (2025)
- [Secure and Trustworthy Artificial Intelligence-Extended Reality (AI-XR) for Metaverses](https://mlsanity.com/paper/2210.13289/) (2022)
- [A Survey of Neural Network Robustness Assessment in Image Recognition](https://mlsanity.com/paper/2404.08285/) (2024)
- [Incremental Satisfiability Modulo Theory for Verification of Deep Neural Networks](https://mlsanity.com/paper/2302.06455/) (2023)
- [Towards Regulatable AI Systems: Technical Gaps and Policy Opportunities](https://mlsanity.com/paper/2306.12609/) (2023)
- [Scalable and Modular Robustness Analysis of Deep Neural Networks](https://mlsanity.com/paper/2108.11651/) (2021)
- [gRoMA: a Tool for Measuring the Global Robustness of Deep Neural Networks](https://mlsanity.com/paper/2301.02288/) (2023)
- [Certifying Knowledge Comprehension in LLMs](https://mlsanity.com/paper/2402.15929/) (2024)
- [PRBench: A Standardized Probabilistic Robustness Benchmark](https://mlsanity.com/paper/2511.01724/) (2025)
- [Non-Parametric Probabilistic Robustness: A Conservative Risk Estimator under Unknown Perturbation Distributions](https://mlsanity.com/paper/2511.17380/) (2025)
- [Propagation of~Interval Belief Structures and~Imprecise Copulas for~Neural Network Verification](https://mlsanity.com/paper/2606.30105/) (2026)
- [Meta Pattern Concern Score: A Novel Evaluation Measure with Human Values for Multi-classifiers](https://mlsanity.com/paper/2209.06408/) (2022)
- [Taming Reachability Analysis of DNN-Controlled Systems via Abstraction-Based Training](https://mlsanity.com/paper/2211.11127/) (2022)
- [Understanding the Complexity and Its Impact on Testing in ML-Enabled Systems](https://mlsanity.com/paper/2301.03837/) (2023)
- [Verified Compositional Neuro-Symbolic Control for Stochastic Systems with Temporal Logic Tasks](https://mlsanity.com/paper/2311.10863/) (2023)
- [Patch Synthesis for Property Repair of Deep Neural Networks](https://mlsanity.com/paper/2404.01642/) (2024)
- [Probably Approximately Global Robustness Certification](https://mlsanity.com/paper/2511.06495/) (2025)

## Abstract (arXiv)

Despite the functional success of deep neural networks (DNNs), their trustworthiness remains a crucial open challenge. To address this challenge, both testing and verification techniques have been proposed. But these existing techniques provide either scalability to large networks or formal guarantees, not both. In this paper, we propose a scalable quantitative verification framework for deep neural networks, i.e., a test-driven approach that comes with formal guarantees that a desired probabilistic property is satisfied. Our technique performs enough tests until soundness of a formal probabilistic property can be proven. It can be used to certify properties of both deterministic and randomized DNNs. We implement our approach in a tool called PROVERO and apply it in the context of certifying adversarial robustness of DNNs. In this context, we first show a new attack-agnostic measure of robustness which offers an alternative to purely attack-based methodology of evaluating robustness being reported today. Second, PROVERO provides certificates of robustness for large DNNs, where existing state-of-the-art verification tools fail to produce conclusive results. Our work paves the way forward for verifying properties of distributions captured by real-world deep neural networks, with provable guarantees, even where testers only have black-box access to the neural network.