BoundLab: A Neural Network Verification Framework Based on Zonotope Abstraction and CROWN Propagation

Title: BoundLab: A Neural Network Verification Framework Based on Zonotope Abstraction and CROWN Propagation Abstract: Introducing the BoundLab open-source framework, which is based on Zonotope abstraction and CROWN propagation techniques, providing a systematic solution for robustness verification and formal analysis of neural networks. Original Author/Maintainer: YuantianDing Source Platform: GitHub Original Link: https://github.com/YuantianDing/BoundLab Release Time: June 12, 2026

With the widespread application of deep learning models in critical safety domains such as autonomous driving, medical diagnosis, and financial risk control, the reliability verification of neural networks has become increasingly important. However, deep neural networks are inherently complex nonlinear systems, and their behavior is difficult to formally analyze using traditional methods.

Research on adversarial attacks has shown that even small, imperceptible perturbations to inputs can cause neural networks to produce completely incorrect outputs. This phenomenon exposes the potential risks of neural networks in safety-critical applications. Therefore, developing verification tools that can rigorously prove the robustness of neural networks has important theoretical and practical value.

The BoundLab project was born in this context. It provides a systematic framework for building neural network verification tools, helping researchers and engineers analyze the safety boundaries of neural networks.

Zonotope Abstraction

Zonotope is a special geometric structure widely used in the field of neural network verification to represent the perturbation range of the input space. Compared with traditional interval arithmetic, Zonotope can capture linear correlations between variables, thus providing tighter boundary estimates. In BoundLab, Zonotope is used to represent the range of activation values when propagating through each layer of the neural network. By maintaining the linear relationship between symbolic variables and actual values, the system can calculate the upper and lower bounds of the output without enumerating all possible inputs.

CROWN Propagation Technology

CROWN (Crown-based Robustness Verification for Deep Neural Networks) is a neural network verification method based on linear boundary propagation. Its core idea is to construct linear upper and lower bounds for each nonlinear activation function, then propagate these bounds layer by layer through the network to finally obtain the boundary estimate of the output. BoundLab implements a CROWN-like propagation mechanism and has made several improvements on this basis, including tighter boundary calculation, more efficient symbolic propagation, etc.

Framework Functional Features

As a verification tool framework, BoundLab provides the following core functions:

• Formal verification support: Robustness verification, safety verification, counterexample generation
• Efficient computation optimization: Matrix multiplication optimization, memory management, automatic parameter tuning
• Experiment and evaluation tools: Depth scaling test, benchmark test suite, visualization report

Precise ε² Handling

In Zonotope computation, shared ε variables produce quadratic terms (ε²). BoundLab implements a precise ε² handling method:

• The range of diagonal term εᵢ² is precisely determined as [0,1]
• The range of non-diagonal term εᵢεⱼ is [-1,1]
• Calculate the true range of residuals via Minkowski sum
• Use interval upper bounds for safe truncation to prevent numerical overflow

Input Splitting Strategy

To improve verification accuracy, BoundLab implements a splitting strategy based on input radius (BaB - Branch and Bound):

• Only shrink the radius of input LpEpsilon
• Sub-regions are generated by center point ± εᵢ/2
• Use a small over-coverage of 1+8·ulp to ensure completeness
• Support multiple splitting strategies: based on smear, automatic differentiation, or random selection

Quadratic Epsilon Registry

BoundLab introduces the PairEpsilon mechanism to manage the epsilon relationship between different input pairs:

• Establish independent epsilon scopes for different input pairs
• Implement precise cancellation of epsilon product terms
• Ensure cancellation consistency through normalized (lo, hi) directions
• Fold the quality of truncation into new epsilon residuals

Softmax Simplex Constraint

For the Softmax layer in Transformers, BoundLab implements simplex constraints:

• The sum of Softmax rows is 1 and each term is non-negative
• The S@V operation can be expressed as a convex combination of V rows
• The output boundary is determined by the minimum lower bound and maximum upper bound of V
• Use a mask mixing strategy to choose between Box and R bounding boxes

Depth Scaling Experiment

Tests on the TinyAttn model (d=16, 8 tokens, ε=0.03) show:

• Square mode: The output widths of L1/L2/L3 layers are 0.2095/0.3697/0.6407, and the matrix multiplication ratios are 21%/37%/53%
• Precise mode: The output width is reduced to 0.1915/0.3046/0.4465, and the matrix multiplication ratios are 15%/26%/39%
• Precise+sym mode: Further optimized to 0.1879/0.2924/0.4186, with ratios of 13%/23%/35%
• +optimize_lambda: Brings an additional improvement of 0.1%/0.5%/1.6%, with computational overhead not exceeding 2x

Memory Optimization Effect

• The square_matmul generator path reduces peak memory usage by more than 5x in the scenario of (64,64)@((64,64) matrix and E=256
• The previously OOM-prone test_transformer test can now pass normally

Verification Correctness

• The 4 strategies of certify_split maintain monotonicity as the budget increases
• Counterexample generation can return concretely verified adversarial examples
• Boundary search can correctly distinguish between verifiable, falsifiable, and unknown cases
• The quadratic registry can control the cancellation error of A@B + A@(-B) below 1e-5

Safety-Critical System Verification

BoundLab can be used to verify neural networks deployed in safety-critical domains such as autonomous vehicles, aerospace control systems, and medical devices. By formally proving the behavioral safety of the network within a specific input perturbation range, it provides theoretical guarantees for these high-risk applications.

Adversarial Defense Evaluation

Researchers can use BoundLab to evaluate the effectiveness of different defense mechanisms. By calculating the boundary tightness of the network after defense processing, the degree of robustness improvement by the defense strategy can be quantified.

Network Architecture Design Guidance

Verification results can be fed back to the network design phase. By analyzing which layers or operations cause boundary expansion, architects can adjust the network structure in a targeted manner to design inherently more robust models.

Education and Research

BoundLab provides a complete experimental platform for research in the field of neural network verification. Its modular design allows researchers to easily insert new verification algorithms, boundary calculation strategies, or splitting heuristics, accelerating innovation in this field.

Current Limitations

• Same-symbol epsilon expansion: The ε⊗ε cancellation function when x and y share input epsilon has not been implemented yet, requiring further mechanism design
• Softmax boundary: The simplex constraint is effective at the node level, but downstream outputs may widen due to the V-hull box strategy
• Automatic differentiation limitations: For models containing softmax/exp, autograd_smear falls back to input_smear because backpropagation involves operations that produce NaNs such as sqrt(0)

Future Development Directions

• Joint differential matrix multiplication: Optimization of single residual transfer, shared symbols, and reset trigger counters
• Batch Box evaluation: Implement batch ONNX export and evaluation in the BaB driver
• Tighter boundaries: Explore new abstract domains and boundary calculation techniques
• Larger-scale networks: Expand verification capabilities through parallelization and approximation methods

BoundLab represents an important progress in the field of neural network verification. By combining Zonotope abstraction and CROWN propagation techniques, this framework provides a solid foundation for building reliable neural network verification tools. Its modular architecture design, rich optimization strategies, and strict correctness guarantees make it a valuable resource for research and application in this field.

For developers engaged in AI safety research, BoundLab is not only a tool but also a learning platform. By reading its implementation, one can deeply understand the core challenges and solutions in neural network verification. As neural networks are increasingly applied in safety-critical domains, verification frameworks like BoundLab will play an increasingly important role.