Formal verification of piece-wise linear feed-forward neural networks
From MaRDI portal
Publication:5096089
DOI10.1007/978-3-319-68167-2_19zbMATH Open1495.68131arXiv1705.01320OpenAlexW2963054787MaRDI QIDQ5096089FDOQ5096089
Publication date: 12 August 2022
Published in: Automated Technology for Verification and Analysis (Search for Journal in Brave)
Abstract: We present an approach for the verification of feed-forward neural networks in which all nodes have a piece-wise linear activation function. Such networks are often used in deep learning and have been shown to be hard to verify for modern satisfiability modulo theory (SMT) and integer linear programming (ILP) solvers. The starting point of our approach is the addition of a global linear approximation of the overall network behavior to the verification problem that helps with SMT-like reasoning over the network behavior. We present a specialized verification algorithm that employs this approximation in a search process in which it infers additional node phases for the non-linear nodes in the network from partial node phase assignments, similar to unit propagation in classical SAT solving. We also show how to infer additional conflict clauses and safe node fixtures from the results of the analysis steps performed during the search. The resulting approach is evaluated on collision avoidance and handwritten digit recognition case studies.
Full work available at URL: https://arxiv.org/abs/1705.01320
Recommendations
- Branch and bound for piecewise linear neural network verification
- Reluplex: a calculus for reasoning about deep neural networks
- Reluplex: an efficient SMT solver for verifying deep neural networks
- Advances in verification of ReLU neural networks
- Verification of piecewise deep neural networks: a star set approach with zonotope pre-filter
Artificial neural networks and deep learning (68T07) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Specification and verification (program logics, model checking, etc.) (68Q60)
Cited In (46)
- Verification of piecewise deep neural networks: a star set approach with zonotope pre-filter
- Enhancing robustness verification for deep neural networks via symbolic propagation
- Reachable sets of classifiers and regression models: (non-)robustness analysis and robust training
- DiffRNN: differential verification of recurrent neural networks
- \textsf{BDD4BNN}: a BDD-based quantitative analysis framework for binarized neural networks
- Robustness verification of semantic segmentation neural networks using relaxed reachability
- Verisig 2.0: verification of neural network controllers using Taylor model preconditioning
- Shared Certificates for Neural Network Verification
- Formal specification for deep neural networks
- SyReNN: a tool for analyzing deep neural networks
- Probabilistic guarantees for safe deep reinforcement learning
- Probabilistic Verification of Neural Networks Against Group Fairness
- Towards a unifying logical framework for neural networks
- Reluplex: a calculus for reasoning about deep neural networks
- Reachability in Simple Neural Networks
- A survey of safety and trustworthiness of deep neural networks: verification, testing, adversarial attack and defence, and interpretability
- Improving neural network verification through spurious region guided refinement
- Advances in verification of ReLU neural networks
- An SMT theory of fixed-point arithmetic
- Robustness verification of ReLU networks via quadratic programming
- An abstraction-based framework for neural network verification
- An SMT-based approach for verifying binarized neural networks
- Verifying feedforward neural networks for classification in Isabelle/HOL
- Verifying Recurrent Neural Networks Using Invariant Inference
- Verifying the generalization of deep learning to out-of-distribution domains
- Exploiting verified neural networks via floating point numerical error
- Static analysis of ReLU neural networks with tropical polyhedra
- Sparse polynomial optimisation for neural network verification
- Deep Statistical Model Checking
- Example Guided Synthesis of Linear Approximations for Neural Network Verification
- Verifying Neural Networks Against Backdoor Attacks
- Reachability is NP-complete even for the simplest neural networks
- Speeding up neural network robustness verification via algorithm configuration and an optimised mixed integer linear programming solver portfolio
- \textsf{CLEVEREST}: accelerating CEGAR-based neural network verification via adversarial attacks
- Neural Network Verification Using Residual Reasoning
- Robustness analysis of continuous-depth models with Lagrangian techniques
- T4V: exploring neural network architectures that improve the scalability of neural network verification
- \textsf{QEBVerif}: quantization error bound verification of neural networks
- Efficient neural network analysis with sum-of-infeasibilities
- LinSyn: synthesizing tight linear bounds for arbitrary neural network activation functions
- Verifying generalization in deep learning
- Analyzing deep neural networks with symbolic propagation: towards higher precision and faster verification
- Robustness verification of support vector machines
- How Many Bits Does it Take to Quantize Your Neural Network?
- Fast BATLLNN: Fast Box Analysis of Two-Level Lattice Neural Networks
- Reachability analysis of a general class of neural ordinary differential equations
This page was built for publication: Formal verification of piece-wise linear feed-forward neural networks
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5096089)
