Source-linked AI summary
Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks
Ruediger Ehlers
TL;DR
Formal verification of piece-wise-linear neural networks is difficult despite their use in deep learning and safety-relevant applications. The paper combines a global linear approximation with SAT- and linear-programming-based phase reasoning, evaluating the approach on collision avoidance and handwritten digit recognition. The authors report substantially shorter verification times, while noting fragility, timeouts, and the need to simplify the original LeNet architecture in experiments.
Problem
Piece-wise-linear neural networks are widely used but remain difficult for modern SMT and ILP solvers to verify, limiting formal assurance of their properties.
Method
The approach combines a global linear approximation with SAT-guided node-phase search, linear programming, conflict analysis, and inference of implied phases and safe fixtures.
Results
The approach yields much shorter verification times and is evaluated on collision avoidance and handwritten digit recognition case studies.
Takeaways & Limitations
The method supports arbitrary convex verification conditions and modern piece-wise-linear node types such as ReLU and MaxPool.
Takeaways & Limitations
The approach remains fragile and prone to timeouts for difficult properties, and experiments required simplifying the original LeNet architecture.
Abstract
from arXiv · showhide
We present an approach for the verification of feed-forward neural networks in which all nodes have a piece-wise linear activation function. Such networks are often used in deep learning and have been shown to be hard to verify for modern satisfiability modulo theory (SMT) and integer linear programming (ILP) solvers. The starting point of our approach is the addition of a global linear approximation of the overall network behavior to the verification problem that helps with SMT-like reasoning over the network behavior. We present a specialized verification algorithm that employs this approximation in a search process in which it infers additional node phases for the non-linear nodes in the network from partial node phase assignments, similar to unit propagation in classical SAT solving. We also show how to infer additional conflict clauses and safe node fixtures from the results of the analysis steps performed during the search. The resulting approach is evaluated on collision avoidance and handwritten digit recognition case studies.
1 Introduction
Neural networks achieve strong performance on difficult tasks, including safety-relevant applications, but their formal verification remains challenging. The paper addresses this challenge with a piece-wise-linear verification approach supporting broader network architectures and verification properties.
- Motivation: Neural networks help solve tasks that are difficult to formalize, including image-based digit recognition and obstacle detection in self-driving cars.Deep-learning systems achieve high classification precision and outperform human classifiers on some tasks.
- Motivation: Safety cases specify environment conditions and desired outputs, making neural-network verification relevant to certification and system-engineering feedback.Examples include detecting all concretizations of an abstract obstacle model and preserving a digit classification for nearby images.
- Related work: Existing verification methods struggle to scale, with reported experiments challenging networks containing only 6 or 26 nodes.Pulina and Tacchella’s approach scales only to small networks, while another SMT-based study found 26-node instances challenging.
- Related work: Piece-wise linear activations improve amenability to formal verification, but prior approaches cited here focus on robustness testing or lack support for general verification properties.These approaches use linear-arithmetic reasoning after selecting node phases, while related methods target robustness rather than general properties.
- Contribution: MaxPool support avoids replacing MaxPool behavior with a much larger number of ReLU nodes.This targets modern architectures in which MaxPool nodes are important for feature detection.
- Contribution: The proposed approach verifies piece-wise-linear networks, including MaxPool and ReLU architectures, against convex specifications using SAT solving, linear programming, and a global linear approximation.The approximation prunes node-phase search, while specialized conflict analysis and phase inference shorten verification times; case studies cover collision avoidance and character recognition.
2 Preliminaries
The paper models feed-forward networks as directed acyclic weighted graphs with linear, ReLU, and MaxPool nodes. Network evaluation assigns values recursively, while node phases describe the active piece-wise-linear behavior used for verification.
- Feed-Forward Neural Networks: The considered networks are multilayer perceptrons with linear, ReLU, and MaxPool nodes represented as directed acyclic weighted graphs.Graph components include nodes, edges, edge weights, node biases, and node types.
- Feed-Forward Neural Networks: A network with n inputs and m outputs represents a function from R^n to R^m through a node-value assignment for each input vector.Input and output node orderings determine how vectors enter and leave the network.
- Node semantics: Linear nodes compute weighted sums of predecessor values plus a bias, whereas ReLU nodes apply the maximum of that sum and zero.These definitions describe the node-value assignment used by the network semantics.
- Node semantics: MaxPool nodes output the maximum predecessor value, ignoring incoming edge weights and node biases.The selected predecessor determines a MaxPool phase; ties permit multiple phases.
- Node phases: ReLU phases distinguish nonpositive pre-activation from nonnegative pre-activation, with zero eligible for either phase.MaxPool phases identify incoming edges whose predecessor value equals the node value.
- Classification and assumptions: Classification assigns the index of the largest output component, and the paper assumes network weights and biases are already given rather than learned during verification.Learning frameworks can obtain these parameters from example databases, while the verification problem operates on the resulting network.
- Solver preliminaries: SAT solvers handle Boolean formulas, linear programming handles real-valued linear constraints, and SMT solvers combine SAT with theory-specific decision procedures.These computational tools provide the foundations for the paper’s verification setting.
3 Efficient Verification of Feed-forward Neural Networks
The paper formulates neural-network verification as finding node assignments satisfying linear input-output constraints, then combines linear approximations with SAT-style phase search to solve it efficiently. The approach tightens approximations, checks partial phase fixtures, learns conflicts, caches feasible fixtures, and propagates implied phases.
- Verification problem: The NN verification problem asks whether a node assignment satisfies the property constraints and exactly matches the network’s input-output behavior.Arbitrary Boolean combinations can be encoded into the network through an additional output neuron, reducing the property to a linear constraint.
- Integrated search: The solver combines a global linear approximation with SAT variables for ReLU and MaxPool phases, using linear programming to check partial phase assignments.The SAT component performs propagation, clause learning, branching, and backtracking, while the LP component checks approximation feasibility before branching.
- Linear approximation: ReLU and MaxPool nodes require linear over-approximations because their input-output behavior is non-linear until node phases are fixed.ReLU constraints use bounds on the weighted input, while MaxPool constraints provide tight linear constraints without requiring upper bounds.
- Linear approximation: Known input bounds and interval arithmetic provide initial lower and upper bounds for node values, which are then tightened by optimizing each node variable under the verification constraints.The tightening process minimizes each variable and its negation to obtain new bounds for subsequent approximations.
- Conflict and fixture analysis: Infeasible partial phase fixtures are discarded by learned conflict clauses, while elastic filtering identifies smaller sets of phase choices that already imply infeasibility.Feasible partial fixtures are also cached, avoiding repeated LP calls for the same fixture or one of its partial fixtures.
- Implied phase inference: Implied phase detection propagates lower and upper flow bounds in linear time, extending SAT-style partial assignments before later LP feasibility checks.This propagation is considerably faster than an LP solver call and makes the subsequent linear approximation tighter.
4 Experiments
The experiments evaluate Planet on vehicle-collision and handwritten-digit verification tasks, comparing it with SMT and ILP solvers and testing robustness properties. The results show that linear approximation constraints substantially improve solver practicality and support nontrivial image-noise verification.
- Experimental setup: Planet combines GLPK 4.611 with a modified Minisat 2.2.0 search procedure for verification experiments.The tool is implemented in C++ and repeatedly tightens the initial approximation, with a 5000-node approximation limit.
- Collision avoidance: 86 out of 100 training attempts produced a collision network with 100% accuracy on all example tuples.The architecture used 40 linear nodes, MapPool nodes with four inputs each, 19 ReLU nodes, and two ReLU output nodes.
- Collision avoidance: 500 vehicle-collision verification instances were generated from safety-margin exploration using bisection over ϵ ∈[0, 0.05] with precision 0.002.The instances were compared against Yices 2.5.2 and Gurobi 7.02, with a one-hour timeout.
- Collision avoidance: Adding the paper’s linear approximation constraints makes Gurobi and Yices practical on the collision benchmarks, while Yices remains slower than Planet.Gurobi becomes slightly faster than Planet in most cases; the comparison is skewed because Yices uses arbitrary-precision arithmetic.
- MNIST digit recognition: 9 minutes 2.4 seconds sufficed to verify that the network never misclassifies the Figure 5(a) image as a 4 under the adjacent-pixel noise model.The model restricts adjacent-pixel noise differences to ≤0.05 while allowing many pixels to have large deviations.
5 Conclusion
The paper presents a piece-wise-linear neural-network verification approach combining a global linear approximation with specialized search techniques. It reports broader verification conditions and practical evaluation, while acknowledging fragility, timeouts, and network-size constraints.
- 5 Conclusion: The approach adds a global linear approximation of network behavior to SMT or ILP verification instances and combines it with SAT-guided node-phase analysis.The specialized techniques include inference of node phases, conflict clauses, and safe node fixtures.
- 5 Conclusion: The method supports arbitrary convex verification conditions and uses them to define a handwritten-digit robustness noise model.
- 5 Conclusion: The approach was released as open-source software to support co-development of verification tools and neural-network architectures that are easier to verify.Its scope is limited to networks whose components all use piece-wise linear activation functions.
- 5 Conclusion: The verification process remains fragile and prone to timeouts on difficult properties, and the experiments required simplifying the original LeNet architecture.Without simplification, obtaining a lower bound for one network variable took more than 30 minutes.