Verify VNN-COMP Benchmark for ACAS Xu Neural Networks

Since R2026a

Step 5 of 9 in Verify and Deploy Airborne Collision Avoidance System (ACAS) Xu Neural Networks

• 4
• 5
• 6

This example shows how to formally verify all of the Verification of Neural Networks Library (VNN-LIB) [1] properties of ACAS Xu neural networks that are part of the Verification of Neural Networks Competition (VNN-COMP) benchmark [3]. This example is step 5 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 Step5VerifyVNNCOMPBenchmarkForACASXuNeuralNetworksExample.m. This project contains all of the steps for this workflow. You can run the scripts in order or run each one independently.

If you have a GPU and Parallel Computing Toolbox™, then the example automatically runs using GPU parallelism.

Define VNN-LIB Properties

VNN-LIB is a standardized format for specifying neural network requirements that must be formally verified.

VNN-COMP uses the ACAS Xu family of neural networks as a benchmark. For more information about the networks, including information about their inputs and outputs, see Explore ACAS Xu Neural Networks.

VNN-COMP defines ten properties that must be verified:

Property	Description	Networks	Input Constraints	Output Requirement
$${\varphi }_1$$	If the intruder is distant and significantly slower than the ownship, then the score of a Clear-of-Conflict advisory must always be above a fixed threshold.	All	$$\rho \ge 55947.691$$ $$v_{\text{own}}\ge 1145$$ $$v_{\text{int}}\le 60$$	The output score for Clear-of-Conflict must not be lesser than -1500.
$${\varphi }_2$$	If the intruder is distant and significantly slower than the ownship, then Clear-of-Conflict must never be the least likely choice.	All	$$\rho \ge 55947.691$$ $$v_{\text{own}}\ge 1145$$ $$v_{\text{int}}\le 60$$	The output score for Clear-of-Conflict must not be the minimum score.
$${\varphi }_3$$	If the intruder is directly ahead and is moving towards the ownship, then the network must not advise Clear-of-Conflict.	All	$$1500\le \rho \le 1800$$ $$-0.06\le \theta \le 0.06$$ $$\psi \ge 3.10$$ $$v_{\text{own}}\ge 980$$ $$v_{\text{int}}\ge 960$$	The output score for Clear-of-Conflict must not be the maximum score.
$${\varphi }_4$$	If the intruder is directly ahead and is moving away from the ownship but at a lower speed than that of the ownship, then the network must not advise Clear-of-Conflict.	All	$$1500\le \rho \le 1800$$ $$-0.06\le \theta \le 0.06$$ $$\psi =0$$ $$v_{\text{own}}\ge 1000$$ $$0\le v_{\text{int}}\le 400$$	The output score for Clear-of-Conflict must not be the maximum score.
$${\varphi }_5$$	If the intruder is near and approaching from the left, the network must advise Strong Right.	Previous advisory Clear-of-Conflict, $$\tau =0$$.	$$250\le \rho \le 400$$ $$0.2\le \theta \le 0.4$$ $$-\pi \le \psi \le -\pi +0.005$$ $$100\le v_{\text{own}}\le 400$$ $$0\le v_{\text{int}}\le 400$$	The output score for Strong Right must be the maximum score.
$${\varphi }_6$$	If the intruder is sufficiently far away, the network must advise Clear-of-Conflict.	Previous advisory Clear-of-Conflict, $$\tau =0$$.	$$12000\le \rho \le 62000$$ $$-\pi \le \theta \le -0.7\text{or}0.7\le \theta \le \pi$$ $$-\pi \le \psi \le -\pi +0.005$$ $$100\le v_{\text{own}}\le 1200$$ $$0\le v_{\text{int}}\le 1200$$	The output score for Clear-of-Conflict must be the maximum score.
$${\varphi }_7$$	If the vertical separation is large, the network must never advise Strong Left or Strong Right.	Previous advisory Clear-of-Conflict, $$\tau =100$$.	$$0\le \rho \le 60760$$ $$-\pi \le \theta \le \pi$$ $$-\pi \le \psi \le \pi$$ $$100\le v_{\text{own}}\le 1200$$ $$0\le v_{\text{int}}\le 1200$$	Neither the output score for Strong Right nor the output score for Strong Left can be the maximum score.
$${\varphi }_8$$	If the vertical separation is large and the previous advisory was Weak Left, then the network must advise Clear-of-Conflict or Weak Left.	Previous advisory Weak Left, $$\tau =100$$.	$$0\le \rho \le 60760$$ $$-\pi \le \theta \le \frac{3\pi }{4}$$ $$-0.1\le \psi \le 0.1$$ $$600\le v_{\text{own}}\le 1200$$ $$600\le v_{\text{int}}\le 1200$$	The output score for Clear-of-Conflict or Weak Left must be the maximum score.
$${\varphi }_9$$	Even if the previous advisory was Weak Right, if there is a nearby intruder, then the network must advise Strong Left.	Previous advisory Weak Right, $$\tau =5$$.	$$2000\le \rho \le 7000$$ $$-0.4\le \theta \le -0.14$$ $$-\pi \le \psi \le -\pi +0.01$$ $$100\le v_{\text{own}}\le 150$$ $$0\le v_{\text{int}}\le 150$$	The output score for Strong Left must be the maximum score.
$${\varphi }_{10}$$	For a distant intruder, the network must advise Clear-of-Conflict.	Previous advisory Strong Left, $$\tau =20$$.	$$36000\le \rho \le 60760$$ $$0.7\le \theta \le \pi$$ $$-\pi \le \psi \le -\pi +0.01$$ $$900\le v_{\text{own}}\le 1200$$ $$600\le v_{\text{int}}\le 1200$$	The output score for Clear-of-Conflict must be the maximum score.

