networkVerificationOptions

Options for network robustness verification for ONNX and PyTorch networks

Since R2026a

expand all in page

    Description

    Add-On Required: This feature requires the Deep Learning Toolbox Interface for alpha-beta-CROWN Verifier add-on.

    Use a NetworkVerificationOptions object to set options for the α-β-CROWN verifier. You can use the NetworkVerificationOptions object as input to the verifyNetworkRobustness and findAdversarialExamples functions with ONNX™ or PyTorch® networks.

    α-β-CROWN is an algorithm for neural network verification. The algorithm efficiently propagates input bounds through the neural network to produce bounds on the output. You can use the output bounds to verify properties of a neural network, such as the robustness of the network to input perturbations.

    Creation

    Create a NetworkVerificationOptions object using the networkVerificationOptions function.

    Syntax

    options = networkVerificationOptions
    options = networkVerificationOptions(Property=Value)

    Description

    options = networkVerificationOptions returns verification options for use with the Deep Learning Toolbox™ Interface for alpha-beta-CROWN Verifier support package. To use the interface to verify the robustness of a classification neural network, use the options object as input to the verifyNetworkRobustness function. To use the interface to find adversarial examples of a classification neural network, use the options object as input to the findAdversarialExamples function.

    options = networkVerificationOptions(Property=Value) returns additional options specified by one or more name-value arguments.

    example

    Properties

    The following properties can be used in MATLAB to interface with the alpha-beta-CROWN verifier using the Deep Learning Toolbox Interface for alpha-beta-CROWN Verifier support package. To learn more about these properties and example configurations, see the alpha-beta-CROWN Github repository.

    Note

    The default values documented here are used internally at runtime and are not visible at the time of object creation. The default values are dependent on the specified Algorithm in verifyNetworkRobustness. For more information see, Algorithm-Specific Internal Defaults.

    General Options

    FieldData TypeDescription
    GeneralSeedpositive integer scalarRandom seed
    GeneralConvModecharacter vector or string scalar

    Convolution mode during bound propagation. Specified as

    • "patches" (default) which is efficient, but may not support all architectures

    • "matrix" which is slow, but supports more architectures

    GeneralDeterministiclogical

    Specified as

    • 1 (true) to use deterministic algorithms with slower performance but better reproducibility

    • 0 (false) (default) otherwise

    GeneralLossReductionFunccharacter vector or string scalar

    Reduction function applied to reduce bounds into a scalar when batch size is not 1. Specified as

    • "sum" (default)

    • "min"

    • "max"

    • "mean"

    GeneralSparseAlphalogical

    Specified as

    • 1 (true) (default) to enable sparse α

    • 0 (false) otherwise

    GeneralSparseIntermlogical

    Specified as

    • 1 (true) (default) to enable sparse intermediate bounds

    • 0 (false) otherwise

    GeneralCompleteVerifiercharacter vector or string scalar

    Complete verification verifier. Specified as

    • "bab" which runs branch and bound

    • "skip" which does not run branch and bound

    See Algorithm-Specific Internal Defaults for default behavior.

    GeneralEnableIncompleteVerificationlogical

    Specified as

    • 1 (true) (default)

    • 0 (false)

    Solver Options

    FieldData TypeDescription
    SolverBatchSizepositive integer scalarBatch size in bound solver that controls number of parallel splits. Default value is 64.
    SolverEarlyStopPatiencepositive integer scalarNumber of iterations before early stopping if no improvement is observed. Default value is 10.
    SolverStartSaveBestpositive numeric scalarStart to save best optimized bounds when i > int(iteration*SolverStartSaveBest). Early iterations are skipped for better efficiency. Default value is 0.5.
    SolverBoundPropMethodcharacter vector or string scalar

    Bound propagation algorithm used for incomplete verification and input split based branch and bound. Specified as

    • "alpha-crown"

    • "crown"

    • "forward"

    • "forward+crown"

    • "alpha-forward"

    • "crown-ibp"

    • "init-crown"

    • "ibp"

    This algorithm is run before branch and bound. See Algorithm-Specific Internal Defaults for default behavior.

    SolverPruneAfterCrownlogical

    Specified as

    • 1 (true) to prune verified labels after the CROWN pass but before the α-CROWN pass

    • 0 (false) (default) otherwise

    SolverCrownBatchSizepositive integer scalarBatch size in batched CROWN. Default is value is 109.
    SolverAlphaCrownLrAlphapositive numeric scalarLearning rate for the optimizable parameter α in α -CROWN bound. Default value is 0.1.
    SolverAlphaCrownIterationpositive integer scalarNumber of iterations for α in α -CROWN incomplete verifier. Default value is 100.
    SolverAlphaCrownShareAlphaslogical

    Specified as

    • 1 (true) to share some α variables to save memory at the cost of looser bounds.

    • 0 (false) (default) otherwise

    SolverAlphaCrownLrDecaypositive numeric scalarLearning rate decay factor during α -CROWN optimization. Default value is 0.98. Use a larger value such as 0.99 when increasing number of iterations.
    SolverAlphaCrownDisableOptimizationstring arrayA list of the names of operators which have bound optimization disabled for improved speed and efficiency. E.g. ["Exp","MaxPool"]
    SolverBetaCrownLrAlphapositive numeric scalarLearning rate for optimizing parameter α during branch and bound. Default value is 0.01.
    SolverBetaCrownLrBetapositive numeric scalarLearning rate for optimizing parameter β during branch and bound. Default value is 0.05.
    SolverBetaCrownLrDecaypositive numeric scalarLearning rate decay factor during β -CROWN optimization. Default value is 0.98. Use a larger value such as 0.99 when increasing number of iterations.
    SolverBetaCrownIterationpositive integer scalarNumber of iterations for optimizing α and β during branch and bound. Default value is 50.
    SolverMultiClassLabelBatchSizepositive integer scalarMaximum target labels to handle in α -CROWN, constrained by the GPU memory limit. Default value is 32.

    Branch and Bound Options

    FieldData TypeDescription
    BabInitialMaxDomainspositive integer scalarNumber of domains that can be added to the domain list at the same time before branch and bound. For multiclass problems this number can be as large as the number of labels. Default value is 1.
    BabBranchingMethodcharacter vector or string scalar

    Branching heuristic. Specified as

    • "kfsb" (default) which is balanced in accuracy and speed

    • "babsr" which is fast, but less accurate

    • "fsb" which is slow, but most accurate

    • "kfsb-intercept-only" which is faster, but may lead to worse branching

    • "sb" which is fast, with smart branching that relies on intermediate CROWN results

    BabBranchingCandidatespositive integer scalarNumber of candidates to consider when using "fsb" or "kfsb". More candidates lead to slower but better branching. Default value is 3.
    BabBranchingReduceOpcharacter vector or string scalar

    Reduction operation to compute branching scores from two sides of a branch. Specified as

    • "min" (default)

    • "max" which can work better on some models

    BabBranchingNonlinearSplitMethodcharacter vector or string scalar

    Branching heuristic. Specified as

    • "shortcut" (default) which is balanced in accuracy and speed

    • "babsr-like" which is fast, but less accurate

    BabBranchingNonlinearSplitNumBranchespositive integer scalarNumber of branches for nonlinear branching. Default value is 2.
    BabBranchingNonlinearSplitFilterlogical

    Specified as

    • 1 (true) to enable KFSB-like filtering in general nonlinear branching.

    • 0 (false) (default) otherwise

    BabBranchingInputSplitEnablelogical

    Specified as

    • 1 (true) to branch on input domain rather than unstable neurons.

    • 0 (false) (default) otherwise

    BabBranchingInputSplitEnhancedBoundPropMethodcharacter vector or string scalar

    Bound propagation method if a problem cannot be verified after BabBranchingInputSplitEnhancedBoundPatience. Specified as

    • "alpha-crown" (default)

    • "crown"

    • "forward+crown"

    • "crown-ibp"

    BabBranchingInputSplitEnhancedBranchingMethodcharacter vector or string scalar

    Branching method if a problem cannot be verified after BabBranchingInputSplitEnhancedBoundPatience. Specified as

    • "naive" (default)

    • "sb"

    BabBranchingInputSplitEnhancedBoundPatiencepositive numeric scalarTime in seconds that will use an enhanced bound propagation method (e.g. α-CROWN) to bound input split subdomains. Default value is 108 seconds.
    BabBranchingInputSplitAttackPatiencepositive numeric scalarTime in seconds after which to start PGD attack to find adversarial examples during input split. Default value is 108 seconds.
    BabBranchingInputSplitSbCoeffThreshpositive numeric scalarThreshold at which to clamp values of coefficient matrix for sb (split-by-score) branching heuristic.

    Attack Options

    FieldData TypeDescription
    AttackPgdOrdercharacter vector or string scalar

    Projected Gradient Descent (PGD) attack order. Specified as

    • "before" (default)

    • "after"

    • "middle"

    • "input_bab"

    • "skip"

    AttackPgdStepspositive integer scalarSteps of PGD attack. Default value is 100.
    AttackPgdRestartspositive integer scalarNumber of random PGD restarts. Default value is 64.
    AttackPgdBatchSizepositive integer scalarBatch size for number of restarts in PGD. Default value is 108.
    AttackPgdEarlyStoplogical

    Specified as

    • 1 (true) (default) to enable early stop PDG when an adversarial example is found

    • 0 (false) otherwise

    AttackPgdLrDecaypositive numeric scalarLearning rate decay factor used in PGD attack. Default value is 0.99.
    AttackPgdAlphapositive numeric scalar

    Step size of PGD attack. Default value is (XUpper - Xlower)/8.

    AttackPgdAlphaScalelogical

    Specified as

    • 1 (true) to scale PGD alpha according to lower and upper bounds of data input.

    • 0 (false) (default) otherwise

    AttackPgdLossModecharacter vector or string scalar

    Loss mode for choosing best delta. Specified as

    • "null" (default)

    • "hinge"

    • "sum"

    AttackAttackModecharacter vector or string scalar

    Attack algorithm. Specified as

    • "PGD" (default) for vanilla PGD

    • "diversed_PGD" for PGD with diversified output

    • "boundary"

    • "diversed_GAMA_PGD" for PGD with diversified output and GAMA loss

    AttackGamaLambdapositive numeric scalarRegularization parameter in GAMA attack. Default value is 10.
    AttackGamaDecaypositive numeric scalarDecay of regularization parameter in GAMA attack. Default value is 0.9.

    Examples

    collapse all

    This example uses:

    Open Live Script

    Create a network verification options object to specify custom properties for formal verification.

    options = networkVerificationOptions(...
    GeneralEnableIncompleteVerification=false,...
    GeneralLossReductionFunc="min",...   
    SolverBatchSize=1000,...
    SolverBoundPropMethod="crown",...
    SolverBetaCrownIteration=10,...
    SolverAlphaCrownIteration=10,...
    SolverAlphaCrownShareAlphas=true,...
    BabBranchingMethod="naive",...
    BabBranchingCandidates=3,...
    BabBranchingInputSplitEnable=true,...
    BabBranchingInputSplitEnhancedBranchingMethod="sb",...
BabBranchingInputSplitEnhancedBoundPropMethod="alpha-crown");

    This example uses:

    Open Live Script

    Load a pretrained classification network. This network is a PyTorch® model that has been trained to predict the class label of images of handwritten digits.

    modelfile = "digitsClassificationConvolutionNet.pt";

    Load the test data and select the first 20 images.

    [XTest,TTest] = digitTest4DArrayData;
