PaperlayerView exact revision on arXiv

Source-linked AI summary

Neural Network Branching for Neural Network Verification

Jingyue Lu, M. Pawan Kumar

arXiv:1912.01329v1cs.LGstat.ML

TL;DR

Neural-network verification needs efficient branching because BaB search can become costly over large domains. This paper learns a graph neural network that imitates strong branching by representing the verified network directly and updating embeddings with forward-backward passes. Across tested properties, the method reduces average branches and time by more than 50%, while transferring across difficulty levels and network sizes.

  • Problem

    BaB-based neural-network verification needs a computationally cheap, high-quality branching strategy because branching choices strongly affect search size and verification time.

    Source: §1 · p. 1

  • Method

    The paper trains a GNN to imitate strong branching while using the verified neural network as its graph input and a customized forward-backward embedding schedule.

    Source: §1 · p. 2, §4 · pp. 5–6

  • Results

    More than 50% fewer branches and at least 50% less average verification time are achieved across three property sets, with transfer to larger networks.

    Source: §6.3 · p. 9, §6.4 · p. 10

  • Takeaways & Limitations

    The learned branching strategy provides an effective BaB component with horizontal transfer across property difficulty and vertical transfer across network size.

    Source: §6.3 · p. 9, §6.4 · p. 10

    The paper focuses on ReLU-based networks and assumes matching data distribution, features, and bounding methods when transferring across networks.

    Source: §1 · p. 2, §4 · p. 6

Abstract

from arXiv · show

Formal verification of neural networks is essential for their deployment in safety-critical areas. Many available formal verification methods have been shown to be instances of a unified Branch and Bound (BaB) formulation. We propose a novel framework for designing an effective branching strategy for BaB. Specifically, we learn a graph neural network (GNN) to imitate the strong branching heuristic behaviour. Our framework differs from previous methods for learning to branch in two main aspects. Firstly, our framework directly treats the neural network we want to verify as a graph input for the GNN. Secondly, we develop an intuitive forward and backward embedding update schedule. Empirically, our framework achieves roughly $50\%$ reduction in both the number of branches and the time required for verification on various convolutional networks when compared to the best available hand-designed branching strategy. In addition, we show that our GNN model enjoys both horizontal and vertical transferability. Horizontally, the model trained on easy properties performs well on properties of increased difficulty levels. Vertically, the model trained on small neural networks achieves similar performance on large neural networks.

1 INTRODUCTION

Formal verification is needed because neural networks can behave incorrectly under small perturbations, while BaB verification performance depends critically on branching quality. The paper proposes a GNN-based branching strategy that imitates strong branching while supporting transfer across properties and network sizes.

Motivation

  • Formal verification is necessary for safety-critical robustness claims because hold-out evaluation cannot establish correctness over all allowed input perturbations.The motivating example is consistent self-driving decisions for every input within a permitted norm ball.Source: §1 · p. 1
  • BaB branching determines how the search space is split, so branching quality directly affects the number of steps and verification time.The effect is especially important for large networks with many possible input or activation split choices.Source: §1 · p. 1
  • Random branching is inefficient, while hand-designed heuristics trade effectiveness against computational cost; strong branching is effective but prohibitively expensive.The paper motivates a cheap strategy that preserves strong-branching quality without exhaustive evaluation of every option.Source: §1 · p. 2

Contributions

  • The proposed framework uses a GNN whose embeddings mimic neural-network forward and backward passes, with shared parameters enabling application across verification properties and network structures.The method is designed to be computationally cheap and memory efficient.Source: §1 · p. 2
  • Supervised training uses broadly representative data from different BaB stages, while online learning fine-tunes decisions for the verification instance during the BaB process.The paper also supplies a convolutional-network verification dataset covering different difficulty levels and network sizes.Source: §1 · p. 2
  • The learned GNN transfers horizontally from easy to harder properties and vertically from small to large networks, although the paper focuses experiments on ReLU networks.The authors state that the framework is applicable to any neural-network architecture, but the reported focus is ReLU-based networks.Source: §1 · p. 2

