Improving abstract propagation for verification of neural networks

Formal verification of neural networks is a crucial technique to increase their dependability in safety critical applications. In this paper we address some scalability challenges in our verification tool NEVER2 by proposing strategies to enhance speed and overall performances. First, we apply a precomputation technique based on symbolic bounds propagation in order to improve the network analysis by determining neuron stability a priori. Second, we combine the strengths of different levels of abstraction towards a refinement strategy. We experiment with the proposed techniques on some verification benchmarks from the annual competition of verification tools for neural networks (VNN-COMP).