Deep neural networks are successful in various tasks but are also susceptible to adversarial examples: malicious input perturbations designed to deceive the network. Many adversarial attacks on image classifiers involve making imperceptible changes bounded by a small ε with respect to an Lₚ norm (e.g., p = 0, 1, 2, ∞), by a small interval neighborhood, or by semantic feature perturbations, such as adjustments in brightness, translation, or rotation. To understand the robustness of a DNN to adversarial examples, most existing works propose to analyze the network's local robustness of a given ε-ball. Despite the significant progress in their efficiency and precision, existing verifiers of ε-ball neighborhoods are limited to verifying small neighborhoods and most of them do not provide global guarantees. In our thesis, we propose several verifiers of different kinds of robustness properties for neural networks: a verifier for computing maximally locally robust interval neighborhoods, a verifier for computing maximally locally robust feature neighborhoods, a verifier for computing global robustness guarantees to different kinds of perturbations, a system relying on global robustness verification to protect the privacy of neural networks' training sets, and a system relying on global robustness verification to provide formal guarantees over the reliability of neural network quantization schemes.
Anan is a PhD student supervised by Prof. Dana Drachsler Cohen.