2 RELATED WORKS

Prior learned branching methods imitate strong branching but typically rely on hand-designed features or generic learning structures. The paper instead exploits the verified neural network’s architecture directly through a customized GNN update schedule.

Learned branching

  • Learning-based branching has been applied to combinatorial optimization and MILP, where repeated instances with shared structure make learned decisions possible.Several MILP methods learn rankings or scores intended to imitate strong branching.Source: §2 · pp. 2–3

Limitations of prior work

  • Earlier learned branching methods rely heavily on hand-designed features or priors and use generic learning structures that do not exploit neural-network architecture.This limitation motivates a representation specialized to neural-network verification.Source: §2 · p. 3

Comparison with concurrent work

  • Gasse et al. (2019) use a GNN for MILP’s bipartite structure, but treating all constraints identically and updating them simultaneously limits expressiveness for neural-network verification.The paper contrasts this with its architecture-aware update schedule designed for neural networks.Source: §2 · p. 3
  • The proposed framework exploits neural-network structure and customized embedding updates to scale in computation and memory, while comparisons focus mainly on BaB-based methods.Some recent verification methods are not explicitly formulated as BaB and therefore are not the primary comparison target.Source: §2 · p. 3

3 BACKGROUND

The paper formulates verification as proving a property over a bounded domain and explains BaB’s branching and bounding components. It motivates architecture-aware branching by contrasting relaxation tightness, computational cost, and available split heuristics.

3 BACKGROUND

  • Formal verification asks whether a modified network output remains nonnegative for every input in a bounded domain; a violation is established by finding a negative output.Boolean properties over linear output forms can be transformed into this sign-checking formulation.Source: §3 · p. 3

3.1 BRANCH AND BOUND

  • BaB recursively partitions the input domain, computes relaxed lower bounds for subdomains, and terminates when the global lower bound exceeds zero or a counterexample is found.The underlying minimum problem is generally NP hard.Source: §3.1 · p. 3

3.2 BOUNDING

  • Convex relaxations turn ReLU verification into linear programs, with tighter relaxations producing tighter but more expensive bounds.Intermediate bounds are often estimated roughly, whereas tighter final output lower bounds can avoid unnecessary splits.Source: §3.2 · pp. 3–4
  • Among the illustrated relaxations, naive is loosest, linear bounds is tighter, and Planet is tightest; the first two have closed forms while Planet requires iteration.This illustrates the computational trade-off between relaxation tightness and bound-computation cost.Source: Figure 1 · p. 4, §3.2 · p. 4

3.3 BRANCHING

  • Branching chooses either an input-domain split or an ambiguous ReLU activation split, and the choice directly affects whether large networks can be verified within a time limit.For large-scale networks, ReLU splitting is reported as more effective than domain splitting.Source: §3.3 · p. 4
  • The proposed alternative uses a GNN to imitate strong branching, aiming to retain its effectiveness while making branching decisions efficiently with GPU computation.Existing alternatives include random selection and hand-designed gradient- or relaxation-based scores.Source: §3.3 · p. 4

4 GNN FRAMEWORK

The framework represents the neural network being verified as a graph, updates node embeddings through layer-ordered forward and backward passes, and scores candidate branching nodes. Its design tracks local relaxation effects and remains memory efficient under stated assumptions.

Overview

  • The verified neural network is the GNN graph; node embeddings are updated from node features and neighboring information, then scored to select a branching node.Potential decisions are selected from input nodes and ambiguous activation nodes.Source: §4 · pp. 5, 7

Nodes

  • Graph nodes represent inputs, hidden activations, and the output, with pre- and post-activation variables combined for each activation node.The graph includes unambiguous activation and output nodes even though they are not all branching candidates.Source: §4 · p. 5

Features and edges

  • Node features include domain or intermediate bounds and optimization-related values, while edges encode the verified network’s weight-matrix connections.The framework uses simple features rather than extensive feature engineering.Source: §4 · p. 5

