PaperlayerView exact revision on arXiv

Source-linked AI summary

Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers

Kaidi Xu, Huan Zhang, Shiqi Wang, Yihan Wang, Suman Jana, Xue Lin, Cho-Jui Hsieh

arXiv:2011.13824v2cs.AIcs.LG

TL;DR

Complete neural-network verification is difficult because BaB relies on expensive LP bounding, while naive LiRPA can be too loose and fail to check infeasible ReLU splits. The paper tightens LiRPA with fast gradient optimization, uses LP only when needed for feasibility, and batches splits for accelerator execution, reporting substantial speedups over LP-based verifiers.

  • Problem

    Complete verification requires definite answers, but LP-based BaB is costly and poorly parallelized, while naive LiRPA may be too loose and incomplete.

  • Method

    The framework uses optimized backward LiRPA bounds, minimal LP feasibility checking, and batch splitting on massively parallel accelerators within BaB.

  • Results

    The verifier significantly outperforms LP-based approaches, with around 30X speedup over basic BaB+LP baselines and up to 3X over recent complete verifiers.

  • Takeaways & Limitations

    Optimized LiRPA can provide bounds competitive with or tighter than LP while enabling efficient complete verification on accelerator hardware.

  • Takeaways & Limitations

    Naive LiRPA-based BaB is not complete because it may fail to detect conflicting ReLU split settings, requiring LP feasibility checks.

Abstract

from arXiv · show

Formal verification of neural networks (NNs) is a challenging and important problem. Existing efficient complete solvers typically require the branch-and-bound (BaB) process, which splits the problem domain into sub-domains and solves each sub-domain using faster but weaker incomplete verifiers, such as Linear Programming (LP) on linearly relaxed sub-domains. In this paper, we propose to use the backward mode linear relaxation based perturbation analysis (LiRPA) to replace LP during the BaB process, which can be efficiently implemented on the typical machine learning accelerators such as GPUs and TPUs. However, unlike LP, LiRPA when applied naively can produce much weaker bounds and even cannot check certain conflicts of sub-domains during splitting, making the entire procedure incomplete after BaB. To address these challenges, we apply a fast gradient based bound tightening procedure combined with batch splits and the design of minimal usage of LP bound procedure, enabling us to effectively use LiRPA on the accelerator hardware for the challenging complete NN verification problem and significantly outperform LP-based approaches. On a single GPU, we demonstrate an order of magnitude speedup compared to existing LP-based approaches.

1 INTRODUCTION

Formal verification is needed to ensure neural networks remain reliable under bounded perturbations, but complete verification is computationally difficult and existing BaB approaches are limited by expensive, poorly parallelized LP bounding. The paper proposes combining LiRPA, optimization, selective LP use, and batch splitting to improve complete verification efficiency.

  • Motivation: Formal verification helps establish that neural-network predictions remain reliable in safety- or security-critical settings despite adversarial perturbations.Imperceptible input changes can unexpectedly alter predictions, motivating formal guarantees.
  • Verification challenge: Complete verification requires a definite yes/no answer and generally entails solving a non-convex global optimization problem, making it NP-hard.Incomplete convex relaxations can verify properties when their sound lower bound is nonnegative but otherwise provide no conclusion.
  • Existing approach: BaB obtains global guarantees by recursively splitting the input domain and bounding each sub-domain with an incomplete verifier.The global lower bound is formed from sub-domain bounds, and verification succeeds only when all leaves satisfy the property.
  • Existing approach: LP-based BaB is constrained by high solving cost and limited parallelization on massively parallel accelerators such as GPUs and TPUs.These limitations reduce the performance and scalability of existing complete verifiers.
  • Paper direction: LiRPA offers highly parallel bound propagation, but naive use can produce loose bounds and fail to preserve completeness during ReLU splitting.The paper therefore targets LiRPA as a faster alternative while addressing its weaknesses in complete verification.
  • Contribution: The proposed framework combines optimized LiRPA bounds, minimal LP use for feasibility checking, and batch splitting, achieving around 30X speedup over basic BaB+LP baselines and up to 3X over recent complete verifiers.The framework is designed to exploit accelerator hardware while retaining complete verification.

