AI Verification Tips and Tricks

R2026b

This page describes tips and techniques for formally verifying neural networks using the verifyNetworkRobustness and estimateNetworkOutputBounds functions, which are found in the AI Verification Library for Deep Learning Toolbox and the Deep Learning Toolbox Interface for alpha-beta-CROWN Verifier support packages. You can use these techniques if verification is slow, uses too much memory, or returns "unproven" results. You can improve performance by choosing the right algorithm, designing verifiable network architectures, and managing floating-point precision. For an introduction to AI verification concepts, including robustness and soundness, see Verification of Neural Networks.

Choose the Right Verification Function

The AI Verification Library for Deep Learning Toolbox™ provides functions for formal verification that work with networks you create in MATLAB^® or import from PyTorch^® and ONNX™ using importNetworkFromPyTorch or importNetworkFromONNX. This table describes when to use each function.

Task	Function	Details
Verify robustness of a classification network	`verifyNetworkRobustness`	Verifies that the network classifies all inputs between the specified lower and upper bounds as the same class
Compute output bounds for a network	`estimateNetworkOutputBounds`	Computes the range of output values that a network returns when the input is between the specified lower and upper bounds

The support package also provides the findAdversarialExamples function, which stochastically searches for inputs between the specified lower and upper bounds that cause misclassification. These inputs are adversarial examples. You can use adversarial examples during training to improve network robustness by augmenting the training data with the identified vulnerabilities. For an example, see Train Image Classification Network Robust to Adversarial Examples. Note that if the function does not find an adversarial example, one or more might still exist.

If you have a PyTorch or ONNX network, you can also use the α,β-CROWN verifier from the Deep Learning Toolbox Interface for alpha-beta-CROWN Verifier support package. For more information, see Compare Verification Algorithms.

The estimateNetworkOutputBounds, verifyNetworkRobustness, and findAdversarialExamples functions define the input region using lower and upper bounds. The input region is the set of all arrays X such that XLower ≤ X ≤ XUpper, elementwise. This definition allows you to specify different ranges of perturbation on each input dimension and to partition the operational design domain into local regions without overlaps or gaps.

Compare Verification Algorithms

The verifyNetworkRobustness and estimateNetworkOutputBounds functions support multiple formal verification algorithms based on CROWN. Each algorithm is sound with respect to real arithmetic, for more information, see Soundness in Floating-Point Arithmetic. Each algorithm offers a different tradeoff between bound tightness, computation time, and memory usage.

Algorithm Bound Tightness Computation Time Memory Usage When to Use

CROWN (default)

Tight

Fast

Medium

Algorithm	Bound Tightness	Computation Time	Memory Usage	When to Use
CROWN (default)	Tight	Fast	Medium	CROWN is the fastest algorithm and uses the least memory. If this algorithm verifies your property or gives sufficiently tight bounds, then you do not need further analysis. By default, the formal verification functions use the CROWN algorithm.
α-CROWN	Tighter	Medium	High	Use when CROWN returns `"unproven"` results or when you need tighter bounds. This algorithm tightens bounds for networks that contain ReLU layers. For networks without ReLU layers, the results are the same as CROWN.
α,β-CROWN	Tightest	Slow	Very High	Use when α-CROWN still returns `"unproven"` results and you need the tightest possible bounds. This algorithm tightens bounds for networks that contain ReLU layers. For networks without ReLU layers, the results are the same as CROWN. For networks that consist of only linear layers (such as convolutions, fully connected, and batch normalization) and piecewise-linear activation functions (such as ReLU), the α,β-CROWN algorithm is a complete verifier. This means that given enough time, the algorithm computes the true bounds for the specified input. Requires an ONNX or PyTorch network and the Deep Learning Toolbox Interface for alpha-beta-CROWN Verifier support package.

CROWN is the fastest algorithm and uses the least memory. If this algorithm verifies your property or gives sufficiently tight bounds, then you do not need further analysis.

By default, the formal verification functions use the CROWN algorithm.

α-CROWN Tighter Medium High Use when CROWN returns "unproven" results or when you need tighter bounds. This algorithm tightens bounds for networks that contain ReLU layers. For networks without ReLU layers, the results are the same as CROWN.

α,β-CROWN

Tightest

Slow

Very High

Use when α-CROWN still returns "unproven" results and you need the tightest possible bounds. This algorithm tightens bounds for networks that contain ReLU layers. For networks without ReLU layers, the results are the same as CROWN.

