Efficient Formal Safety Analysis of Neural Networks

2018/09/19 by Shiqi Wang, Wang, Shiqi, Kexin Pei +7 · 71 citations
Computer Science · Mathematics · #Adversarial Robustness in Machine Learning #Artificial Intelligence (cs.AI) #Explainable Artificial Intelligence (XAI) #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Machine Learning (cs.LG) #Machine Learning (stat.ML) #cs.AI #cs.LG #cs.LO #stat.ML

paper · pdf · doi:10.48550/arxiv.1809.08098

Accepted to NIPS'18

openalex publication_date 2018/09/19 · arxiv created 2018/11/07 · arxiv updated 2018/11/09 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

Neural networks are increasingly deployed in real-world safety-critical domains such as autonomous driving, aircraft collision avoidance, and malware detection. However, these networks have been shown to often mispredict on inputs with minor adversarial or even accidental perturbations. Consequences of such errors can be disastrous and even potentially fatal as shown by the recent Tesla autopilot crash. Thus, there is an urgent need for formal analysis systems that can rigorously check neural networks for violations of different safety properties such as robustness against adversarial perturbations within a certain L-norm of a given image. An effective safety analysis system for a neural network must be able to either ensure that a safety property is satisfied by the network or find a counterexample, i.e., an input for which the network will violate the property. Unfortunately, most existing techniques for performing such analysis struggle to scale beyond very small networks and the ones that can scale to larger networks suffer from high false positives and cannot produce concrete counterexamples in case of a property violation. In this paper, we present a new efficient approach for rigorously checking different safety properties of neural networks that significantly outperforms existing approaches by multiple orders of magnitude. Our approach can check different safety properties and find concrete counterexamples for networks that are 10× larger than the ones supported by existing analysis techniques. We believe that our approach to estimating tight output bounds of a network for a given input range can also help improve the explainability of neural networks and guide the training process of more robust neural networks.

Cited by

• Exact and Asymptotically Complete Robust Verifications of Neural Networks via Ising Solvers
• Bridging Efficiency and Safety: Formal Verification of Neural Networks with Early Exits
• Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification
• BEAVER: An Efficient Deterministic LLM Verifier
• Faster Verified Explanations for Neural Networks
• NegBLEURT Forest: Leveraging Inconsistencies for Detecting Jailbreak Attacks
• Tight Robustness Certification Through the Convex Hull of ℓ₀ Attacks
• Tighter Truncated Rectangular Prism Approximation for RNN Robustness Verification
• Verified SHAP: Provable Bounds for Exact Shapley Values of Neural Networks
• BaB-prob: Branch and Bound with Preactivation Splitting for Probabilistic Verification of Neural Networks
• Influence-Guided Concolic Testing of Transformer Robustness
• Hidden Cost of Randomized Smoothing
• A Survey of Recent Scalability Improvements for Semidefinite Programming with Applications in Machine Learning, Control, and Robotics
• Randomized Smoothing of All Shapes and Sizes
• Verifying Individual Fairness in Machine Learning Models
• Improved Adversarial Robustness by Reducing Open Space Risk via Tent Activations
• Mini-Batch Robustness Verification of Deep Neural Networks
• QNNVerifier: A Tool for Verifying Neural Networks using SMT-Based Model Checking
• Exact Verification of Graph Neural Networks with Incremental Constraint Solving
• Adaptive Verifiable Training Using Pairwise Class Similarity
• Robust Deep Reinforcement Learning through Adversarial Loss
• Towards Compact and Robust Deep Neural Networks
• Attack as Defense: Characterizing Adversarial Examples using Robustness
• A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks
• Non-Stochastic Information Theory
• Defending Against Physically Realizable Attacks on Image Classification
• Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees
• Towards Understanding the Adversarial Vulnerability of Skeleton-based Action Recognition
• On ℓ_p-norm Robustness of Ensemble Stumps and Trees
• Mining Verdict Boundaries for Neural Network Verification
• Evaluating the Safety of Deep Reinforcement Learning Models using Semi-Formal Verification
• Enhancing Certified Robustness via Smoothed Weighted Ensembling
• NeuroDiff: Scalable Differential Verification of Neural Networks using Fine-Grained Approximation
• Towards Evaluating and Training Verifiably Robust Neural Networks
• Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition
• Universal Approximation with Certified Networks
• Evaluations and Methods for Explanation through Robustness Analysis
• Towards Assessment of Randomized Smoothing Mechanisms for Certifying Adversarial Robustness
• Interior-Point Vanishing Problem in Semidefinite Relaxations for Neural Network Verification
• Auditing AI models for Verified Deployment under Semantic Specifications
• Automatic Perturbation Analysis for Scalable Certified Robustness and Beyond
• Towards Stable and Efficient Training of Verifiably Robust Neural Networks
• Security and Machine Learning in the Real World
• An efficient nonconvex reformulation of stagewise convex optimization problems
• MUC-G4: Minimal Unsat Core-Guided Incremental Verification for Deep Neural Network Compression
• A Systematic Mapping Study on Testing of Machine Learning Programs
• Fast Falsification of Neural Networks using Property Directed Testing
• Data-Driven Falsification of Cyber-Physical Systems
• Logic Gate Neural Networks are Good for Verification
• Out of the Shadows: Exploring a Latent Space for Neural Network Verification
• Evaluating the Robustness of Nearest Neighbor Classifiers: A Primal-Dual Perspective
• Towards Verifying Robustness of Neural Networks Against Semantic Perturbations
• Software Engineering for AI-Based Systems: A Survey
• Resilient Cyberphysical Systems and their Application Drivers: A Technology Roadmap
• Denoised Smoothing: A Provable Defense for Pretrained Classifiers
• On the Security Risks of ML-based Malware Detection Systems: A Survey
• Learning Lyapunov Functions for Piecewise Affine Systems with Neural Network Controllers
• Enhancing Gradient-based Attacks with Symbolic Intervals
• Debona: Decoupled Boundary Network Analysis for Tighter Bounds and Faster Adversarial Robustness Proofs
• On Training Robust PDF Malware Classifiers
• Adaptive Branch-and-Bound Tree Exploration for Neural Network Verification
• Logic-Gated Time-Shared Feedforward Networks for Alternating Finite Automata: Exact Simulation and Learnability
• Practical Solutions for Machine Learning Safety in Autonomous Vehicles
• TorchLean: Formalizing Neural Networks in Lean
• Evaluation and Verification of Physics-Informed Neural Models of the Grad-Shafranov Equation
• The Luna Bound Propagator for Formal Analysis of Neural Networks
• Is the Rush to Machine Learning Jeopardizing Safety? Results of a Survey
• Enhancing Certifiable Robustness via a Deep Model Ensemble
• Provable Certificates for Adversarial Examples: Fitting a Ball in the Union of Polytopes
• Support is All You Need for Certified VAE Training
• Adversarial Examples in Environment Perception for Automated Driving (Review)

Related

• DeepSafe: A Data-driven Approach for Checking Adversarial Robustness in Neural Networks
• Automated Repair of Neural Networks
• Safety Verification of Deep Neural Networks
• Towards the Quantification of Safety Risks in Deep Neural Networks
• The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural Networks