2 BACKGROUND

The paper formulates neural-network verification as proving output properties over bounded input domains and explains BaB, LP relaxation, and backward LiRPA bound propagation. BaB recursively splits domains and combines sound sub-domain bounds, while LiRPA computes efficient linear output bounds through layerwise backward propagation.

  • Formal NN definition: A feedforward ReLU network recursively maps inputs through weighted pre-activations and post-activation values to a final output.The notation defines h^(i)(x)=W^(i)g^(i−1)(x), g^(i)(x)=ReLU(h^(i)(x)), and f(x)=h^(L)(x), ignoring biases.
  • Verification problem: Formal verification asks whether every input in a bounded domain produces an output satisfying a specified property.Many studied properties reduce to Boolean expressions over linear output equations.
  • Verification problem: A sound lower bound on the network minimum can establish a property without solving the non-convex optimization problem exactly.The bound must remain valid for all inputs in the domain.
  • Branch and Bound: BaB recursively partitions the input domain into independent sub-domains and computes a relaxed, sound lower bound for each one.The global lower bound is the minimum of the sub-domain bounds; verification requires the property to hold on every leaf.
  • Branch and Bound: BaB is sound when the bounding method is sound, but completeness additionally requires feasibility checking for sub-domain constraints.Considering all possible sub-domains does not by itself guarantee a definite answer.
  • LP bounding: LP bounding relaxes each activation unit into a convex linear domain and uses a linear solver to obtain a sub-domain lower bound.Tighter intermediate activation bounds produce tighter LP bounds, and branching heuristics select activation nodes expected to improve the bound.
  • LiRPA: Backward LiRPA propagates linear upper and lower output relationships through linear and relaxed ReLU layers until they are expressed in terms of the input.The resulting bounds are linear functions of x and remain sound over the input domain; this paper uses backward-mode methods such as CROWN and DeepPoly.
  • LiRPA: LiRPA computes a lower bound on its final linear expression over the input domain, for example using Hölder’s inequality on an ℓp-norm ball.ReLU states determine whether relaxation is needed, with stable positive neurons requiring no relaxation.

3 PROPOSED ALGORITHM

The proposed framework optimizes LiRPA bounds for fast, parallel BaB verification, while using LP selectively to recover completeness when LiRPA cannot check split feasibility.

  • 3.1 Optimized LiRPA for Complete Verification: Optimized LiRPA jointly adjusts intermediate ReLU bounds and output bounds, potentially producing tighter bounds than LP’s fixed-relaxation optimization.LP optimizes output bounds while keeping intermediate bounds fixed; LiRPA makes intermediate bounds depend on optimizable parameters α.
  • 3.1 Optimized LiRPA for Complete Verification: Gradient descent optimizes α on GPUs, preserving fast bound computation while enabling bounds that can outperform LP.The inner optimization has closed-form solutions, and projected gradient descent constrains each α coordinate to [0, 1].
  • 3.1 Optimized LiRPA for Complete Verification: Figure 3 compares optimized LiRPA bounds over 0 to 200 iterations with LP bounds, illustrating the effect of iterative bound optimization.The procedure first uses heuristic α values, then applies gradient descent to tighten LiRPA bounds and intermediate-layer relaxations.
  • 3.2 Completeness with Minimal Usage of LP Bounding Procedure: Naive LiRPA BaB is incomplete because LiRPA can lose feasibility information and fail to detect conflicting ReLU split constraints.LP preserves these constraints through its linear solver and can identify infeasible sub-domains.
  • 3.4 Our Complete Verification Framework: Batch splitting computes LiRPA bounds for multiple sub-domains on GPUs, while the algorithm switches to LP after the search-tree depth exceeds threshold η.The algorithm maintains unverified sub-domains, filters verified domains, and uses LP as a fallback for completeness.
  • 3.2 Completeness with Minimal Usage of LP Bounding Procedure: The framework invokes LP only when LiRPA bounding is stuck or all unstable neurons are split, providing minimal feasibility checking for completeness.Theorem 3.2 states that detecting all infeasible leaf sub-domains with LP is sufficient for complete BaB verification.

4 EXPERIMENTS

