PaperlayerView exact revision on arXiv

Source-linked AI summary

Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification

Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, J. Zico Kolter

arXiv:2103.06624v2cs.LGcs.AIcs.CRstat.ML

TL;DR

Neural-network bound propagation is efficient but cannot fully encode BaB neuron-split constraints, producing loose bounds and limiting verification efficiency. β-CROWN introduces optimizable β parameters to encode these constraints while retaining GPU-friendly propagation. It improves complete and incomplete verification, including higher verified accuracy than SDP-FO with three orders of magnitude less verification time.

  • Problem

    Bound-propagation verifiers are efficient but cannot fully handle BaB neuron-split constraints, leading to loose bounds and inefficient verification.

  • Method

    β-CROWN uses optimizable β parameters and joint intermediate-layer optimization to encode neuron splits within GPU-friendly bound propagation.

  • Results

    β-CROWN leads in complete and incomplete verification settings, obtaining higher verified accuracy than SDP-FO while reducing verification time by three orders of magnitude.

  • Takeaways & Limitations

    β-CROWN combines the split-constraint handling of LP verification with the efficiency and GPU parallelization of bound propagation.

  • Takeaways & Limitations

    The verifier is limited to ReLU-focused BaB, norm-based perturbations, relatively small models, and demonstrated image-classification robustness tasks.

Abstract

from arXiv · show

Bound propagation based incomplete neural network verifiers such as CROWN are very efficient and can significantly accelerate branch-and-bound (BaB) based complete verification of neural networks. However, bound propagation cannot fully handle the neuron split constraints introduced by BaB commonly handled by expensive linear programming (LP) solvers, leading to loose bounds and hurting verification efficiency. In this work, we develop $β$-CROWN, a new bound propagation based method that can fully encode neuron splits via optimizable parameters $β$ constructed from either primal or dual space. When jointly optimized in intermediate layers, $β$-CROWN generally produces better bounds than typical LP verifiers with neuron split constraints, while being as efficient and parallelizable as CROWN on GPUs. Applied to complete robustness verification benchmarks, $β$-CROWN with BaB is up to three orders of magnitude faster than LP-based BaB methods, and is notably faster than all existing approaches while producing lower timeout rates. By terminating BaB early, our method can also be used for efficient incomplete verification. We consistently achieve higher verified accuracy in many settings compared to powerful incomplete verifiers, including those based on convex barrier breaking techniques. Compared to the typically tightest but very costly semidefinite programming (SDP) based incomplete verifiers, we obtain higher verified accuracy with three orders of magnitudes less verification time. Our algorithm empowered the $α,\!β$-CROWN (alpha-beta-CROWN) verifier, the winning tool in VNN-COMP 2021. Our code is available at http://PaperCode.cc/BetaCROWN

1 Introduction

Neural-network verification is difficult because non-convex, high-dimensional networks must satisfy specifications over bounded input domains. β-CROWN addresses the weakness of bound propagation on BaB neuron-split constraints while retaining GPU efficiency and improving verification performance.

  • Neural-network verification seeks guarantees over all inputs in a bounded domain, but the underlying optimization is difficult because networks are non-convex and high-dimensional.
  • BaB recursively splits verification domains and bounds each subdomain, but traditional methods use expensive LP solvers to encode neuron-split constraints.
  • Bound propagation methods produce looser bounds because they cannot fully account for neuron-split constraints, causing unnecessary branching and missed infeasible subdomains.
  • β-CROWN encodes neuron splits with optimizable β parameters, jointly tightens intermediate-layer bounds, and remains GPU-parallelizable like bound propagation.
  • β-CROWN supports incomplete verification by terminating BaB early, achieving higher verified accuracy than powerful incomplete verifiers while reducing verification time by three orders of magnitude relative to SDP-FO.

2 Background

