VNN: Verification-Friendly Neural Networks with Hard Robustness Guarantees
This work addresses the problem of providing formal correctness guarantees for safety-critical applications in machine learning, though it is incremental as it builds on existing verification techniques.
The paper tackles the challenge of formal verification for deep neural networks, which often suffers from scalability and precision issues, by proposing a post-training optimization framework that generates verification-friendly neural networks (VNNs) with comparable prediction performance, enabling more robust and time-efficient verification.
Machine learning techniques often lack formal correctness guarantees, evidenced by the widespread adversarial examples that plague most deep-learning applications. This lack of formal guarantees resulted in several research efforts that aim at verifying Deep Neural Networks (DNNs), with a particular focus on safety-critical applications. However, formal verification techniques still face major scalability and precision challenges. The over-approximation introduced during the formal verification process to tackle the scalability challenge often results in inconclusive analysis. To address this challenge, we propose a novel framework to generate Verification-Friendly Neural Networks (VNNs). We present a post-training optimization framework to achieve a balance between preserving prediction performance and verification-friendliness. Our proposed framework results in VNNs that are comparable to the original DNNs in terms of prediction performance, while amenable to formal verification techniques. This essentially enables us to establish robustness for more VNNs than their DNN counterparts, in a time-efficient manner.