Experiments evaluate the verifier on CIFAR10 across Base, Wide, and Deep models, showing substantial speedups over LP-based and other state-of-the-art baselines.

  • Results: 10X, 4X, and 20X faster than the best LP-based verifier on Base, Wide, and Deep models, respectively.The comparison is against Lu and Kumar (2020).
  • Setup: The evaluation uses CIFAR10 with Base, Wide, and Deep networks across Easy, Medium, and Hard verification difficulty levels.The task verifies that an l∞ perturbation does not cause a classifier to predict a predefined wrong label.
  • Comparisons against state-of-the-art verifiers: The comparison includes five baselines: BABSR, MIPPLANET, GNN, GNN-ONLINE, and BDD+ BABSR, using one CPU and one GPU with a 3,600-second timeout.The baselines include LP-based BaB methods, a customized MIP solver, and a GPU-accelerated Lagrangian decomposition verifier.
  • Base-model results: 5∼40X faster than baseline BaBSR and 2∼20X faster than GNN split baselines on Base across Easy, Medium, and Hard levels.The speedup comes from the faster LiRPA-based bounding procedure while using BaBSR’s basic branching heuristic without GNNs.
  • Evaluation metrics: Table 1 compares average solving time, average branch count, and the percentage of timed-out properties across methods and models.Figure 4 plots the percentage of solved properties as running time increases.
  • Larger-model performance: 30X speedup over BABSR and 20X less running time than GNN-ONLINE on the Deep model.The method is also reported as significantly faster than the GPU-based Lagrangian decomposition verifier.

5 RELATED WORK

Related work spans complete verification with SMT, MILP, and BaB frameworks, as well as incomplete convex-relaxation methods and GPU-accelerated alternatives.

  • Complete verifiers: Early complete verifiers use SMT and MILP, while higher-order logic provers have not demonstrated scalability to neural-network verification.These approaches typically do not scale well in the neural-network setting.
  • GPU-accelerated verification: GPUPoly accelerates DeepPoly on CUDA but remains an incomplete verifier and makes gradient-based bound optimization less accessible.Its CUDA C++ implementation requires manual effort for customization and gradient computation.
  • GPU-accelerated verification: Lagrangian decomposition provides GPU-accelerated complete BaB verification without LP, but solves a more complicated optimization problem and typically needs hundreds of iterations per sub-domain.This distinguishes it from LiRPA-based bounding.
  • Incomplete verifiers: Incomplete verification methods commonly replace nonlinear ReLU activations with linear or semidefinite constraints to obtain relaxations.The cited methods also study tightening these relaxations.

6 CONCLUSION

The paper uses LiRPA to accelerate BaB bounding for complete neural-network verification on massively parallel hardware and reports speedups across models and properties.

  • Conclusion: The verifier combines LiRPA-based bounding with a fast gradient-based procedure to tighten bounds during complete BaB verification.The approach targets massively parallel accelerators.
  • Conclusion: Up to 5X speedup is reported compared to state-of-the-art verifiers across multiple models and properties.The conclusion summarizes the method’s reported cross-model performance.

A.1 Proof of Theorem 3.1

The counterexample shows that pure LiRPA-based BaB can retain infeasible split sub-domains and therefore fail to establish a property that is actually true.

  • Counterexample: The counterexample uses a two-ReLU network whose hidden nodes share the same input, with the verification property f ≥0 over x=[−1,1].Because the hidden nodes are identical, the ground-truth output range is [0,0].
  • Counterexample: A complete verifier should obtain the optimal lower bound 0 after splitting the two ReLU nodes together.This bound proves the nonnegativity property.
  • Feasibility failure: Only the first two split sub-domains are feasible, while pure LiRPA cannot identify the infeasibility of the other two.The estimated bounds for the infeasible sub-domains can therefore affect the global minimum.
  • Feasibility failure: Pure LiRPA reports a global lower bound of −1 instead of 0 and consequently cannot verify the property.The failure arises from taking the minimum over all four sub-domains, including infeasible ones.

A.2 Proof of Theorem 3.2

