Verification-Friendly Deep Neural Networks
Anahita Baninajjar Ahmed Rezine Amir Aminifar
Machine learning techniques often lack formal correctness guarantees. This is
evidenced by the widespread adversarial examples that plague most deep-learning
applications. This resulted in several research efforts that aim at verifying
deep neural networks, with a particular focus on safety-critical applications.
However, formal verification techniques still face major scalability and
precision challenges when dealing with the complexity of such networks. 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 robustness in
the resulting networks. Our proposed framework proves to result in networks
that are comparable to the original ones in terms of prediction performance,
while amenable to verification. This essentially enables us to establish
robustness for more VNNs than their deep neural network counterparts, in a more
time-efficient manner.