Towards Practical Verification of Machine Learning: The Case of Computer Vision Systems

By Kexin Pei, Yinzhi Cao, Junfeng Yang, Suman Sekhar Jana. 2017

108 citations recorded by the source corpus.

Due to the increasing usage of machine learning (ML) techniques in security- and safety-critical domains, such as autonomous systems and medical diagnosis, ensuring correct behavior of ML systems, especially for different corner cases, is of growing importance. In this paper, we propose a generic framework for evaluating security and robustness of ML systems using different real-world safety properties. We further design, implement and evaluate VeriVis, a scalable methodology that can verify a diverse set of safety properties for state-of-the-art computer vision systems with only blackbox access. VeriVis leverage different input space reduction techniques for efficient verification of different safety properties. VeriVis is able to find thousands of safety violations in fifteen state-of-the-art computer vision systems including ten Deep Neural Networks (DNNs) such as Inception-v3 and Nvidia's Dave self-driving system with thousands of neurons as well as five commercial third-party vision APIs including Google vision and Clarifai for twelve different safety properties. Furthermore, VeriVis can successfully verify local safety properties, on average, for around 31.7% of the test images. VeriVis finds up to 64.8x more violations than existing gradient-based methods that, unlike VeriVis, cannot ensure non-existence of any violations. Finally, we show that retraining using the safety violations detected by VeriVis can reduce the average number of violations up to 60.2%.

Subfields: Artificial Intelligence, Computer Vision and Pattern Recognition, Safety, Robustness & Interpretability

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computer Vision and Pattern Recognition

In Safety, Robustness & Interpretability

Citations in the corpus

Risks from Learned Optimization in Advanced Machine Learning Systems (2019, methodology): “an SMT solver that in principle allows for verification of arbitrary propositions about activations in the network,[32] and black-box algorithms[33].”
A survey of safety and trustworthiness of deep neural networks: Verification, testing, adversarial attack and defence, and interpretability (2018, methodology): “Works like [Pei et al., 2017a, Guo et al., 2018] are in principle based on differential analysis of multiple DNNs, thus more than one DNN inputs are expected.”
DeepGauge: Multi-Granularity Testing Criteria for Deep Learning Systems (2018, methodology): “Formal methods can provide formal guarantees about safety and robustness of verified DL systems [22, 28, 39, 40, 50, 53].”
DeepHunter: a coverage-guided fuzz testing framework for deep neural networks (2019, background): “The reliability of DNNs has been investigated by recent work with formal guarantees [18, 25, 37, 39, 45, 47].”
Adversarial Examples on Object Recognition (2020, unknown): “[133] x x x *** ** *** * Rotation Tr.”
An abstract domain for certifying neural networks (2019, background): “This induces a new adversarial region Note that because we deal with regions (and not only concrete images) as well as rotations that employ linear interpolation, we cannot simply enumerate all possible rotations as done for simpler rotation algorithms and concrete images [Pei et al. 2017b].”
Invariance-inducing regularization using worst-case transformations suffices to boost accuracy and spatial robustness (2019, background): “g.[11, 13, 34, 20, 14, 2, 10]) that worst-case prediction performance drops dramatically for neural network classifiers obtained using standard training, even for rather small transformation sets.”
DeepMutation: Mutation Testing of Deep Learning Systems (2018, background): “such as theoretical aspects [52], [53], [54] of mutation testing, performance enhancement [55], [56], [57], [58], [15], platform and tool support [59], [60], [61], [27], as well as more general mutation testing applications for test generation [56], [62], [63], networks [64], [65].”