Verify Local Robustness of ACAS Xu Neural Networks

In this exercise, you will use formal verification methods to prove that an aircraft collision avoidance neural network is robust to small input perturbations. You will learn the difference between verified, unproven, and violated results, and explore techniques to refine inconclusive verification.

Duration: ~20 minutes

What you will learn:

How verifyNetworkRobustness formally proves a network's output is stable within input bounds
The three possible verification outcomes: verified, unproven, violated
Two refinement techniques: input bisection and the α-CROWN algorithm
How to find adversarial counterexamples when robustness cannot be proven

Background: ACAS Xu Collision Avoidance

ACAS Xu (Airborne Collision Avoidance System for unmanned aircraft) uses neural networks to recommend steering advisories that prevent mid-air collisions. Each network takes 5 inputs describing the relative geometry and velocities of two aircraft:

ρ -- distance from ownship to intruder (ft)
θ -- angle to intruder relative to ownship heading direction (rad)
ψ -- heading angle of intruder relative to ownship heading direction (rad)
-- speed of ownship (ft/s)
-- speed of intruder (ft/s)

The network outputs one of 5 advisories: Clear-of-Conflict (no action), Weak Left/Right (gentle turn), or Strong Left/Right (urgent maneuver).

In this exercise, we analyze the "Left Abeam" scenario: two aircraft separated by 15,000 ft with the intruder directly to the left (

). The previous advisory was Clear-of-Conflict and the expected output is Weak Right.

Load the ACAS Xu Network

What we are doing: Loading the network corresponding to no vertical separation and previous advisory Clear-of-Conflict.

What to expect: The variable net should be a dlnetwork with 5 inputs and 5 outputs.

timeUntilLossOfVerticalSeparation = 1;
previousAdvisory = 1;
net = helper.loadACASNetwork(previousAdvisory, timeUntilLossOfVerticalSeparation);

Define the Nominal Input & Run Network Inference

What we are doing: Specifying the Left Abeam encounter scenario. Features are ordered as

. We set the distance to

ft.

X = [15000 pi/2 -0.4296 954.6 1050];
scores2label(predict(net, X), helper.classNames)
ans = categorical
     Weak Right 

Task 1: Verify Robustness with Small Perturbation

What to do: Add uncertainty of around

% to the velocities while keeping geometric inputs fixed. Then call verifyNetworkRobustness to prove that the network advises Weak Right (class 3) for every possible set of inputs between xLower and xUpper.

What to expect: With a small 3% perturbation, the verifier should return "verified".

dX = 0.03;
xLower = X .* [1 1 1 1-dX 1-dX];
xUpper = X .* [1 1 1 1+dX 1+dX];
 
xLower = dlarray(xLower, "BC");
xUpper = dlarray(xUpper, "BC");
 
label = 3; % Weak Right
 
% Hint: Use verifyNetworkRobustness with the network, bounds, and label
verifyNetworkRobustness(net, xLower, xUpper, label)
ans = categorical
     verified 

Explore an Unproven Result

What we are doing: Increasing the uncertainty to around

%. With a wider input range, the CROWN algorithm's overapproximation of nonlinear layers (ReLU) may produce output bounds that are too loose to separate the correct class from all others.

Why this matters: An "unproven" result does not mean the network is wrong -- it means the verification algorithm cannot determine the answer with the current precision.

What to expect: The result should be "unproven".

dX = 0.08;
xLower = dlarray(X .* [1 1 1 1-dX 1-dX], "BC");
xUpper = dlarray(X .* [1 1 1 1+dX 1+dX], "BC");
 
[result, detailedResult] = verifyNetworkRobustness(net, xLower, xUpper, label);
disp(result)
     unproven 
disp(table([helper.classNames;detailedResult],'VariableNames',"Robustness Verification per Class",'RowNames',["Class Name","Result"]))
                                                Robustness Verification per Class                              
                  _____________________________________________________________________________________________

    Class Name    Clear-of-Conflict  Weak Left          Weak Right         Strong Left        Strong Right     
    Result        unproven           verified           <undefined>        verified           unproven         

