The deployment pipeline of deep neural networks (DNNs) in safety-critical settings involves formally verifying their trustworthiness. Domain experts design a large number of specifications (~10-100K), typically defined for inputs in the test set, to cover DNN behavior under diverse real-world scenarios. If the DNN is proved to be trustworthy, then it can be deployed. Otherwise, it is repaired or retrained. While there has been a lot of work in recent years on developing precise and scalable DNN verifiers, existing verifiers are inefficient when applied inside the deployment pipeline. This inefficiency is because the verifier needs to be run from scratch for every new specification and DNN.

The increasing prevalence of neural networks (NNs) in safety-critical applications calls for methods to certify their behavior and guarantee safety. This paper presents a backward reachability approach for safety verification of neural feedback loops (NFLs), i.e., closed-loop systems with NN control policies. While recent works have focused on forward reachability as a strategy for safety certification of NFLs, backward reachability offers advantages over the forward strategy, particularly in obstacle avoidance scenarios. Prior works have developed techniques for backward reachability analysis for systems without NNs, but the presence of NNs in the feedback loop presents a unique set of problems due to the nonlinearities in their activation functions and because NN models are generally not invertible. To overcome these challenges, we use existing forward NN analysis tools to find affine bounds on the control inputs and solve a series of linear programs (LPs) to efficiently find an approximation of the backprojection (BP) set, i.e., the set of states for which the NN control policy will drive the system to a given target set. We present an algorithm to iteratively find BP set estimates over a given time horizon and demonstrate the ability to reduce conservativeness in the BP set estimates by up to 88\% with low additional computational cost. We use numerical results from a double integrator model to verify the efficacy of these algorithms and demonstrate the ability to certify safety for a linearized ground robot model in a collision avoidance scenario where forward reachability fails.

We present NN4SysBench, a benchmark suite for neural network verification, comprised of benchmarks from neural networks for systems (or NN4Sys). NN4Sys is booming: there are hundreds of proposals of using neural networks in computer systems—databases, OSes, and networked systems—that are safety critical. We observe that NN4Sys has some unique characteristics that to- day’s neural network verification tools overlooked. This benchmark aims at bridging the gap between NN4Sys and NN-verification by tailoring impactful NN4Sys instances to benchmarks that today’s NN-verification tools can work on.

As AI/ML-based systems are deployed in increasingly autonomous and safety-critical applications, there is increasing concern for many reasons about the behaviors of the ML in the wild, perhaps most of all because the problems for which ML is applied are so complex that it’s not possible to know in all cases what the ML will do. In this talk I will introduce the concept of undeterminism, extracted from my experience in developing techniques for communication protocol conformance testing, and argue that undeterminism yields inherent uncertainty. I show why systems cannot have certainty and ML simultaneously and that there is a clear set of tradeoffs that should guide research in formal methods for ML for the foreseeable future.

Can neural networks help us better exploit the inherent structure in the neural network verification problem? In this talk, I will present some recent efforts to speed-up formal verification of neural networks using deep learning. Specifically, we use deep learning to make branching decisions for branch-and-bound, compute descent directions for bound computation, and reduce the search space for counterexample generation. The common methodology behind all these approaches is a graph neural network (GNN) whose architecture closely resembles the network we wish to verify. Using shared parameters, the GNN can be trained on smaller networks and tested on larger ones. Using standard verification tasks, I will show some promising results for our approach.

In this talk, I will describe two recent Branch and Bound (BaB) verifiers developed by our group to ensure different safety properties of neural networks. The BaB verifiers involve two main steps: (1) recursively splitting the original verification problem into easier independent subproblems by splitting input or hidden neurons; and (2) for each split subproblem, using fast but incomplete bound propagation techniques to compute sound estimated bounds for the outputs of the target neural network. One of the key limitations of existing BaB verifiers is computing tight relaxations of activation functions' (i.e., ReLU) nonlinearities. Our recent works (α-CROWN and β-CROWN) introduce a primal-dual approach and jointly optimize the corresponding Lagrangian multipliers for each ReLU with gradient ascent. Such an approach is highly parallelizable and avoids calls to expensive LP solvers. Our verifiers not only provide tighter output estimations than existing bound propagation methods but also can fully leverage GPUs with massive parallelization. Our verifier, α, β-CROWN (alpha-beta-CROWN), won the second International Verification of Neural Networks Competition (VNN-COMP 2021) with the highest total score.

