This paper proposes a novel, abstraction-based, certified training method for robust image classifiers. Via abstraction, all perturbed images are mapped into intervals before feeding into neural networks for training. By training on intervals, all the perturbed images that are mapped to the same interval are classified as the same label, rendering the variance of training sets to be small and the loss landscape of the models to be smooth. Consequently, our approach significantly improves the robustness of trained models. For the abstraction, our training method also enables a sound and complete black-box verification approach, which is orthogonal and scalable to arbitrary types of neural networks regardless of their sizes and architectures. We evaluate our method on a wide range of benchmarks in different scales. The experimental results show that our method outperforms state of the art by (i) reducing the verified errors of trained models up to 95.64%; (ii) totally achieving up to 602.50x speedup; and (iii) scaling up to larger models with up to 138 million trainable parameters. The demo is available at https://github.com/zhangzhaodi233/ABSCERT.git.

The robustness of deep neural networks (DNNs) is crucial to the hosting system’s reliability and security. Formal verification has been demonstrated to be effective in providing provable robustness guarantees. To improve its scalability, over-approximating the non-linear activation functions in DNNs by linear constraints has been widely adopted, which transforms the verification problem into an efficiently solvable linear programming problem. Many efforts have been dedicated to defining the so-called tightest approximations to reduce overestimation imposed by over-approximation. In this paper, we study existing approaches and identify a dominant factor in defining tight approximation, namely the approximation domain of the activation function. We find out that tight approximations defined on approximation domains may not be as tight as the ones on their actual domains, yet existing approaches all rely only on approximation domains. Based on this observation, we propose a novel dual-approximation approach to tighten overapproximations, leveraging an activation function’s underestimated domain to define tight approximation bounds. We implement our approach with two complementary algorithms based respectively on Monte Carlo simulation and gradient descent into a tool called DualApp. We assess it on a comprehensive benchmark of DNNs with different architectures. Our experimental results show that DualApp significantly outperforms the state-of-the-art approaches with 100% − 1000% improvement on the verified robustness ratio and 10.64% on average (up to 66.53%) on the certified lower bound.

With the applications of deep learning in safety-critical domains such as autonomous driving systems gaining ground, it demands rigorous verification to guarantee the safety and reliability of corresponding systems. As the intelligent component in such systems, neural networks (NNs) must be robust in that their outputs are not affected by minor perturbation to inputs. Many research studies have shown that formal methods are effective ways to the robustness verification of NNs. However, most of the existing approaches are focused on NNs that contain monotonic activation functions, such as ReLU, Tanh, and Sigmoid. In this work, we propose an approach to verify the robustness of NNs with the nonmonotonic activation function called Swish. Such networks have been proved to have a better performance on image classification than other NNs. In our approach, we turn the robustness verification problem into a constraint-solving problem using the linear approximation technique. We first model the affine function of an NN into a linear constraint model. Then, for nonlinear activation functions, we leverage an efficient approximation strategy to linearly approximate them. Finally, we utilize the constraint solver gurobi to solve the model, which reveals that the model satisfies the robustness property. We develop a prototype tool and evaluate it with open-sourced NNs. Experimental results showed the effectiveness and efficiency of our approach.

The robustness of deep neural networks is crucial to modern AI-enabled systems and should be formally verified. Sigmoid-like neural networks have been adopted in a wide range of applications. Due to their non-linearity, Sigmoid-like activation functions are usually over-approximated for efficient verification, which inevitably introduces imprecision. Considerable efforts have been devoted to finding the so-called tighter approximations to obtain more precise verification results. However, existing tightness definitions are heuristic and lack theoretical foundations. We conduct a thorough empirical analysis of existing neuron-wise characterizations of tightness and reveal that they are superior only on specific neural networks. We then introduce the notion of network-wise tightness as a unified tightness definition and show that computing network-wise tightness is a complex non-convex optimization problem. We bypass the complexity from different perspectives via two efficient, provably tightest approximations. The results demonstrate the promising performance achievement of our approaches over state of the art: (i) achieving up to 251.28% improvement to certified lower robustness bounds; and (ii) exhibiting notably more precise verification results on convolutional networks.

Abstract In the Internet of Things, smart devices are expected to correctly capture and process data from environments, regardless of perturbation and adversarial attacks. Therefore, it is important to guarantee the robustness of their intelligent components, e.g. neural networks, to protect the system from environment perturbation and adversarial attacks. In this paper, we propose a formal verification technique for rigorously proving the robustness of neural networks. Our approach leverages a tight liner approximation technique and constraint substitution, by which we transform the robustness verification problem into an efficiently solvable linear programming problem. Unlike existing approaches, our approach can automatically generate adversarial examples when a neural network fails to verify. Besides, it is general and applicable to more complex neural network architectures such as CNN, LeNet and ResNet. We implement the approach in a prototype tool called WiNR and evaluate it on extensive benchmarks, including Fashion MNIST, CIFAR10 and GTSRB. Experimental results show that WiNR can verify neural networks that contain over 10 000 neurons on one input image in a minute with a 6.28% probability of false positive on average.

Formal robustness verification of deep neural networks (DNNs) is a promising approach for achieving a provable reliability guarantee to AI-enabled software systems. Limited scalability is one of the main obstacles to the verification problem. In this paper, we propose eager falsification to accelerate the robustness verification of DNNs. It divides the verification problem into a set of independent subproblems and solves them in descending order of their falsification probabilities. Once a subproblem is falsified, the verification terminates with a conclusion that the network is not robust. We introduce a notion of label affinity to measure the falsification probability and present an approach to computing the probability based on symbolic interval propagation. Our approach is orthogonal to existing verification techniques. We integrate it into four state-of-the-art verification tools, i.e., MIPVerify, Neurify, DeepZ, and DeepPoly, and conduct extensive experiments on 8 benchmark datasets. The experimental results show that our approach can significantly improve these tools by up to 200x speedup when the perturbation distance is in a reasonable range.