Abstract neural networks

DOI10.1007/978-3-030-65474-0_4MaRDI QIDQ2233525zbMATH OpenOpenAlexFDO

Authors Matthew Sotoudeh, Aditya V. Thakur

Publication date 18 October 2021

Full work available at URL https://arxiv.org/abs/2009.05660

zbMATH Keywords

abstractionsoundnessdeep neural networks

Mathematics Subject Classification ID

Artificial neural networks and deep learning (68T07) Specification and verification (program logics, model checking, etc.) (68Q60) Networks and circuits as models of computation; circuit complexity (68Q06)

Abstract: Deep Neural Networks (DNNs) are rapidly being applied to safety-critical domains such as drone and airplane control, motivating techniques for verifying the safety of their behavior. Unfortunately, DNN verification is NP-hard, with current algorithms slowing exponentially with the number of nodes in the DNN. This paper introduces the notion of Abstract Neural Networks (ANNs), which can be used to soundly overapproximate DNNs while using fewer nodes. An ANN is like a DNN except weight matrices are replaced by values in a given abstract domain. We present a framework parameterized by the abstract domain and activation functions used in the DNN that can be used to construct a corresponding ANN. We present necessary and sufficient conditions on the DNN activation functions for the constructed ANN to soundly over-approximate the given DNN. Prior work on DNN abstraction was restricted to the interval domain and ReLU activation function. Our framework can be instantiated with other abstract domains such as octagons and polyhedra, as well as other activation functions such as Leaky ReLU, Sigmoid, and Hyperbolic Tangent.

Recommendations

• \textsc{NeVer}: a tool for artificial neural networks verification
• An abstraction-based framework for neural network verification
• Reluplex: a calculus for reasoning about deep neural networks
• Reluplex: an efficient SMT solver for verifying deep neural networks
• Safety verification of deep neural networks

Cites work

• Automating abstract interpretation
• Deep learning
• Donut domains: efficient non-convex domains for abstract interpretation
• Making abstract interpretations complete
• Reluplex: an efficient SMT solver for verifying deep neural networks
• Symbolic optimization with SMT solvers
• Systematic generation of diverse benchmarks for DNN verification
• The octagon abstract domain
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(17)

• A domain-theoretic framework for robustness analysis of neural networks
• Deep statistical model checking
• SyReNN: a tool for analyzing deep neural networks
• The octatope abstract domain for verification of neural networks
• Towards global neural network abstractions with locally-exact reconstruction
• Abstraction based connectionist analogy processor
• \textsc{NeVer}: a tool for artificial neural networks verification
• Bisimulations for neural network reduction
• Neural Network Verification Using Residual Reasoning
• Enhancing robustness verification for deep neural networks via symbolic propagation
• Verifying generalization in deep learning
• Analyzing deep neural networks with symbolic propagation: towards higher precision and faster verification
• Star-based reachability analysis of deep neural networks
• \textsf{CLEVEREST}: accelerating CEGAR-based neural network verification via adversarial attacks
• SpecRepair: Counter-Example Guided Safety Repair of Deep Neural Networks
• Verifying low-dimensional input neural networks via input quantization
• The hexatope and octatope abstract domains for neural network verification

This page was built for publication: Abstract neural networks

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2233525)