We need efficient computational methods with provable guarantees that can cope with the complex nature and high nonlinearity of many real-world systems. Practitioners often design heuristic algorithms tailored to specific applications, but the theoretical underpinnings of these methods remain a mystery, and this limits their usage in safety-critical systems. In this talk, we aim to address the above issue for some machine learning problems. First, we study the problem of certifying the robustness of neural networks against adversarial inputs. Then we study when simple local search algorithms could solve a class of nonlinear problems to global optimality. We discuss our recent results in addressing these problems and demonstrate them on tensor decomposition with outliers and video processing.

Recent works have tried to increase the verifiability of adversarially trained networks by running the attacks over domains larger than the original perturbations and adding various regularization terms to the objective. However, these algorithms either underperform or require complex and expensive stage-wise training procedures, hindering their practical applicability. We present IBP-R, a novel verified training algorithm that is both simple and effective. IBP-R induces network verifiability by coupling adversarial attacks on enlarged domains with a regularization term, based on inexpensive interval bound propagation, that minimizes the gap between the non-convex verification problem and its approximations. By leveraging recent branch-and-bound frameworks, we show that IBP-R obtains state-of-the-art verified robustness-accuracy trade-offs for small perturbations on CIFAR-10 while training significantly faster than relevant previous work. Additionally, we present UPB, a novel branching strategy that, relying on a simple heuristic based on $\beta$-CROWN, reduces the cost of state-of-the-art branching algorithms while yielding splits of comparable quality.

Data poisoning attacks aim at manipulating model behaviors through distorting training data. Previously, an aggregation-based certified defense, Deep Partition Aggregation (DPA), was proposed to mitigate this threat. DPA predicts through an aggregation of base classifiers trained on disjoint subsets of data, thus restricting its sensitivity to dataset distortions. In this work, we propose an improved certified defense against general poisoning attacks, namely Finite Aggregation. In contrast to DPA, which directly splits the training set into disjoint subsets, our method first splits the training set into smaller disjoint subsets and then combines duplicates of them to build larger (but not disjoint) subsets for training base classifiers. This reduces the worst-case impacts of poison samples and thus improves certified robustness bounds. In addition, we offer an alternative view of our method, bridging the designs of deterministic and stochastic aggregation-based certified defenses. Empirically, our proposed Finite Aggregation consistently improves certificates on MNIST, CIFAR-10, and GTSRB, boosting certified fractions by up to 3.05%, 3.87% and 4.77%, respectively, while keeping the same clean accuracies as DPA's, effectively establishing a new state of the art in (pointwise) certified robustness against data poisoning.

In this talk, I will discuss how algorithms for neural network verification can be used to solve robotics problems. I will first introduce our toolbox NeuralVerification.jl, followed by the discussion of two applications. The first is to build verified models for human behavior prediction in human-robot systems. The second is to develop safe controllers for dynamic models encoded in deep neural networks. To support real-time computation in robotics tasks, I will also discuss potential approaches to speed up the computation of the verification algorithms.

Randomized smoothing is a leading approach to producing certifiably robust classifiers. The goal of optimal randomized smoothing is to maximize the average certified radius over the space of smoothing distributions. We theoretically study this problem through the lens of infinite-dimensional optimization over measure spaces, and prove that the nonconvex infinite program is lower-bounded by a conic linear program wherein the classifier's confidence acts as a surrogate objective to optimize. A semi-infinite linear programming approximation to the problem is presented, whose sub-problems are proven to attain nontrivial strong duality. A proof-of-concept experiment demonstrates the effectiveness of the proposed approach.

A variety of methods have been proposed to try to explain how deep neural networks make their decisions. Key to those approaches is the need to sample the pixel space efficiently in order to derive importance maps. However, it has been shown that the sampling methods used to date introduce biases and other artifacts, leading to inaccurate estimates of the importance of individual pixels and severely limit the reliability of current explainability methods. Unfortunately, the alternative -- to exhaustively sample the image space is computationally prohibitive. In this paper, we introduce EVA (Explaining using Verified perturbation Analysis) -- the first explainability method guarantee to have an exhaustive exploration of a perturbation space. Specifically, we leverage the beneficial properties of verified perturbation analysis -- time efficiency, tractability and guaranteed complete coverage of a manifold -- to efficiently characterize the input variables that are most likely to drive the model decision. We evaluate the approach systematically and demonstrate state-of-the-art results on multiple benchmarks.

