PaperlayerView exact revision on arXiv

Source-linked AI summary

Output Reachable Set Estimation and Verification for Multi-Layer Neural Networks

Weiming Xiang, Hoang-Dung Tran, Taylor T. Johnson

arXiv:1708.03322v2cs.LG

TL;DR

The paper addresses the difficulty of estimating MLP output reachable sets and verifying their safety. It introduces maximum sensitivity, computes it through optimization for monotonic activations, and uses simulation-based reachable-set estimation to support automated verification, demonstrated on a two-joint robotic arm.

  • Problem

    MLPs are difficult to verify for safety because their complex structures and activation functions make output behavior hard to analyze, while simple neural-network properties can be NP-complete to verify.

  • Method

    The method introduces maximum sensitivity for bounded disturbances around nominal inputs and computes it layer by layer through a chain of optimization problems, including convex optimizations for monotonic activation functions.

  • Results

    The proposed reachable-set estimation and safety-verification procedures were validated numerically and applied to safety verification of a two-joint robotic arm model.

  • Takeaways & Limitations

    The approach provides a simulation-based way to estimate MLP output reachable sets and verify safety based on those estimates.

  • Takeaways & Limitations

    The verification procedure can return UNCERTAIN when the estimated reachable set intersects the unsafe region, so the result is not always decisive.

Abstract

from arXiv · show

In this paper, the output reachable estimation and safety verification problems for multi-layer perceptron neural networks are addressed. First, a conception called maximum sensitivity in introduced and, for a class of multi-layer perceptrons whose activation functions are monotonic functions, the maximum sensitivity can be computed via solving convex optimization problems. Then, using a simulation-based method, the output reachable set estimation problem for neural networks is formulated into a chain of optimization problems. Finally, an automated safety verification is developed based on the output reachable set estimation result. An application to the safety verification for a robotic arm model with two joints is presented to show the effectiveness of proposed approaches.

I. INTRODUCTION

The paper addresses the difficulty of assuring neural-network output safety by developing reachable-set estimation and verification methods for multi-layer perceptrons. Its approach combines maximum sensitivity, finite simulations, and optimization-based analysis.

  • Motivation: Neural networks are widely applied but are often treated as black boxes without effective methods to assure output safety specifications.The paper notes that verification is difficult because neural networks are large-scale, nonlinear, and non-convex.
  • Related work: Existing verification work includes SMT-based methods, abstraction-refinement, and reachable-set estimation approaches for neural networks.The paper identifies reachable-set results as having potential for extension to safety verification.
  • Approach: The proposed method estimates an MLP’s output reachable set from finitely many simulations using maximum sensitivity to bridge sampled and bounded-input behavior.Maximum sensitivity characterizes the maximum output deviation caused by bounded disturbance around a nominal input.
  • Approach: A chain of optimization problems computes maximum sensitivity layer by layer for the considered MLP class.The estimated reachable set is constructed through input-space discretization as a union of reachtubes.
  • Outcome: Safety verification is performed using the estimated output reachable set, and a robotic-arm application demonstrates the proposed approaches.The paper’s sections cover maximum sensitivity, reachable-set estimation, verification, and robotic-arm application.

A. Multi-Layer Neural Networks

The paper models an MLP as a layered feedforward network whose neuron outputs are generated by weighted inputs, biases, and activation functions. It focuses on monotonic activation functions and the resulting nonlinear input-output mapping.

  • Network structure: An MLP contains an input layer, hidden computation layers, and an output layer that produces the output vector.Each layer contains a specified number of neurons, with the input layer indexed as layer 0 and the output layer as layer L.
  • Neuron model: Each neuron transforms weighted inputs and a bias through an activation function to produce its output.The activation function describes the neuron’s reaction to its inputs and may be nonlinear.
  • Activation assumption: The paper assumes activation functions are monotonic, so x1 ≤ x2 implies f(x1) ≤ f(x2).The logistic function is given as an example satisfying this assumption.
  • Network mapping: The output of layer ℓ−1 serves as the input to layer ℓ, producing a composed mapping F from input x[0] to output y[L].The mapping is expressed as the composition fL ◦ fL−1 ◦ · · · ◦ f1.
  • Safety motivation: Although an MLP can approximate nonlinear real-valued functions, slight input perturbations can produce unexpected or incorrect outputs.The paper therefore identifies output reachable-set estimation as necessary for safety verification.