For example, $${\varphi }_6$$ states that for two aircraft with no vertical separation and previous advisory Clear-of-Conflict, the network must continue to advise Clear-of-Conflict if the two aircraft are more than 12,000 ft apart.

This example has two differences compared to Katz et al. [2]:

• The final layer of the networks used in Ref. [2] is unusual, because the predicted class corresponds to the index of the minimum output of the network, rather than the maximum output. To use MATLAB® functions like scores2label, this example applies a scaling of -1 to the final fully connected layer in the networks, such that the predicted class corresponds to the index of the maximum output of the network. The output requirements in the table are expressed in terms of the scaled networks, so "minimum scores" in Ref. [2] correspond to "maximum scores" in this example.

• To reflect the requirements used in VNN-COMP, in this example, you verify requirements $${\varphi }_1,...,{\varphi }_4$$ for all networks, rather than for a subset of all networks as in Ref. [2].

The ten VNN-COMP properties can be categorized into four groups:

• Properties $${\varphi }_5,{\varphi }_6,{\varphi }_9,{\varphi }_{10}$$ are all robustness requirements: Within the region defined by the input constraints, the relevant networks must always predict the correct class.

• Property $${\varphi }_1$$ is a stability requirement of the output scores associated with Clear-of-Conflict: The score must not be less than -1500.

• Property $${\varphi }_2$$ is a requirement similar to robustness. It requires that, within a specified region, Clear-of-Conflict must never be the least likely class.

• Properties $${\varphi }_3,{\varphi }_4,{\varphi }_7,{\varphi }_8$$ are requirements similar to robustness, but there is more than one class that the network is allowed to predict.

This example shows how to use the verifyNetworkRobustness function to verify all ten properties. This function verifies the robustness of neural networks. To prove more general properties, modify the networks to transform the properties into robustness properties.

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.

Verify VNN-LIB Property

First, define the verifyVNNLIBProperty function that proves or disproves a VNN-LIB property phi for a network net.

function results = verifyVNNLIBProperty(net,phi,NameValueArgs)

Define two name-value arguments, MaxNumInputsSplits and MiniBatchSize. The MaxNumInputSplits argument specifies the maximum number of iterations of the adaptive mesh algorithm. The MiniBatchSize argument specifies the number of hypercuboids to analyze simultaneously.

    arguments
        net (1,1) dlnetwork
        phi (1,1) {mustBeInteger}
        NameValueArgs.MaxNumInputSplits (1,1) {mustBeInteger} = 150
        NameValueArgs.MiniBatchSize (1,1) {mustBeInteger} = 8192
    end

Load the lower and upper bounds, the true label within those bounds for the property phi, and the output class labels for the property phi. To load the bounds and labels, use the selectVNNLIBProperty function, which is attached to this example as a supporting file.

[XLower,XUpper,label,outputClassLabels] = helpers.selectVNNLIBProperty(phi);
XUpper = dlarray(XUpper,"BC");
XLower = dlarray(XLower,"BC");

Initialize and run the adaptive mesh loop, as described in the Verify Global Stability of ACAS Xu Neural Network Using Adaptive Mesh example.

cubes = helpers.CubeBatch(XLower,XUpper);
verifiedCubes = helpers.CubeBatch;
cubeQueue = helpers.CubeBatchQueue;
enqueue(cubeQueue,cubes);
numProcessed = 0;
numVerified = 0;
numUnproven = 0;
verifiedLabelBatch = [];
adversarialExample = [];

XDiff = XUpper - XLower;
zeroVolumeDimensions = all(XDiff == 0, 2);
XDiff(zeroVolumeDimensions,:) = [];
totalVolume = sum(prod(XDiff));

loopCounter = 1;
while ~isempty(cubeQueue) && all(ismember(verifiedLabelBatch,label)) && loopCounter < NameValueArgs.MaxNumInputSplits
    cubes = getCubes(cubeQueue,NameValueArgs.MiniBatchSize);
    idxLabel = predictAtCenters(net,cubes);
    
    result = verifyNetworkRobustness(net,cubes.xLower,cubes.xUpper,idxLabel,MiniBatchSize=NameValueArgs.MiniBatchSize);
    idxVerified = (result == "verified");
    idxUnproven = (result == "unproven");
    
    verifiedMiniBatch = getSubset(cubes,idxVerified);
    verifiedLabelBatch = [verifiedLabelBatch idxLabel(idxVerified)]; %#ok<AGROW>
    verifiedCubes = addSubset(verifiedCubes,verifiedMiniBatch);

