A High Parallelization Method for Automated Formal Verification of Deep Neural Networks
摘要
The verification of DNNs has garnered significant attention recently, especially with the growing willingness of their utilization in safety and security-critical applications. Due to the complexity and large size of such networks, ensuring guarantees about their behavior in an automated way remains a challenging task. Despite the challenges, achieving automated formal verification would represent an important step towards their wider adoption. In this paper, we consider the problem of formally verifying DNNs based on an optimized strategy that enables the combination and parallel invocation of a set of existing verification techniques. Our approach involves computing interval over-approximations of the output set for feed-forward neural networks with input uncertainty. We achieve such an over-approximation by leveraging various existing approaches and adapting bound reduction methods for the verification of some desired properties, e.g., robustness. In particular, we propose an automated approach that supports the formal verification of various types of DNN specifications with arbitrary, bounded, multivariate, linear, and non-linear activation functions. We report on the workflow of our approach process, its implementation in a framework, and provide an illustration of the technique using the DNN of the ACAS Xu benchmark pertaining to an Airborne Collision Avoidance System.