B. Problem Formulation

The problem formulation seeks a small over-approximation of an MLP’s outputs over a bounded input set and uses it to determine whether a safety specification holds. Exact reachable-set computation is difficult because MLPs are large, nonlinear, and non-convex.

  • Reachable set: The output reachable set is the collection of outputs F(x[0]) generated by inputs x[0] in a given set X.An output reachable-set estimation is a set that contains the exact output reachable set.
  • Estimation problem: Exact output reachable-set computation is extremely difficult for large, nonlinear, and non-convex MLPs.The paper proposes over-approximation as a more practical alternative.
  • Estimation problem: The estimation problem asks for a set ˜Y containing Y while making ˜Y as small as possible.This formalizes the objective of producing a tight over-approximation.
  • Safety specification: The safety specification is a predicate over the MLP output, and safety requires the specified condition to hold for the output.The specification is represented by a set in output space describing the safety requirement.
  • Verification: Because Y is contained in its estimation ˜Y, checking the estimation can soundly establish safety when it does not intersect the unsafe region.The paper states that the estimated reachable set is sufficient for safety verification.

III. MAXIMUM SENSITIVITY FOR NEURAL NETWORKS

The paper introduces maximum sensitivity to bound output deviations from bounded input disturbances and computes it layer by layer. Under monotonic activations, the computation becomes a chain of efficiently solvable optimization problems.

  • Maximum sensitivity: Maximum sensitivity measures the maximum output deviation caused by bounded disturbances around a nominal input.This worst-case definition is intended for safety verification rather than average sensitivity analysis.
  • Maximum sensitivity: Unlike expectation-based sensitivity, maximum sensitivity preserves the worst-case information needed for sound safety verification.The paper contrasts its definition with sensitivities based on average deviations over continuous input and weight intervals.
  • Single-layer computation: For one layer, maximum sensitivity is computed by sequentially solving optimization problems for neuron output bounds and sensitivity values.Monotonicity and the infinity norm are used to identify the relevant extrema.
  • Layer-by-layer computation: For an MLP, the method propagates each layer’s output and disturbance bound to the next layer until obtaining εF(x[0], δ) at the output layer.The update uses x[ℓ] = y[ℓ−1] and δ[ℓ] = ε(x[ℓ−1], δ[ℓ−1]).
  • Computational properties: The maximum-sensitivity calculation is converted into a chain of optimization problems, including convex programs for problems (8) and (9).The paper states that existing tools such as cvx and linprog can efficiently solve the convex problems, while (10) and (11) search finite sets.

IV. REACHABLE SET ESTIMATION AND VERIFICATION

The paper estimates MLP output reachable sets by discretizing bounded inputs into lattices, simulating lattice centers, and expanding outputs using maximum-sensitivity reachtubes. The resulting over-approximation supports sound safety verification, with tighter estimates requiring smaller radii and more computation.

  • Reachable set estimation: The input set is covered by finitely many lattices, whose smaller radius yields a more precise approximation but increases their number.For a unit box in R^n, the number of lattices with radius δ is ⌈1/2δ⌉^n.
  • Reachable set estimation: Finite simulations at lattice centers are combined with maximum-sensitivity computations to construct output reachtubes for each lattice.The reachtubes are unioned to estimate the output reachable set.
  • Reachable set estimation: The union of output reachtubes contains all possible outputs generated from the bounded input set, providing an over-approximation of the reachable set.This containment is stated in Proposition 2 and follows from covering the input set with lattices.
  • Example 1: For X1 with δ = 0.1, 25 reachtubes were computed and all 10000 random outputs lay within the estimated reachable set.The experiment used 25 lattices and therefore 25 simulations.
  • Example 1: Smaller radii produced tighter output reachable-set estimates, at the expense of more simulations and computation time.The tested radii were δ ∈ {0.1, 0.05, 0.025, 0.0125}.
  • Safety verification: The MLP is certified safe when its estimated reachable set does not intersect the complement of the safety specification.If the intersection is nonempty, the algorithm may return UNCERTAIN rather than establish safety.
  • Safety verification: In Example 2, δ = 0.1 yielded uncertainty, whereas δ = 0.05 established safety while increasing simulations from 15 to 60.The finer discretization improved verification precision but required more simulations.

