Reluplex: an efficient SMT solver for verifying deep neural networks
From MaRDI portal
Publication:2151238
DOI10.1007/978-3-319-63387-9_5zbMath1494.68167arXiv1702.01135OpenAlexW2594877703MaRDI QIDQ2151238
Kyle Julian, Mykel J. Kochenderfer, Clark Barrett, Guy Katz, David L. Dill
Publication date: 1 July 2022
Full work available at URL: https://arxiv.org/abs/1702.01135
satisfiability modulo theories (SMT)rectified linear unit (ReLU)deep neural networks (DNNs)airborne collision avoidance systemReLU function
Artificial neural networks and deep learning (68T07) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items (92)
Deep Statistical Model Checking ⋮ DiffRNN: differential verification of recurrent neural networks ⋮ Robustness verification of quantum classifiers ⋮ \textsf{BDD4BNN}: a BDD-based quantitative analysis framework for binarized neural networks ⋮ Verisig 2.0: verification of neural network controllers using Taylor model preconditioning ⋮ Robustness verification of semantic segmentation neural networks using relaxed reachability ⋮ Static analysis of ReLU neural networks with tropical polyhedra ⋮ Exploiting verified neural networks via floating point numerical error ⋮ Verifying low-dimensional input neural networks via input quantization ⋮ Toward neural-network-guided program synthesis and verification ⋮ Bisimulations for neural network reduction ⋮ Modeling design and control problems involving neural network surrogates ⋮ Global optimization of objective functions represented by ReLU networks ⋮ Metrics and methods for robustness evaluation of neural networks with generative models ⋮ Reachability in Simple Neural Networks ⋮ Sparse polynomial optimisation for neural network verification ⋮ Risk-aware shielding of partially observable Monte Carlo planning policies ⋮ Speeding up neural network robustness verification via algorithm configuration and an optimised mixed integer linear programming solver portfolio ⋮ Reluplex: a calculus for reasoning about deep neural networks ⋮ \textsf{CLEVEREST}: accelerating CEGAR-based neural network verification via adversarial attacks ⋮ Neural Network Verification Using Residual Reasoning ⋮ T4V: exploring neural network architectures that improve the scalability of neural network verification ⋮ Robustness analysis of continuous-depth models with Lagrangian techniques ⋮ On the (complete) reasons behind decisions ⋮ Chordal sparsity for SDP-based neural network verification ⋮ Synthesizing ReLU neural networks with two hidden layers as barrier certificates for hybrid systems ⋮ Reachability analysis of deep ReLU neural networks using facet-vertex incidence ⋮ Verifying Neural Network Controlled Systems Using Neural Networks ⋮ Verification of machine learning based cyber-physical systems: a comparative study ⋮ Fast BATLLNN: Fast Box Analysis of Two-Level Lattice Neural Networks ⋮ SMT-based modeling and verification of spiking neural networks: a case study ⋮ Generating probabilistic safety guarantees for neural network controllers ⋮ Bridging formal methods and machine learning with model checking and global optimisation ⋮ Temporal logic explanations for dynamic decision systems using anchors and Monte Carlo tree search ⋮ Boosting robustness verification of semantic feature neighborhoods ⋮ Verifying feedforward neural networks for classification in Isabelle/HOL ⋮ The octatope abstract domain for verification of neural networks ⋮ Quantitative Verification for Neural Networks using ProbStars ⋮ Verification of Recurrent Neural Networks with Star Reachability ⋮ Automatic Abstraction Refinement in Neural Network Verification using Sensitivity Analysis ⋮ BERN-NN: Tight Bound Propagation For Neural Networks Using Bernstein Polynomial Interval Arithmetic ⋮ Reachability is NP-complete even for the simplest neural networks ⋮ Spanning attack: reinforce black-box attacks with unlabeled data ⋮ Safety Verification for Deep Neural Networks with Provable Guarantees (Invited Paper). ⋮ An SMT-based approach for verifying binarized neural networks ⋮ SyReNN: a tool for analyzing deep neural networks ⋮ Abstract neural networks ⋮ Probabilistic Lipschitz analysis of neural networks ⋮ Verification of piecewise deep neural networks: a star set approach with zonotope pre-filter ⋮ Probabilistic guarantees for safe deep reinforcement learning ⋮ How Many Bits Does it Take to Quantize Your Neural Network? ⋮ SpecRepair: Counter-Example Guided Safety Repair of Deep Neural Networks ⋮ Shared Certificates for Neural Network Verification ⋮ Example Guided Synthesis of Linear Approximations for Neural Network Verification ⋮ Verifying Neural Networks Against Backdoor Attacks ⋮ Probabilistic Verification of Neural Networks Against Group Fairness ⋮ Towards global neural network abstractions with locally-exact reconstruction ⋮ Towards Logical Specification of Statistical Machine Learning ⋮ A survey of safety and trustworthiness of deep neural networks: verification, testing, adversarial attack and defence, and interpretability ⋮ Optimization problems for machine learning: a survey ⋮ A game-based approximate verification of deep neural networks with provable guarantees ⋮ Towards formal XAI: formally approximate minimal explanations of neural networks ⋮ \textsc{OccRob}: efficient SMT-based occlusion robustness verification of deep neural networks ⋮ \textsf{QEBVerif}: quantization error bound verification of neural networks ⋮ Verifying generalization in deep learning ⋮ Efficient neural network analysis with sum-of-infeasibilities ⋮ LinSyn: synthesizing tight linear bounds for arbitrary neural network activation functions ⋮ Star-based reachability analysis of deep neural networks ⋮ Robustness verification of support vector machines ⋮ Analyzing deep neural networks with symbolic propagation: towards higher precision and faster verification ⋮ Synergies between machine learning and reasoning -- an introduction by the Kay R. Amel group ⋮ ABBA neural networks: coping with positivity, expressivity, and robustness ⋮ Probabilistic reach-avoid for Bayesian neural networks ⋮ Learning safe neural network controllers with barrier certificates ⋮ Modelling and verifying robotic software that uses neural networks ⋮ Verifying the generalization of deep learning to out-of-distribution domains ⋮ Complexity of reachability problems in neural networks ⋮ Improving neural network verification through spurious region guided refinement ⋮ Inverse problems are solvable on real number signal processing hardware ⋮ Advances in verification of ReLU neural networks ⋮ Strong mixed-integer programming formulations for trained neural networks ⋮ The hexatope and octatope abstract domains for neural network verification ⋮ Enhancing robustness verification for deep neural networks via symbolic propagation ⋮ Reachable sets of classifiers and regression models: (non-)robustness analysis and robust training ⋮ Risk verification of stochastic systems with neural network controllers ⋮ An SMT theory of fixed-point arithmetic ⋮ Cryptanalytic extraction of neural network models ⋮ Robustness verification of ReLU networks via quadratic programming ⋮ Neural network repair with reachability analysis ⋮ On neural network equivalence checking using SMT solvers ⋮ Reachability analysis of a general class of neural ordinary differential equations ⋮ Task-Aware Verifiable RNN-Based Policies for Partially Observable Markov Decision Processes
Uses Software
This page was built for publication: Reluplex: an efficient SMT solver for verifying deep neural networks