Embedding updates

  • All node embeddings start at zero, and only nodes in the same network layer are updated simultaneously in a layer-by-layer forward-backward schedule.This differs from standard simultaneous GNN updates over the whole graph.Source: §4 · pp. 5–6
  • Forward updates capture local relaxation information, while backward updates capture how splitting a node affects later-layer relaxations; repeated rounds address smaller effects elsewhere.The schedule follows the layerwise computation of intermediate bounds and relaxation changes.Source: §4 · p. 6

Generalization and efficiency

  • The update scheme is memory efficient because it processes one layer at a time, but applying a trained model assumes matching information about data distribution, features, and bounding methods.The authors state that the scheme should generalize across differing network architectures under these assumptions.Source: §4 · pp. 6–7

5 PARAMETER ESTIMATION

The framework estimates GNN parameters by ranking branching decisions according to relative improvement, while online learning adapts the model to individual properties and a fail-safe heuristic limits poor decisions.

5 PARAMETER ESTIMATION

  • The relative improvement measure compares a split's average subproblem lower-bound gain with the maximum possible gain, providing the ranking signal.Source: §5 · p. 7
  • Branching nodes are grouped into improvement-based classes, and a pairwise hinge-rank loss trains the GNN to score higher-quality decisions above lower-quality ones.The loss avoids exhaustive ranking when many decisions have similar performance.Source: §5 · p. 7
  • A fail-safe strategy invokes a cheap heuristic when the GNN's lower-bound improvement falls below a preset threshold, helping it recover on subsequent subdomains.The motivation is that poor decisions can propagate through similar child subdomains and increase the total number of splits.Source: §5 · pp. 7–8
  • Online learning fine-tunes the trained GNN when heuristic decisions outperform its choice, using a loss amplified when the heuristic improvement exceeds a threshold.The update uses one gradient step with a small learning rate.Source: §5 · p. 8
  • Online learning is property specific and produces a small but significant performance improvement by adapting the GNN to the property being solved.Source: §5 · p. 8

6 EXPERIMENTS

The experiments compare GNN branching with MIPplanet and BaBSR on CIFAR-10 convolutional networks, testing difficulty transfer and transfer to wider and deeper models. GNN reduces branching and solving time substantially, while online learning provides additional gains and the learned model transfers vertically.

6.1 SETUP

  • The study evaluates robustly trained CIFAR-10 convolutional networks against MIPplanet and BaBSR using average time, branch counts, and timeout ratios.BaBSR and MIPplanet were selected based on their prior performance on MNIST verification.Source: §6.1 · pp. 8–9, §6.3 · p. 9

6.2 TRAINING DATASET

  • Training data combine complete strong-branching runs on 25% of non-timeout properties with at least 20 sampled training points for each remaining property across different BaB stages.Samples are generated after randomly many cheap-heuristic steps, with the maximum set to q = 10.Source: §6.2 · p. 9

6.3 BASE MODEL

  • The base-model evaluation contains 467 easy, 773 medium, and 426 hard properties generated using BaBSR and categorized by solving time.Source: §6.3 · p. 9
  • More than 50% fewer branches and at least 50% lower average solving time are achieved across easy, medium, and hard properties; online learning improves 61.52% of properties in branches and 60.20% in time over standard GNN.These comparisons evaluate branching strategies under the same verification framework.Source: §6.3 · p. 9, Table 1 · p. 10
  • GNN provides consistent high-quality performance across base-model properties, while BaBSR generally beats MIPplanet even though MIPplanet wins on a subset.Source: §6.3 · p. 10, Table 1 · p. 10

6.4 TRANSFERABILITY: LARGER MODELS

  • A model trained on the Base network retains similar results on Wide and Deep networks, demonstrating vertical transferability despite more expensive LP subproblems.The large-model results are reported for 300 Wide-model and 250 Deep-model properties.Source: §6.4 · p. 10, Table 2 · p. 10
  • Across Base, Wide, and Deep models, cactus plots show GNN consistently outperforming BaBSR and MIPplanet, with further small improvements from online learning.Source: Figure 3 · p. 10

