PaperlayerView exact revision on arXiv

Source-linked AI summary

Branch and Bound for Piecewise Linear Neural Network Verification

Rudy Bunel, Jingyue Lu, Ilker Turkaslan, Philip H. S. Torr, Pushmeet Kohli, M. Pawan Kumar

arXiv:1909.06588v5cs.LGcs.LOstat.ML

TL;DR

Formal verification must scale beyond existing methods for safety-critical neural-network applications. The paper formulates verification as MIP and develops a Branch-and-Bound family that unifies prior methods, adds ReLU branching, and evaluates them with comprehensive benchmarks. The resulting methods improve performance, including support for high-dimensional convolutional problems, while the authors note that heuristic branching and tighter bounds remain challenging.

  • Problem

    Formal verification is important for safety-critical neural-network deployment, but existing approaches remain difficult to scale to realistic networks.

  • Method

    The paper uses a Mixed Integer Linear Programming formulation to build a Branch-and-Bound framework encompassing previous verification methods and developing new branching and bounding methods.

  • Results

    The new methods achieve considerable performance improvements, including speed-ups of almost two orders of magnitude in some cases, and ReLU branching handles high-dimensional convolutional problems.

  • Takeaways & Limitations

    Comprehensive datasets and benchmarks support systematic comparison of verification methods and analysis of factors affecting verification difficulty.

  • Takeaways & Limitations

    The authors identify expensive tighter bounds and heuristic branching that may fail when verification problems change as remaining challenges.

Abstract

from arXiv · show

The success of Deep Learning and its potential use in many safety-critical applications has motivated research on formal verification of Neural Network (NN) models. In this context, verification involves proving or disproving that an NN model satisfies certain input-output properties. Despite the reputation of learned NN models as black boxes, and the theoretical hardness of proving useful properties about them, researchers have been successful in verifying some classes of models by exploiting their piecewise linear structure and taking insights from formal methods such as Satisifiability Modulo Theory. However, these methods are still far from scaling to realistic neural networks. To facilitate progress on this crucial area, we exploit the Mixed Integer Linear Programming (MIP) formulation of verification to propose a family of algorithms based on Branch-and-Bound (BaB). We show that our family contains previous verification methods as special cases. With the help of the BaB framework, we make three key contributions. Firstly, we identify new methods that combine the strengths of multiple existing approaches, accomplishing significant performance improvements over previous state of the art. Secondly, we introduce an effective branching strategy on ReLU non-linearities. This branching strategy allows us to efficiently and successfully deal with high input dimensional problems with convolutional network architecture, on which previous methods fail frequently. Finally, we propose comprehensive test data sets and benchmarks which includes a collection of previously released testcases. We use the data sets to conduct a thorough experimental comparison of existing and new algorithms and to provide an inclusive analysis of the factors impacting the hardness of verification problems.

1. Introduction

The paper targets the limited scalability of formal neural-network verification for safety-critical deployment. It introduces a Branch-and-Bound framework that unifies existing methods, improves performance, supports ReLU branching for difficult convolutional problems, and provides broader benchmarks.

  • Motivation: Formal verification is needed for safety-critical neural-network deployment because testing cannot establish the absence of bugs.Current model evaluation mostly relies on held-out data, while formal verification aims to verify safety-critical behaviors.
  • Motivation: Existing formal methods exploit ReLU networks' piecewise-linear structure but remain difficult to scale to large real-world networks.Earlier methods progressed beyond simple one-hidden-layer networks, yet non-trivial approaches are still not scalable to realistic models.
  • Contributions: The paper formulates neural-network verification as a Branch-and-Bound framework based on Mixed Integer Linear Programming, containing state-of-the-art methods as special cases.The framework provides a common representation for comparing and extending verification methods.
  • Contributions: The authors combine strengths of existing methods and report performance improvements, including speed-ups of almost two orders of magnitude in some cases.They analyze bounds, branching choices, and branching guidance strategies when designing the new methods.
  • Contributions: A new computationally cheap ReLU branching strategy uses network architecture to handle high-dimensional convolutional verification problems.It addresses limitations of input-domain branching and demonstrates benefits against methods using input-domain or ReLU branching.
  • Contributions: The paper introduces comprehensive benchmarks spanning trained and synthetic fully connected or convolutional networks, enabling broader comparisons and analyses of verification difficulty.The datasets vary ϵ on the same network and include TwinStream to study bounding and branching strategies.
  • Contributions: This article extends a preliminary NeurIPS 2018 version with clearer framework exposition, convolutional branching strategies, new datasets, and additional baselines.The stated extensions include a running toy example and synthetic models.

