# DISCO Verification: Division of Input Space into COnvex polytopes for neural network verification

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 15 of its 29 references that are in the map.
- First posted on arXiv 17 May 2021.

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

- [Membership Inference Attacks against Machine Learning Models](https://mlsanity.com/paper/1610.05820/) (2016)
- [Robustness May Be at Odds with Accuracy](https://mlsanity.com/paper/1805.12152/) (2018)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Stealing Machine Learning Models via Prediction APIs](https://mlsanity.com/paper/1609.02943/) (2016)
- [Transferability in Machine Learning: from Phenomena to Black-Box Attacks using Adversarial Samples](https://mlsanity.com/paper/1605.07277/) (2016)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Complexity of Linear Regions in Deep Networks](https://mlsanity.com/paper/1901.09021/) (2019)
- [Bounding and Counting Linear Regions of Deep Neural Networks](https://mlsanity.com/paper/1711.02114/) (2017)
- [Deep ReLU Networks Have Surprisingly Few Activation Patterns](https://mlsanity.com/paper/1906.00904/) (2019)
- [ShapeShifter: Robust Physical Adversarial Attack on Faster R-CNN Object Detector](https://mlsanity.com/paper/1804.05810/) (2018)
- [Imperceptible, Robust, and Targeted Adversarial Examples for Automatic Speech Recognition](https://mlsanity.com/paper/1903.10346/) (2019)
- [Provable Robustness of ReLU networks via Maximization of Linear Regions](https://mlsanity.com/paper/1810.07481/) (2018)
- [CNN-Cert: An Efficient Framework for Certifying Robustness of Convolutional Neural Networks](https://mlsanity.com/paper/1811.12395/) (2018)
- [Universal Approximation with Certified Networks](https://mlsanity.com/paper/1909.13846/) (2019)

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

- [Sound and Complete Neural Network Repair with Minimality and Locality Guarantees](https://mlsanity.com/paper/2110.07682/) (2021)

## Abstract (arXiv)

The impressive results of modern neural networks partly come from their non linear behaviour. Unfortunately, this property makes it very difficult to apply formal verification tools, even if we restrict ourselves to networks with a piecewise linear structure. However, such networks yields subregions that are linear and thus simpler to analyse independently. In this paper, we propose a method to simplify the verification problem by operating a partitionning into multiple linear subproblems. To evaluate the feasibility of such an approach, we perform an empirical analysis of neural networks to estimate the number of linear regions, and compare them to the bounds currently known. We also present the impact of a technique aiming at reducing the number of linear regions during training.