For networks that consist of only linear layers (such as convolutions, fully connected, and batch normalization) and piecewise-linear activation functions (such as ReLU), the α,β-CROWN algorithm is a complete verifier. This means that given enough time, the algorithm computes the true bounds for the specified input.

Requires an ONNX or PyTorch network and the Deep Learning Toolbox Interface for alpha-beta-CROWN Verifier support package.

Design Verifiable Networks

The architecture of your neural network affects the tightness of verification bounds, the memory usage, and the computation time. Use the following recommendations to design networks that are both high-performing and verifiable. For a complete list of supported layers, see Deep Learning Layers Supported for Formal Verification.

Prefer convolutional architectures. These networks offer a good balance between bound tightness and memory usage.
For time-series applications, prefer convolution1dLayer with 1-D pooling layers over recurrent layers such as lstmLayer or gruLayer. Recurrent layers have many nonlinearities that compound verification errors over time steps, producing increasingly loose bounds for long sequences.
Prefer reluLayer and leakyReluLayer activation layers. The α-CROWN and α,β-CROWN algorithms can tighten bounds for networks that contain these layers.
Prefer batchNormalizationLayer over layerNormalizationLayer. Layer normalization computes cross-channel statistics at run time, which is more memory intensive and produces looser bounds.
Prefer average pooling over max pooling. Average pooling produces tighter bounds.
Avoid padding in the network. Padding can cause large memory overheads during verification.
Use additionLayer and depthConcatenationLayer for combination. These layers increase network capacity without reducing verifiability.

Balance Network Size and Depth

Network width and depth both affect verification performance. Wider networks have more hidden units per layer, and shallower networks have fewer layers. Wide, shallow networks tend to produce tighter verification bounds but use more memory. Thin, deeper networks use less memory, but tend to produce looser bounds because overapproximation compounds through each layer.

This table summarizes the approximate memory and runtime tradeoffs for the CROWN family of formal verification algorithms as network size and depth change.

	Shallow	Deep
Thin	Memory: Good Runtime: Good	Memory: Good Runtime: Moderate
Wide	Memory: Moderate Runtime: Good	Memory: Moderate Runtime: Moderate

Shallow

Deep

Thin

Memory: Good

Runtime: Good

Memory: Good

Runtime: Moderate

Wide

Memory: Moderate

Runtime: Good

Memory: Moderate

Runtime: Moderate

Soundness in Floating-Point Arithmetic

Formal verification algorithms are sound with respect to real arithmetic. This means the algorithm guarantees correct verification for the network interpreted over exact real numbers, rather than the floating-point arithmetic that hardware uses. The software runs the algorithm using floating-point arithmetic. Because software uses finite-precision, floating-point representations in place of exact real numbers, there is always some unavoidable roundoff error in the numerical computations.

The verifyNetworkRobustness and estimateNetworkOutputBounds functions check for soundness issues caused by the accumulation of roundoff error. These issues occur when any lower bound exceeds the upper bound, which invalidates the remaining verification. If the algorithm detects a soundness issue, the verifyNetworkRobustness and estimateNetworkOutputBounds functions show a warning and return <undefined> or NaN results, respectively.

To mitigate soundness issues, use these strategies:

Enable GPU determinism — Nondeterministic GPU operations can introduce different accumulation effects between the lower and upper bound propagation. This can happen when you use a GPU to verify networks with max pooling, average pooling, or convolution layers. To remove this effect, enable GPU determinism by calling deep.gpu.deterministicAlgorithms(true).
Increase floating-point precision — Convert your input data, network learnables, and states from single to double precision before verification and prediction, including any normalization statistics on the network input layer. For example:
```
net = dlupdate(@double,net);
net.State = dlupdate(@double,net.State); % If network has state parameters
```
Converting to double precision reduces the size of roundoff errors that accumulate through the network layers and verification algorithm.
Consider the network architecture — For recommendations on designing verifiable networks, see Design Verifiable Networks.

These strategies also help reduce the effects of roundoff error between the verification results and the inference results, where the inference results are the output of the minibatchpredict function or generated C/C++ code.

The effects of floating-point roundoff are typically negligible because input ranges are many orders of magnitude larger than machine precision. However, in rare cases, floating-point rounding errors can accumulate and cause the prediction outputs from the minibatchpredict function or generated C/C++ code to be outside the computed verification bounds. The effect is more pronounced when input ranges are a similar order of magnitude to the machine precision, for example, if the input range is 1e-7 and the neural network and input bounds are in single precision.