PaperlayerView exact revision on arXiv

Source-linked AI summary

Algorithms for Verifying Deep Neural Networks

Changliu Liu, Tomer Arnon, Christopher Lazarus, Christopher Strong, Clark Barrett, Mykel J. Kochenderfer

arXiv:1903.06758v2cs.LGstat.ML

TL;DR

Verifying neural networks over effectively infinite input spaces is difficult, and pointwise validation can miss incorrect generalization or adversarial vulnerabilities. This article introduces a unified framework, surveys reachability, optimization, and search methods, and compares them through implementations and benchmark experiments.

  • Problem

    Pointwise validation cannot check all inputs in an effectively infinite input space and may miss incorrect generalization or adversarial vulnerabilities.

  • Method

    The article introduces a unified mathematical framework, classifies existing verification methods, provides pedagogical implementations, and compares them on benchmark problems.

  • Results

    The survey identifies reachability, optimization, and search as three basic verification methods and reports that bound tightness and runtime vary across algorithms and network depth.

  • Takeaways & Limitations

    The framework connects existing algorithms and supports their comparison across benchmark verification problems.

  • Takeaways & Limitations

    Over-approximation error can accumulate quickly with network depth, while tight estimation may require prohibitively large initial partitions for networks with many inputs.

Abstract

from arXiv · show

Deep neural networks are widely used for nonlinear function approximation with applications ranging from computer vision to control. Although these networks involve the composition of simple arithmetic operations, it can be very challenging to verify whether a particular network satisfies certain input-output properties. This article surveys methods that have emerged recently for soundly verifying such properties. These methods borrow insights from reachability analysis, optimization, and search. We discuss fundamental differences and connections between existing algorithms. In addition, we provide pedagogical implementations of existing methods and compare them on a set of benchmark problems.

1 Introduction

Neural networks combine simple layered computations to represent complex nonlinear functions, but checking their behavior over effectively infinite input spaces requires formal verification. This article surveys sound verification methods based on reachability, optimization, and search, presenting a unified framework, implementations, and benchmarks.

  • Background: Neural networks map inputs to outputs through affine transformations followed by nonlinear activation functions such as ReLU.ReLU sets negative inputs to zero, while learned transformation matrices allow networks to represent complex nonlinear functions.
  • Motivation: Testing many sampled inputs cannot establish behavior over the effectively infinite input space or prevent failures on unseen and adversarial inputs.A network may perform well on sampled points while failing to generalize to new situations.
  • Verification problem: Formal verification checks whether every input in a set X produces an output in a specified set Y, supporting classification and control properties.The surveyed algorithms are sound, although approximations can sacrifice completeness for computational efficiency.
  • Method categories: The survey classifies methods into reachability, optimization, and search, with search commonly combined with reachability or optimization.Reachability propagates sets layer by layer; optimization encodes the network as constraints; search seeks counterexamples.
  • Scope and contributions: The article provides a unified mathematical framework, pedagogical implementations, and benchmark comparisons while excluding testing, binarized networks, recurrent networks, training, floating-point robustness, and compression.The implementation is provided in Julia, and the article also distinguishes its scope from other reviews.

2 Problem Formulation

This section formalizes feedforward neural networks and verification as checking whether every output reachable from an input set satisfies an output constraint. It also describes supported set representations and the possible verification results.

  • 2.1 Feedforward Neural Network: A feedforward network composes layers that apply affine transformations followed by monotone, non-decreasing activation functions such as ReLU.Each layer uses a weight matrix, bias vector, and activation function; the article focuses mainly on ReLU networks.
  • 2.2 Verification Problem: The verification problem asks whether all inputs in X ⊆ D_x produce outputs in Y ⊆ D_y.The network is represented as y = f(x), and the input and output sets impose the corresponding constraints.
  • 2.2 Verification Problem: Classification robustness requires every input within an allowable ℓ_p disturbance of x_0 to preserve the desired label, expressed by y_i* > y_j for all j ≠ i*.The ℓ_∞ and ℓ_1 norms are common because they lead to linear constraints.
  • 2.2 Verification Problem: The framework supports general input and output geometries, while simplifying analysis to polytopes and polytope complements.Representations include H-polytopes, V-polytopes, hyperrectangles, zonotopes, convex star sets, and halfspaces.
  • 2.2 Verification Problem: Zonotopes use affine transformations of unit-hypercube parameters, whereas convex star sets allow those parameters to satisfy general polytope constraints.Star sets can encode any zonotope and are used in symbolic reachability analysis.
  • 2.3 Results: A counter-example result provides x* ∈ X when the property is violated, while an adversarial result reports the maximum allowable disturbance preserving f(x) ∈ Y.The adversarial quantity is defined relative to an ℓ_p norm; exceeding it violates the property.
  • 2.3 Results: A reachability result returns the output reachable set, and the property is violated when that set does not belong to Y.Polytope complements encode unbounded sets and are used as convex constraints in optimization-based methods.