2. Problem Specification

The paper specifies verification as proving a property over a bounded input domain for a neural-network function. It focuses on piecewise-linear networks and Boolean properties formed from linear output inequalities, while restricting attention to complete methods.

  • Verification problem: Given a network function, bounded input domain, and property, verification asks whether the property holds for every input in that domain.The formulation represents the network as ˆx_n = f(x_0) and evaluates the property on its outputs.
  • Verification problem: Adversarial robustness can be represented by an L∞ input neighborhood around a training sample together with output inequalities favoring the original label.The domain constrains the perturbation distance by ϵ, while the property compares output labels.
  • Scope: The paper focuses on piecewise-linear neural networks, whose input domain decomposes into polyhedra where the network function is linear.This includes fully connected and convolutional linear transformations but excludes sigmoid- and tanh-based activations.
  • Properties: The considered properties are Boolean formulas over linear inequalities on network outputs.Robustness properties are described as conjunctions requiring the original label's output to exceed competing labels.
  • Scope: The study focuses on complete verification algorithms, which must report all correct properties.Unsound and incomplete methods, along with several additional-assumption settings, are outside the paper's scope.

3. Verification Formalism

The paper converts neural-network verification into satisfiability and optimization formulations, then into MIP using binary ReLU variables. These formulations support a unified treatment of existing verification methods and motivate specialized Branch-and-Bound solvers.

  • 3.1 Verification as a Satisfiability Problem: Verification methods search for counterexamples by constraining variables for network inputs, hidden units, outputs, and their relationships.A satisfying assignment corresponds to an input-output configuration that violates the target property.
  • 3.1 Verification as a Satisfiability Problem: The verification satisfiability problem is transformed into global optimization by adding output layers so the property holds when the scalar minimum is positive.Boolean formulas over linear inequalities can be encoded through additional linear and maxpooling layers.
  • 3.1 Verification as a Satisfiability Problem: The canonical ReLU formulation assigns input, linear-layer, and activation constraints; an assignment is a counterexample, while unsatisfiability proves the property.The formulation explicitly distinguishes proving the absence of counterexamples from merely failing to find one.
  • 3.1 Verification as a Satisfiability Problem: The formulation is not limited to ReLU-only networks because MaxPooling operations can be converted into linear layers and ReLU activations.The paper notes that canonical conversion does not itself simplify resolution.
  • 3.1 Verification as a Satisfiability Problem: The running toy example verifies y > -5 for a one-hidden-layer network over C = [−2; 2] × [−2; 2].Figure 1 illustrates the same property and network used to explain the formulations.
  • 3.2 Mixed Integer Linear Programming Formulation: Big-M encoding replaces ReLU nonlinearities with binary variables using lower and upper bounds on hidden-unit preactivations.The binary variable records whether a ReLU is blocked or passing, while integer constraints preserve the remaining difficulty.
  • 3.2 Mixed Integer Linear Programming Formulation: Interval arithmetic propagates input bounds layer by layer to obtain intermediate bounds needed by the MIP encoding.The resulting generic non-convex problem becomes a MIP, but optimization remains NP-hard and depends on solver and encoding quality.

4. Branch and Bound for Verification

The paper casts neural-network verification as global optimization and organizes existing methods within a Branch-and-Bound framework. BaB repeatedly partitions problems, computes bounds, and prunes subproblems that cannot contain counterexamples.

  • Canonical formulation: Verification is reformulated as global optimization, with the sign of the minimum determining whether the original property holds.A positive global minimum certifies the inequality property after adding a final network layer.
  • Generic framework: BaB repeatedly splits the input domain or an unfixed ReLU into subproblems, then computes lower and upper bounds for each.The best upper bound is retained as a candidate global minimum while lower bounds guide pruning.
  • Generic framework: Subproblems whose lower bound exceeds the current global upper bound are pruned because they cannot contain the global minimum.For satisfiability, lower bounds above zero similarly exclude counterexamples.
  • Framework components: The framework separates branching, bounding, and search strategies, each of which affects subproblem hardness, bound quality, or early pruning.Branching determines the partition, bounding estimates extrema through relaxations, and search chooses the next subproblem.
  • Existing methods: Reluplex and Planet fit the BaB perspective as ReLU-splitting methods with convex relaxations, while their search and prioritization strategies differ.Reluplex prioritizes violated constraints and uses SMT-driven splitting; Planet lacks a heuristic for choosing split variables.