If the label predicted at the center of any hypercuboid is different from the true label, then the center of that hypercuboid is an adversarial example and the property is violated. Save the first such example and terminate the execution of the loop.

    tf = ~ismember(verifiedLabelBatch,label);
    if any(tf)
        verifiedCubeBatchCenters = getCenters(verifiedCubes);
        adversarialExamples = verifiedCubeBatchCenters(:,tf);
        adversarialExample = adversarialExamples(:,1);
        break
    end

    unprovenCubes = getSubset(cubes,idxUnproven);

If any hypercuboids remain unproven, search for adversarial examples using the findAdversarialExamples function. If the function returns an adversarial example, then the property is violated. Save the example and terminate the execution of the loop.

    if ~isempty(unprovenCubes)  
        options = adversarialOptions("fgsm",MiniBatchSize=NameValueArgs.MiniBatchSize);
        adversarialExample = findAdversarialExamples(net, ...
            unprovenCubes.xLower,unprovenCubes.xUpper, ...
            idxLabel(1:getNumCubes(unprovenCubes)), ...
            Algorithm=options);
        if ~isempty(adversarialExample)
            break
        end
    end

Further divide the unproven hypercuboids, as described in the Verify Global Stability of ACAS Xu Neural Network Using Adaptive Mesh example. To ensure that the function verifies all hypercuboids, set the tolPerDim argument to zero.

    tolPerDim = 0;
    helpers.bisectAndUpdateQueue(cubeQueue,unprovenCubes,tolPerDim);

    numVerified = numVerified + sum(idxVerified);
    numUnproven = numUnproven + sum(idxUnproven);
    numRemaining = numCubesInQueue(cubeQueue);
    numProcessed = numProcessed + getNumCubes(cubes);

Update the progress plot using the updateAndPlotMetrics function, which is defined at the bottom of this example.

    unverifiedVolume = volumeOfCubesInQueue(cubeQueue) / totalVolume;
    updateAndPlotMetrics(verifiedLabelBatch,verifiedCubes,totalVolume,numVerified,numRemaining,unverifiedVolume,outputClassLabels)
    loopCounter = loopCounter + 1;    
end

Save the output variables in the results structure.

results.verifiedLabelBatch = verifiedLabelBatch;
results.tfCubeQueueIsEmpty = isempty(cubeQueue);
results.adversarialExample = adversarialExample;
results.cubeQueue = cubeQueue;
results.phi = phi;
results.label = label;
end

Verify Properties $${\varphi }_5,{\varphi }_6,{\varphi }_9,{\varphi }_{10}$$

Keep track of the results by using a structure that saves the verification results as well as any adversarial examples. Initialize the struct by using the createVNNLIBResultStruct function, which is defined at the bottom of this example.

vnnlibResults = createVNNLIBResultStruct;
rng(0)

Properties $${\varphi }_5,{\varphi }_6,{\varphi }_9,{\varphi }_{10}$$ each apply to a single network. For each property, load the correct network, then verify the property by using the verifyVNNLIBProperty function.

Property $${\varphi }_5$$ states: If the intruder is near and approaching from the left, the network must advise Strong Right.

phi = 5;
previousAdvisory = 1;
tau = 1;

Load the network by using the loadACASNetwork function, which is attached to this example as a supporting file.

net = helpers.loadACASNetwork(previousAdvisory,tau);

Verify the property phi and plot the result by using the verifyVNNLIBProperty function.

figure
results = verifyVNNLIBProperty(net,phi);

vnnlibResults = recordResults(vnnlibResults,results,1);

phi_5(network_1): verified

Property $${\varphi }_6$$ states: If the intruder is sufficiently far away, the network must advise Clear-of-Conflict.

phi = 6;
previousAdvisory = 1;
tau = 1;

Load the network by using the loadACASNetwork function, which is attached to this example as a supporting file.

net = helpers.loadACASNetwork(previousAdvisory,tau);

Verify the property phi and plot the result by using the verifyVNNLIBProperty function.

figure
results = verifyVNNLIBProperty(net,phi);

vnnlibResults = recordResults(vnnlibResults,results,1);

phi_6(network_1): verified

Property $${\varphi }_9$$ states: Even if the previous advisory was Weak Right, if there is a nearby intruder, then the network must advise Strong Left.

phi = 9;
previousAdvisory = 3;
tau = 3;

Load the network by using the loadACASNetwork function, which is attached to this example as a supporting file.

net = helpers.loadACASNetwork(previousAdvisory,tau);

Verify the property phi and plot the result by using the verifyVNNLIBProperty function.

figure
results = verifyVNNLIBProperty(net,phi);

vnnlibResults = recordResults(vnnlibResults,results,1);

phi_9(network_1): verified

