DOCSEARCHbyAlgolia
Submit Docs

alpha-beta-CROWN

repository·main·Indexed 18 days ago

https://github.com/verified-intelligence/alpha-beta-crown

An efficient, scalable, and GPU-accelerated neural network verifier that uses linear bound propagation and branch-and-bound techniques to provide provable robustness guarantees. Winner of VNN-COMP 2021 through 2025, it supports large convolutional networks and includes a Python API and a CLI via abcrown.py. The package integrates BaB-Attack and supports cut extraction using CPLEX.

Tokens
11K
Snippets
34
Records
48
Agent score
64%

What's inside abcrown

  1. Overview of ResNet CIFAR-10 benchmark models

    main

    This repository provides ResNet benchmarks on CIFAR-10 to support verification of non-feedforward architectures. The models are trained using adversarial training with an $L_{\infty}$ perturbation $\epsilon=2/255$.

    Available Models

    • ResNet-2B: 2 residual blocks (5 convolutional layers + 2 linear layers).
    • ResNet-4B: 4 residual blocks (9 convolutional layers + 2 linear layers).
    • ResNet-18: Standard ResNet-18 architecture.

    Model Performance Summary

    Model# ReLUsClean acc.PGD acc. ($\epsilon=2/255$)PGD acc. ($\epsilon=1/255$)CROWN/DeepPoly verified acc. ($\epsilon=2/255$)CROWN/DeepPoly verified acc. ($\epsilon=1/255$)
    ResNet-2B624469.25%54.82%62.24%26.88%57.16%
    ResNet-4B1443677.20%61.41%69.75%0.24%23.28%

  2. Data preprocessing requirements for CIFAR-10 ResNet benchmarks

    main

    When using these ResNet models for verification, ensure your data follows these preprocessing specifications:

    • Normalization: Input images must be normalized using the mean and standard deviation computed from the CIFAR-10 training set.
    • Perturbation Budget: The perturbation budget is element-wise. For unnormalized images, use eps=2/255, and ensure values are clipped to the [0, 1] range.
    • Implementation Reference: A PyTorch example for loading data (including preprocessing and channel ordering) is provided in cifar_eval.py within this directory.

  3. Understand the α,β-CROWN input components

    main

    The verifier requires three primary input components:

    1. Model file: Can be a Pytorch model (requires the Pytorch definition/structure) or an ONNX model (only requires the .onnx file). Pytorch models are generally recommended.
    2. Data loader: Can be a built-in dataset (e.g., MNIST, CIFAR), a customized dataloader (Python function), or data loaded from a VNNLIB file.
    3. Specifications: Defines the robustness properties. Supported types include:
      • Lp norm (e.g., $L_2$ and $L_{\infty}$ norm perturbations).
      • Element-wise bounds (per-element ranges).
      • VNNLIB general specifications (input and output constraints defined in VNNLIB format).

  4. Define constraints using the IOConstraints DSL

    main

    The IOConstraints class is the recommended entry point for defining input and output regions. It supports several modes:

    • Expression DSL: Use boolean combinations of comparisons involving input_vars or output_vars.
    • Bounds + Clauses: Pass lower, upper, and clauses directly.
    • VNNLIB: Load an existing property via vnnlib_path="path/to/spec.vnnlib".

    DSL Syntax Cheat Sheet:

    GoalDSL Example
    1-D bound(x[0] > -0.1) & (x[0] < 0.1)
    Tensor L∞ box(x > lower_tensor) & (x < upper_tensor)
    Logit ordering(y[0] > y[1]) & (y[0] > y[2])
    Linear inequalityy[0] - y[1] > 0
    OR between specs(y[0] > 0) | (y[1] > 0)
    Pin to a pointpoint = torch.tensor([1.0]); (x > point) & (x < point)

    Important Constraints Rules:

    • For output constraints, only strict specifications are accepted (<, >). Non-strict operators (>=, <=) are not allowed for output constraints.
    • Comparisons can involve input_vars or output_vars against scalars, lists, NumPy arrays, or torch tensors.

  5. Interpret CPLEX cut results

    main

    When analyzing the output of the cut extraction process, you can use either the human-readable .mps file or the efficient binary files.

    Using the .mps file

    In the generated output_filename.mps, cuts are identified by constraints starting with specific letters such as r, i, m, q, or L. Coefficients are stored in a sparse format. For example, searching for m1038 will show all coefficients for the 1038th cut.

    Using binary files

    The output_filename.indx and output_filename.cuts files contain the same information as the .mps file but are optimized for performance and are much smaller (e.g., ~20MB for 300K lines). These are the preferred files for programmatic handling within the verifier.

  6. Verify using VNNLIB specifications

    main

    VNNLIB files can contain both data and specifications. When using VNNLIB:

    1. Pytorch Model: Set model: path to the Pytorch model file, model: name to the definition in model_defs.py, and provide model: input_shape. Use --vnnlib_path to specify the VNNLIB file.
    2. ONNX Model: Set model: onnx_path to the ONNX file and specification: vnnlib_path to the VNNLIB file.
    3. Batch Verification: To verify many specifications efficiently, list all VNNLIB filenames in a .csv file (one per line) and point to it in the config to avoid reloading the model repeatedly.

    Example (Single VNNLIB with Pytorch):

    python abcrown.py --config exp_configs/tutorial_examples/pytorch_model_with_one_vnnlib.yaml

  7. Configure element-wise bounds perturbation

    main

    Element-wise bounds allow specifying different ranges for each input dimension (similar to $L_{\infty}$ but with per-element flexibility).

    To use this:

    1. Set specification: type to bound in the configuration file.
    2. Ensure your dataloader returns the per-element lower and upper bounds.

    Example Command:

    python abcrown.py --config exp_configs/tutorial_examples/custom_cifar_data_element_bound.yaml

  8. Configure Gurobi and CPLEX for benchmarks

    main

    Certain VNN-COMP benchmarks require external solvers:

    Gurobi

    Required for: eran, mnistfc, marabou-cifar10, verivital, safenlp, malbeware, and sat_relu. Gurobi is installed via the Conda environment setup, but you must activate it using the grbgetkey command with a valid license.

    CPLEX

    Required for: oval21 and oval22.

    1. Download IBM CPLEX (version >= 22.1.1) from the IBM community site.
    2. Run the installer non-interactively using a response.txt file.
    3. Build the C++ interface for CPLEX. Ensure build-essential (with g++ >= 8.0) is installed.
    4. If CPLEX is installed in a non-default location, update CPX_PATH in complete_verifier/cuts/CPLEX_cuts/Makefile before running make.
    # Install IBM CPLEX >= 22.1.1