5. Improved BaB for NN Verification

The paper improves BaB verification through tighter, selectively computed bounds and new input- and ReLU-branching heuristics. These methods target different problem scales, while ReLU branching addresses the limited reach of input-only splitting in large networks.

  • Framework-guided improvements: The framework exposes optimization, verification, and machine-learning techniques that can be combined to improve neural-network verification.The authors use the unified framework to identify techniques for speeding verification algorithms.
  • Better Bounding: Tighter intermediate bounds produce tighter convex relaxation hulls, but updating all bounds can be computationally expensive.Experiments therefore examine updating all layers versus only selected layers.
  • Branching on Input Domains: BaB splits the longest input-domain dimension, while BaBSB selects the dimension whose split most improves estimated lower bounds.BaBSB evaluates candidate dimensions using an efficient lower-bound approximation.
  • Branching on ReLU Activation Nodes: Input-domain splitting is effective for low-dimensional, small-scale problems but becomes inadequate for large networks because its cost grows with input dimensions and ignores ReLU branching points.This motivates computationally cheap heuristics for branching on ReLU nonlinearities in convolutional networks.
  • Branching on ReLU Activation Nodes: BaBSR prioritizes unfixed ReLU nodes using scores that estimate their potential lower-bound improvement, selecting the node with the largest score.The score is designed to avoid the cost of recomputing full bounds for every candidate split.
  • Branching on ReLU Activation Nodes: The ReLU heuristic is less reliable when a convolutional layer is sparse or when all ReLU scores are close to zero.The authors recommend other selection strategies, such as random choices favoring non-sparse layers, in those cases.

6. Experimental Setup

The experiments compare verification methods under controlled solver, approximation, branching, and benchmark settings. The setup includes diverse neural-network properties and datasets designed to probe accuracy, scalability, and factors affecting verification difficulty.

  • Evaluation protocol: A two-hour timeout is used for each experiment unless otherwise stated.
  • Compared methods: BlackBox directly encodes the verification problem into Gurobi without exploiting the network’s structure.
  • Compared methods: Reluplex and Planet use publicly available implementations with GLPK for linear programming, whereas the other methods use Gurobi LP solving.This solver difference should be considered when interpreting results.
  • Compared methods: Figure 3 evaluates lower-bound quality as input-domain area shrinks, comparing rebuilt linear approximations with fixed constraints and updated input bounds.Rebuilding becomes especially advantageous for deeper networks.
  • Compared methods: The Branch-and-Bound implementations combine approximation strategies with input-domain or ReLU branching heuristics.ReLU methods include naive first-or-random choices and advanced prioritization criteria.
  • Data sets: The benchmark covers six property datasets, including CollisionDetection, ACAS, Robust MNIST, PCAMNIST, and TwinStream, with fully connected and convolutional networks.The datasets span adversarial-robustness properties, collision avoidance, controlled architecture parameters, and correlated hidden nodes.

7. Analysis