Insights into the detailed results: For the classes Weak Left and Strong Left, the function returns verified. This means that the network does not predict either of these classes anywhere within the input bounds. This makes sense, since the expected outcome is for the advisory to tell the aircraft to turn right. For the class Weak Right, the function returns <undefined>, because Weak Right is the expected label. For the classes Strong Right and Clear-of-Conflict, the function returns unproven. This suggests that increasing the range of velocities moves the overapproximating region calculated by the formal verification algorithm through the decision boundary between Strong Right and Weak Right, and Clear-of-Conflict and Weak Right.

Task 2: Refine with the α-CROWN Algorithm

What to do: The α-CROWN algorithm fine-tunes the polyhedral constraints to reduce overapproximations from ReLU activation functions. Re-run verification on the same

% bounds using Algorithm="alpha-crown".

What to expect: The α-CROWN algorithm should return "verified", proving robustness even for the wider perturbation.

% Hint: Same call as Task 1 but with an additional Algorithm name-value argument
verifyNetworkRobustness(net, xLower, xUpper, label, Algorithm="alpha-crown")
ans = categorical
     verified 

Compare Output Bounds: CROWN vs. α-CROWN

What we are doing: Computing the estimated output score bounds from both algorithms and plotting them side-by-side. estimateNetworkOutputBounds returns the lower and upper bound for each of the 5 output scores.

What to expect: The α-CROWN bounds (red) should be noticeably tighter than the CROWN bounds (blue).

[YLowerCROWN, YUpperCROWN] = estimateNetworkOutputBounds(net, xLower, xUpper);

[YLowerAlphaCROWN, YUpperAlphaCROWN] = estimateNetworkOutputBounds(net, xLower, xUpper, Algorithm="alpha-crown");

helper.displayBoundComparison(YLowerCROWN, YUpperCROWN, YLowerAlphaCROWN, YUpperAlphaCROWN)

A Genuinely Non-Robust Case

What we are doing: Increasing the uncertainty to around

%. At this scale, the input range covers physically different scenarios -- a very slow intruder may not pose a collision threat, causing the network to legitimately change its advisory.

What to expect: Neither algorithm can verify robustness because the network genuinely outputs different advisories within this range.

dX = 0.25;
xLower = dlarray(X .* [1 1 1 1-dX 1-dX], "BC");
xUpper = dlarray(X .* [1 1 1 1+dX 1+dX], "BC");
xUpper(4:5) = clip(xUpper(4:5), 0, 1200);
 
[result, detailedResult] = verifyNetworkRobustness(net, xLower, xUpper, label, Algorithm="alpha-crown");
disp(result)
     unproven 
disp(table([helper.classNames;detailedResult],'VariableNames',"Robustness Verification per Class",'RowNames',["Class Name","Result"]))
                                                Robustness Verification per Class                              
                  _____________________________________________________________________________________________

    Class Name    Clear-of-Conflict  Weak Left          Weak Right         Strong Left        Strong Right     
    Result        unproven           unproven           <undefined>        unproven           unproven         

Task 3: Find an Adversarial Example

What to do: Use findAdversarialExamples to search for an input within the bounds that causes the network to change its advisory. The function uses a random starting point, so run it in a loop until it finds a counterexample.

What to expect: An adversarial input where the network predicts Clear-of-Conflict instead of Weak Right. This makes physical sense: a much slower intruder does not pose a collision threat.

for ii = 1:100
    % Hint: findAdversarialExamples takes the network, bounds, and target label
    xAdversarial = findAdversarialExamples(net, xLower, xUpper, label);
    if ~isempty(xAdversarial)
        disp("Adversarial example found after " + ii + " attempts.")
        break
    end
end
Adversarial example found after 50 attempts.
scores2label(predict(net, xAdversarial), helper.classNames)
ans = categorical
     Clear-of-Conflict 

Summary

In this exercise, you learned three key verification outcomes:

Verified -- formal proof that the network output is stable within the input bounds
Unproven -- the algorithm cannot determine robustness; refinement (α-CROWN, bisection) may resolve it
Adversarial counterexample -- a concrete input where the network changes its prediction, proving non-robustness

In the next exercise, you will scale this analysis to verify the network's stability across its entire operating domain using an adaptive mesh approach.

Export Results

if ~isfolder("results"), mkdir("results"); end
export("Part2_LocalRobustness.m", fullfile("results", "Part2_LocalRobustness.html"));