The background formulates verification as minimizing a network output over an input region and reviews LP, CROWN, and BaB-based relaxations. These methods trade tightness and split-constraint handling against computational efficiency.

  • 2.1 The neural network verification problem and its LP relaxation: A feedforward ReLU network maps inputs through weighted affine layers and activations, with verification formulated as minimizing its scalar output over an allowed input region.
  • 2.1 The neural network verification problem and its LP relaxation: Robustness verification commonly uses an ℓ∞ ball around a data point and proves f(x) > 0 for every input in that region.
  • 2.1 The neural network verification problem and its LP relaxation: Incomplete verifiers relax non-convex ReLU constraints to obtain tractable lower bounds, whereas complete verifiers can determine the exact answer given sufficient time.
  • 2.1 The neural network verification problem and its LP relaxation: LP verifiers replace unstable ReLU constraints with linear constraints and can handle neuron splits, but linear solvers are expensive and difficult to accelerate on GPUs.
  • 2.2 CROWN: efficient incomplete verification by propagating linear bounds: CROWN propagates linear bounds backward through the network using relaxed ReLU constraints, offering GPU-efficient computation that can be several magnitudes faster than LP verification.
  • 2.3 Branch and Bound and Neuron Split Constraints: BaB divides the input domain by splitting unstable ReLU neurons, verifies subdomains with lower bounds, and guarantees completeness when all unstable neurons are split.

3 β-CROWN for Complete and Incomplete Verification

β-CROWN incorporates neuron split constraints into bound propagation through optimizable α and β parameters, preserving soundness and CROWN-like efficiency. Joint optimization tightens bounds, supports complete BaB verification, and enables strong incomplete verification when stopped early.

  • β-CROWN bound propagation: β-CROWN adds Lagrangian multiplier parameters β to bound propagation, allowing neuron split constraints to be enforced without an LP solver.The extra β(i)ᵀS(i) terms modify the linear relationship between the network output and intermediate pre-activations.
  • Soundness and efficiency: β-CROWN remains sound for any β ≥0 and has the same asymptotic complexity as CROWN when β is fixed.When β = 0, it produces the same results as CROWN; optimization is used to tighten bounds rather than to preserve validity.
  • Connection to LP: With optimally set α and β and fixed intermediate bounds, β-CROWN produces the optimal objective of the LP with split constraints.The method has both primal and dual interpretations, with β corresponding to dual variables for neuron split constraints.
  • Joint optimization: Optimizing α and β parameters for intermediate-layer bounds tightens relaxations that are fixed and potentially loose in typical LP formulations.Each unstable intermediate neuron can have independent optimization variables, producing tighter final bounds.
  • β-CROWN BaB: β-CROWN can detect infeasible subdomains because an infeasible primal problem yields an unbounded dual objective.This enables β-CROWN with BaB to provide completeness without relying on a slow LP solver for infeasibility detection.
  • β-CROWN BaB: Terminating β-CROWN BaB early yields an incomplete but sound lower bound, while exploring more subdomains progressively tightens the bound.Its efficient exploration of many subdomains makes early-stopped BaB useful for incomplete verification.

4 Experimental Results

Experiments show β-CROWN performs strongly in both complete and incomplete verification, combining fast verification with high verified accuracy and tight bounds.

  • Complete verification: β-CROWN FSB achieves the fastest average running time among baselines with minimal timeouts, while β-CROWN BaBSR also outperforms literature baselines.The comparison includes A.set BaBSR, Fast-and-Complete, and BaDNB.
  • Complete verification: Over 90% of examples are solved within 10 seconds, with a 2 to 3 orders of magnitude speedup over CPU-based MIPplanet and BaBSR.
  • Incomplete verification: β-CROWN FSB achieves better verified accuracy on all evaluated models than strong incomplete verifiers using multi-neuron linear relaxations, with similar or less time.The evaluated baselines include kPoly, OptC2V, and PRIMA.
  • Incomplete verification: β-CROWN is 3 orders of magnitude faster than SDP-FO while achieving consistently higher average verified accuracy across seven models.The comparison covers one MNIST and six CIFAR-10 models.
  • Bound tightness: For adversarially trained networks, β-CROWN FSB consistently outperforms SDP-FO in bound tightness while requiring 3 minutes per point versus 178 minutes.LP verification with triangle relaxations produces much looser bounds.
  • Competition results: The α,β-CROWN verifier, based on β-CROWN and the same codebase, was entered in VNN-COMP 2021.

5 Related Work