Experiments show that solver performance depends on network size, input dimension, property difficulty, margins, and branching or bounding choices. BaBSB performs strongly on small networks, while BaBSR and ERAN are more effective on high-dimensional Robust MNIST networks; generalization remains limited for some evaluations.

  • Small Networks: BaBSB achieves 98.40% success on ACAS within one hour, compared with Reluplex’s 79.26% at two hours.The runtime needed to match Reluplex’s success rate is two orders of magnitude smaller.
  • Small Networks: Smart branching and better lower bounds substantially reduce the number of subdomains explored.The analysis attributes much of the performance gap between BaBSB and BaB to smart branching.
  • Large Networks: On high-dimensional Robust MNIST networks, BaBSB becomes ineffective, while BaBSR and ERAN are the only methods outperforming or matching MIPplanet on the screened properties.ReluBaB, Reluplex, and Neurify time out on every property under the 100-second limit; BaBSR and ERAN are evaluated across all properties.
  • Large Networks: BaBSR performs best overall on the reduced Robust MNIST Network and Robust MNIST Network, but MIPplanet slightly wins on the most challenging reduced-network properties.BaBSR’s advantage is largest on easy properties and narrows as difficulty increases.
  • Varying Parameters: Larger input dimensions, wider networks, and smaller satisfiability margins make verification harder across methods.The PCAMNIST results also show similar difficulty trends for almost all solvers, although the data set contains only 27 networks.
  • TwinStream: On TwinStream, MIPplanet solves all properties most effectively, whereas ReLU splitting is preferred for highly correlated layers and may suit larger networks through BaBSRL.The data set contains only UNSAT properties, and BaBSRL is presented as an expected option rather than an experimentally established winner there.

8. Conclusion

The conclusion presents the unified Branch-and-Bound framework as a way to diagnose weaknesses in existing verification methods and develop improved variants. It reports performance gains while emphasizing unresolved costs in bounding, branching heuristics, and LP solving, and provides data sets for future comparisons.

  • Contributions: The unified Branch-and-Bound framework exposes weaknesses in existing methods and supports new methods with considerable performance enhancements.The conclusion frames these improvements across the paper’s comprehensive data sets.
  • Limitations and Future Work: Tighter intermediate bounds can accelerate convergence but are expensive, while heuristic branching may fail when problem characteristics change.The conclusion identifies GPU-based bound computation and learned heuristics as possible directions, with offline-cost trade-offs.
  • Limitations and Future Work: LP solving remains the main bottleneck for BaB-based methods because it is used largely to decide whether branching should occur.The authors suggest learning to imitate LP decisions as a possible way to reduce total runtime.
  • Future Work: The released data sets are intended to support comprehensive evaluation and comparison of future verification methods.They are positioned as a resource for addressing the remaining methodological issues.

Appendix A. Planet Approximation

The Planet relaxation approximates ReLU constraints by removing integrality and deriving a tight upper bound through linear constraints.

  • Planet Approximation: The formulation assumes negative lower bounds and positive upper bounds for the relevant variables.Bounds can be updated when this sign condition does not hold.
  • Planet Approximation: Level-0 Sherali–Adams relaxation removes integrality constraints without adding further constraints.Its feasible domain is therefore the continuous relaxation of the mixed-integer formulation.
  • Planet Approximation: The ReLU upper-bound function is concave because it is the minimum of increasing and decreasing linear functions.Its maximum occurs where those two functions are equal.
  • Planet Approximation: The derived upper bound matches the upper bound used by Planet.The equivalence follows by substituting the optimal intermediate value into the relaxation.

Appendix B. MaxPooling

MaxPooling constraints can be encoded directly with binary variables or transformed into linear functions and ReLUs, extending the verification framework to networks containing pooling units.

  • MaxPooling: MaxPooling selects the largest among its input values, and binary variables encode which input attains that maximum.The encoding uses upper and lower bounds in the associated constraints.
  • MaxPooling: A MaxPooling unit can be decomposed into pairwise maxima, which are then represented as sums of ReLU units.This requires a pre-computed lower bound for the ReLU input.
  • MaxPooling: The MIP formulations encode ReLU activations with binary variables, nonnegativity constraints, and upper bounds tied to activation indicators.One formulation uses the activation-specific upper bound u_i, while another uses M_i = max(−l_i, u_i).
  • MaxPooling: The alternative M_i formulation is fundamentally the same encoding but uses slightly looser bounds.Its bound is not as tight on one side as the activation-specific bounds.
  • MaxPooling: The MIP encodings depend on obtaining lower and upper bounds for network activations.These bounds are therefore a prerequisite for encoding the activation constraints.

C.2.1 Interval Analysis