In recent years, a multitude of approaches to certify the prediction of neural networks have been proposed.Classically, complete verification techniques struggle with large networks as the combinatorial space grows exponentially, implying that realistic networks are difficult to be verified.In this paper, we propose a new hybrid approach to the robustness verification of ReLU networks with quantum computers.By applying Benders decomposition, the verification problem is split into a quadratic unconstrained binary optimization and a linear program which are solved by quantum and classical computers, respectively.Further, we improve existing hybrid methods based on the Benders decomposition by reducing the overall number of iterations and placing a limit on the maximum number of qubits required.We show that, in a simulated environment, our certificate is sound, and provide bounds on the minimum number of qubits necessary to obtain a reasonable approximation.

It has increasingly been recognised that verification can contribute to the validation and debugging of neural networks before deployment, particularly in safety-critical areas. While considerable progress has been made in recent years, present techniques still do not scale to large architectures used in many applications. In this paper we show that substantial gains can be obtained by employing Parametric ReLU activation functions in lieu of plain ReLU functions. We give training procedures that produce networks which achieve one order of magnitude gain in verification overheads and 30-100% fewer timeouts with an SoA Symbolic Interval Propagation-based verification toolkit, while not compromising the resulting accuracy. Furthermore, we show that adversarial training combined with our approach improves certified robustness up to 36% compared to adversarial training performed on baseline ReLU networks.

Cloud based machine learning inference is an emerging paradigm where users share their data with a service provider. Due to increased concerns over data privacy, several recent works have proposed using Adversarial Representation Learning (ARL) to learn a privacy-preserving encoding of sensitive user data before it is shared with an untrusted service provider. Traditionally, the privacy of these encodings is evaluated empirically as they lack formal guarantees. In this work, we develop a framework that provides formal privacy guarantees for an arbitrarily trained neural network by linking its local Lipschitz constant with its local sensitivity. To use local sensitivity for guaranteeing privacy, we extend the Propose-Test-Release~(PTR) framework to make it compatible and tractable for neural network based queries. We verify the efficacy of our framework on real world datasets, and elucidate the role of ARL in improving the privacy-utility tradeoff.

Randomized smoothing is sound when using infinite precision. However, we show that randomized smoothing is no longer sound for limited floating-point precision. We present a simple example where randomized smoothing certifies a radius of $1.26$ around a point, even though there is an adversarial example in the distance $0.8$ and extend this example further to provide false certificates for CIFAR10. We discuss the implicit assumptions of randomized smoothing and show that they do not apply to generic image classification models whose smoothed versions are commonly certified. In order to overcome this problem, we propose a sound approach to randomized smoothing when using floating-point precision with essentially equal speed and matching the certificates of the standard, unsound practice for standard classifiers tested so far. Our only assumption is that we have access to a fair coin.

Neural networks are increasingly applied in safety critical domains, their verification thus is gaining importance.A large class of recent algorithms for proving input-output relations offeed-forward neural networks are based on linear relaxations andsymbolic interval propagation. However, due to variable dependencies, theapproximations deteriorate with increasing depth of the network.In this paper we present DPNeurifyFV, a novel branch-and-bound solver for ReLU networks with low dimensional input-space that is based on symbolic interval propagation with fresh variables and input-splitting.A new heuristic for choosing the fresh variables allows to ameliorate the dependency problem, while our novel splitting heuristic, in combination with several other improvements, speeds up the branch-and-bound procedure.We evaluate our approach on the airborne collision avoidance networks ACAS Xu and demonstrate runtime improvements compared to state-of-the-art tools.

Polynomial Networks (PNs) have demonstratedpromising performance on face and image recognition recently. However, robustness of PNs is unclear and thus obtaining certificates becomes imperative for enabling their adoption in real-world applications. Existing verification algorithms on ReLU neural networks (NNs) based on branch and bound (BaB) techniques cannot be trivially applied to PN verification. In this work, we devise a new bounding method, equipped with BaB for global convergence guarantees, called VPN. One key insight is that we obtain much tighter bounds than the interval bound propagation baseline. This enables sound and complete PN verification with empirical validation on MNIST, CIFAR10 and STL10 datasets. We believe our method has its own interest to NN verification.

