SMT-Based Neural Network Verification
Description
SMT-based neural network verification decides exactly whether any input in a defined region can make a trained neural network violate a stated property, and if one can, returns that input as a counterexample. SMT (satisfiability modulo theories) solvers decide whether a set of logical and arithmetic constraints can all hold at once: here the network's weighted sums become linear equations, each piecewise-linear activation such as ReLU becomes a constraint with two cases (inactive at zero, or active and passing its input through), and the input region and the negation of the property become further linear constraints. The solver searches for values that satisfy every constraint with a simplex-based linear-programming engine: it first tries to repair an activation whose current values break it, and splits it into its two cases only when repairs keep failing, while bounds on each neuron (in Marabou, by default, the linear bounds that bound propagation computes) rule cases out early. Reluplex (Katz et al., 2017) introduced this lazy treatment of ReLU inside the simplex method and used it on a prototype airborne collision avoidance network; Marabou, its maintained successor, keeps the same search structure with a newer search procedure, adds parallel solving, and can emit a proof certificate for an 'unsatisfiable' answer. The answer is 'unsat', meaning no input in the region violates the property, or 'sat' with a concrete counterexample, and for networks whose activations are all piecewise-linear the procedure is complete; the price is that the number of cases can grow exponentially with the number of neurons, so it is practical for small networks such as controllers, policies and surrogate models with few inputs rather than large image models.
Example Use Cases
Safety
A warehouse robotics team trains hundreds of candidate deep reinforcement learning policies for driving between shelves from range-sensor readings. Before field trials it encodes 'no move into an obstacle in the next step' and 'no repeating left-right loop over several steps' as queries over each small policy network, runs Marabou on every candidate, discards each policy for which a counterexample reading is returned, and takes only the survivors to the physical robot.
An aircraft systems developer replaces a large collision-avoidance lookup table with a set of small neural networks. For each network it writes regions of encounter geometry, such as an intruder close ahead and closing, together with the advisory that must never be issued there, and runs the solver on each. Regions returned as unsatisfiable go into the certification evidence; any counterexample encounter is replayed in simulation and drives retraining.
A medical-device manufacturer uses a small network to recommend infusion rates from a handful of patient measurements. Its safety engineers prove that, for every combination of measurements within the clinically plausible ranges, the recommended rate never exceeds the maximum set by the device's hazard analysis, and use any counterexample returned to retrain the network or add an output limit.
Limitations
- Deciding these queries for ReLU networks is NP-complete, and the search may split on every neuron whose case is undecided, so time can grow exponentially with network size and with the number of steps a property spans. In a study of robot navigation policies kept to 16 neurons per hidden layer, single-step collision queries took seconds, but 12-step cycle queries usually ran for hours and nearly three in ten of them hit the 12-hour limit.
- The solver runs on ordinary processors, and its own tool paper reports a non-trivial performance gap to GPU-based bound-propagation verifiers, especially on larger networks; in the 2023 verification competition it solved 594 benchmark instances to alpha-beta-CROWN's 721. It is therefore best suited to small networks with few inputs, such as controllers, policies and surrogate models.
- Exact answers hold only for piecewise-linear activations such as ReLU, max, absolute value and leaky ReLU. Sigmoid and tanh are handled by an over-approximation that is refined step by step, and softmax and bilinear layers only through a convex relaxation, so for networks that use them the procedure is no longer complete and can end without a decisive answer.
- The query covers the network and a region of its inputs written as linear constraints, nothing more. A counterexample may lie in a part of the region no real sensor could produce, and a proof says nothing about the environment the network acts in, so choosing a region that is realistic yet small enough to solve takes domain knowledge, and a closed-loop safety claim needs further analysis.
- An 'unsat' answer is only as trustworthy as the solver's implementation. Marabou can emit a proof certificate that an independent checker validates, but proof production works with only some of its features and not in parallel mode, and in the tool paper's collision-avoidance experiments certificates were produced for 113 of 180 benchmarks.