The proof establishes completeness by separating feasible from infeasible ReLU-split sub-domains and using LP feasibility checks to remove the latter. LiRPA then gives exact minima on feasible leaf sub-domains where all ReLUs are fixed.

  • Sub-domain construction: The worst case with N unstable ReLU neurons produces 2^N leaf sub-domains, each corresponding to one assignment of ReLU splits.The split assignments impose positive or negative constraints on the neurons’ pre-activation values.
  • Feasibility partition: Some split sub-domains are infeasible because neuron constraints can be mutually inconsistent, so only feasible sub-domains cover the original input domain.The feasible and infeasible sets are disjoint, while infeasible sub-domains are empty.
  • Feasibility checking: LP detects infeasible sub-domains by encoding the fixed ReLU predicates and linear neuron equations as constraints over the input.A feasible LP provides an input satisfying the neuron assignments; an infeasible LP certifies that no such input exists.
  • Global bound: Removing infeasible sub-domains from the LiRPA minimum prevents them from contributing to the global lower bound.Without this filtering, LiRPA may minimize over sub-domains that contain no valid input.
  • Exactness and completeness: Every feasible leaf has no unstable ReLU neurons, making the network linear there and allowing LiRPA to compute its exact minimum.Because feasible leaves cover the original domain, the minimum across their exact minima is the exact global minimum.

B EXPERIMENTAL SETUP

The experiments evaluate the verifier on robustly trained CIFAR-10 convolutional networks using the same benchmark examples and model families as prior state-of-the-art verifiers. Comparisons use specified CPU and GPU hardware and fixed implementation settings.

  • Datasets and models: Evaluation uses the challenging CIFAR-10 dataset with robustly trained Base, Wide, and Deep convolutional networks.The model structures match those used in the GNN-ONLINE and BABSR studies.
  • Verification property: The verification property requires preserving the correct label against a specified wrong label within an l∞ perturbation radius ϵ.The condition is expressed as a positive logit difference for the correct and wrong labels over all perturbed inputs.
  • Hardware and settings: Experiments run on one Intel I7-7700K CPU and one Nvidia GTX 1080 Ti GPU, using one CPU core for fair comparisons.The parallel batch sizes are 400, 200, and 200 for Base, Wide, and Deep models, respectively.
  • Optimization settings: The verifier optimizes LiRPA bounds with 100 gradient-descent steps to obtain the initial bound.The setting is applied under the reported GPU memory constraint η = 12,000.

C ABLATION STUDY

The ablation study shows that optimized LiRPA bounds and GPU batch splitting are complementary components of the complete verification framework. Optimized bounds are essential, while combining both techniques gives the largest speedup.

  • Component ablation: Unoptimized LiRPA with batched splits cannot beat the BABSR baseline because its bounds are too loose to improve the global lower bound quickly.The result isolates bound tightness as a key requirement for effective batched verification.
  • Component ablation: Optimized LiRPA without batch splits achieves around 2 ∼10X speedup compared to BABSR.This uses single-node splitting with GPU batch size 1.
  • Component ablation: Combining batch splits and optimized LiRPA achieves up to 44X speedup compared to BABSR.The full combination outperforms either component used alone.

D COMPLETE VERIFICATION WITH LiRPA ON CPU VS GPU

The CPU-versus-GPU study compares LiRPA verification across CPU core counts and GPU acceleration on Base, Wide, and Deep networks. More CPU cores reduce runtime, but GPU acceleration provides a substantially larger gain, especially for larger models.

  • CPU scaling: Runtime decreases as CPU core count increases, but the speedup is not linear because of linear-algebra library and hardware limitations.The comparison includes the Base, Wide, and Deep networks.
  • GPU scaling: GPU acceleration creates a large gap over eight CPU cores, with the difference most apparent on Wide and Deep models.The result indicates stronger GPU benefits on the larger network variants.
  • Baseline comparison: Even with one CPU core, the method is significantly faster than BABSR and competitive with GNN-ONLINE, which additionally uses one GPU.This comparison supports the efficiency of LiRPA-based verification beyond GPU acceleration alone.
  • Comparison setup: Figure 5 compares one, two, four, and eight CPU cores without a GPU against one CPU core plus one GPU and GNN-ONLINE.BABSR verification times are reported in captions because they fall outside the plotted range.
Loading 2011.13824v2…