Activation bounds can be computed by interval analysis or by optimizing over the Planet relaxation; the latter is more expensive but produces tighter bounds for subsequent MIP encoding.

  • Interval Analysis: Interval arithmetic propagates lower and upper bounds through affine layers and applies ReLU directly to the bounds.The affine propagation uses positive and negative parts of the weights.
  • Interval Analysis: Planet-based bound computation incrementally builds a layer-wise relaxation and optimizes each activation subject to its constraints.The resulting bounds are used to construct the relaxation for later layers and the final MIP encoding.
  • Interval Analysis: The relaxation optimum is a valid activation bound because the optimization is convex and the relaxed feasible domain contains the original feasible domain.Convexity ensures the optimum is attained for the relaxation problem.
  • Interval Analysis: Planet bounds are more expensive to obtain than interval-analysis bounds but are tighter.The tighter bounds can improve the subsequent encoding of the verification problem.
  • Interval Analysis: Verification can be formulated as satisfiability by asking whether a counterexample exists, or as optimization by minimizing the network output.The optimization formulation explicitly searches for the smallest output.

C.3 Comparison

The comparison evaluates MIP encoding, bound-quality, and optimization variants, showing that optimization avoids spurious counterexamples and tighter bounds improve performance on deeper networks.

  • C.3 Comparison: Planet-opt and BlackBox are the only methods that solve CollisionDetection with 100% accuracy.The other methods return spurious counterexamples rather than failing because of timeouts.
  • C.3 Comparison: Big-M constants can make satisfiability-only formulations terminate on zero-valued solutions that are not valid counterexamples.Optimization formulations avoid this issue by searching for negative outputs and can interrupt once one is found.
  • C.3 Comparison: Interval has the worst bounds and is much slower than the other methods on the deeper ACAS network.The comparison therefore exposes the effect of bound quality as network complexity increases.
  • C.3 Comparison: Planet-symfeasible performs worse than Planet-feasible and Planet-opt because its bounds are slightly worse.The variants differ in encoding or solving strategy while otherwise sharing the Planet-feasible setup.
  • C.3 Comparison: BaBSR performs best on easy properties but worse than MIPplanet on difficult properties.This pattern is also observed for properties of the reduced Robust network.

Appendix D. PCAMNIST Details

Appendix D describes PCAMNIST and TwinStream constructions used to study verification difficulty. It also defines tunable properties and reports network accuracies and aggregate performance plots.

  • PCAMNIST: PCAMNIST varies input features, network depth, and hidden-layer width to study factors influencing verification performance.Inputs are the first k PCA eigenvectors of MNIST digits.
  • Verification properties: Its properties ask whether some input makes the odd-class score exceed the even-class score by a chosen confidence margin.Changing the confidence can make the property true or false and adjust its difficulty.
  • Aggregate evaluation: Figure 12 presents cactus plots for PCAMNIST as a generic data set, complementing the separate analyses of individual factors.The appendix frames these plots as an aggregate view of the data set.
  • TwinStream networks: TwinStream networks duplicate the same architecture, weights, and inputs across two streams, then subtract their outputs and add a positive bias margin.The resulting output is always equal to the final bias value.
  • Network accuracy: Table 4 reports the accuracies of networks trained for the PCAMNIST data set.The supplied passage identifies the table but does not include its numerical values.

Appendix F. Additional Performance Details

Appendix F compares verification methods separately on SAT and UNSAT properties because their verification behavior differs. The figures show dataset-dependent differences in solving success and time efficiency.

  • Decision types: SAT and UNSAT properties are analyzed separately because verification behaves differently for the two decision types.The comparison reports results on subsets sorted by decision type.
  • CollisionDetection: On CollisionDetection, BlackBox’s errors occur on SAT properties because it returns incorrect counterexamples.The figure describes proportions of properties verifiable under varying time budgets.
  • ACAS: On ACAS, planet solves none of the SAT properties, whereas the proposed methods solve them efficiently but leave some unresolved.The comparison is based on proportions verified under varying time budgets.
  • Reduced Robust networks: On the reduced Robust network set, MIPplanet slightly outperforms BaBSR on challenging UNSAT problems, while BaBSR is much faster on simple problems.The figure reports similar performance on SAT and UNSAT properties overall.
  • Robust networks: On the full Robust Network set, BaBSR significantly outperforms MIPplanet on both SAT and UNSAT properties.The large SAT gap is presented as evidence that Branch-and-Bound effectively finds counterexamples on large networks.
Loading 1909.06588v5…