The ability to deploy neural networks in real-world, safety-critical systems is severely limited by the presence of adversarial examples: slightly perturbed inputs that are misclassified by the network. In recent years, several techniques have been proposed for training networks that are robust to such examples; and each time stronger attacks have been devised, demonstrating the shortcomings of existing defenses. This highlights a key difficulty in designing an effective defense: the inability to assess a network's robustness against future attacks. We propose to address this difficulty through formal verification techniques. We construct ground truths: adversarial examples with a provably-minimal distance from a given input point. We demonstrate how ground truths can serve to assess the effectiveness of attack techniques, by comparing the adversarial examples produced by those attacks to the ground truths; and also of defense techniques, by computing the distance to the ground truths before and after the defense is applied, and measuring the improvement. We use this technique to assess recently suggested attack and defense techniques.

We use formal verification to assess the effectiveness of techniques for finding adversarial examples or for defending against adversarial examples. This paper proposes a method for computing adversarial examples with minimum distance to the original inputs. The authors propose to employ provably minimal-distance examples as a tool to evaluate the robustness of a trained network. The paper describes a method for generating adversarial examples that have minimal distance to the training example used to generate them