DeepCert: Verification of Contextually Relevant Robustness for Neural Network Image Classifiers

We introduce DeepCert, a tool-supported method for verifying the robustness\nof deep neural network (DNN) image classifiers to contextually relevant\nperturbations such as blur, haze, and changes in image contrast. While the\nrobustness of DNN classifiers has been the subject of intense research in\nrecent years, the solutions delivered by this research focus on verifying DNN\nrobustness to small perturbations in the images being classified, with\nperturbation magnitude measured using established Lp norms. This is useful for\nidentifying potential adversarial attacks on DNN image classifiers, but cannot\nverify DNN robustness to contextually relevant image perturbations, which are\ntypically not small when expressed with Lp norms. DeepCert addresses this\nunderexplored verification problem by supporting:(1) the encoding of real-world\nimage perturbations; (2) the systematic evaluation of contextually relevant DNN\nrobustness, using both testing and formal verification; (3) the generation of\ncontextually relevant counterexamples; and, through these, (4) the selection of\nDNN image classifiers suitable for the operational context (i)envisaged when a\npotentially safety-critical system is designed, or (ii)observed by a deployed\nsystem. We demonstrate the effectiveness of DeepCert by showing how it can be\nused to verify the robustness of DNN image classifiers build for two benchmark\ndatasets (`German Traffic Sign' and `CIFAR-10') to multiple contextually\nrelevant perturbations.\n