chmod +x cplex_studio2211.linux_x86_64.bin
cat > response.txt <<EOF
INSTALLER_UI=silent
LICENSE_ACCEPTED=true
EOF
sudo ./cplex_studio2211.linux_x86_64.bin -f response.txt

# Build the C++ code for CPLEX interface
sudo apt install build-essential
make -C complete_verifier/cuts/CPLEX_cuts/

  9. Install α,β-CROWN using uv

    main

    α,β-CROWN requires Python 3.11 and PyTorch 2.11. It is recommended to use uv for installation. Note that CUDA >= 12.6 is required.

    1. Install uv:
    curl -LsSf https://astral.sh/uv/install.sh | sh
    1. Clone the repository recursively to include the auto_LiRPA submodule:
    git clone --recursive https://github.com/Verified-Intelligence/alpha-beta-CROWN.git
cd alpha-beta-CROWN
    1. Create the environment and install dependencies:
    uv sync
source .venv/bin/activate
    # Install uv.
curl -LsSf https://astral.sh/uv/install.sh | sh

# Clone the repository
git clone --recursive https://github.com/Verified-Intelligence/alpha-beta-CROWN.git
cd alpha-beta-CROWN

# Sync environment
uv sync
source .venv/bin/activate

  10. Download and prepare CROWN-IBP models

    main

    To use the pre-trained models for the crown-ibp module, you must download the compressed archives and rename the files to match the expected local naming convention. This process involves downloading CIFAR and MNIST models from various sources (including huan-zhang.com and ucla.edu) and extracting them.

    Note that these models are sourced from the original CROWN-IBP, auto_LiRPA, and IBP with short warmup repositories but have been renamed for compatibility with this project.

    # Download and extract CIFAR 2px model
wget https://download.huan-zhang.com/models/crown-ibp/crown_ibp_cifar_2px.tar.gz
tar xf crown_ibp_cifar_2px.tar.gz

# Download and prepare DM-Large models
wget https://download.huan-zhang.com/models/crown-ibp/models_crown-ibp_dm-large.tar.gz
tar xf models_crown-ibp_dm-large.tar.gz
mv models_crown-ibp_dm-large/cifar_dm-large_2_255/IBP_large_best.pth cifar_model_dm_large_2px.pth
mv models_crown-ibp_dm-large/cifar_dm-large_8_255/IBP_large_best.pth cifar_model_dm_large_8px.pth
mv models_crown-ibp_dm-large/mnist_dm-large_0.2/IBP_large_best.pth mnist_model_dm_large_0.2.pth
mv models_crown-ibp_dm-large/mnist_dm-large_0.4/IBP_large_best.pth mnist_model_dm_large_0.4.pth

# Download specific Batch Normalization (BN) models
wget -O cifar_model_dm_large_bn_8px.pth http://web.cs.ucla.edu/~zshi/files/auto_LiRPA/cifar/cnn_7layer_bn_cifar
wget http://d.huan-zhang.com/storage/models/cifar_model_dm_large_bn_full_8px.pth

  11. Run VNN-COMP 2022 benchmarks in batch mode

    main

    To evaluate VNN-COMP 2022 benchmarks, use a CSV file where each line contains: path to ONNX file, path to VNNLIB file, and timeout threshold.

    Setup Steps:

    1. Clone the benchmark repository to the same parent folder as alpha-beta-CROWN.
    2. Run the setup script in the benchmark folder to extract files and download models.

    Execution: Set general: root_path in your config to the benchmark directory.

    # Assuming vnncomp2022_benchmarks is in the parent directory
python abcrown.py --config exp_configs/vnncomp22/tinyimagenet_2022.yaml
    python abcrown.py --config exp_configs/vnncomp22/tinyimagenet_2022.yaml

  12. Load a customized Pytorch model

    main

    To use a model defined in your own Python source file, use the Customized primitive in the model: name section of your configuration file.

    Example Configuration Pattern: If your model is defined as simple_conv_model() in custom/custom_model_data.py, set the config as follows:

    model:
  name: Customized("custom_model_data", "simple_conv_model", in_channel=3, out_dim=10)

    The verifier will call the specified function with the provided arguments to obtain the model definition.