X = XTest(:,:,:,1:20);
labels = TTest(1:20);

    Verify the network robustness to an input perturbation between –0.01 and 0.01 for each pixel. Create lower and upper bounds for the input.

    perturbation = 0.01;
XLower = X - perturbation;
XUpper = X + perturbation;

    Create a custom network verification options object to use the "crown" algorithm with 100 projected gradient descent (PGD) restarts.

    options = networkVerificationOptions(GeneralCompleteVerifier="skip",...
    SolverBoundPropMethod="crown",...
    AttackPgdRestarts=100);

    Verify the network robustness for each test image with the created network verification options. Specify the input data permutation from MATLAB to Python® dimension ordering as [4 3 1 2] and number of classes as 10.

    numClasses = 10;
result = verifyNetworkRobustness(modelfile,XLower,XUpper,labels,numClasses, ...
        Algorithm=options, ...
        InputDataPermutation=[4 3 1 2]);
    Warning: Starting and configuring the Python interpreter for the alpha-beta-CROWN verifier. This may take a few minutes.

    summary(result)
    result: 20×1 categorical

     verified          4 
     violated         13 
     unproven          3 
     <undefined>       0

    Algorithms

    expand all

    References

    [1] Zhang, Huan, Tsui-Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh, and Luca Daniel. “Efficient Neural Network Robustness Certification with General Activation Functions.” arXiv, 2018. https://doi.org/10.48550/ARXIV.1811.00866.

    [2] Xu, Kaidi, Huan Zhang, Shiqi Wang, Yihan Wang, Suman Jana, Xue Lin, and Cho-Jui Hsieh. “Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers.” arXiv, 2020. https://doi.org/10.48550/ARXIV.2011.13824.

    [3] Wang, Shiqi, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J. Zico Kolter. "Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification." Advances in neural information processing systems 34 (2021)

    Version History

    Introduced in R2026a

    See Also

    |

    Topics

    External Websites