REAL-TIME Certification of robustness for AE-DNNs with the Diff MILP Model

Deep neural networks (DNNs) are often brittle to small perturbations, which has led to extensive research to certify their robustness. Most existing methods focus on _local_ robustness, i.e., in the neighborhood of fixed specific inputs. However, these techniques are often impractical for guaranteeing robustness to _real-time_ inputs on embedded systems, due to excessive latency and computational cost. To tackle real-time certification, we proceed in two steps. First, offline, we solve _global_ robustness problems, which are significantly more complex than local robustness. Namely, we compute _bounds_ on the difference of output values across different DNN decision classes under both $L_{\infty }$- _and_ $L_1$-perturbations. We then use the results online to perform real-time certification. On vanilla DNNs, however, global bounds are deemed overly pessimistic, because of inputs that are not In Distribution (ID). We propose alternative "AE-DNNs" to vanilla DNNs to use in exploitation, projecting inputs on an AutoEncoder (AE) latent space learnt from ID samples. With a sufficiently large latent space, ID inputs are only changed slightly and (Linear) AE-DNNs accuracy is close to Vanilla DNNs, with much smaller (3-15x) global bounds than Vanilla DNNs. To compute these bounds accurately, we develop novel _Diff_ MILP models, explicitly representing the small differential variables between the input and its perturbation, instead of implicitly representing them as differences between 2 larger values (standard MILP encoding). Online, our method certifies in real-time over 70% of incoming images for AE-DNNs used _in exploitation_, across standard benchmarks (MNIST, Fashion MNIST and CIFAR-10), with $L_1$-perturbations of $1,4,2$, respectively, requiring only 0.5 ms of latency on a single CPU core.