Property $${\varphi }_{10}$$ states: For a distant intruder, the network advises Clear-of-Conflict.

phi = 10;
previousAdvisory = 4;
tau = 5;

Load the network by using the loadACASNetwork function, which is attached to this example as a supporting file.

net = helpers.loadACASNetwork(previousAdvisory,tau);

Verify the property phi and plot the result by using the verifyVNNLIBProperty function.

figure
results = verifyVNNLIBProperty(net,phi);

vnnlibResults = recordResults(vnnlibResults,results,1);

phi_10(network_1): verified

Verify VNN-LIB Property $${\varphi }_1$$

Property $${\varphi }_1$$ states: For each of the 45 networks, if the intruder is distant and significantly slower than the ownship, then the score of a Clear-of-Conflict advisory must always be above a fixed threshold (-1500).

To rephrase this stability property as a robustness property, add a fully connected layer to the network that creates two channels: one that is exactly zero, and one that adds 1500 to the Clear-of-Conflict output channel. If property $${\varphi }_1$$ is true, then the resulting network always predicts the second channel. Therefore, to verify $${\varphi }_1$$, verify the robustness of the amended network.

phi = 1;
figure
counter = 1;
for previousAdvisory = 1:5
    for tau = 1:9
        net = helpers.loadACASNetwork(previousAdvisory,tau);

Define the weights and biases of the fully connected layer.

        w = [1 0 0 0 0; ... % return Clear-of-Conflict score
            0 0 0 0 0];     % return zero
        b = [1500; ...      % add 1500 to Clear-of-Conflict score
            0];             % return zero

Add the fully connected layer to the network.

        net = addLayers(net, fullyConnectedLayer(2,Name="phi1",Weights=w,Bias=b));
        net = connectLayers(net,"fc_7","phi1");
        net = initialize(net);

Verify $${\varphi }_1$$.

        results = verifyVNNLIBProperty(net,phi);
        vnnlibResults = recordResults(vnnlibResults,results,counter);
        counter = counter + 1;
    end
end

phi_1(network_1): verified
phi_1(network_2): verified
phi_1(network_3): verified
phi_1(network_4): verified
phi_1(network_5): verified
phi_1(network_6): verified
phi_1(network_7): verified
phi_1(network_8): verified
phi_1(network_9): verified
phi_1(network_10): verified
phi_1(network_11): verified
phi_1(network_12): verified
phi_1(network_13): verified
phi_1(network_14): verified
phi_1(network_15): verified
phi_1(network_16): verified
phi_1(network_17): verified
phi_1(network_18): verified
phi_1(network_19): verified
phi_1(network_20): verified
phi_1(network_21): verified
phi_1(network_22): verified
phi_1(network_23): verified
phi_1(network_24): verified
phi_1(network_25): verified
phi_1(network_26): verified
phi_1(network_27): verified
phi_1(network_28): verified
phi_1(network_29): verified
phi_1(network_30): verified
phi_1(network_31): verified
phi_1(network_32): verified
phi_1(network_33): verified
phi_1(network_34): verified
phi_1(network_35): verified
phi_1(network_36): verified
phi_1(network_37): verified
phi_1(network_38): verified
phi_1(network_39): verified
phi_1(network_40): verified
phi_1(network_41): verified
phi_1(network_42): verified
phi_1(network_43): verified
phi_1(network_44): verified
phi_1(network_45): verified

Verify VNN-LIB Property $${\varphi }_2$$

Property $${\varphi }_2$$ states: For each of the 45 networks, if the intruder is distant and significantly slower than the ownship, then Clear-of-Conflict must never be the least likely choice.

Similar to property $${\varphi }_1$$, you can amend the network to convert this property into a robustness property.

• First, multiply the network output scores by -1. For the amended network, Clear-of-Conflict must now never be the most likely choice.

• Next, add a layer that creates two output channels: one that returns the Clear-of-Conflict output score, and a second that returns the highest score of all four other output scores. This new output channel is equivalent to "any class other than Clear-of-Conflict". If property $${\varphi }_2$$ is true, then the resulting network always predicts the second channel. Therefore, to verify $${\varphi }_2$$, verify the robustness of the amended network.

To calculate the maximum of two output scores, use a ReLU layer:

$$\max (a,b)=a+\text{ReLU}(b-a).$$

To calculate the maximum of more than two output scores, use more than one ReLU layer.

phi = 2;
figure
counter = 1;
for previousAdvisory = 1:5
    for tau = 1:9        
        net = helpers.loadACASNetwork(previousAdvisory,tau);

Multiply the network output by -1.

        net.Learnables.Value{end-1} = -net.Learnables.Value{end-1}; % -Weights
        net.Learnables.Value{end} = -net.Learnables.Value{end}; % -Bias