3 Overview of Methods

The survey organizes verification algorithms around reachability, optimization, and search, then compares their soundness, completeness, scalability, and representative techniques. Methods combine these foundations differently, trading exactness, efficiency, and search capability.

  • Method Categories: The survey groups existing methods into five categories built from reachability, optimization, and search.The categories are reachability, primal optimization, dual optimization, search and reachability, and search and optimization.
  • Reachability: Reachability methods analyze the network layer by layer to compute reachable sets.ExactReach is sound and complete but does not scale because its number of polytopes grows exponentially; Ai2 and MaxSens use approximations for better scalability but are incomplete.
  • Optimization: Primal optimization encodes ReLU networks as linear or mixed-integer linear constraints to search for counterexamples.NSVerify is sound and complete, MIPVerify is complete and estimates maximum allowable input disturbance, while ILP is not complete because it considers one linear segment.
  • Optimization: Dual optimization simplifies constraints by replacing the primal problem with a more complex objective, often using relaxations.Duality formulates an efficiently solvable unconstrained convex problem, while ConvDual uses a fixed dual-feasible solution for greater computational efficiency.
  • Search and Reachability: Reachability combined with search can improve efficiency and accuracy, but over-approximation makes these methods sound and potentially incomplete.ReluVal reduces output over-approximation through symbolic interval analysis and iterative input-range bisection; Neurify tightens this with symbolic linear relaxation and constraint refinement.
  • Search and Reachability: Fast-Lin is generally more scalable than Fast-Lip, whereas Fast-Lip provides better solutions for ℓ1 bounds.Fast-Lip builds on Fast-Lin's activation bounds and estimates the network's local Lipschitz constant.
  • Search: Search is commonly combined with reachability or optimization because those methods provide directions for finding falsifying inputs.Search may operate in the input or hidden spaces, and DLV searches layer by layer in hidden spaces while supporting any activation function.

4 Preliminaries

The preliminaries establish interval and geometric-set operations used to propagate bounds, refine domains, and bound gradients through neural networks. These operations explain how verification methods control over-approximation and search complexity.

  • Common Operations: The chapter introduces node-wise bounds, set splitting, and gradient bounds as common components of verification algorithms.Node-wise bounds support methods including MIPVerify, Duality, ConvDual, Planet, and Reluplex; set splitting supports ReluVal, BaB, ExactReach, Ai2, and Neurify.
  • Interval Arithmetic: Interval arithmetic propagates lower and upper bounds layer by layer through linear mappings and monotone non-decreasing activations.The implementation can return either after-activation bounds ℓi, ui or before-activation bounds ˆℓi, ˆui.
  • Geometric Sets: For polytope and star-set reachable representations, node bounds are computed by solving linear programs.The bounds minimize or maximize a node coordinate subject to the representation's linear constraints.
  • Set Split: Set splitting reduces over-approximation by decreasing activation-status ambiguity in nonlinear regions.Both input intervals and hidden-node reachable sets can be refined during verification.
  • Interval Refinement: Interval refinement splits a high-dimensional hyperrectangle into two intervals along a selected coordinate.BaB selects the longest dimension, i∗ = arg max_i(ui − li), as its split index.
  • Constraint Refinement: Constraint refinement splits polytopes or star sets by adding complementary halfspace constraints.For ReLU, these constraints can represent alternative activation states of a node.
  • Gradient Bounds: Gradient bounds are propagated using the chain rule and interval arithmetic over activation derivatives and layer mappings.Point-wise gradients are evaluated at a single input, while ReluVal and FastLip compute maximum gradients over an input set.

5 Reachability

