Source-linked AI summary
Efficient Formal Safety Analysis of Neural Networks
Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, Suman Jana
TL;DR
Neural networks can violate safety properties after small input perturbations, while existing formal methods struggle with scalability, false positives, or concrete counterexamples. The paper introduces Neurify, combining symbolic linear relaxation with directed constraint refinement to tighten output bounds and focus solver effort. Neurify supports diverse safety checks at substantially greater scale and speed, while the method may also aid robust training and explainability.
Problem
Formal safety analysis must verify properties or find concrete counterexamples, but existing methods struggle to scale and scalable relaxations can produce false positives without concrete counterexamples.
Method
Neurify combines symbolic linear relaxation for tighter output over-approximations with directed constraint refinement focused on potentially overestimated nodes.
Results
Neurify outperforms existing formal analysis systems by several orders of magnitude and scales to networks with more than 10,000 ReLU nodes.
Takeaways & Limitations
The method’s rigorous output-range estimates may help guide robust-network training and improve neural-network explainability.
Takeaways & Limitations
Exact decision-boundary estimation remains difficult because ReLU-piece combinations grow exponentially with network size, making exhaustive enumeration prohibitively expensive.
Abstract
from arXiv · showhide
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$\times$ 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.
1 Introduction
Neural networks can make dangerous errors under small adversarial or accidental input changes, motivating formal checkers that either verify safety properties or produce concrete counterexamples. Existing methods face scalability, false-positive, and counterexample-generation limitations, while Neurify combines tighter bounds with targeted refinement to improve analysis efficiency and scale.
- Motivation: Minor adversarial, lighting, or orientation changes can cause neural networks to produce dangerous mispredictions, including in critical deployment domains.These errors may have disastrous or potentially fatal consequences.
- Safety-analysis goal: Formal safety checkers should either guarantee a property over an input range or find a concrete input violating it.Examples include robustness to perturbations within an L-norm and prediction invariance under lighting changes.
- Challenges: Exhaustive ReLU-piece enumeration is prohibitively expensive because the number of linear-piece combinations grows exponentially with network size.Sampling-based methods may also require enormous datasets to obtain tight decision-boundary bounds.
- Approach: Neurify combines symbolic linear relaxation with directed constraint refinement to tighten output bounds and iteratively reduce relaxation errors.It focuses solver effort on potentially overestimated nodes relevant to the safety property.
- Empirical scope: Neurify checks diverse safety properties and provides concrete counterexamples while targeting networks 10× larger than those supported by existing techniques.The system evaluates six property types across nine networks and five datasets.
- Implications: Tight, rigorous output ranges may also help guide robust-network training and improve neural-network explainability.This proposed use extends beyond formal safety-property checking.
2 Background
Prior analysis methods use symbolic intervals, input bisection, or linear relaxation to bound neural-network outputs, but each has important efficiency or accuracy limitations. Linear relaxation scales better than exact piecewise analysis, yet its quality depends strongly on accurately estimated ReLU bounds.
- Symbolic interval analysis: Symbolic interval analysis tracks dependencies with linear equations and concretizes only ReLUs whose outputs cannot be represented by one linear equation.For a ReLU input expression Eq, it uses exact symbolic intervals when l ≥ 0 or u ≤ 0, and [l, u] when l < 0 < u.
- Input bisection: Input bisection tightens output intervals by splitting an input feature range and reuniting the resulting child intervals.Its efficiency decreases drastically as the number of input dimensions increases.
- Linear relaxation: Linear relaxation replaces each ReLU’s nonlinear constraint with three linear constraints that can be solved efficiently for output bounds.The relaxation expands the feasible region beyond the two original piecewise-linear components.
- Limitations: Naive interval propagation can substantially overestimate ReLU bounds, limiting the accuracy of linear relaxation.The prior approach also cannot efficiently refine estimated bounds as more computing power becomes available.
3 Approach
Neurify combines symbolic linear relaxation with directed constraint refinement to rigorously check neural-network safety properties, prove safe cases, and validate or refine potential counterexamples.
- Symbolic Linear Relaxation: Neurify combines symbolic interval analysis and linear relaxation to compute tighter output bounds while partially preserving input dependencies.The relaxation uses bounds on intermediate ReLU inputs and is described as the tightest achievable under its criterion.
- Directed Constraint Refinement: Directed constraint refinement locates overestimated ReLU nodes, prioritizes influential nodes by output gradient, and splits their input ranges into two cases.The split cases exclude zero from the target node’s input interval, so they require no relaxation there.
- Safety Checking: Neurify uses a linear solver to prove safety when relaxed constraints are unsatisfiable and otherwise obtains potential counterexamples for validation.Candidate counterexamples are directly checked on the target network because relaxation can introduce false positives.
- Symbolic Linear Relaxation: 59.64% more overestimation error is cut on average than with symbolic interval analysis.The tighter bounds also reduce the time needed to prove a property by several orders of magnitude.
- Directed Constraint Refinement: Iterative solver-based refinement tightens output ranges and improves scalability for difficult safety properties.Only ReLU nodes operating in the nonlinear region need relaxation and are treated as overestimated nodes.
- Safety Properties: The framework supports diverse input-output safety properties, including prediction invariance over specified input ranges and class-confidence constraints.The solver checks whether the target class remains above competing outputs under the defined input constraints.
4 Experiments
Neurify was evaluated across nine neural-network models and multiple safety properties, including large-scale autonomous-driving and malware-detection networks. Its symbolic linear relaxation and directed constraint refinement improved verification coverage and efficiency over prior approaches.
- Experimental setup: Neurify was tested on nine models trained over five datasets, with safety properties summarized using satisfied, violated, and timed-out cases.Evaluations included ACAS Xu, Drebin, MNIST, convolutional MNIST, and a convolutional self-driving-car model.
- Properties checked by model: Neurify formally analyzed Dave, a convolutional self-driving-car network with over 10,000 ReLU nodes, under L∞, L1, brightness, and contrast perturbations.The safe steering-deviation range was defined as less than 30 degrees from the original steering angle.
- Properties checked by model: Neurify verified safe and unsafe cases for most Drebin malware-app examples within a 3,600-second timeout.The checked property concerned whether adding app permissions without changing functionality causes malware to be misclassified as benign.
- Comparisons with other formal checkers: Neurify achieved average speedups of 20× over ReluVal and up to 5,000× over Reluplex on ACAS Xu properties.The comparison covered properties φ1–φ10 from prior work and additional properties φ11–φ15.
- Comparisons with other formal checkers: As L∞ bounds increased, ReluVal and Reluplex verified fewer MNIST cases quickly, while Neurify consistently outperformed both.At larger bounds, counterexamples became frequent enough for Neurify to find them more easily, although verified-safe cases dropped because of real violations and overestimation errors.
- Benefits of each technique: Symbolic linear relaxation tightened output intervals by at least 100% over naive interval arithmetic and helped ReluVal find 15% more MNIST cases on average.Combining symbolic linear relaxation with directed constraint refinement enabled 18.88% more verified cases on average than symbolic linear relaxation alone.
5 Conclusion
Neurify combines symbolic linear relaxation with directed constraint refinement to verify neural-network safety properties and produce concrete counterexamples. The system outperforms prior formal-analysis tools by several orders of magnitude and scales to networks with more than 10,000 ReLU nodes.
- Conclusion: Neurify computes tight network-output over-approximations with symbolic linear relaxation and refines bounds using directed constraint refinement.The system was designed to verify safety properties and provide concrete counterexamples.
- Conclusion: Neurify outperforms state-of-the-art formal analysis systems by several orders of magnitude and scales to networks with more than 10,000 ReLU nodes.The conclusion presents scalability and comparative efficiency as the main empirical outcomes.
A Proofs
The proofs characterize when symbolic interval propagation overestimates ReLU nodes and show that exact output bounds are recovered when no overestimated nodes remain.
- An overestimated ReLU node must have inputs spanning both positive and negative values over the input range.Otherwise ReLU is exact and no relaxation is needed.
- If earlier layers contain no overestimated nodes, a node’s symbolic lower and upper equations both equal its ground-truth equation.The proof establishes this inductively across network layers.
- A network with no overestimated nodes has zero output-layer error.This follows because every output node’s symbolic bounds equal its ground-truth equation.
A.2 Symbolic Linear Relaxation
Symbolic linear relaxation approximates ReLU nodes with tight linear bounds, while directed constraint refinement removes remaining overestimation by splitting ambiguous cases.
- Symbolic Linear Relaxation: Symbolic linear relaxation uses Equation 4 to produce upper and lower linear bounds for ReLU outputs.The bounds depend on concrete and symbolic lower and upper interval endpoints.
- Symbolic Linear Relaxation: The Equation 4 relaxations have the least possible maximum distance from the actual ReLU output.The proof separately establishes optimality for the upper and lower bounds.
- Directed Constraint Refinement: Directed constraint refinement splits n overestimated nodes into 2^n cases, producing an exact network function after all splits.Each split constrains the nodes to be linear, eliminating output overestimation.
- Symbolic Linear Relaxation: The method minimizes overestimation by tracking relaxed input dependencies and refining the intermediate nodes responsible for output error.Different layers can incur different approximation errors because their symbolic input intervals differ.
- Symbolic Linear Relaxation: For later overestimated nodes, independently bounding the symbolic lower and upper equations yields tighter approximations than treating them as one interval.The method divides the analysis into four cases based on the concrete ranges of both equations.
C Different Optimization and Implementation Details
Neurify combines optimized numerical computation, parallel linear solving, outward rounding, and convolution support to implement scalable formal analysis.
- Neurify uses OpenBLAS3 for matrix multiplication and lp_solve 5.54 for linear constraints generated during directed constraint refinement.Matrix multiplication was identified as a major determinant of symbolic relaxation and interval propagation performance.
- Parallelization: Directed constraint refinement runs independent linear programs in parallel using a thread pool with periodic queue rebalancing.Rebalancing addresses uneven refinement workloads across overestimated nodes.
- Outward Rounding: Outward rounding after every floating-point computation prevents precision losses from being amplified during propagation.The prototype uses 32-bit floats and can switch to 64-bit arithmetic if needed.
- Supporting Convolutional Layers: Convolutional layers propagate symbolic intervals by multiplying interval inputs with concrete convolution kernels.This follows the matrix-multiplication structure of convolution operations.
D Experimental Setup
The evaluation covers fully connected and convolutional networks across aircraft, malware, handwritten-digit, and autonomous-driving tasks, including models with thousands of ReLU nodes.
- The experiments use nine models spanning fully connected ACAS Xu, Drebin, and MNIST networks plus convolutional MNIST and self-driving-car models.The models are trained on five datasets and include multiple architectures.
- ACAS Xu: ACAS Xu models have five inputs, five outputs, six fully connected layers, and fifty ReLU nodes per layer.They advise aircraft-collision decisions based on intruder and ownship conditions.
- MNIST_FC: The fully connected MNIST models use 28x28-pixel digit images and achieve accuracies of 96.59%, 97.43%, and 98.27%.The evaluation includes three architectures with different numbers of ReLU nodes.
- Drebin_FC: The Drebin models contain 784,544 binary input features and achieve accuracies of 97.61%, 98.53%, and 99.01%.The study examines whether adding app permissions without changing functionality causes malware misclassification.
- ConvNet: The convolutional MNIST model contains about 5,000 ReLU nodes, exceeding the scale supported by traditional solver-based systems such as Reluplex.It is described as a comparably large convolutional model.
- Self-driving Car: The self-driving-car model has over 10,000 ReLU nodes and one regression output, with properties evaluated under L∞, L1, brightness, and contrast bounds.The architecture uses 3 × 100 × 100 inputs and resembles NVIDIA’s DAVE-2 model.
E Additional Results
Neurify has formally verified or provided counterexamples for thousands of safety properties across different models.
- Neurify has either formally verified or provided counterexamples for thousands of safety properties.
E.1 Cases verified by Neurify for Each Model
Neurify was evaluated on large convolutional and fully connected MNIST models under bounded L∞ perturbations, with verification results summarized across safety-property settings.
- ConvNet: Neurify verifies most properties for a large convolutional MNIST model within L∞≤5.The safety property concerns misclassification within ranges bounded by L∞≤ϵ, with ϵ from 1 to 25 and a 3600-second timeout.
- ConvNet: Table 7 reports percentages of 100 randomly selected MNIST ConvNet images that Neurify formally verified as safe or violated across L∞ bounds from 1 to 25.
- MNIST_FC: Neurify evaluates three fully connected MNIST models on misclassification properties with L∞≤ϵ for ϵ from 1 to 15.Table 8 reports cases formally verified as safe or accompanied by concrete counterexamples among 100 random images within 3600 seconds.
- Refinement analysis: Figure 7 relates formal analysis time to average and maximal refinement depth for 37 ACAS Xu and 60 MNIST safety properties verified safe.
E.2 Benefits of Each Technique
Additional experiments examine the effects of directed constraint refinement and Neurify’s counterexample-search ability, including how refinement depth relates to analysis time.
- Benefits of Each Technique: The additional experiments illustrate the benefits of symbolic linear relaxation and directed constraint refinement in Neurify.
- Benefits of Depths in Refinement: Directed constraint refinement forms a DFS search tree, with each refinement iteration increasing the tree depth.
- Benefits of Depths in Refinement: Formal analysis time is exponential in the maximum and average refinement depth across the evaluated ACAS Xu and MNIST cases.
- Benefits of Adversarial Searching Ability: Figure 8 compares Neurify’s concrete-counterexample ability with CW attacks using 5, 10, and 20 random input seeds on three MNIST models.The evaluation uses 60 safety properties that Neurify verified to be violated.