Create new layers to compute the maximum output scores by using the maxNet function, which is defined at the bottom of this example. This function implements the equation $$\max (a,b)=a+\text{ReLU}(b-a)$$ using a residual network.

        netLayer1 = maxNet(2,3,5,"maxNet1");
        netLayer2 = maxNet(1,3,4,"maxNet2");
        netLayer3 = maxNet(1,3,3,"maxNet3");

        net = addLayers(net, netLayer1);
        net = addLayers(net, netLayer2);
        net = addLayers(net, netLayer3);
        net = connectLayers(net,net.OutputNames{1},netLayer1.Name);
        net = connectLayers(net,netLayer1.Name,netLayer2.Name);
        net = connectLayers(net,netLayer2.Name,netLayer3.Name);
        net = expandLayers(net);
        net = initialize(net);
        
        results = verifyVNNLIBProperty(net,phi);
        vnnlibResults = recordResults(vnnlibResults,results,counter);

        counter = counter + 1;
    end
end

phi_2(network_1): verified
phi_2(network_2): violated
phi_2(network_3): violated
phi_2(network_4): violated
phi_2(network_5): violated
phi_2(network_6): violated
phi_2(network_7): verified
phi_2(network_8): verified
phi_2(network_9): verified
phi_2(network_10): violated
phi_2(network_11): violated
phi_2(network_12): violated
phi_2(network_13): violated
phi_2(network_14): violated
phi_2(network_15): violated
phi_2(network_16): violated
phi_2(network_17): violated
phi_2(network_18): violated
phi_2(network_19): violated
phi_2(network_20): violated
phi_2(network_21): timeout
phi_2(network_22): violated
phi_2(network_23): violated
phi_2(network_24): violated
phi_2(network_25): violated
phi_2(network_26): violated
phi_2(network_27): violated
phi_2(network_28): violated
phi_2(network_29): timeout
phi_2(network_30): violated
phi_2(network_31): violated
phi_2(network_32): violated
phi_2(network_33): violated
phi_2(network_34): violated
phi_2(network_35): violated
phi_2(network_36): violated
phi_2(network_37): violated
phi_2(network_38): violated
phi_2(network_39): violated
phi_2(network_40): violated
phi_2(network_41): violated
phi_2(network_42): violated
phi_2(network_43): violated
phi_2(network_44): violated
phi_2(network_45): violated

Verify Generalized Robustness Properties $${\varphi }_3,{\varphi }_4,{\varphi }_7,{\varphi }_8$$

Properties $${\varphi }_3,{\varphi }_4,{\varphi }_7,{\varphi }_8$$ each state that, within a given input region, a network must return one of several allowed advisories.

Similar to property $${\varphi }_2$$, convert these properties into robustness properties by adding layers such that the network has two output channels: one for the allowed classes, and one for the disallowed classes.

Property $${\varphi }_3$$ states: For each of the 45 networks, if the intruder is directly ahead and is moving towards the ownship, then the network must not advise Clear-of-Conflict. $${\varphi }_3$$ applies to all 45 networks.

phi = 3;
figure
counter = 1;
for previousAdvisory = 1:5
    for tau = 1:9
        net = helpers.loadACASNetwork(previousAdvisory,tau);
        
        netLayer1 = maxNet(2,3,5,"maxNet1");
        netLayer2 = maxNet(1,3,4,"maxNet2");
        netLayer3 = maxNet(1,3,3,"maxNet3");

        net = addLayers(net,netLayer1);
        net = addLayers(net,netLayer2);
        net = addLayers(net,netLayer3);
        net = connectLayers(net,net.OutputNames{1},netLayer1.Name);
        net = connectLayers(net,netLayer1.Name,netLayer2.Name);
        net = connectLayers(net,netLayer2.Name,netLayer3.Name);
        net = expandLayers(net);
        net = initialize(net);

        results = verifyVNNLIBProperty(net,phi);
        vnnlibResults = recordResults(vnnlibResults,results,counter);
        counter = counter + 1;
    end
end

phi_3(network_1): verified
phi_3(network_2): verified
phi_3(network_3): verified
phi_3(network_4): verified
phi_3(network_5): verified
phi_3(network_6): verified
phi_3(network_7): violated
phi_3(network_8): violated
phi_3(network_9): violated
phi_3(network_10): verified
phi_3(network_11): verified
phi_3(network_12): verified
phi_3(network_13): verified
phi_3(network_14): verified
phi_3(network_15): verified
phi_3(network_16): verified
phi_3(network_17): verified
phi_3(network_18): verified
phi_3(network_19): verified
phi_3(network_20): verified
phi_3(network_21): verified
phi_3(network_22): verified
phi_3(network_23): verified
phi_3(network_24): verified
phi_3(network_25): verified
phi_3(network_26): verified
phi_3(network_27): verified
phi_3(network_28): verified
phi_3(network_29): verified
phi_3(network_30): verified
phi_3(network_31): verified
phi_3(network_32): verified
phi_3(network_33): verified
phi_3(network_34): verified
phi_3(network_35): verified
phi_3(network_36): verified
phi_3(network_37): verified
phi_3(network_38): verified
phi_3(network_39): verified
phi_3(network_40): verified
phi_3(network_41): verified
phi_3(network_42): verified
phi_3(network_43): verified
phi_3(network_44): verified
phi_3(network_45): verified