V. APPLICATION IN SAFETY VERIFICATION FOR ROBOTIC ARM MODELS

The robotic-arm case study evaluates MLP safety across normal, buffering, and forbidden input zones, showing that reducing the lattice radius can change verification from uncertain to safe.

  • Verification results: For another input set, δ = 0.1 leaves safety undecided because the estimated reachable set intersects the unsafe region, whereas δ = 0.05 confirms safety when it lies within the safe region.These figures illustrate how the radius affects the verification outcome.
  • Robotic-arm model: The MLP predicts the robotic arm end position from joint angles θ1 and θ2 using two inputs, two outputs, and one hidden layer of five neurons.Training data were collected only from the normal working zone; tanh and purelin were used in the hidden and output layers, respectively.
  • Operating zones: The input space [0, 2π] × [0, 2π] is divided into normal working, forbidden, and buffering zones.The buffering zone lies between the normal and forbidden zones and may contain occasional operations outside the normal working region.
  • Verification results: With δ = 0.05, safety is uncertain because the estimated reachable set extends outside the safe region, despite 5000 simulations finding no unsafe output.The finite simulations are not sufficient to soundly claim safety.
  • Verification results: With δ = 0.02, the reachable set is contained in the safe region, which is sufficient to claim safety for the robotic-arm MLP model.This verification covers both the normal working and buffering zones.

VI. RELATED WORK

The related-work discussion distinguishes this reachability-based MLP approach from SMT verification, piecewise-linear activation approximations, pointwise robustness checks, and Lyapunov methods for recurrent networks.

  • SMT and reachability: Reluplex applies SMT-based verification to neural networks with ReLU activations, whereas this paper targets neural-network reachability.Reluplex extends Simplex by exploiting ReLU's piecewise-linear structure.
  • SMT and reachability: Layer-by-layer methods have been developed for computing output reachable sets of ReLU neural networks.The cited approach formulates the computation as set manipulations for a restricted network class.
  • Activation handling: Prior sigmoid-verification methods replace activation functions with piecewise-linear approximations and use black-box SMT solvers, while this approach over-approximates neuron outputs with lower and upper bounds.The paper states that its approach does not approximate the activation functions themselves.
  • Scope of analysis: Local adversarial-robustness methods check behavior around one fixed point, whereas this paper considers a set over a continuous domain.The distinction is between point-centered robustness and input-set reachability.
  • Dynamical-system methods: Lyapunov-function approaches support reachability analysis for recurrent neural networks modeled by differential equations, unlike the nonlinear algebraic MLPs studied here.The paper presents this modeling difference as a reason for using a different approach.

VII. CONCLUSIONS

The paper presents simulation-based output reachable-set estimation and safety verification for MLPs, using maximum sensitivity computed through optimization problems and demonstrating the approach on a two-joint robotic arm.

  • Conclusions: The method estimates MLP output reachable sets from finitely many sampled inputs by using maximum sensitivity results.The maximum-sensitivity computation is based on the monotonicity assumption for activation functions.
  • Conclusions: Maximum sensitivity is formulated as a chain of optimization problems that are essentially convex optimizations for the considered activation-function class.The resulting sensitivity information supports reachable-set estimation.
  • Conclusions: Safety verification is performed from the estimated output reachable set, and numerical examples validate the proposed algorithms.The paper also applies the verification procedure to a robotic arm model with two joints.
Loading 1708.03322v2…