Reachability methods verify neural-network properties by propagating input sets through each layer and checking whether the resulting output reachable set satisfies the output constraint. They differ mainly in how they handle nonlinear mappings, trading exactness and dependency tracking against computational tractability.

  • 5.1 Overview: Reachability methods propagate an input set layer by layer, then check whether the output reachable set is contained in the required output set.The network computation applies an affine map followed by an activation at each layer; the final inclusion check determines whether the property holds.
  • 5.2 ExactReach: Exact reachability tracks reachable sets for every linear segment, splitting sets whenever they cross nonlinear regions.This approach is applicable to piecewise linear networks, but the number of linear segments can grow substantially.
  • 5.1 Overview: Over-approximation supports arbitrary nonlinear activations by replacing reachable sets or nonlinear functions with tractable approximations.Set over-approximation uses geometric templates, whereas function over-approximation relaxes activations between linear lower and upper bounds.
  • 5.1 Overview: Split-and-join computes sets for individual linear regions and joins them by over-approximation, while interval arithmetic computes separate bounds for each node.Symbolic propagation retains dependencies through symbolic lower and upper bounds, unlike ordinary interval arithmetic.
  • 5.2 ExactReach: Exact reachability produces a tight output set, whereas Ai2 keeps the number of output geometric objects equal to the number of input objects and is therefore more scalable but incomplete.The survey identifies over-approximation as the source of Ai2's incompleteness and notes that symbolic propagation can further improve efficiency.
  • 5.4 MaxSens: MaxSens avoids growth in the number of geometric objects during propagation, but over-approximation error accumulates with network depth and may require a prohibitively large initial partition.Sparse partitions can become overly conservative, while specification-guided partitioning adapts resolution to the verification problem.

6 Primal Optimization

Primal optimization encodes a neural network’s nonlinear constraints within optimization problems, using exact, relaxed, or mixed-integer linear representations. These formulations trade modeling simplicity, tightness, feasibility, and completeness in different ways.

  • Optimization formulation: Primal verification formulates an optimization problem whose main difficulty is the network’s nonlinear, non-convex constraint.The objective may depend on inputs, outputs, and their domains.
  • Optimization formulation: Decision variables can represent all network nodes or the binary activation status of ReLU units.NSVerify, MIPVerify, and ILP use both kinds of variables.
  • Linear encodings: For fixed activation patterns, ReLU networks become linear constraints; ILP uses the pattern of a reference input and iteratively adds omitted inequalities.The reference input is chosen as the center of the input constraint set in the implementation.
  • Relaxations: Relaxed linear encodings preserve feasibility by dropping some ReLU inequalities, but the resulting optimization can permit violations of the original constraints.Slack variables can estimate such violations, and Planet uses them to detect conflicts among activation patterns.
  • Relaxations: Triangle relaxation uses node bounds to encode ReLU constraints, while parallel relaxation changes one constraint and is used in FastLin before reachability analysis.Node-wise triangle relaxation can lose dependencies between nodes; k-ReLU was introduced to make the relaxation tighter.
  • Mixed-integer encodings: Mixed-integer encodings represent ReLU constraints with binary variables, but naive formulations require a sufficiently large m or may produce errors.Bound-aware mixed-integer constraints can provide tighter encodings when node bounds are available.

7 Dual Optimization

Dual optimization transforms network-constrained verification into simpler optimization problems over dual variables, often using relaxations for nonlinear activations. The resulting dual values provide bounds used to determine whether properties are satisfied.

  • Dual formulation: Dual optimization simplifies complicated primal network constraints into multiple independent optimization problems, with objectives measuring output-constraint violation.The dual problem provides a valid bound on the violation.
  • Dynamic programming: Dynamic programming reduces a nonlinear optimization problem to one whose objective depends only on the network input by propagating value functions backward.The backward recursion constructs a dual network whose mappings run opposite to the original network.
  • Dual variables: Dual-network variables encode the weights of hidden-node values in the objective and coincide with backpropagated gradients when hidden-layer objectives are zero.They are also related to Lagrange multipliers when bounds on node variables are ignored.
  • Relaxations: Approximations of nonlinear activation dual functions make the dual network tractable; ConvDual uses triangle relaxation and FastLin uses parallel relaxation.Relaxations are introduced because the dual function can depend on the activation input.
  • Verification criterion: The optimal solution of the dual problem provides an upper bound on the primal problem, and a negative dual value certifies satisfiability.For the stated dual formulation, negativity of the optimum determines that the problem is satisfied.

8 Search and Reachability

