Source-linked AI summary
Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks
Guy Katz, Clark Barrett, David Dill, Kyle Julian, Mykel Kochenderfer
TL;DR
Safety-critical use of DNNs is hindered by the difficulty of providing formal behavioral guarantees. The paper presents Reluplex, an extension of simplex for ReLU constraints, and evaluates it on ACAS Xu networks, where it proves safety and robustness properties and scales beyond prior methods.
Problem
Safety-critical DNN applications need formal guarantees, but DNN verification is difficult because networks are nonlinear and non-convex.
Method
Reluplex extends the simplex algorithm to handle non-convex ReLU constraints while searching for satisfying assignments.
Results
Reluplex proved safety and robustness properties for ACAS Xu networks with 300 ReLU nodes each and scaled to networks an order of magnitude larger than existing techniques could analyze.
Takeaways & Limitations
The ACAS Xu results indicate that Reluplex can verify properties of real-world DNNs without simplifying the networks.
Takeaways & Limitations
Floating-point arithmetic improves confidence through tableau restoration but does not guarantee soundness.
Abstract
from arXiv · showhide
Deep neural networks have emerged as a widely used and effective means for tackling complex, real-world problems. However, a major obstacle in applying them to safety-critical systems is the great difficulty in providing formal guarantees about their behavior. We present a novel, scalable, and efficient technique for verifying properties of deep neural networks (or providing counter-examples). The technique is based on the simplex method, extended to handle the non-convex Rectified Linear Unit (ReLU) activation function, which is a crucial ingredient in many modern neural networks. The verification procedure tackles neural networks as a whole, without making any simplifying assumptions. We evaluated our technique on a prototype deep neural network implementation of the next-generation airborne collision avoidance system for unmanned aircraft (ACAS Xu). Results show that our technique can successfully prove properties of networks that are an order of magnitude larger than the largest networks verified using existing methods.
1 Introduction
DNNs are increasingly used in safety-critical systems, but their nonlinear, non-convex structure makes formal verification difficult. Reluplex extends simplex to verify ReLU networks and scales to substantially larger ACAS Xu networks than prior techniques.
- Motivation: Safety-critical DNN controllers require formal guarantees because small input perturbations can produce unexpected and unsafe behavior.The paper highlights autonomous vehicles and airborne collision avoidance as applications where this issue matters.
- Motivation: DNN verification is difficult because networks are large, nonlinear, non-convex, and experimentally beyond general-purpose LP and SMT tools.Existing dedicated tools had handled only very small networks, such as one hidden layer with 10 to 20 hidden nodes.
- Reluplex: Reluplex extends the simplex algorithm to support ReLU constraints by gradually satisfying their piecewise-linear conditions during search.The method permits temporary inconsistency between ReLU inputs and outputs before repairing the constraints.
- Reluplex: Many ReLUs can be ignored or discarded during search, reducing the search space by an order of magnitude or more, although some cases require splitting and backtracking.The problem remains NP-complete, so worst-case performance can still be poor.
- Evaluation: Reluplex successfully proved safety and robustness properties for ACAS Xu networks with 300 ReLU nodes each.The proved properties included appropriate advisories for distant or nearby collision-course intruders and robustness to small adversarial perturbations for certain inputs.
- Evaluation: The evaluation demonstrated scalability to DNNs an order of magnitude larger than those analyzable with existing techniques.The contributions include encoding DNN properties for Reluplex and implementation techniques supporting performance and scalability.
2 Background
The paper introduces DNN structure, ReLU activations, SMT, linear real arithmetic, and the simplex calculus as foundations for Reluplex. Simplex maintains tableaux, bounds, and assignments through pivoting and update operations governed by derivation rules.
- Neural Networks: A ReLU computes max(0, x) after a hidden node’s linear combination, introducing the nonlinearity used in the paper.The running example uses ReLUs on two hidden nodes and has an output always identical to its input.
- SMT and Linear Real Arithmetic: SMT determines satisfiability of theory formulas through a SAT engine coupled with a theory solver that checks the consistency of Boolean decisions.The relevant theory for DNNs is linear real arithmetic over rational constants and linear atoms.
- Linear Real Arithmetic and Simplex: The simplex method decides conjunctions of linear atoms using configurations containing basic variables, a tableau, bounds, and a variable assignment.Initial tableaux are derived from input atoms, and initial assignments satisfy tableau equations even when bounds may be violated.
- Linear Real Arithmetic and Simplex: Pivoting exchanges a basic leaving variable with a non-basic entering variable and rewrites the tableau accordingly.The entering variable must have a nonzero tableau coefficient, and substitutions preserve tableau form.
- Simplex Calculus: Update operations adjust non-basic variables, while pivot rules make an out-of-bounds basic variable adjustable through a variable with sufficient slack.Subsequent updates may move other variables outside their bounds, requiring later correction.
- Simplex Calculus: The simplex calculus uses guarded assignment rules to derive successive configurations, with soundness, completeness, and termination dependent on appropriate rule strategies.Figure 3 presents the derivation rules in guarded assignment form.
3 From Simplex to Reluplex
Reluplex extends simplex with native ReLU constraints, avoiding eager enumeration of all activation cases. Its rules repair violations, split selectively when needed, and can find feasible solutions without splitting in simple examples.
- Motivation: 2^n sub-problems can arise when n ReLUs are encoded as disjunctions, making naïve SMT encoding practical only for very small networks.Reluplex instead extends the real-arithmetic theory with a ReLU predicate.
- Encoding DNNs: Reluplex represents each ReLU node with backward- and forward-facing variables linked by a ReLU constraint.The backward-facing variable connects to the preceding layer, while the forward-facing variable connects to the following layer.
- Reluplex Procedure: Reluplex corrects out-of-bounds variables and broken ReLU semantics through Pivot and Update operations.Its configuration augments simplex with a set of ReLU connections and replaces simplex success handling with ReLU-specific rules.
- Reluplex Procedure: ReluSplit guesses whether a ReLU connection is active or inactive by setting a lower or upper bound to zero.Splitting makes derivations non-linear; the procedure is nevertheless shown to be sound and complete.
- Example: The worked example reaches a feasible solution without splitting on any ReLU connection, using updates to adjust ReLU variables.The example proceeds through bound fixes, pivots, and updates before the algorithm halts.
4 Efficiently Implementing Reluplex
Reluplex improves practical performance through tighter bounds, ReLU elimination, conflict analysis, and floating-point arithmetic. Tableau restoration increases confidence in floating-point results, but does not guarantee soundness.
- Tighter Bound Derivation: Tighter bound derivation uses tableau coefficients and current variable bounds to constrain basic variables during search.The derived bounds can subsequently support additional, tighter bounds.
- Tighter Bound Derivation: Tighter bounds can eliminate ReLUs without splitting by proving that a connection must be active or inactive.A strictly positive lower bound on either ReLU variable implies activity, while an upper bound below zero for the backward variable implies inactivity.
- Conflict Analysis: Conflict analysis can undo several irrelevant nested splits when contradictory bounds identify an earlier split as the conflict’s source.If l(x) > u(x), Reluplex can immediately backtrack or return UNSAT when no splits remain.
- Floating Point Arithmetic: Floating-point arithmetic is used because Reluplex may require millions of pivot operations involving costly rational-number arithmetic.The implementation includes practices for limiting roundoff and safeguards that measure error and restore the initial tableau when a threshold is exceeded.
- Floating Point Arithmetic: Tableau restoration increases confidence in floating-point results but does not guarantee soundness.True soundness with floating-point arithmetic remains a future goal.
5 Case Study: The ACAS Xu System
ACAS Xu replaces a memory-intensive lookup table with 45 ReLU DNNs that produce horizontal maneuver advisories. Reluplex verifies safety-relevant properties over their continuous input domains.
- ACAS Xu’s DNN representation replaces a lookup table requiring over 2GB with 45 networks requiring less than 3MB.
- Finite sampling cannot exclude erroneous advisories at other continuous inputs, motivating formal verification of the DNNs.
- The seven-dimensional system state includes relative position, aircraft headings and speeds, time to loss of vertical separation, and the previous advisory.
- Each network has five inputs, five outputs, six hidden layers, and 300 ReLU nodes.
- Reluplex verifies that the system avoids unnecessary turns, keeps alerting regions uniform, and avoids strong alerts at high τ values.
6 Evaluation
The evaluation compares Reluplex with general-purpose solvers and tests safety, consistency, and robustness properties on ACAS Xu networks. It proves many properties, finds known inconsistencies, and exposes scalability limits for global robustness.
- General-purpose SMT and LP solvers performed poorly on eight satisfiable ACAS Xu properties, while Reluplex was evaluated directly on the ReLU networks.
- Reluplex tested ten quantitative properties across ACAS Xu networks, interpreting UNSAT as proof that no violating input exists.
- Properties φ3 and φ4 establish that networks never issue a COC advisory when the intruder is directly ahead.
- A counterexample to φ8 exposed an inconsistency with the lookup table that had also appeared in simulations and was slated for correction by retraining.
- Local robustness testing found adversarial inputs for some neighborhoods and bounded another point’s optimal δ between 0.025 and 0.05.
- Global robustness was proved only for small networks because duplicating the network doubles ReLU nodes and removes the restriction to a small input domain.
7 Related Work
Related approaches verify neural networks through approximations, local convexification, discretization, or hybrid lookup-table analysis. Reluplex instead directly supports ReLU constraints within an SMT procedure.
- Prior sigmoid-network verification replaced activations with piecewise-linear approximations and handled networks with at most 20 hidden nodes.
- A ReLU adversarial-example method fixes activation states within a sufficiently small neighborhood, making the problem convex but limiting boundary cases.
- Another robustness method discretizes a local neighborhood into finitely many points and propagates consistency through the network layer by layer.
- Hybrid analysis of the lookup-table ACAS X controller identifies safe input regions, suggesting a future combination with Reluplex for end-to-end collision avoidance.
8 Conclusion and Next Steps
Reluplex extends simplex to reason about non-convex ReLU constraints while allowing temporary inconsistencies that are progressively repaired. The authors identify scalability, soundness, conflict analysis, and broader layer support as next steps.
- Reluplex extends simplex for ReLU networks, temporarily tolerating inconsistent ReLU inputs and outputs before repairing them during search.
- Some ReLU connections may require splitting for termination, but many verification problems avoid such splits and remain efficient.
- Future work targets greater scalability, stronger soundness guarantees, externally checkable proofs, and support for additional piecewise-linear layers.
I Verifying Properties in DNNs with ReLUs is NP-Complete
DNN property satisfiability is NP-complete, shown by reducing 3-SAT to ReLU networks whose linear constraints encode Boolean assignments and clause satisfaction.
- Complexity: NP-completeness follows by reducing any 3-SAT formula ψ to a ReLU DNN N and property ϕ, with satisfiability preserved in both directions.The construction first proves membership in NP and then establishes NP-hardness through the reduction.
- Reduction construction: The reduction represents each 3-SAT clause with a disjunction gadget that outputs 1 exactly when at least one of its three literals is true.Negative literals are transformed by a gadget computing 1 − xj before entering the disjunction gadget.
- Reduction construction: A conjunction gadget sums clause outputs and requires y ∈ [n, n], enforcing simultaneous satisfaction of all n clauses.The output condition holds if and only if every clause has a satisfied literal, so the network property matches ψ.
- Continuous inputs: The construction relaxes Boolean inputs by constraining each xi to [0, 1] while forcing feasible values near either 0 or 1 using auxiliary ReLU gadgets.The auxiliary gadget ensures xi ∈ [0, ϵ] or xi ∈ [1 − ϵ, 1].
- Continuous inputs: With relaxed inputs, clause outputs remain near 0 when all literals are false and near 1 when at least one literal is true.Requiring y ∈ [n(1 − ϵ), n] therefore preserves equivalence between network satisfiability and satisfiability of ψ.
II The Reluplex Calculus is Sound and Complete
The Reluplex calculus preserves satisfiability while refining simplex configurations, and its rules support sound and complete derivations ending in either a witness or a refutation.
- Invariant preservation: Each derivation maintains tableau equivalence and an assignment satisfying the current tableau equations.Pivot rules preserve equivalent equations, while update rules adjust assignments without violating the tableau.
- Soundness: Reluplex splitting creates active and inactive branches, and at least one branch preserves a satisfying assignment whenever the original state is satisfiable.The branch choice follows the sign of the satisfying assignment for the split variable.
- Invariant preservation: Reluplex derivations preserve the initial ReLU relation set and tighten bounds without weakening lower or upper constraints.The relation set remains R0, while lower bounds can only increase and upper bounds can only decrease.
- Soundness: The calculus is sound: a SAT leaf yields an assignment satisfying every original constraint, while a satisfiable formula cannot have a refutation.The argument uses the preserved ReLU relations and the invariant that a satisfying assignment remains represented in the derivation tree.
- Completeness: The calculus is complete because eager ReLU splitting followed by a terminating simplex strategy produces either a witness or a refutation for every formula.After all applicable splits, satisfying variable bounds also satisfy the ReLU constraints, allowing ReluSuccess to replace simplex Success.
Property φ3.
Property φ3 requires ACAS Xu to avoid choosing COC as minimal in two directly-ahead intruder scenarios: approaching, or moving away more slowly than the ownship.
- Property φ3.: For an intruder directly ahead and moving toward the ownship, the COC score must not be minimal.The property is tested on all networks except N1,7, N1,8, and N1,9 under the stated range constraints.
- Property φ3.: For an intruder directly ahead and moving away more slowly than the ownship, the COC score must not be minimal.This case is tested on all networks except N1,7, N1,8, and N1,9.
Property φ7.
Property φ7 requires that, when vertical separation is large, neither strong turn command is assigned the minimal score.
- Property φ7.: Under large vertical separation, the network must never assign the minimal score to either “strong right” or “strong left.”The property is tested on network N1,9 across the stated ranges for ρ, θ, ψ, vown, and vint.
Property φ8.
Property φ8 specifies desired advisory outputs under three constrained ACAS Xu scenarios involving intruder distance, separation, and prior advisories.
- For a large vertical separation after a previous “weak left” advisory, the network outputs COC or continues advising “weak left” on N2,9.The input ranges constrain ρ, θ, ψ, vown, and vint; the desired property makes either “weak left” or COC minimal.
- With a previous “weak right” advisory and a nearby intruder, the network outputs a “strong left” advisory on N3,3.The desired property requires the score for “strong left” to be minimal within the specified input constraints.
- For a far-away intruder, the network advises COC on N4,5.The desired property requires the score for COC to be minimal over the stated ranges of ρ, θ, ψ, vown, and vint.