7 DISCUSSION

The discussion identifies the verifiable network itself as a useful graph input for improving BaB branching and proposes extending GNN-based decisions to other BaB components. The appendix specifies how BaB branches, bounds, prunes, and terminates on satisfiability properties.

7 DISCUSSION

  • Using the neural network being verified as the GNN's graph input improves branching and suggests applying GNNs to LP initialization and lazy verification.Source: §7 · p. 10

APPENDIX A. BRANCH AND BOUND ALGORITHM

  • BaB repeatedly selects a subproblem, splits it, computes upper and lower bounds, prunes subproblems, and stops when the global bound gap is below ϵ.Source: Appendix A · p. 12
  • For satisfiability verification, initializing the global upper bound to 0 prunes subproblems with lower bounds above 0, while an upper bound below 0 provides early termination through a counterexample.Source: Appendix A · p. 12

APPENDIX B. IMPLEMENTATION OF FORWARD AND BACKWARD PASSES

The appendix implements forward and backward GNN message passing over verification-network nodes, combining local relaxation features with neighboring embeddings. Updates use bounds, primal and dual values, relaxation intercepts, and direction-specific neighborhood information.

APPENDIX B. IMPLEMENTATION OF FORWARD AND BACKWARD PASSES

  • The implementation uses linear intermediate-bound relaxations and Planet relaxation for the final output lower bound, with corresponding LP-derived primal and dual values.The GNN mirrors the verified network's structure and uses these solver quantities as embedding-update inputs.Source: Appendix B · p. 13, §B.2 · p. 15

B.1.1 INPUT NODES

  • Input-node embeddings are initialized once from lower and upper domain bounds plus the associated primal solution, then updated during backward passes.The first forward pass computes µ0[j] from the input feature vector; later input updates occur only backward.Source: §B.1.1 · p. 13

B.1.2 ACTIVATION NODES

  • Activation-node local features include bounds, relaxation intercepts, biases, primal values, and dual values.The relaxation intercept measures the amount of relaxation introduced at an ambiguous node.Source: §B.1.2 · p. 13
  • Forward updates combine local node features with embeddings from the previous network layer, while backward updates use the next layer's embeddings.The forward and backward procedures update activation-node embeddings through analogous three-step computations with direction-specific modifications.Source: §B.1.2 · p. 13, §B.2.1 · p. 15
  • ReLU gates pass no neighbor information when ui[j] ≤ 0, all information when li[j] ≥ 0, and a bound-dependent fraction when their bounds have different signs.For ambiguous gates, the update uses α and α′, with α′ = 1 − α for 0 < α < 1 and α′ = α otherwise.Source: §B.1.2 · p. 14

B.1.3 OUTPUT NODE

  • Output-node embeddings use output bounds, primal values, and layer bias locally, then combine neighbor information before the final update.Output nodes have no associated activation unit, so their neighbor information is computed directly.Source: §B.1.3 · p. 15

B.2.1 ACTIVATION NODES

  • Backward activation updates further weight local information using dual values, which indicate how relaxing associated constraints affects the final objective.For convolutional successor layers, neighbor aggregation is divided by the number of connecting nodes to obtain a consistent measure.Source: §B.2.1 · p. 15

APPENDIX C. ALGORITHM FOR GENERATING TRAINING DATASET

The training-data procedure mixes complete strong-branching runs with cheaper heuristic moves before strong-branching samples, aiming to cover properties and BaB stages efficiently. Experiment hyperparameters were selected from a small validation-set search, leaving room for better choices.

