Source-linked AI summary
Reachability Analysis of Deep Neural Networks with Provable Guarantees
Wenjie Ruan, Xiaowei Huang, Marta Kwiatkowska
TL;DR
The paper addresses the challenge of certifying DNN correctness by formulating reachability as bounding a Lipschitz-continuous function over network outputs for a given input set. It solves this problem with adaptive nested optimisation and evaluates a tool that provides provable guarantees, verifies safety, compares robustness quantitatively, and handles networks beyond existing tools.
Problem
Certifying DNNs for safety-critical deployment is challenging, while the relevant reachability objective involves global bounds for highly non-convex functions that gradient-based optimisation cannot guarantee.
Method
The paper formulates generic reachability as computing lower and upper bounds of a Lipschitz-continuous output function and solves it with adaptive nested optimisation using Lipschitz constants and convergent bound refinement.
Results
The implemented DeepGO tool provides provable guarantees, verifies DNN safety, quantitatively compares robustness, and applies to networks beyond existing constraint-based tools.
Takeaways & Limitations
Reachability analysis supports both qualitative safety verification and principled quantitative robustness comparison for DNNs, including networks with deep layers and nonlinear activation functions.
Takeaways & Limitations
The approach assumes knowledge of a Lipschitz constant and, in its reachability setup, represents the input space as a box constraint.
Abstract
from arXiv · showhide
Verifying correctness of deep neural networks (DNNs) is challenging. We study a generic reachability problem for feed-forward DNNs which, for a given set of inputs to the network and a Lipschitz-continuous function over its outputs, computes the lower and upper bound on the function values. Because the network and the function are Lipschitz continuous, all values in the interval between the lower and upper bound are reachable. We show how to obtain the safety verification problem, the output range analysis problem and a robustness measure by instantiating the reachability problem. We present a novel algorithm based on adaptive nested optimisation to solve the reachability problem. The technique has been implemented and evaluated on a range of DNNs, demonstrating its efficiency, scalability and ability to handle a broader class of networks than state-of-the-art verification approaches.
1 Introduction
The paper frames DNN certification as a generic reachability problem and proposes an adaptive nested optimisation approach with provable bounds, broad network applicability, and empirical evaluation.
- Safety-critical deployment requires DNN certification with guarantees comparable to those used for systems such as airplanes and automobiles.
- The reachability problem computes upper and lower bounds for a Lipschitz-continuous function over network outputs and an input subspace.
- Existing guaranteed approaches are restricted either to constraint-solving formulations or to searches over discretised vector spaces.
- Adaptive nested optimisation provides provable error bounds without dependence on network size, enabling scalability to large networks.
- The method requires a Lipschitz constant for the network rather than directly translating activation functions and parameters into linear constraints.
- DeepGO1 is evaluated against SHERLOCK and Reluplex and demonstrated on networks beyond existing tools’ capabilities.
2 Related Works
Related work addresses safety verification, adversarial example generation, and output range analysis through constraint solving, discretised search, or heuristic optimisation, often with limited network scale or guarantees.
- Safety Verification: Safety verification uses constraint solving or discretised-space search, with prior methods limited to small networks or relying on local assumptions for guarantees.
- Adversarial Example Generation: Adversarial example generation commonly uses gradient descent, evolutionary techniques, or saliency maps, which may find examples efficiently without guarantees.
- Output Range Analysis: Output range analysis has been formulated with MILP or combined local and global search, but both cited approaches work only on small networks.
3 Lipschitz Continuity of DNNs
The paper establishes Lipschitz continuity for feed-forward DNN layers and networks, including sigmoid, hyperbolic tangent, and softmax components, using bounded Jacobian norms.
- A feed-forward DNN composes parameterised layer functions and typically maps normalised inputs in [0, 1]^n to softmax outputs in [0, 1]^m.
- A function is Lipschitz continuous when output distance is bounded by a constant K times input distance; the smallest such K is Kbest.
- Prior work bounds Lipschitz constants for ReLU, max-pooling, and contrast-normalisation layers using operator norms of learned parameters.
- The paper extends Lipschitz-continuity results to sigmoid, hyperbolic tangent, and softmax layers.
- Bounded Jacobian norms imply Lipschitz continuity on a box-constrained domain.
- For softmax, the supremum can be estimated from preceding layers’ Lipschitz constants and the DNN input’s box constraints.
4 Problem Formulation
The paper defines reachability as bounded function values over an input subspace and shows that instantiating the output function yields output-range, safety, and robustness analyses.
- For a Lipschitz-continuous output function o, reachability computes lower and upper bounds over values produced from an input set X′.
- Because the network and output function are Lipschitz continuous, every value between the bounds is reachable by some input.
- Instantiating o reduces generic reachability to output or logit range analysis, safety verification, and robustness comparisons.
- Output Range Analysis: Output range analysis uses the class projection Πj to quantify how a label confidence varies over an input subspace and error tolerance.
- Safety Verification: Safety is characterised by a reduction whose decision error bound is 2ϵ.
- Robustness: Robustness compares reachability diameters across homogeneous networks or across input subspaces for a fixed network.
5 Confidence Reachability with Guarantees
The paper solves Lipschitz-based reachability over box-constrained inputs by constructing convergent lower and upper bounds for a potentially non-convex objective. Adaptive nested optimisation decomposes high-dimensional search into one-dimensional subproblems while retaining provable error guarantees.
- Problem formulation: The objective w=o·f is minimized over a box-constrained input space, with maximization handled by transformation to minimization.The network-output function is assumed Lipschitz continuous, and the input space is treated as a box constraint.
- Lower-bound construction: Because w is highly non-convex, the method constructs a continuous lower bound h(x,y) satisfying h(x,y) ≤ w(x) and h(x,x) = w(x).The lower bound supports global optimization where gradient-based schemes cannot guarantee the global minimum.
- Lower-bound construction: The function H(x; Yi)=maxy∈Yi h(x,y) produces a sequence of lower bounds l_i that increases toward the global minimum.Adding points to Yi strengthens the lower-bound function while preserving l_i ≤ minx w(x).
- Bound refinement: The upper bound u_i is updated with the best observed objective value, while iterations terminate when |u_i−l_i| ≤ ϵ.The upper and lower sequences provide the stopping criterion and the certified approximation interval.
- Convergence guarantees: The lower bounds are strictly increasing and converge to minx∈[a,b] w(x), while the upper bounds converge to the same value, so u_i−l_i tends to zero.The convergence proof establishes both monotonicity and asymptotic closure of the certified interval.
- Nested optimisation: The nested scheme decomposes multidimensional optimization into sequential one-dimensional subproblems and back-propagates their minima to obtain the global minimum.Adaptive optimization considers active univariate subproblems together, and the overall error bound grows linearly with the one-dimensional error bounds.
6 Proof of NP-completeness
The paper proves the generic reachability problem is NP-complete by establishing polynomial-time membership and reducing 3-SAT to DNN reachability. The reduction constructs a four-layer ReLU network whose output reaches zero exactly when the Boolean formula is unsatisfiable.
- Complexity result: The generic reachability problem is shown to be NP-complete.The section explicitly establishes NP membership and provides a reduction from 3-SAT.
- NP membership: The one-dimensional optimization procedure converges in linear time with respect to the size of region [a, b].Its improvement per iteration is linear with respect to the error bound ϵ.
- NP membership: A nondeterministic algorithm guesses the dimensions and ordering needed to reach the global optimum, then applies one-dimensional optimization backward across them.The guess is polynomial-time, and the one-dimensional procedure has polynomial-time convergence.
- 3-SAT reduction: The 3-SAT reduction constructs a four-layer DNN with n input neurons and m output neurons, representing variables and clauses respectively.The two hidden layers use ReLU units, while the output layer has no ReLU.
- 3-SAT reduction: The clause neurons are positive exactly when their corresponding clauses are satisfied, while the output layer negates these values and takes their maximum.The resulting function w = o·f reaches zero precisely when at least one clause is unsatisfied.
- 3-SAT reduction: The constructed function cannot reach zero when the formula is satisfiable, whereas an unsatisfiable formula yields a clause and output value equal to zero.This establishes the equivalence required for the reduction.
7 Experiments
Experiments compare the reachability tool with constraint-based methods and evaluate safety, robustness, scalability, and supported network architectures. The results show stable performance on benchmark networks, quantitative safety and robustness comparisons, and applicability to larger and more varied DNNs.
- Comparison with State-of-the-art Methods: The tool averages around 5s on six benchmark networks, a 36-fold improvement over SHERLOCK and nearly 100-fold over Reluplex, excluding timeouts.This comparison uses results from a more powerful experimental platform for the baselines than for the tool.
- Comparison with State-of-the-art Methods: The algorithm’s performance is not considerably affected by increasing neuron and layer counts, unlike Reluplex and SHERLOCK.The reported comparison is based on the six benchmark neural networks and Fig. 2.
- Safety and Robustness Verification by Reachability Analysis: DNN-6 is safest overall, while Feature-1 and Feature-2 are more easily perturbed than Feature-3 and Feature-4.No evaluated DNN is 100% safe on the selected features, and safety rankings are consistent across DNNs for the same feature.
- Safety and Robustness Verification by Reachability Analysis: DNN-6 and DNN-5 are most robust overall, whereas DNN-1, DNN-2, and DNN-3 are less robust; Feature-3 and Feature-4 are more robust than Feature-1 and Feature-2.Robustness is compared using boxplots of reachability diameters for networks and features.
- Safety and Robustness Verification by Reachability Analysis: For Feature-3, DNN-4 is guaranteed safe with output range [94.2%, 100%], while DNN-7 has output range [1.8%, 100.0%] and admits adversarial images.The DNN-7 example demonstrates that reachability can quantify the worst adversarial example, not only classify a network as safe or unsafe.
- A Comprehensive Comparison with the State-of-the-arts: The approach handles all known layers used in classification tasks because they are Lipschitz continuous, whereas several comparison tools support only ReLU or ReLU and max-pooling.The compared methods include Planet, MIP, BaB, SHERLOCK, and Reluplex.
- A Comprehensive Comparison with the State-of-the-arts: On ACAS-Xu, the approach performs similarly to BaB and better than other available comparisons, but its stated strength is large-scale networks rather than small-network runtime.The authors report that their laptop was less powerful than the baseline experimental platform.
- A Comprehensive Comparison with the State-of-the-arts: The method’s complexity depends on the number of changed input dimensions rather than hidden neurons and supports state-of-the-art networks with millions of neurons.Other compared tools are reported to handle hundreds or thousands of neurons, while the method handles millions.
8 Conclusion
The paper presents and evaluates a reachability-analysis tool for DNNs with provable guarantees. It supports deep networks and nonlinear activation functions, enabling safety verification and quantitative robustness comparison, while future work targets greater scalability and broader model classes.
- 8 Conclusion: The implemented tool provides provable guarantees for deep neural networks with deep layers and nonlinear activation functions.The paper positions this as a step toward practical guaranteed safety verification for DNNs.
- 8 Conclusion: Experiments demonstrate that reachability analysis can verify DNN safety and quantitatively compare model robustness.The conclusion frames these capabilities as the main demonstrated uses of the tool.
- 8 Conclusion: Future work includes GPU parallelization for larger ImageNet-trained models and generalization to RNNs and deep reinforcement learning.These directions extend scalability and applicability beyond the evaluated feed-forward DNN setting.