Related work spans solver-based complete verification, GPU bound propagation, multi-neuron relaxations, semidefinite methods, and verification-aware training, with β-CROWN addressing split-constraint handling.

  • Complete verification: Early complete verifiers relied on MILP or SMT solvers and were limited to very small problem instances.
  • Complete verification: BaB methods exploit network structure by combining LP-based incomplete verification for bounding with ReLU splits for branching.
  • GPU bound propagation: GPU bound-propagation approaches avoid LP solvers, but prior Lagrangian decomposition typically required hundreds of iterations to approach LP solutions.
  • Incomplete verification: Multi-neuron linear relaxations and joint linear-layer/ReLU relaxations were introduced to overcome the limitations of per-neuron convex relaxations.
  • Incomplete verification: SDP relaxations typically produce tight bounds but require significantly more computation than linear-relaxation methods.
  • Verification-aware training: Verification-aware training improves verified accuracy, whereas β-CROWN BaB can obtain non-trivial verified accuracy on relatively large networks without verification-specific training.

6 Conclusion

β-CROWN fully encodes BaB neuron split constraints through bound propagation and jointly optimizes intermediate bounds. The method is presented as leading in both complete and incomplete verification, while remaining limited in scope and model scale.

  • 6 Conclusion: β-CROWN fully encodes BaB neuron split constraints and can jointly optimize intermediate-layer bounds for tighter verification bounds.The method is described as GPU-friendly and faster than LP solvers while solving an equivalent split-constrained LP problem.
  • 6 Conclusion: BaB-based verification remains limited to relatively small models far from ImageNet scale.This limitation is shared by existing BaB-based complete verifiers, including β-CROWN.
  • 6 Conclusion: β-CROWN can support robustness, correctness, and fairness checks for neural networks in real-world applications.The societal-impact passage describes the verifier as useful for checking certain neural-network properties.

A.1 Proofs for deriving β-CROWN using bound propagation

The appendix derives β-CROWN by propagating relaxed ReLU bounds backward through the network and adding β multipliers for split constraints. Recursive matrix identities establish the resulting bound formula and its relationship to CROWN.

  • A.1 Proofs for deriving β-CROWN using bound propagation: CROWN relaxes each ReLU using valid linear lower or upper bounds determined by neuron bounds and coefficient signs.For unstable neurons, the lower-bound slope is a free variable between 0 and 1, while sign determines whether lower or upper bounds are used.
  • A.1 Proofs for deriving β-CROWN using bound propagation: The recursive function Ω tracks products of network weights and relaxed-ReLU matrices across layers.Examples such as Ω(3, 1) and Ω(5, 2) illustrate the matrix products used in the theorem.
  • A.1 Proofs for deriving β-CROWN using bound propagation: Induction shows that the recursively propagated quantities reproduce the theorem’s coefficients and constants at the input layer.The proof establishes a′ = a(m−1), P′ = P(m−1), q′ = q(m−1), and c′ = c(m−1).
  • A.1 Proofs for deriving β-CROWN using bound propagation: β-CROWN enforces per-neuron split constraints by adding β multipliers during backward bound propagation.The proof introduces these multipliers at each layer and propagates their effects recursively toward the input.
  • A.1 Proofs for deriving β-CROWN using bound propagation: Setting β = 0 recovers the standard CROWN propagation rule, requiring only a small implementation change for β-CROWN.The additional term is β(i+1)^⊤S(i+1) after linear propagation through a ReLU layer.

A.2 Proofs for the connection to the dual space

The appendix derives β-CROWN’s dual formulation by assigning dual variables to all verification constraints, including neuron splits. Backward propagation in dual space matches the primal β-CROWN construction and reaches the split-constrained LP optimum when parameters are optimal.

  • A.2 Proofs for the connection to the dual space: The dual objective can be written as dLP = −∥a + Pβ∥1·ϵ + (P⊤x0 + q)⊤β + a⊤x0 + c.The appendix derives this expression from the recursively propagated quantities and applies it to prove the dual theorem.
  • A.2 Proofs for the connection to the dual space: The dual formulation assigns β variables to the per-neuron split constraints introduced by BaB.The primal problem is rewritten in Lagrangian dual form with variables for the network and split constraints.
  • A.2 Proofs for the connection to the dual space: Dual variables propagate backward through the network using rules that match β-CROWN’s relaxed-ReLU matrices and split terms.The simplified recursion is ν(i) = D(i)ν̂(i) − β(i)S(i), alongside ν̂(i−1) = W(i)^⊤ν(i).
  • A.2 Proofs for the connection to the dual space: β-CROWN’s primal and dual constructions are equivalent because β modifies backward propagation in the same way as the corresponding dual variables.The appendix explicitly identifies the β-CROWN term with the transformed dual propagation term.
  • A.2 Proofs for the connection to the dual space: When α and β are optimal with fixed intermediate bounds, β-CROWN produces the same solution as LP with split constraints.The result follows from equivalence to the rewritten dual LP and strong duality.