This paper presents the Veritex tool for reachability analysis and repair of deep neural networks (DNNs). Veritex includes methods for exact (sound and complete) analysis and over-approximative (sound and incomplete) reachability analysis of DNNs using novel set representations, including the facet-vertex incidence matrix, face lattice, and $\mathcal{V}$-zono. In addition to sound and complete safety verification of DNNs, these methods can also efficiently compute the exact output reachable domain, as well as the exact unsafe input space that causes safety violations of DNNs in the output. More importantly, based on the exact unsafe input-output reachable domain, Veritex can repair unsafe DNNs on multiple safety properties with negligible performance degradation. The repair is conducted by updating the DNN parameter through retraining. The approach also works in the absence of the safe model reference and the original dataset for learning. Veritex primarily addresses the issue of constructing provably safe DNNs, which is not yet significantly addressed in most of the current formal methods for trustworthy artificial intelligence (AI). The utility of Veritex is evaluated for these two aspects, specifically safety verification and DNN repair. Benchmarks for verification include the ACAS Xu networks, and benchmarks for the repair include unsafe ACAS Xu networks and an unsafe agent trained in deep reinforcement learning (DRL).

Contrastive adversarial training has successfully improved the robustness of contrastive learning (CL). However, the robustness metric used in these methods is linked to attack algorithms, image labels and downstream tasks, all of which may affect the consistency and reliability of robustness metric for CL. To address these problems, this paper proposes a novel Robustness Verification framework for Contrastive Learning (RVCL). Furthermore, we use extreme value theory to reveal the relationship between the robust radius of the CL encoder and that of the supervised downstream task. Extensive experimental results on various benchmark models and datasets verify our theoretical findings, and further demonstrate that our proposed RVCL is able to evaluate the robustness of both models and images.

We consider the problem of whether a Neural Network (NN) model satisfies global individual fairness. Individual Fairness suggests that similar individuals with respect to a certain task are to be treated similarly by the decision model. In this work, we have two main objectives. The first is to construct a verifier which checks whether the fairness property holds for a given NN in a classification task or provide a counterexample if it is violated, i.e., the model is fair if all similar individuals are classified the same, and unfair if a pair of similar individuals are classified differently. To that end, We construct a sound and complete verifier that verifies global individual fairness properties of ReLU NN classifiers using distance-based similarity metrics. The second objective of this paper is to provide a method for training provably fair NN classifiers from unfair (biased) data. We propose a fairness loss that can be used during training to enforce fair outcomes for similar individuals. We then provide provable bounds on the fairness of the resulting NN. We run experiments on commonly used fairness datasets that are publicly available and we show that global individual fairness can be improved by 96 % without significant drop in test accuracy.

ACAS Xu is an air-to-air collision avoidance system designed for unmanned aircraft that issues horizontal turn advisories to avoid an intruder aircraft. Analysis of this system has spurred a significant body of research in the formal methods community on neural network verification. While many powerful methods have been developed, most work focuses on open-loop properties of the networks, rather than the main point of the system—collision avoidance—which requiresclosed-loop analysis. In this work, we develop a technique to verify a closed-loop approximation of the system using state quantization and back-reachability. We use favorable assumptions for the analysis—perfect sensor information, instantfollowing of advisories, ideal aircraft maneuvers, and an intruder that only flies straight. When the method fails to prove the system is safe, we refinethe quantization parameters until generating counterexamples where the original (non-quantized) system also has collisions.

We present Marvel, a verification-based reinforcement learning framework that synthesizes safe programmatic controllers for environments with continuous state and action space. The key idea is the integration of program reasoning techniques into reinforcement learning training loops. Marvel performs abstraction-based program verification to reason about a programmatic controller and its environment as a closed-loop system. Based on a novel verification-guided synthesis loop for training, Marvel minimizes the amount of safety violation in the system abstraction, which approximates the worst-case safety loss, using gradient-descent style optimization. Experimental results demonstrate the substantial benefits of leveraging verification feedback for safe-by-construction of programmatic controllers.

We consider the problem of certifying the robustness of deep neural networks against real-world distribution shifts. To do so, we bridge the gap between hand-crafted specifications and realistic deployment settings by proposing a novel neural-symbolic verification framework, in which we train a generative model to learn perturbations from data and define specifications with respect to the output of the learned model. A unique challenge arising from this setting is that existing verifiers cannot tightly approximate sigmoid activations, which are fundamental to many state-of-the-art generative models. To address this challenge, we propose a general meta-algorithm for handling sigmoid activations which leverages classical notions of counter-example-guided abstraction refinement. The key idea is to ``lazily'' refine the abstraction of sigmoid functions to exclude spurious counter-examples found in the previous abstraction, thus guaranteeing progress in the verification process while keeping the state-space small. Experiments on the MNIST and CIFAR-10 datasets show that our framework significantly outperforms existing methods on a range of challenging distribution shifts.

