DISCO Verification: Division of Input Space into COnvex polytopes for neural network verification
This work addresses the problem of formal verification for neural networks, which is crucial for safety-critical applications, but it appears incremental as it builds on existing partitioning methods.
The paper tackles the difficulty of verifying neural networks due to their nonlinear behavior by partitioning the input space into convex polytopes to create linear subproblems for analysis, and it empirically analyzes linear region counts and compares them to known bounds while exploring training techniques to reduce these regions.
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.