2021/02/18 by Leonard Berrada, Berrada, Leonard, Sumanth Dathathri +14 · 1 citation
Computer Science · Engineering · #Adversarial Robustness in Machine Learning #Explainable Artificial Intelligence (XAI) #Fault Detection and Control Systems
paper · pdf · doi:10.48550/arxiv.2102.09479
Most real world applications require dealing with stochasticity like sensor\nnoise or predictive uncertainty, where formal specifications of desired\nbehavior are inherently probabilistic. Despite the promise of formal\nverification in ensuring the reliability of neural networks, progress in the\ndirection of probabilistic specifications has been limited. In this direction,\nwe first introduce a general formulation of probabilistic specifications for\nneural networks, which captures both probabilistic networks (e.g., Bayesian\nneural networks, MC-Dropout networks) and uncertain inputs (distributions over\ninputs arising from sensor noise or other perturbations). We then propose a\ngeneral technique to verify such specifications by generalizing the notion of\nLagrangian duality, replacing standard Lagrangian multipliers with "functional\nmultipliers" that can be arbitrary functions of the activations at a given\nlayer. We show that an optimal choice of functional multipliers leads to exact\nverification (i.e., sound and complete verification), and for specific forms of\nmultipliers, we develop tractable practical verification algorithms.\n We empirically validate our algorithms by applying them to Bayesian Neural\nNetworks (BNNs) and MC Dropout Networks, and certifying properties such as\nadversarial robustness and robust detection of out-of-distribution (OOD) data.\nOn these tasks we are able to provide significantly stronger guarantees when\ncompared to prior work -- for instance, for a VGG-64 MC-Dropout CNN trained on\nCIFAR-10, we improve the certified AUC (a verified lower bound on the true AUC)\nfor robust OOD detection (on CIFAR-100) from 0 % \→ 29 %. Similarly,\nfor a BNN trained on MNIST, we improve on the robust accuracy from 60.2 %\n\→ 74.6 %. Further, on a novel specification -- distributionally\nrobust OOD detection -- we improve the certified AUC from 5 % \→\n23 %.\n