Property $${\varphi }_4$$ states: For each of the 45 networks, if the intruder is directly ahead and is moving away from the ownship, but at a lower speed than that of the ownship, then the network must not advise Clear-of-Conflict.

phi = 4;
figure
counter = 1;
for previousAdvisory = 1:5
    for tau = 1:9
        net = helpers.loadACASNetwork(previousAdvisory,tau);

        netLayer1 = maxNet(2,3,5,"maxNet1");
        netLayer2 = maxNet(1,3,4,"maxNet2");
        netLayer3 = maxNet(1,3,3,"maxNet3");
        
        net = addLayers(net,netLayer1);
        net = addLayers(net,netLayer2);
        net = addLayers(net,netLayer3);
        net = connectLayers(net,net.OutputNames{1},netLayer1.Name);
        net = connectLayers(net,netLayer1.Name,netLayer2.Name);
        net = connectLayers(net,netLayer2.Name,netLayer3.Name);
        net = expandLayers(net);
        net = initialize(net);

        results = verifyVNNLIBProperty(net,phi);
        vnnlibResults = recordResults(vnnlibResults,results,counter);
        counter = counter + 1;
    end
end

phi_4(network_1): verified
phi_4(network_2): verified
phi_4(network_3): verified
phi_4(network_4): verified
phi_4(network_5): verified
phi_4(network_6): verified
phi_4(network_7): violated
phi_4(network_8): violated
phi_4(network_9): violated
phi_4(network_10): verified
phi_4(network_11): verified
phi_4(network_12): verified
phi_4(network_13): verified
phi_4(network_14): verified
phi_4(network_15): verified
phi_4(network_16): verified
phi_4(network_17): verified
phi_4(network_18): verified
phi_4(network_19): verified
phi_4(network_20): verified
phi_4(network_21): verified
phi_4(network_22): verified
phi_4(network_23): verified
phi_4(network_24): verified
phi_4(network_25): verified
phi_4(network_26): verified
phi_4(network_27): verified
phi_4(network_28): verified
phi_4(network_29): verified
phi_4(network_30): verified
phi_4(network_31): verified
phi_4(network_32): verified
phi_4(network_33): verified
phi_4(network_34): verified
phi_4(network_35): verified
phi_4(network_36): verified
phi_4(network_37): verified
phi_4(network_38): verified
phi_4(network_39): verified
phi_4(network_40): verified
phi_4(network_41): verified
phi_4(network_42): verified
phi_4(network_43): verified
phi_4(network_44): verified
phi_4(network_45): verified

Property $${\varphi }_7$$ states: If the vertical separation is large, the network never advises Strong Left or Strong Right. $${\varphi }_7$$ applies to a single network, previous advisory Clear-of-Conflict, $$\tau =100$$.

phi = 7;
figure
previousAdvisory = 1;
tau = 9;

net = helpers.loadACASNetwork(previousAdvisory,tau);

netLayer1 = maxNet(1,2,5,"maxNet1");
netLayer2 = maxNet(1,2,4,"maxNet2");

net = addLayers(net,netLayer1);
net = addLayers(net,netLayer2);
net = connectLayers(net,net.OutputNames{1},netLayer1.Name);
net = connectLayers(net,netLayer1.Name,netLayer2.Name);
net = expandLayers(net);
net = initialize(net);

Property $${\varphi }_7$$ tends to take a long time to verify. To avoid timing out, increase MaxNumInputSplits to 500.

results = verifyVNNLIBProperty(net,phi,MaxNumInputSplits=500);

vnnlibResults = recordResults(vnnlibResults,results,1);

phi_7(network_1): violated

Property $${\varphi }_8$$ states: For a large vertical separation and a previous Weak Left advisory, the network advises Clear-of-Conflict or Weak Left. $${\varphi }_8$$ applies to a single network, previous advisory Weak Left, $$\tau =100$$.

phi = 8;
figure
previousAdvisory = 2;
tau = 9;

net = helpers.loadACASNetwork(previousAdvisory,tau);

netLayer = maxNet(1,2,5,"maxNet");
net = addLayers(net, netLayer);
net = connectLayers(net,net.OutputNames{1},netLayer.Name);
net = expandLayers(net);
net = initialize(net);

results = verifyVNNLIBProperty(net,phi);

vnnlibResults = recordResults(vnnlibResults,results,1);

phi_8(network_1): violated

Summarize VNN-COMP Verification Results

Summarize the results using the plotResults function, defined at the bottom of this example.

plotResults(vnnlibResults)

In this example, of the 186 properties, 137 were verified, 2 timed out, and 47 were violated. Finding adversarial examples is nondeterministic, so these numbers can change when rerunning the example.

Save the verification results to a MAT-file.

save(fullfile(matlab.project.rootProject().RootFolder,"artifacts","vnnlibResults"),"vnnlibResults")

Supporting Functions

plotClassProportion

The plotClassProportion function plots the percentage of the ODD that corresponds to the different advisory classes.