A.3 Proof for soundness and completeness

The appendix establishes that β-CROWN with branch and bound is sound and complete. Completeness follows because fully splitting unstable ReLUs makes each subdomain linear, allowing optimized β to recover the exact LP solution.

  • A.3 Proof for soundness and completeness: β-CROWN with branch and bound on split ReLU neurons is sound and complete.This is stated as Theorem 3.3 and proved separately for soundness and completeness.
  • A.3 Proof for soundness and completeness: Soundness follows because each subdomain receives a valid lower bound for every β ≥ 0, and BaB takes the minimum across subdomains.The union of subdomains covers the original domain, so the minimum bound remains valid globally.
  • A.3 Proof for soundness and completeness: Completeness requires solving every fully split subdomain exactly, with up to 2^N subdomains for N unstable neurons.Once all unstable ReLUs are split, each subdomain becomes a linear network with linear input constraints.
  • A.3 Proof for soundness and completeness: In fully split subdomains, the β objective is concave, so supergradient ascent with line search can converge to the globally optimal β.No relaxed ReLU or intermediate-layer α′ and β′ variables remain in this case.
  • A.3 Proof for soundness and completeness: The complete verifier processes subdomains in batches, filters verified domains, and terminates on proof, counterexample, tolerance, or memory thresholds.The algorithm supports early stopping when bounds are sufficiently close or the subdomain set reaches η.

B.2 Comparisons to other GPU based complete verifiers

β-CROWN addresses the limitations of GPU-based BaB verifiers by encoding neuron split constraints during bound propagation, while retaining soundness and completeness without LP solvers.

  • CROWN-based BaB omits neuron split constraints, producing looser bounds, unnecessary branches, and incomplete verification.LP solvers are therefore needed to check inconsistent splits and guarantee completeness.
  • β-CROWN incorporates per-neuron split constraints, reducing branches and solving time while avoiding LP solvers.The method is sound and complete when combined with branch and bound.
  • β-CROWN jointly optimizes more intermediate-layer variables than prior α-only optimization, with O(L^2d^2) free variables instead of O(Ld).The method shares fewer variables across intermediate and final bounds than the compared approach.
  • Incomplete subdomains can be detected when optimized lower bounds exceed maintained upper bounds, although insufficient convergence may delay infeasibility detection.Completeness is guaranteed after all unstable neurons are split, when the problem becomes concave and line search guarantees convergence.

C.1 Experimental Setup

The experiments use GPU-based optimization of α and β on a single workstation, with a separate multithreaded setup for small MLP models.

  • The solver optimizes α and β with Adam for 20 iterations using learning rates 0.1 and 0.05, respectively.Learning rates are decayed during optimization.

C.2 Additional Experiments

Additional experiments compare β-CROWN with LP, SDP, and GPU-based verifiers, examining verified accuracy, bound tightness, runtime, hardware effects, and α/β optimization.

  • Small MLP models use MILP-computed intermediate bounds because tighter bounds help β-CROWN, but MILP is not scalable beyond these models.This setup is an implementation exception rather than the main focus of the work.
  • β-CROWN FSB consistently outperforms BIGM+A.SET BABSR and Fast-and-Complete in verified accuracy, while LP verifiers require significantly more time.The comparison includes jointly optimized intermediate bounds for LP baselines.
  • β-CROWN BaB significantly outperforms LP verifiers in lower-bound tightness, including those using CROWN and jointly optimized intermediate bounds.Tighter intermediate bounds improve LP performance, but a substantial gap remains.
  • β-CROWN remains strong on a single CPU, while GPU execution provides at least a 2x performance boost on the evaluated small models.The results attribute performance to both algorithmic efficiency and GPU acceleration.
  • Joint α and β optimization gives optimal ablation performance, with β optimization having greater impact than α optimization.Joint optimization reduces runtime on CIFAR-10 Base and Wide, but disabling it can slightly help on the easy Deep model.
  • β-CROWN BaBSR improves lower bounds faster than BIGM+A.SET BABSR across four CNN-A-Adv examples within 180 seconds.The experiment plots lower bound against time, with larger lower bounds indicating better verification progress.
Loading 2103.06624v2…