APPENDIX C. ALGORITHM FOR GENERATING TRAINING DATASET

  • Training data covers BaB stages by taking cheap-heuristic steps before collecting strong-branching samples, while 25% of non-timeout properties receive complete strong-branching runs.For remaining properties, the procedure generates at least B samples, choosing a random number of cheap steps up to q between strong-branching decisions.Source: Appendix C · p. 16
  • The dataset-generation algorithm stops sampling when a BaB process terminates or the required per-property sample count is reached.This design combines stage coverage with computational efficiency.Source: Appendix C · p. 16

APPENDIX D. EXPERIMENT DETAILS

  • Hyperparameters were chosen by testing a small set of candidate values on the validation set, and the authors note that better settings may exist.This is an explicit limitation of the experiment-detail selection procedure.Source: Appendix D · p. 17

D.1 TRAINING DETAILS

The experiments train and evaluate a GNN branching strategy against established verification baselines, using strong-branching data and a fail-safe heuristic. The GNN is intended to retain strong branching quality while reducing computational cost across verification settings.

D.1 TRAINING DETAILS

  • Strong-branching data generation is expensive, requiring roughly 200 seconds per sample, so the authors train on a small Base model to exploit vertical transferability.Each sub-domain contains roughly 1300 ambiguous ReLU nodes, with about 140 selected for strong branching.Source: §D.1 · p. 17
  • 85.8% training accuracy and 83.1% validation accuracy are achieved when branching decisions with m_v above 0.9 count as correct.The model uses hinge rank loss and converges within 60 epochs; each training epoch takes less than 400 seconds.Source: §D.1 · p. 17

D.2 VERIFICATION EXPERIMENT DETAILS

  • The fail-safe procedure compares GNN and BaBSR relative improvements and selects the branching decision with the higher value when the GNN margin is below 0.2.Online learning updates the model only after the same failed decision occurs at least twice.Source: §D.2 · pp. 17–18

D.3 BASELINES

  • BaBSR is used as a strong baseline because it significantly outperforms Neurify, which times out on 183 of 200 test properties.The comparison restricts Neurify to one CPU core and a two-minute timeout.Source: §D.3 · p. 18
  • MIPplanet is also a strong baseline, averaging 1732.18 seconds versus 2736.60 seconds for the newer MIP algorithm and winning on 78 of 100 properties.The comparison uses 100 randomly selected CIFAR Base properties with a 3600-second timeout.Source: §D.3 · p. 18
  • The MIPplanet comparison differs mainly in intermediate bound computation, which is complementary to the paper’s focus on branching decisions.The authors state that their branching approach could still be applied if improved intermediate bounds help verification.Source: §D.3 · p. 18

E.1 FAIL-SAFE HEURISTIC DEPENDENCE

  • The GNN accounts for more than 90% of branching decisions on average across the three CIFAR models, indicating limited reliance on the fail-safe heuristic.BaBSR alone is equivalent to removing the GNN and using only the fail-safe heuristic.Source: §E.1 · p. 19, Table 4 · p. 19

E.2 GNN FEATURE ANALYSIS

Feature analysis shows that expensive LP information improves GNN performance, while the framework remains stronger than BaBSR without it. Additional analyses examine timing, robustness to outliers, and transfer across datasets and model sizes.

E.2 GNN FEATURE ANALYSIS

  • Removing primal and dual LP information worsens performance, but GNN-R still outperforms BaBSR, making cheap features a viable lower-cost option.Users can remove expensive LP features or use a smaller GNN architecture depending on LP cost.Source: §E.2 · pp. 19–20, Table 5 · p. 20

E.3 MIPPLANET BRANCHING NUMBER

  • MIPplanet branch counts are not comparable with BaBSR, GNN, or GNN-online because Gurobi’s cutting and branching behavior decouples branch number from solving time.On timed-out Wide-model properties, MIPplanet branch counts range from 1 to 7479.Source: §E.3 · p. 20, Table 6 · p. 20

E.4 LP SOLVING TIME AND GNN COMPUTING TIME

  • GNN evaluation takes 0.02, 0.03, and 0.08 seconds on Base, Wide, and Deep CIFAR models, versus 1.1, 4.9, and 9.6 seconds for one LP solve.LP solving time grows substantially faster with network size than GNN evaluation time.Source: §E.4 · p. 20