Continuous deep learning models, referred to as Neural Ordinary Differential Equations (Neural ODEs), have received considerable attention over the last several years. Despite their burgeoning impact, there is a lack of formal analysis techniques for these systems. In this paper, we consider a general class of neural ODEs with varying architectures and layers, and introduce a novel reachability framework that allows for the formal analysis of their behavior. The methods developed for the reachability analysis of neural ODEs are implemented in a new tool called NNVODE. Specifically, our work extends an existing neural network verification tool to support neural ODEs. We demonstrate the capabilities of our methods through the analysis of a set of benchmarks that include neural ODEs used for classification, and in control and dynamical systems, including an evaluation of the efficacy and capabilities of our approach with respect to existing software tools within the continuous-time systems reachability literature, when it is possible to do so.

This paper proposes a theoretical and computational framework fortraining and robustness verification of implicit neural networks based upon non-Euclidean contraction theory. The basic idea is to cast the robustness analysis of a neural network as a reachability problem and use (i) the $\ell_{\infty}$-norm input-output Lipschitz constant and (ii) the tight inclusion function of the network to over-approximate its reachable sets. First, for a given implicit neural network, we use $\ell_{\infty}$-matrix measures to propose sufficient conditions for its well-posedness, design an iterative algorithm to compute its fixed points, and provide upper bounds for its $\ell_\infty$-norm input-output Lipschitz constant. Second, we introduce a related embedded network and show that the embedded network can be used to provide an $\ell_\infty$-norm box over-approximation of the reachable sets of the original network. Moreover, we use the embedded network to design an iterative algorithm for computing the upper bounds of the original system's tight inclusion function. Third, we use the upper bounds of the Lipschitz constants and the upper bounds of the tight inclusion functions to design two algorithms for the training and robustness verification of implicit neural networks. Finally, we apply our algorithms to train implicit neural networks on the MNIST dataset and compare the robustness of our models with the models trained via existing approaches in the literature.

This work concerns the development of deep networks that are certifiably robust to adversarial attacks. Joint robust classification-detection was recently introduced as a certified defense mechanism, where adversarial examples are either correctly classified or assigned to the abstain'' class. In this work, we show that such a provable framework can be extended to networks with multiple explicit abstain classes, where the adversarial examples are adaptively assigned to those. While naively adding multiple abstain classes can lead tomodel degeneracy'', we propose a regularization approach and a training method to counter this degeneracy by promoting full use of the multiple abstain classes. Our experiments demonstrate that the proposed approach consistently achieves favorable natural vs. robust verified accuracy tradeoff, outperforming state-of-the-art algorithms for various choices of number of abstain classes.

With the rapidly advancing improvements to thealready successful Deep Learning artifacts, Neu-ral Networks (NN) are poised to permeate agrowing number of everyday applications, includ-ing ones where safety is paramount and, there-fore, formal guarantees are a precious commodity.To this end, Formal Methods, a long-standing,mathematically-inspired field of research saw aneffervescent outgrowth targeting NN and advanc-ing almost as rapidly as AI itself. Without a doubt,the most challenging problem facing this newresearch direction is the scalability to the ever-growing NN models. This paper stems from thisneed and introduces Relational Coefficients forInput partitioning Heuristic (ReCIPH), accelerat-ing NN analysis. Extensive experimentation issupplied to assert the added value to two differentsolvers handling several models and properties(coming, in part, from two industrial use-cases).

Deep learning models have achieved great success in many fields, yet they are vulnerable to adversarial examples. This paper follows a causal perspective to look into the adversarial vulnerability and proposes Causal Intervention by Semantic Smoothing (CISS), a novel framework towards robustness against natural language attacks. Instead of merely fitting observational data, CISS learns causal effects p(y|do(x)) by smoothing in the latent semantic space to make robust predictions, which scales to deep architectures and avoids tedious construction of noise customized for specific attacks. CISS is provably robust against word substitution attacks, as well as empirically robust even when perturbations are strengthened by unknown attack algorithms. For example, on YELP, CISS surpasses the runner-up by 6.7% in terms of certified robustness against word substitutions, and achieves 79.4% empirical robustness when syntactic attacks are integrated.

