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 (68)
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? ⋮ 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 ⋮ Learning safe neural network controllers with barrier certificates ⋮ Improving neural network verification through spurious region guided refinement ⋮ Advances in verification of ReLU neural networks ⋮ Strong mixed-integer programming formulations for trained neural networks ⋮ 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