Search-and-reachability methods combine conservative reachable-set computation with targeted input refinement to resolve uncertain cases. Symbolic propagation and influence-guided splitting improve bounds while retaining a search-based path to counterexamples.

  • Method combinations: ReluVal, Neurify, FastLin, and FastLip combine reachability approximations with search strategies for finding potential violations.Their combinations include symbolic intervals, linear relaxation, network approximation, binary search, and local Lipschitz estimation.
  • Symbolic intervals: Symbolic interval propagation tracks input dependencies layer by layer, producing tighter bounds than ordinary interval arithmetic.The resulting output reachable set is a hyperrectangle formed from concrete lower and upper bounds.
  • Symbolic intervals: ReluVal propagates symbolic bounds through affine layers and ReLU activations, distinguishing always-active, never-active, and undetermined nodes.Undetermined nodes receive relaxed bounds, while concrete maxima can discard input dependencies when the symbolic upper bound is negative.
  • Verification and search: ReluVal checks reachable-set inclusion, samples uncertain intervals for counterexamples, and returns holds, violated, or unknown outcomes.An uncertain interval is refined when its reachable set overlaps the target output set without being contained in it.
  • Verification and search: Iterative interval refinement bisects the input feature with the highest gradient-based smear value to reduce overapproximation.The smear value combines gradient bounds with the corresponding input radius.
  • Neurify: Symbolic linear relaxation cuts 59.64% more over-approximation error than ReluVal’s symbolic interval propagation, but its relaxed set is not always a subset of the concretized set.The upper bound remains valid, while the relaxed lower bound can become negative.

9 Search and Optimization

Search-and-optimization methods exploit the piecewise linearity of ReLU networks to compute output bounds through alternating local optimization and global feasibility search. Sherlock tightens bounds iteratively, while related branching methods search activation assignments and can determine whether counterexamples exist.

  • Sherlock: Sherlock combines local and global search to compute tight output bounds for ReLU networks.Local search optimizes within one linear segment, while global search seeks a point improving the bound by solver-specified ϵ.
  • Sherlock: Local search solves a linear program within the activation pattern of a sampled point, producing a local optimum on that line segment.The network is encoded with linear constraints that confine the function to the segment containing the reference point.
  • Sherlock: Global search solves a feasibility problem to test whether the current bound can improve by at least ϵ, then restarts local search from any improving point.If no improving point exists, the last local-search bound is retained.
  • Sherlock: Sherlock classifies a property as holds, violated, or unknown by comparing its ϵ-expanded reachable set with the output constraint.Smaller ϵ makes the result more accurate and less likely to be unknown; violated cases can return a counterexample.
  • Sherlock: For verification alone, a single NSVerify feasibility step can be more computationally efficient than Sherlock’s repeated optimization calls.Sherlock’s key advantage is producing tight bounds, whereas direct feasibility checking targets only the given output constraint.
  • Planet: Planet’s elastic filtering fixes the node with the largest positive slack to identify conflicts faster during activation-assignment search.Conflicts are added back to the clauses before the SAT problem is solved again.
  • Reluplex: Reluplex-style search branches on broken ReLU nodes, exploring active and inactive assignments until it finds a counterexample or proves none exists.The worst-case search traverses a binary tree of depth |U|, with complexity 2^|U|.

10 Comparison and Results

The article compares pedagogical implementations of neural-network verification algorithms across bound-tightening, runtime, and benchmark experiments. Results expose a trade-off between bound tightness, completeness, runtime, and scalability.

  • Algorithm comparison: The implementations compare algorithms grouped by reachability, optimization, and search, including methods that encode the same properties through different input and output sets.The comparison also covers bound-tightening techniques and algorithms with different supported specifications and result types.
  • Bound experiments: Planet and Ai2z + Planet typically provide the tightest bounds, followed by Ai2z and ConvDual, Neurify, ReluVal, and Ai2 Box.Bounds generally loosen deeper in the network, although the trend is less clear for ConvDual and Ai2z.
  • Bound experiments: Triangular LP relaxation produces the tightest bounds but is computationally expensive, while Ai2z bounds can reduce runtime without changing the resulting bounds.ConvDual and Ai2z produced the same bounds, as did interval arithmetic and Ai2z box.
  • Performance experiments: Higher true positive rates generally require significantly longer runtimes, with average runtimes differing by multiple orders of magnitude across the range.At low true positive rates, the relationship is non-monotonic and may reflect the sample size or different approximation schemes.
  • Performance experiments: Complete algorithms generally run longer and scale less well to larger networks, whereas incomplete algorithms often terminate faster but can return :violated for properties that hold.Algorithms that return fewer incorrect :violated results also tend to take longer, and optimization-based methods showed numerical stability issues in MIPVerify and Planet.
  • Benchmark experiments: The experiments demonstrate that many algorithms can verify realistic ACAS Xu networks, while the pedagogical implementations may be slower because readability was favored over speed.Some implementations are simplified versions of the originals but still produce the same results.
Loading 1903.06758v2…