# Scaling #DNN-Verification Tools with Efficient Bound Propagation and Parallel Computing

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 21 of its 31 references that are in the map.
- First posted on arXiv 10 Dec 2023.

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

- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [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)
- [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)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Efficient Formal Safety Analysis of Neural Networks](https://mlsanity.com/paper/1809.08098/) (2018)
- [The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results](https://mlsanity.com/paper/2109.00498/) (2021)
- [Quantitative Verification of Neural Networks And its Security Applications](https://mlsanity.com/paper/1906.10395/) (2019)
- [Verifying Learning-Based Robotic Navigation Systems](https://mlsanity.com/paper/2205.13536/) (2022)
- [Safe Reinforcement Learning using Formal Verification for Tissue Retraction in Autonomous Robotic-Assisted Surgery](https://mlsanity.com/paper/2109.02323/) (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)
- [BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networks](https://mlsanity.com/paper/2103.07224/) (2021)
- [Towards Hierarchical Task Decomposition using Deep Reinforcement Learning for Pick and Place Subtasks](https://mlsanity.com/paper/2102.04022/) (2021)
- [Centralizing State-Values in Dueling Networks for Multi-Robot Reinforcement Learning Mapless Navigation](https://mlsanity.com/paper/2112.09012/) (2021)
- [Curriculum Learning for Safe Mapless Navigation](https://mlsanity.com/paper/2112.12490/) (2021)
- [Safe Deep Reinforcement Learning by Verifying Task-Level Properties](https://mlsanity.com/paper/2302.10030/) (2023)
- [Constrained Reinforcement Learning and Formal Verification for Safe Colonoscopy Navigation](https://mlsanity.com/paper/2303.03207/) (2023)
- [Online Safety Property Collection and Refinement for Safe Deep Reinforcement Learning in Mapless Navigation](https://mlsanity.com/paper/2302.06695/) (2023)

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

- [Solving Probabilistic Verification Problems of Neural Networks using Branch and Bound](https://mlsanity.com/paper/2405.17556/) (2024)

## Abstract (arXiv)

Deep Neural Networks (DNNs) are powerful tools that have shown extraordinary results in many scenarios, ranging from pattern recognition to complex robotic problems. However, their intricate designs and lack of transparency raise safety concerns when applied in real-world applications. In this context, Formal Verification (FV) of DNNs has emerged as a valuable solution to provide provable guarantees on the safety aspect. Nonetheless, the binary answer (i.e., safe or unsafe) could be not informative enough for direct safety interventions such as safety model ranking or selection. To address this limitation, the FV problem has recently been extended to the counting version, called #DNN-Verification, for the computation of the size of the unsafe regions in a given safety property's domain. Still, due to the complexity of the problem, existing solutions struggle to scale on real-world robotic scenarios, where the DNN can be large and complex. To address this limitation, inspired by advances in FV, in this work, we propose a novel strategy based on reachability analysis combined with Symbolic Linear Relaxation and parallel computing to enhance the efficiency of existing exact and approximate FV for DNN counters. The empirical evaluation on standard FV benchmarks and realistic robotic scenarios shows a remarkable improvement in scalability and efficiency, enabling the use of such techniques even for complex robotic applications.