E.5 GEOMETRIC MEAN

  • Geometric-mean results are consistent with arithmetic-mean results, supporting the analyses against potential outlier bias.This consistency is reported for both the main and large-model evaluations.Source: §E.5 · p. 20, Table 7 · p. 21, Table 8 · p. 21

E.6 ADDITIONAL PLOTS

  • GNN outperforms BaBSR across easy, medium, and hard Base-model properties, demonstrating horizontal transferability; online learning adds small improvements.On hard properties, BaBSR solves more properties but has worse average time than MIPplanet, while GNN remains best overall.Source: Figure 6 · p. 21

APPENDIX F. MNIST DATASET

  • The MNIST appendix tests horizontal transfer on the Base model and vertical transfer on Wide and Deep models using properties generated with BaBSR.The Base model is chosen for training-data generation because its smaller size makes this process more efficient.Source: Appendix F · p. 21, §F.1 · p. 21, Table 9 · p. 22

F.2 TRAINING DETAILS

The MNIST GNN is trained on data generated from a small Base model, with strong-branching samples produced from selected ambiguous ReLU nodes. Training reaches validation accuracy comparable to the CIFAR model.

F.2 TRAINING DETAILS

  • The MNIST training set contains 18,231 samples and the validation set contains 5,921 samples generated from 538 verification properties.The Base model is deliberately chosen for efficient training-data generation.Source: §F.2 · p. 22
  • Each MNIST training sample takes roughly 45 seconds to generate after selecting about 80 of roughly 480 ambiguous ReLU nodes for strong branching.The procedure uses B = 20 and q = 10.Source: §F.2 · p. 22
  • The trained MNIST GNN reaches 86.5% training accuracy and 83.1% validation accuracy, converging in 70 epochs.Each epoch takes less than 400 seconds.Source: §F.2 · p. 22

F.3 EXPERIMENT RESULTS

MNIST experiments evaluate transfer across difficulty levels and model sizes, finding that GNN-based branching remains effective on larger models while MIPplanet degrades. Online learning further improves the trained GNN, but transfer across datasets fails in the tested setting.

F.3 EXPERIMENT RESULTS

  • GNN-Online outperforms other methods on Wide and Deep models, while MIPplanet performs best on the small Base model.Table 10 compares average solving time, average branch count, and timeout percentage.Source: §F.3 · p. 22, Table 10 · p. 23, Figure 7 · p. 23
  • MIPplanet times out on almost all Wide and Deep properties, whereas GNN consistently outperforms BaBSR across Base, Wide, and Deep models.The authors interpret this as evidence of vertical transferability from smaller to larger networks.Source: §F.3 · p. 22, Figure 7 · p. 23
  • Online learning effectively fine-tunes the trained GNN and provides further performance improvements, especially on the Wide model.The method is evaluated as an additional version of the trained GNN.Source: §F.3 · p. 22, Figure 7 · p. 23

F.4 FAIL-SAFE HEURISTIC DEPENDENCE

  • GNN branching decisions account for most decisions in the MNIST experiments, as evaluated through the fail-safe usage ratios.Table 11 reports average, minimum, and maximum fail-safe heuristic usage by model.Source: §F.4 · p. 23, Table 11 · p. 23

F.5 GEOMETRIC MEAN

  • Geometric-mean results confirm that the arithmetic-mean analyses are not biased by outliers.The corresponding geometric-mean performance results are reported in Table 12.Source: §F.5 · p. 23, Table 12 · p. 23

F.6 TRANSFERABILITY BETWEEN DATASETS

  • A CIFAR-trained GNN fails to transfer to MNIST: BaBSR outperforms it on all 20 tested MNIST Base properties.The authors attribute this result to significant differences between MNIST and CIFAR images.Source: §F.6 · p. 24

Related papers

Loading 1912.01329v1…