Randomized smoothing is a leading approach to producing certifiably robust classifiers. The goal of optimal randomized smoothing is to maximize the average certified radius over the space of smoothing distributions. We theoretically study this problem through the lens of infinite-dimensional optimization over measure spaces, and prove that the nonconvex infinite program is lower-bounded by a conic linear program wherein the classifier's confidence acts as a surrogate objective to optimize. A semi-infinite linear programming approximation to the problem is presented, whose sub-problems are proven to attain nontrivial strong duality. A proof-of-concept experiment demonstrates the effectiveness of the proposed approach.

The increasing prevalence of neural networks (NNs) in safety-critical applications calls for methods to certify their behavior and guarantee safety. This paper presents a backward reachability approach for safety verification of neural feedback loops (NFLs), i.e., closed-loop systems with NN control policies. While recent works have focused on forward reachability as a strategy for safety certification of NFLs, backward reachability offers advantages over the forward strategy, particularly in obstacle avoidance scenarios. Prior works have developed techniques for backward reachability analysis for systems without NNs, but the presence of NNs in the feedback loop presents a unique set of problems due to the nonlinearities in their activation functions and because NN models are generally not invertible. To overcome these challenges, we use existing forward NN analysis tools to find affine bounds on the control inputs and solve a series of linear programs (LPs) to efficiently find an approximation of the backprojection (BP) set, i.e., the set of states for which the NN control policy will drive the system to a given target set. We present an algorithm to iteratively find BP set estimates over a given time horizon and demonstrate the ability to reduce conservativeness in the BP set estimates by up to 88\% with low additional computational cost. We use numerical results from a double integrator model to verify the efficacy of these algorithms and demonstrate the ability to certify safety for a linearized ground robot model in a collision avoidance scenario where forward reachability fails.

Please use the email address from the speaker's ICML profile. If the user has multiple ICML profiles, then use the profile the speaker will register with. When a valid ICML profile email address entered, a green checkbox will appear. The registration status is indicated to the right of the speaker's name with the first letter of the session. Tutorials + Conference Sessions would appear T,C. Underlined means the registration is complimentary. Brackets indicates that the person checked in into the meeting.

Data poisoning attacks aim at manipulating model behaviors through distorting training data. Previously, an aggregation-based certified defense, Deep Partition Aggregation (DPA), was proposed to mitigate this threat. DPA predicts through an aggregation of base classifiers trained on disjoint subsets of data, thus restricting its sensitivity to dataset distortions. In this work, we propose an improved certified defense against general poisoning attacks, namely Finite Aggregation. In contrast to DPA, which directly splits the training set into disjoint subsets, our method first splits the training set into smaller disjoint subsets and then combines duplicates of them to build larger (but not disjoint) subsets for training base classifiers. This reduces the worst-case impacts of poison samples and thus improves certified robustness bounds. In addition, we offer an alternative view of our method, bridging the designs of deterministic and stochastic aggregation-based certified defenses. Empirically, our proposed Finite Aggregation consistently improves certificates on MNIST, CIFAR-10, and GTSRB, boosting certified fractions by up to 3.05%, 3.87% and 4.77%, respectively, while keeping the same clean accuracies as DPA's, effectively establishing a new state of the art in (pointwise) certified robustness against data poisoning.

We present NN4SysBench, a benchmark suite for neural network verification, comprised of benchmarks from neural networks for systems (or NN4Sys). NN4Sys is booming: there are hundreds of proposals of using neural networks in computer systems—databases, OSes, and networked systems—that are safety critical. We observe that NN4Sys has some unique characteristics that to- day’s neural network verification tools overlooked. This benchmark aims at bridging the gap between NN4Sys and NN-verification by tailoring impactful NN4Sys instances to benchmarks that today’s NN-verification tools can work on.

A variety of methods have been proposed to try to explain how deep neural networks make their decisions. Key to those approaches is the need to sample the pixel space efficiently in order to derive importance maps. However, it has been shown that the sampling methods used to date introduce biases and other artifacts, leading to inaccurate estimates of the importance of individual pixels and severely limit the reliability of current explainability methods. Unfortunately, the alternative -- to exhaustively sample the image space is computationally prohibitive. In this paper, we introduce EVA (Explaining using Verified perturbation Analysis) -- the first explainability method guarantee to have an exhaustive exploration of a perturbation space. Specifically, we leverage the beneficial properties of verified perturbation analysis -- time efficiency, tractability and guaranteed complete coverage of a manifold -- to efficiently characterize the input variables that are most likely to drive the model decision. We evaluate the approach systematically and demonstrate state-of-the-art results on multiple benchmarks.