Source-linked AI summary
An approach to reachability analysis for feed-forward ReLU neural networks
Alessio Lomuscio, Lalit Maganti
TL;DR
Formal verification methods have largely not targeted neural networks, despite their anticipated role in future AI systems. This paper studies reachability in ReLU feed-forward networks by encoding it as a linear-programming problem, then evaluates the method on benchmark controllers and networks, finding that it solves several practical cases while remaining bounded by network and search complexity.
Problem
Formal-verification techniques have largely targeted programs or traditional models, leaving systems based on neural networks insufficiently addressed.
Method
The paper formally encodes reachability in ReLU feed-forward neural networks as an associated linear-programming problem and solves it with Gurobi.
Results
The methodology solves reachability for several neural networks of interest, including three-layer deep networks of significant size and benchmark controllers.
Takeaways & Limitations
The approach provides a practical methodology for analyzing whether specified outputs can be produced by ReLU feed-forward networks.
Takeaways & Limitations
The current methodology is restricted to feed-forward networks, while recurrent-network reachability remains future work.
Abstract
from arXiv · showhide
We study the reachability problem for systems implemented as feed-forward neural networks whose activation function is implemented via ReLU functions. We draw a correspondence between establishing whether some arbitrary output can ever be outputed by a neural system and linear problems characterising a neural system of interest. We present a methodology to solve cases of practical interest by means of a state-of-the-art linear programs solver. We evaluate the technique presented by discussing the experimental results obtained by analysing reachability properties for a number of benchmarks in the literature.
1 Introduction
The paper addresses the limited formal-verification support for neural-network-based AI systems by studying reachability in ReLU feed-forward networks. It connects whether a network can produce an output with linear-programming problems and evaluates the approach on literature benchmarks.
- Formal verification is increasingly sought for complex and safety-relevant AI systems, including autonomous vehicles and decision-making systems.
- Existing AI-verification research largely targets programs or traditional finite-state and multi-agent-system models rather than neural networks.
- The paper studies reachability for possibly multilayer feed-forward neural networks whose activation functions are ReLUs.
- The proposed method checks whether a particular output, potentially representing a bug, can ever be produced by a given neural network.
- The paper encodes neural networks and reachability questions as linear programs, applies the technique to a pole-balancing benchmark, and evaluates scalability on networks of various sizes.
- Existing dataset-based correctness checks are probabilistic, while prior linear-programming work on ReLU networks was tailored to adversarial inputs rather than reachability.
2 Preliminaries
The preliminaries define feed-forward neural networks as weighted directed acyclic graphs organized into layers, with activation functions and vector-matrix representations. They introduce the computed network function and the linear and mixed-integer linear-programming concepts used later.
- A feed-forward neural network is a weighted, directed, acyclic graph whose vertices are organized into ordered layers.
- Each layer after the first is associated with an activation function, and this paper restricts those functions to ReLU.
- ReLU is defined as ReLU(x) = max(x, 0) and is described as replacing sigmoid and tanh partly because it improves convergence during training.
- Layer weights and biases are represented with matrices and vectors, supporting the usual affine transformation followed by activation.
- The network computes a function by composing the layer functions f^(i)(x) = σ^(i)(W^(i)x + b^(i)) across layers.
- A linear program has a linear objective and linear constraints, while a mixed-integer linear program additionally permits integer variables and constraints.
- The experiments use the Gurobi solver, which the paper characterizes as performing well across a wide range of problems.
3 Verifying Reachability for FFNN
The paper defines FFNN reachability as whether an output set can be produced from an input set, then reduces this question to feasibility of a linear program encoding the ReLU network.
- Motivation: This reachability formulation supports safety analysis and can identify whether a specified output, potentially representing a bug, is ever produced.The paper positions the approach as addressing the limited formal-verification methodology available for neural-network systems.
- Reachability definition: Reachability asks whether some output in O can be computed from some input in I through the network.The input and output sets are restricted to those representable by finitely many linear constraints.
- Linear encoding: The method formally encodes ReLU FFNNs layer by layer using real variables for layer values and binary variables for activation states.A sufficiently large constant M appears in the encoding constraints.
- Linear encoding: The network encoding combines input constraints, layer constraints, and output constraints into a single reachability linear program.The resulting program uses Cin, C, and Cout, with objective z = 0.
- Correctness: O is reachable from I if and only if the corresponding linear program has a feasible solution.The equivalence follows by mapping feasible network computations to assignments of the LP variables and conversely.
4 Verifying a Neural Controller for the Inverted Cart Problem
The paper applies LP-based reachability analysis to a ReLU neural controller for the inverted pendulum on a cart, identifying both satisfied and violated control specifications. Floating-point tolerances are incorporated to avoid unsound conclusions.
- Controller and system: The controller is trained with reinforcement learning because the system’s inherent non-linearity prevents traditional controller methods from being used directly.The network is produced using KERAS and KERAS-RL.
- Controller and system: The inverted pendulum controller receives four state variables and outputs q-values for left and right actions through three 16-node ReLU hidden layers.The output layer has two nodes and no ReLU activation.
- Reachability encoding: Floating-point tolerances and epsilon variables are used to link layers safely, because careless rounding can make a safe assessment unsound.The experiments use 1e−6 generally and 1e−4 for binary inputs.
- Specifications and results: The first specification is unreachable, indicating a strong preference for applying 10N when the pendulum leans right in the specified state.The result concerns S = (0, 0, −5, 0) and compares the two action q-values.
- Reachability encoding: The network is compiled into an LP and solved with Gurobi; a feasible solution demonstrates that the queried configuration and output can occur, while infeasibility proves unreachability by completeness.This procedure supports both reachability and safety conclusions for the analyzed input space.
- Specifications and results: The analysis finds a bug in the synthesized controller in under 1s, whereas testing is incomplete and may take considerably longer to reveal the need for retraining.The solver-produced values can be fed back into the network to confirm the violation.
5 Experimental Results
Experiments evaluate the LP reachability methodology across control, text-classification, and image-recognition networks, with scalability shaped by state-space size, variable counts, binary variables, and constraints. The reported benchmarks include fast solves for several networks and longer solves for demanding acrobot specifications.
- Experimental scope: The experiments assess scalability rather than validating the benchmark problems, and reachability is not applicable to some cases such as Reuters and MNIST.The evaluations use Gurobi on an Intel Core i7-4790 CPU.
- Control benchmarks: Inverted-pendulum reachability queries were each solved in less than 1 sec, including additional specifications tested for performance degradation.The authors report no tested IPCP specification that required more than 1 sec.
- Control benchmarks: Pendulum and Mountain Car specifications were verified in less than 1 sec, while more complex acrobot specifications took up to 45 sec.The demanding acrobot cases required searching a large part of a relatively high-dimensional state space.
- Classification benchmarks: A Reuters network experiment fixed all but 50 binary inputs and omitted softmax to reduce encoding complexity.The network is shallow but contains many input and hidden neurons.
- Classification benchmarks: 45 secs was sufficient to find an input producing a known pre-softmax output for a network with a binary input.The authors describe this performance as attractive given the hidden-layer size and number of binary variables.
- Image-recognition benchmark: The MNIST feed-forward portion produced the known input in just over 2 secs, despite network layers containing between 10^2 and 10^3 nodes.Softmax was omitted from the encoding.
- Scaling factors: The authors conjecture that the larger number of binary variables caused the performance gap between the Reuters and MNIST experiments.This is presented as a conjecture rather than an established causal result.
- Scaling factors: Overall, the methodology solved reachability for several networks, including deep three-layer networks, with performance depending chiefly on state-space size, variable counts, binary variables, and constraints.The conclusion concerns the methodology paired with the studied optimisations.
6 Conclusions
The paper establishes a linear-programming correspondence for reachability in feed-forward neural networks and demonstrates that the method handles networks of significant size. Future work extends the investigation to recurrent networks and synthesised engineering controllers.
- The paper formally relates reachability in feed-forward neural networks to an associated linear programming problem.The methodology also addresses floating-point arithmetic and optimises the corresponding linear program.
- Experimental results demonstrate that the method can solve reachability for networks of significant size.
- Future work will study recurrent networks and apply the results to synthesised controllers in engineering.