Verifying Properties of Binarized Deep Neural Networks

By Nina Narodytska, Shiva Prasad Kasiviswanathan, Leonid Ryzhyk, Shmuel Sagiv, Thomas J. Walsh. 2017

237 citations recorded by the source corpus.

Understanding properties of deep neural networks is an important challenge in deep learning. In this paper, we take a step in this direction by proposing a rigorous way of verifying properties of a popular class of neural networks, Binarized Neural Networks, using the well-developed means of Boolean satisfiability. Our main contribution is a construction that creates a representation of a binarized neural network as a Boolean formula. Our encoding is the first exact Boolean representation of a deep neural network. Using this encoding, we leverage the power of modern SAT solvers along with a proposed counterexample-guided search procedure to verify various properties of these networks. A particular focus will be on the critical property of robustness to adversarial perturbations. For this property, our experimental results demonstrate that our approach scales to medium-size deep neural networks used in image classification tasks. To the best of our knowledge, this is the first work on verifying properties of deep neural networks using an exact Boolean encoding of the network.

Subfields: Artificial Intelligence, Electrical and Electronic Engineering, Hardware and Architecture

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Electrical and Electronic Engineering

In Hardware and Architecture

Citations in the corpus

Reachability Analysis of Deep Neural Networks with Provable Guarantees (2018, methodology): “h as the error bounds. Existing approaches for analysing DNNs with a guarantee work by either reducing the problem to a constraint satisfaction problem that can be solved by MILP [9, 11, 12, 13], SAT [14] or SMT [7, 12] techniques, or applying search algorithms over discretised vector spaces [6, 15]”
Toward Scalable Verification for Safety-Critical Deep Networks (2018, background): “The simplicity and smaller size of low-precision networks will make them more amenable to verification than full-precision networks [2, 11], as well as more suitable for use on low-power edge devices [10].”
Three Modern Roles for Logic in AI (2020, unknown): “, [39, 40, 43, 48, 58, 82, 84].”
Towards Trustable Explainable AI (2020, methodology): “…et al. , 2018b; Katz et al. , 2017] but also motivated efforts aiming at devising approaches to ex-plainable artiﬁcial intelligence (XAI) [Ribeiro et al. , 2018; Lundberg and Lee, 2017; Ignatiev et al. , 2018; Narodytska et al. , 2018a; Ribeiro et al. , 2016; Ignatiev et al. , 2019a; Monroe, 2018].”
A Unified View of Piecewise Linear Neural Network Verification (2017, background): “The scope of this paper does not include approaches relying on additional assumptions such as twice differentiability of the network [8, 20], limitation of the activation to binary values [4, 15] or restriction to a single linear domain [2].”
Piecewise Linear Neural Network verification: A comparative study (2017, methodology): “At the other end of the spectrum, Narodytska et al. (2017) and Cheng et al. (2017c) use SAT solvers to propose verification methods for the specialised case of Binarized Neural Networks (Hubara et al., 2016).”