function plotClassProportion(property,numCubesVerified,numCubesRemaining,outputClassLabels)
hold off
bar([outputClassLabels;"Unverified"],...
    property);
ylim([0 1.1])
ylabel("Proportion of ODD")
text(1:length(property),property,num2str(property'),'vert','bottom','horiz','center');
str = sprintf('numCubesVerified: %d\nnumCubesRemaining: %d',numCubesVerified,numCubesRemaining);
annotation("textbox",[0.15 0.4 0.3 0.2], ...
    String=str, ...
    FitBoxToText="on", ...
    BackgroundColor="white");
end

predictAtCenters

The predictAtCenters function computes the network advisory at the center of each hypercuboid.

function idxLabel = predictAtCenters(net,cubes)
cubeCenters = getCenters(cubes);
advisory = predict(net,cubeCenters);
[~,idxLabel] = max(extractdata(advisory));
end

updateAndPlotMetrics

The updateAndPlotMetrics function calculates the percentage of the ODD corresponding to the different advisory classes and updates the verification progress plot.

function updateAndPlotMetrics(verifiedLabelBatch,verifiedCubeBatch,totalVolume,numCubesVerified,numCubesRemaining,unverifiedVolume,outputClassLabels)
propVerifiedVolumePerClass = zeros(1,numel(outputClassLabels)+1);
for ii = 1:numel(outputClassLabels)
    predictClassIdx = (verifiedLabelBatch == ii);
    s = verifiedCubeBatch.xUpper(:,predictClassIdx) - verifiedCubeBatch.xLower(:,predictClassIdx);
    zeroVolDims = all(s==0,2);
    s(zeroVolDims,:) = [];
    verifiedCubeVolumePerClass = sum(prod(s,1));
    propVerifiedVolumePerClass(ii) = verifiedCubeVolumePerClass / totalVolume;
end
propVerifiedVolumePerClass(numel(outputClassLabels)+1) = unverifiedVolume;
plotClassProportion(propVerifiedVolumePerClass,numCubesVerified,numCubesRemaining,outputClassLabels)
drawnow
end

recordResults

The recordResults function updates the vnnlibResults structure with the results of the verification.

function vnnlibResults = recordResults(vnnlibResults,results,networkIdx)
field = "phi_" + results.phi;
if results.tfCubeQueueIsEmpty && all(ismember(results.verifiedLabelBatch,results.label)) && isempty(results.adversarialExample) % all hypercuboids are verified and no adversarial examples were found
    disp("phi_" + results.phi + "(network_" + networkIdx + "): verified");
    vnnlibResults.(field).results{networkIdx} = "verified";
    vnnlibResults.(field).adversarialExamples{networkIdx} = [];
elseif ~all(ismember(results.verifiedLabelBatch,results.label)) || ~isempty(results.adversarialExample) % an adversarial example exists
    vnnlibResults.(field).results{networkIdx} = "violated";
    vnnlibResults.(field).adversarialExamples{networkIdx} = extractdata(results.adversarialExample(:,1));
    disp("phi_" + results.phi + "(network_" + networkIdx + "): violated");
else % the calculation timed out
    vnnlibResults.(field).results{networkIdx} = "timeout";
    vnnlibResults.(field).adversarialExamples{networkIdx} = [];
    disp("phi_" + results.phi + "(network_" + networkIdx + "): timeout");
end
end

plotResults

The plotResults function plots the percentages of networks that were verified, violated, and timed out for each property.

function plotResults(vnnlibResults)
fields = fieldnames(vnnlibResults);
numFields = numel(fields);

verified_counts = zeros(1,numFields);
unproven_counts = zeros(1,numFields);
violated_counts = zeros(1,numFields);

for i = 1:numFields
    vals = vnnlibResults.(fields{i}).results;
    if iscell(vals)
        vals = string(vals);
    end
    verified_counts(i) = sum(vals == "verified");
    unproven_counts(i) = sum(vals == "timeout");
    violated_counts(i) = sum(vals == "violated");
end

data = [verified_counts; unproven_counts; violated_counts]';

figure
bar(data,"stacked",BarWidth=0.7);
legend(["verified";"timed out";"violated"], ...
    Location="northeast", ...
    Box="on", ...
    FontSize=12);

xticklabels = cell(1, numFields);
for i = 1:numFields
    xticklabels{i} = ['$\phi_{',num2str(i),'}$'];
end
set(gca,XTickLabel=xticklabels,TickLabelInterpreter="latex");

xlabel("VNN-LIB Property");
ylabel("Count");

total_verified = sum(verified_counts);
total_unproven = sum(unproven_counts);
total_violated = sum(violated_counts);

str = sprintf(['verified: %d\n', ...
    'timed out: %d\n', ...
    'violated: %d'], ...
    total_verified, ...
    total_unproven, ...
    total_violated);

annotation("textbox", [0.67, 0.4, 0.18, 0.15], ...
    String=str, ...
    Interpreter="tex", ...
    FontSize=12, ...
    EdgeColor="none", ...
    BackgroundColor=[1 1 1 0.8], ...
    FitBoxToText="on");

box on
set(gca,FontSize=12);

hold on
y_offset = zeros(1, numFields);
for cat = 1:3
    for i = 1:numFields
        count = data(i,cat);
        if count > 0
            if i >= 5
                y = sum(data(i,:));
                x = i;
                text(x, y + 0.5, num2str(count), ...
                    HorizontalAlignment="center", ...
                    VerticalAlignment="bottom", ...
                    FontWeight="bold", ...
                    FontSize=10, ...
                    Color="k");
            else
                y = y_offset(i) + count/2;
                x = i;
                text(x,y,num2str(count), ...
                    HorizontalAlignment="center", ...
                    VerticalAlignment="middle", ...
                    FontWeight="bold", ...
                    FontSize=10, ...
                    Color="k");
            end
        end
        y_offset(i) = y_offset(i) + count;
    end
end
hold off
end

createVNNLIBResultStruct

The createVNNLIBResultStruct function initializes a structure to keep track of the verification results for each network and property, including any adversarial examples.

function vnnlibResults = createVNNLIBResultStruct
vnnlibResults = struct();
vnnlibResults.phi_1.results              = cell(45,1);
vnnlibResults.phi_1.adversarialExamples  = cell(45,1);
vnnlibResults.phi_2.results              = cell(45,1);
vnnlibResults.phi_2.adversarialExamples  = cell(45,1);
vnnlibResults.phi_3.results              = cell(45,1);
vnnlibResults.phi_3.adversarialExamples  = cell(45,1);
vnnlibResults.phi_4.results              = cell(45,1);
vnnlibResults.phi_4.adversarialExamples  = cell(45,1);
vnnlibResults.phi_5.results              = cell(1,1);
vnnlibResults.phi_5.adversarialExamples  = cell(1,1);
vnnlibResults.phi_6.results              = cell(1,1);
vnnlibResults.phi_6.adversarialExamples  = cell(1,1);
vnnlibResults.phi_7.results              = cell(1,1);
vnnlibResults.phi_7.adversarialExamples  = cell(1,1);
vnnlibResults.phi_8.results              = cell(1,1);
vnnlibResults.phi_8.adversarialExamples  = cell(1,1);
vnnlibResults.phi_9.results              = cell(1,1);
vnnlibResults.phi_9.adversarialExamples  = cell(1,1);
vnnlibResults.phi_10.results             = cell(1,1);
vnnlibResults.phi_10.adversarialExamples = cell(1,1);
end

maxNet

The maxNet function returns a network layer containing a network that calculates the maximum of two output scores out of a total of numInputs classes.

function netLayer = maxNet(outIdx1,outIdx2,numInputs,layerName)
net = dlnetwork;
w = eye(numInputs);
w1 = zeros(2,numInputs);
w1(1,:) = w(outIdx1,:);
w1(2,:) = w(outIdx2,:);
keepRows = 1:numInputs;
keepRows([outIdx1,outIdx2]) = [];
w2 = w(keepRows,:);

tempNet = [...
    identityLayer(Name="identity")
    fullyConnectedLayer(2,Weights=w1,Name="y_iy_j")
    fullyConnectedLayer(1,Name="y_i-y_j", Weights=[1 -1]) % Difference between channels: y_i-y_j
    reluLayer(Name="relu_y_i-y_j")]; % ReLU difference between channels: relu(y_i-y_j)
net = addLayers(net,tempNet);

tempNet = fullyConnectedLayer(1,Name="y_j",Weights=[0 1]); % Propagate the second channel: y_j
net = addLayers(net,tempNet);

tempNet = additionLayer(2,Name="addition"); % ReLU(y_i-y_j) + y_j = max(y_i,y_j)
net = addLayers(net,tempNet);

tempNet = fullyConnectedLayer(numInputs-2,Weights=w2,Name="y_k");
net = addLayers(net,tempNet);

tempNet = depthConcatenationLayer(2,Name="depthcat");
net = addLayers(net,tempNet);

net = connectLayers(net,"y_iy_j","y_j");
net = connectLayers(net,"identity","y_k");
net = connectLayers(net,"relu_y_i-y_j","addition/in1");
net = connectLayers(net,"y_j","addition/in2");
net = connectLayers(net,"addition","depthcat/in1");
net = connectLayers(net,"y_k","depthcat/in2");
netLayer = networkLayer(net,Name=layerName);
end

References

[1] VNN-LIB. https://www.vnnlib.org/. Accessed 4 Sep. 2025.

[2] Katz, Guy, et al. “Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks.” arXiv:1702.01135, arXiv, 19 May 2017. arXiv.org, https://doi.org/10.48550/arXiv.1702.01135.

[3] VNN-COMP. VNN-COMP/Vnncomp2025_benchmarks. 7 May 2025, Shell. 16 Jul. 2025. GitHub, https://github.com/VNN-COMP/vnncomp2025_benchmarks.