Verify VNN-COMP Benchmark for ACAS Xu Neural Networks Using α,β-CROWN
This example shows how to formally verify Verification of Neural Networks Library (VNN-LIB) properties of ACAS Xu neural networks in native ONNX™ model format using the Deep Learning Toolbox™ Interface for alpha-beta-CROWN Verifier support package. This example is step 6 in a series of examples that take you through formally verifying a set of neural networks that output steering advisories to aircraft to prevent them from colliding with other aircraft.
To run this example, open Verify and Deploy Airborne Collision Avoidance System (ACAS) Xu Neural Networks and navigate to Step6VerifyVNNLIBPropertiesOfACASXuNeuralNetworksUsingAlphaBetaCROWNExample.m. This project contains all of the steps for this workflow. You can run the scripts in order or run each one independently.
By default, the example uses a GPU if one is available. Using a GPU requires a Parallel Computing Toolbox™ license and a supported GPU device. For information on supported devices, see GPU Computing Requirements (Parallel Computing Toolbox) (Parallel Computing Toolbox). Otherwise, the example uses the CPU.
α,β-CROWN Algorithm
α,β-CROWN is an algorithm for neural network verification that builds on several algorithms from the CROWN family of formal verification methods:
CROWN [4] — A formal verification framework that uses convex relaxations to compute certified bounds on neural network outputs under input and/or weight perturbations. It enables formally verified robustness at scale, by efficiently bounding worst-case behavior layer-by-layer without exhaustive enumeration. CROWN is an incomplete verification algorithm, meaning that for networks with nonlinear behavior, the bounds on neural network outputs are not exact and overapproximate the exact bounds.
α-CROWN [5] — Extends CROWN using tighter, optimization-based bounds by introducing learnable dual variables (α) that are optimized to strengthen layer-wise convex relaxations. Compared to CROWN, α-CROWN has increased memory and runtime costs. Like CROWN, α-CROWN is an incomplete verification algorithm. For a comparison of CROWN and α-CROWN, see
estimateNetworkOutputBounds.β-CROWN [6] — Further refines bounds by jointly optimizing split constraints (β), enabling branch-and-bound with strong, data-dependent relaxations that significantly tighten certificates and scale to larger networks. For networks with only piecewise linear activations, such as ReLU layers, and no other sources of non-linearity, β-CROWN provides complete verification. This means that β-CROWN can return exact neural network output bounds. However, this can add significant memory and runtime costs.
In MATLAB®, you can verify PyTorch® and ONNX neural network models using Deep Learning Toolbox™ Interface for alpha-beta-CROWN Verifier. This support package provides an interface to the α,β-CROWN algorithm implementation developed by the Verified Intelligence group [1].
Load ACAS Xu Neural Networks
Load and save the networks. The example prepares the networks as shown in Explore ACAS Xu Neural Networks.
acasXuNetworkFolder = fullfile(matlab.project.rootProject().RootFolder,"."); zipFile = matlab.internal.examples.downloadSupportFile("nnet","data/acas-xu-neural-network-dataset.zip"); filepath = fileparts(zipFile); unzip(zipFile,acasXuNetworkFolder); matFolder = fullfile(matlab.project.rootProject().RootFolder,"acas-xu-neural-network-dataset","networks-mat"); helpers.convertACASXuFromONNXAndSave(matFolder);
Importing ONNX files and converting to MAT format... ......... .......... .......... .......... ...... Import and conversion complete.
Setup α,β-CROWN Options
Set the options for α,β-CROWN network verification following the work by Verified Intelligence [1].
This table shows the options provided by Verified Intelligence [3], together with the equivalent options in MATLAB.
YAML File Provided by Verified Intelligence [3] | Equivalent Options in MATLAB |
| |
|
|
|
|
| |
|
|
|
|
| |
|
|
| |
|
|
|
|
| |
| |
|
|
|
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
|
|
|
|
This implementation of the α,β-CROWN algorithm supports iterative input splitting, similar to the adaptive mesh approach described in Verify VNN-COMP Benchmark for ACAS Xu Neural Networks. To enable this mode of verification, set the BabBranchingInputSplitEnable option to true.
Set the algorithm options using the networkVerificationOptions function.
options = networkVerificationOptions(... GeneralEnableIncompleteVerification=false,... GeneralLossReductionFunc="min",... SolverBatchSize=1000,... SolverBoundPropMethod="crown",... SolverBetaCrownIteration=10,... SolverAlphaCrownIteration=10,... SolverAlphaCrownShareAlphas=true,... BabBranchingMethod="naive",... BabBranchingCandidates=3,... BabBranchingInputSplitEnable=true,... BabBranchingInputSplitEnhancedBoundPatience=20,... BabBranchingInputSplitEnhancedBranchingMethod="sb",... BabBranchingInputSplitEnhancedBoundPropMethod="alpha-crown",... BabBranchingInputSplitAttackPatience=80,... BabBranchingInputSplitSbCoeffThresh=0.01,... AttackPgdOrder="after",... AttackPgdRestarts=10000);
Verify Robustness Property Using α,β-CROWN
Verify property , which states: If the intruder is sufficiently far away, the network advises Clear-of-Conflict.
Load the lower and upper bounds and true label within those bounds for the property phi. To load the bounds and label, use the selectVNNLIBProperty function, which is attached to this example as a supporting file. To learn more about the VNN-COMP properties, see Verify VNN-COMP Benchmark for ACAS Xu Neural Networks.
phi = 6; [XLower,XUpper] = helpers.selectVNNLIBProperty(phi); label = [1 1];
Load the network to which applies.
previousAdvisory = 1; tau = 1; net = helpers.loadACASNetwork(previousAdvisory,tau);
The algorithm options specified by Verified Intelligence [1] are intended for the VNN-COMP [2] versions of the ACAS Xu neural networks. To use them, first rescale the network weights and the input data using the renormalizeNetwork and renormalizeInput functions, which are defined at the bottom of this example. For more information about the different data normalizations available for the ACAS Xu neural networks, see Explore ACAS Xu Neural Networks.
net = renormalizeNetwork(net); XLower = renormalizeInput(XLower); XUpper = renormalizeInput(XUpper);
The verifyNetworkRobustness function can verify the robustness of ONNX and PyTorch networks using the α,β-CROWN algorithm. Export the renormalized model to ONNX by using the exportONNXNetwork function.
modelfile = "phi6_previousAdvisory_1_tau_1.onnx"; modelfile = fullfile(matlab.project.rootProject().RootFolder,"artifacts",modelfile); exportONNXNetwork(net,modelfile)
Verify the property using the α,β-CROWN algorithm.
numClasses = 5; result = verifyNetworkRobustness(modelfile,XLower,XUpper,label,numClasses,Algorithm=options)
The results agree with the verification of in Verify VNN-COMP Benchmark for ACAS Xu Neural Networks. For the complete VNN-COMP verification results of the α,β-CROWN algorithm, see https://github.com/VNN-COMP/vnncomp2025_results/tree/main/alpha_beta_crown/2025_acasxu_2023.
Supporting Functions
renormalizeNetwork
The renormalizeNetwork function rescales the weights and biases of the first and last fully connected layers in the networks to use the same normalization as the VNN-COMP benchmark [2].
function net = renormalizeNetwork(net) % Input normalization factors meanInput = [19791.091 0 0 650 600]; rangeInput = [60261 2*pi 2*pi 1100 1200]; % Output normalization factors meanOutput = 7.5188840201005975; rangeOutput = 373.94992; % Rescale the weights and bias of first fully connected layer to % incorporate input normalization W1 = net.Learnables.Value{1}; b1 = net.Learnables.Value{2}; WEnd = net.Learnables.Value{end-1}; bEnd = net.Learnables.Value{end}; % Rescale the weights and bias of last fully connected layer to % incorporate output normalization net.Learnables.Value{1} = W1.*rangeInput; net.Learnables.Value{2} = W1*meanInput' + b1; net.Learnables.Value{end-1} = WEnd/rangeOutput; net.Learnables.Value{end} = (bEnd - meanOutput) / rangeOutput; end
renormalizeInput
The renormalizeInput function rescales the inputs to the neural networks to use the same normalization as the VNN-COMP benchmark [2].
function XScaled = renormalizeInput(X) mean = [19791.091 0 0 650 600]; range = [60261 2*pi 2*pi 1100 1200]; if iscolumn(X) XScaled = (X' - mean)./range; XScaled = XScaled'; else XScaled = (X - mean)./range; end end
References
[1] Verified Intelligence. Verified-Intelligence/Alpha-Beta-CROWN. 29 Jun. 2021, Python. 3 Sep. 2025. GitHub, https://github.com/Verified-Intelligence/alpha-beta-CROWN.
[2] VNN-COMP. VNN-COMP/Vnncomp2025_benchmarks. 7 May 2025, Shell. 16 Jul. 2025. GitHub, https://github.com/VNN-COMP/vnncomp2025_benchmarks.
[3] “Alpha-Beta-CROWN/Complete_verifier/Exp_configs/Vnncomp23/Acasxu.Yaml at 1a3533a02cddfc971213a9ef28002c8e131f7c96 · Verified-Intelligence/Alpha-Beta-CROWN.” GitHub, https://github.com/Verified-Intelligence/alpha-beta-CROWN/blob/1a3533a02cddfc971213a9ef28002c8e131f7c96/complete_verifier/exp_configs/vnncomp23/acasxu.yaml.
[4] Zhang, Huan, et al. “Efficient Neural Network Robustness Certification with General Activation Functions.” arXiv:1811.00866, arXiv, 2 Nov. 2018. arXiv.org, https://doi.org/10.48550/arXiv.1811.00866.
[5] Xu, Kaidi, et al. “Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers.” arXiv:2011.13824, arXiv, 16 Mar. 2021. arXiv.org, https://doi.org/10.48550/arXiv.2011.13824.
[6] Wang, Shiqi, et al. “Beta-CROWN: Efficient Bound Propagation with Per-Neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification.” arXiv:2103.06624, arXiv, 31 Oct. 2021. arXiv.org, https://doi.org/10.48550/arXiv.2103.06624.
