### Install alpha-beta-CROWN

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/docs/abcrown_api.md

Commands to clone the repository and install the package.

```bash
git clone --recursive https://github.com/Verified-Intelligence/alpha-beta-CROWN.git
cd alpha-beta-CROWN
```

```bash
pip install .
```

--------------------------------

### Install α,β-CROWN using pip

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/README.md

Install the α,β-CROWN library using pip, after ensuring a compatible PyTorch version is installed. This method is suitable for adding the verifier to an existing environment.

```bash
(cd auto_LiRPA; pip install -e .)
pip install -r complete_verifier/requirements.txt
```

--------------------------------

### Setup Conda Environment for α,β-CROWN

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/README.md

Create and activate a conda environment named 'alpha-beta-crown' using the provided environment.yaml file. Ensure CUDA is installed.

```bash
# Remove the old environment, if necessary.
conda deactivate; conda env remove --name alpha-beta-crown
# install all dependents into the alpha-beta-crown environment
conda env create -f complete_verifier/environment.yaml --name alpha-beta-crown
```

--------------------------------

### Initialize and Solve Verification

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/docs/abcrown_api.md

Example of setting up a verification specification using symbolic variables and executing the solver.

```python
from abcrown import (
    ABCrownSolver, VerificationSpec, ConfigBuilder, input_vars, output_vars
)

# Construct spec with L-infinity box and logit ordering
x = input_vars((1, 28, 28))
y = output_vars(3)
input_constraint = (x >= base - eps) & (x <= base + eps)
output_constraint = (y[0] > y[1]) & (y[0] > y[2])

spec = VerificationSpec.build_spec(
    input_vars=x,
    output_vars=y,
    input_constraint=input_constraint,
    output_constraint=output_constraint,
)
# Config (defaults)
config = ConfigBuilder.from_defaults()

# Solve
solver = ABCrownSolver(spec, model, config=config)
result = solver.solve()
print(result.status, result.success)
```

--------------------------------

### Install BaB-Attack and Dependencies

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/exp_configs/bab_attack/README.md

Clone the alpha-beta-CROWN repository and create a conda environment to install all necessary dependencies for BaB-Attack.

```bash
git clone https://github.com/huanzhang12/alpha-beta-CROWN
# Remove the old environment, if necessary.
conda deactivate; conda env remove --name bab-attack
conda env create -f complete_verifier/environment.yaml --name bab-attack  # install all dependents into the bab-attack environment
conda activate bab-attack  # activate the environment
```

--------------------------------

### Install CPLEX via Shell

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/cuts/CPLEX_cuts/README.md

Commands to download, set permissions, and execute the CPLEX installer.

```bash
wget http://d.huan-zhang.com/storage/programs/cplex_studio2211.linux_x86_64.bin
chmod +x cplex_studio2211.linux_x86_64.bin
./cplex_studio2211.linux_x86_64.bin
```

--------------------------------

### Run Robustness Verification with Configuration File

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/README.md

Execute the α,β-CROWN verifier using the command-line interface with a specified configuration file. This example demonstrates running robustness verification on a CIFAR-10 ResNet network.

```bash
conda activate alpha-beta-crown  # activate the conda environment
cd complete_verifier
python abcrown.py --config exp_configs/tutorial_examples/cifar_resnet_2b.yaml
```

--------------------------------

### Run Basic Verification Example

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/docs/abcrown_usage.md

Execute a basic verification task using a PyTorch model, Linf norm specification, and a built-in dataset. The model name is specified in the config file, and dataset normalization is handled automatically.

```bash
python abcrown.py --config exp_configs/tutorial_examples/basic.yaml
```

--------------------------------

### Install CPLEX for Benchmarks

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/docs/vnn_comp.md

Installs IBM CPLEX version 22.1.1 or later using a silent installation process and builds the C++ interface. Requires sudo privileges and a modern g++ compiler.

```bash
# Install IBM CPLEX >= 22.1.1
# Download from https://community.ibm.com/community/user/datascience/blogs/xavier-nodet1/2020/07/09/cplex-free-for-students
chmod +x cplex_studio2211.linux_x86_64.bin  # Any version >= 22.1.0 should work. Change executable name here.
# You can directly run the installer: ./cplex_studio2211.linux_x86_64.bin; the response.txt created below is for non-interactive installation.
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. Assuming we are still inside the alpha-beta-CROWN folder.
sudo apt install build-essential  # A modern g++ (>=8.0) is required to compile the code.
# Change CPX_PATH in complete_verifier/cuts/CPLEX_cuts/Makefile if you installed CPLEX to a non-default location, like inside your home folder.
make -C complete_verifier/cuts/CPLEX_cuts/
```

--------------------------------

### Clone and Install α,β-CROWN Verifier

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/docs/vnn_comp.md

Clones the verifier repository, sets up a conda environment with specified package versions, and exports the Python path. Ensure you have conda installed and activated.

```bash
# Clone verifier code.
git clone --recursive https://github.com/Verified-Intelligence/alpha-beta-CROWN.git
cd alpha-beta-CROWN
# Remove the old environment, if necessary.
conda deactivate; conda env remove --name alpha-beta-crown
# Create conda environment with fixed package versions.
conda env create -f complete_verifier/environment.yaml --name alpha-beta-crown
conda activate alpha-beta-crown

# Get python installation path. You will need to use this path in later steps.
export VNNCOMP_PYTHON_PATH=$(python -c 'import os; print(os.path.dirname(os.path.realpath("/proc/self/exe")))')
echo "Please run \"export VNNCOMP_PYTHON_PATH=${VNNCOMP_PYTHON_PATH}\" before you run vnncomp scripts."
```

--------------------------------

### Verify with Custom Box Data Example

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/docs/abcrown_usage.md

This configuration is for generating synthetic data for a toy ReLU model using a completely customized dataloader.

```bash
python abcrown.py --config exp_configs/tutorial_examples/custom_box_data_example.yaml
```

--------------------------------

### Get Default Configuration

Source: https://context7.com/verified-intelligence/alpha-beta-crown/llms.txt

Retrieve the default configuration dictionary for the verifier using `default_config()`. This can be a starting point for custom configurations.

```python
from abcrown import ConfigBuilder, default_config

# Get default configuration as dictionary
config_dict = default_config()
```

--------------------------------

### Generate MPS File for CPLEX

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/cuts/CPLEX_cuts/README.md

Example command to generate an MPS file using the alpha-beta-crown configuration.

```bash
ALPHA_BETA_CROWN_MIP_DEBUG=1 python abcrown.py --config exp_configs/vnncomp21/oval21.yaml --select_instance 5
```

--------------------------------

### Run VNN-COMP Benchmarks with Scripts

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/docs/vnn_comp.md

Executes VNN-COMP benchmarks using provided scripts, requiring the VNNCOMP_PYTHON_PATH environment variable to be set correctly. This example runs the 'vit' benchmark.

```bash
# Please set this environment variable properly, see above instructions
export VNNCOMP_PYTHON_PATH=${HOME}/miniconda3/envs/alpha-beta-crown/bin
# Please check the path to the alpha-beta-CROWN repository and change it accordingly
./run_all_categories.sh v1 ${HOME}/alpha-beta-CROWN/vnncomp_scripts $(pwd) results_vit.csv counterexamples_vit "vit" all  # Example to run the vit benchmark
```

--------------------------------

### VNNLIB Constraint Analysis Example

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/docs/read_vnnlib.md

Demonstrates how constraints on X and Y variables are analyzed and reflected in output ranges. This is useful for understanding how assertions affect variable bounds in verification.

```python
(assert (or (and (<= X_0 0.66) (>= Y_2 Y_3) (<= Y_4 0.1))
            (and (<= X_1 3) (>= X_2 0.2) (<= Y_3 1.0))
        )
)
```

```python
[
    (
        [[0.6, 0.66], [-0.5, 0.5], [-0.5, 0.5], [0.45, 0.5], [-0.5, -0.45]], 
        [(
            array([[ 0.,  0., -1.,  1.,  0.],[ 0.,  0.,  0.,  0.,  1.]]), 
            array([0. , 0.1])
        )]
    ), 
    (
        [[0.6, 0.679857769], [-0.5, 0.5], [0.2, 0.5], [0.45, 0.5], [-0.5, -0.45]], 
        [(
            array([[0., 0., 0., 1., 0.]]), 
            array([1.])
        )]
    )
]
```

--------------------------------

### VNNLIB Output Explanation Example

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/docs/read_vnnlib.md

Explains the output of VNNLIB assertions, showing how matrix multiplications with variable vectors translate to inequalities. This helps in understanding the derived constraints.

```text
X_range:
(List[X_lower_bound, X_higher_bound]): [[-0.295233916, -0.212261512], [-0.063661977, -0.022281692], [-0.499999896, -0.498408347], [-0.5, -0.454545455], [-0.5, -0.375]], which indicates -0.295233916 <= X_0 <= -0.212261512, -0.063661977 <= X_1 <= -0.022281692, ... and so on

(Note: If one of the following is True, then assertion returns True)
mat: array([[ 0.,  1.,  0.,  0.,  0.], [ 0.,  0., -1.,  1.,  0.],[ 0.,  0.,  0.,  0.,  1.]])
rhs: array([0.5, 0. , 0.1])
--> mat * y <= rhs
So, Y_1 <= 0.5, -Y_2 + Y_3 <= 0, Y_4 <= 0.1
Or, Y_1 <= 0.5, Y_2 >= Y_3, Y_4 <= 0.1

    OR

mat: array([[-1.,  0.,  1.,  0.,  0.],[ 0.,  0.,  0.,  1.,  0.]]), 
rhs: array([0., 1.])
--> mat * y <= rhs
So, -Y_0 + Y_2 <= 0, Y_3 <= 1.0
Or, Y_2 <= Y_0, Y_3 <= 1.0

    OR

mat: array([[ 0.,  1.,  0.,  0.,  0.], [ 0.,  0., -1.,  0.,  0.]]), 
rhs: array([ 1., -2.])
--> mat * y <= rhs
So, Y_1 <= 1, -Y_2 <= -2
Or, Y_1 <= 1, Y_2 >= 2
```

--------------------------------

### Scalar Safe vs Unsafe Toy Example

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/docs/abcrown_api.md

A simple example demonstrating verification for a scalar function. It checks if the output of a residual function meets a specific condition.

```python
class SimpleResidual(torch.nn.Module):
    def forward(self, x):
        return 1.5 - x

def run_scalar_demo(x_value):
    x = input_vars(1); y = output_vars(1)
    point = torch.tensor([x_value])
    spec = VerificationSpec.build_spec(
        x,
        y,
        input_constraint=(x >= point) & (x <= point),
        output_constraint=(y[0] > 0.0),
    )
    result = ABCrownSolver(spec, SimpleResidual()).solve()
    print(f"x={x_value} -> {result.status}")
```

--------------------------------

### Clone VNN-COMP Benchmarks

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/docs/vnn_comp.md

Clones the repositories for VNN-COMP benchmarks from 2021 to 2025 and executes their setup scripts to download necessary files.

```bash
git clone https://github.com/VNN-COMP/vnncomp2021.git

git clone https://github.com/VNN-COMP/vnncomp2022_benchmarks.git
# Unzip and download necessary files
(cd vnncomp2022_benchmarks; ./setup.sh)

git clone https://github.com/VNN-COMP/vnncomp2023_benchmarks.git
# Unzip and download necessary files
(cd vnncomp2023_benchmarks; ./setup.sh)

git clone https://github.com/VNN-COMP/vnncomp2024_benchmarks.git
# Unzip and download necessary files
(cd vnncomp2024_benchmarks; ./setup.sh)

git clone https://github.com/VNN-COMP/vnncomp2025_benchmarks.git
# Unzip and download necessary files
(cd vnncomp2025_benchmarks; ./setup.sh)
```

--------------------------------

### Run Verification with Custom Model Loader

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/docs/abcrown_usage.md

Perform verification using a PyTorch model defined in a custom Python file. This example demonstrates loading a model via the 'Customized' primitive, specifying the model's definition file and function name.

```bash
python abcrown.py --config exp_configs/tutorial_examples/custom_model.yaml
```

--------------------------------

### Verify PyTorch Model with Single VNNLIB Specification

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/docs/abcrown_usage.md

This example verifies a PyTorch model using a single VNNLIB file. Ensure the ONNX model and VNNLIB config file are accessible by cloning the vnncomp2021 repository.

```bash
# To get the ONNX model and VNNLIB config file, first clone the vnncomp2021 repository, put it at the same folder as the alpha-beta-CROWN repo folder.
# git clone https://github.com/stanleybak/vnncomp2021 ../../vnncomp2021
python abcrown.py --config exp_configs/tutorial_examples/pytorch_model_with_one_vnnlib.yaml
```

--------------------------------

### Verify Linf Norm with Custom Dataloader for PyTorch Model

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/docs/abcrown_usage.md

This example demonstrates using a customized dataloader to load your own datasets, such as CIFAR10, with a PyTorch model. The dataloader function should return values compatible with PyTorch.

```bash
python abcrown.py --config exp_configs/tutorial_examples/custom_cifar_data_example.yaml
```

--------------------------------

### Verify ONNX Model with Linf Norm on Built-in Dataset

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/docs/abcrown_usage.md

This example shows how to verify an ONNX model on a built-in dataset like CIFAR-10 with Linf norm perturbation. Provide the path to the ONNX model using 'model: onnx_path'.

```bash
# To get the ONNX model and VNNLIB config file, first clone the vnncomp2021 repository, put it at the same folder as the alpha-beta-CROWN repo folder.
# git clone https://github.com/VNN-COMP/vnncomp2021 ../../vnncomp2021
python abcrown.py --config exp_configs/tutorial_examples/onnx_with_built-in_dataset_linf_bound.yaml
```

--------------------------------

### VNNLIB Constraint Explanation Example

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/docs/read_vnnlib.md

Illustrates how assertions in VNNLIB files can constrain the original ranges of variables. It shows modifications to X ranges based on assertions in different clauses.

```python
X_range:
[[0.6, 0.679857769], [-0.5, 0.5], [-0.5, 0.5], [0.45, 0.5], [-0.5, -0.45]]

However, in the first clause, X_0 is asserted to be <= 0.66. We, thus, modify X_0_range from [0.6, 0.679857769] to [0.6, 0.66]. Similarly, in the second clause, X_2 is asserted to be >= 0.2. We, thus, modify X_2_range from [-0.5, 0.5] to [-0.2, 0.5]. Note that, though X_1 is asserted to be <= 3, we do not modify its range since the original range better constrains X_1 value.

Y value assertion runs the same as in littleGeneral.vnnlib.
```

--------------------------------

### Configure Alpha-Beta-CROWN demo

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/examples_abcrown/demo.ipynb

Initializes the configuration object using default settings.

```python
# Step 3: config (defaults)
def build_demo_config():
    """Config for the image classification spec."""
    return (
        ConfigBuilder.from_defaults()
    )
```

--------------------------------

### Configure Solver Options

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/docs/abcrown_api.md

Demonstrates how to use ConfigBuilder to set and update solver configurations.

```python
cfg = (
    ConfigBuilder.from_defaults()
    .set(general__device="cpu")
    .set(attack__pgd_order="skip")
    ()
)
```

```python
builder = ConfigBuilder.from_defaults()
builder.set(attack__pgd_order="skip")              # simple path override
builder.update({"attack": {"pgd_order": "skip"}})  # deep-merge mapping
```

--------------------------------

### Import Alpha-Beta-CROWN modules

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/examples_abcrown/demo.ipynb

Required imports for initializing the solver, configuration, and verification specifications.

```python
import torch

from abcrown import (
    ABCrownSolver,
    ConfigBuilder,
    VerificationSpec,
    input_vars,
    output_vars,
)
```

--------------------------------

### Run benchmarks using configuration files

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/docs/vnn_comp.md

Executes specific benchmark properties using a YAML configuration file to reduce overhead.

```bash
cd alpha-beta-CROWN/complete_verifier
python abcrown.py --config exp_configs/vnncomp22/cifar100_small_2022.yaml
```

--------------------------------

### Access verification results and statistics

Source: https://context7.com/verified-intelligence/alpha-beta-crown/llms.txt

Extracts the verification status, timing statistics, and adversarial examples from the result object returned by the verifier.

```python
# Access result fields
print(f"Status: {result.status}")
# Possible values: 'verified', 'safe-incomplete', 'unsafe-pgd', 'unsafe-bab', 'unknown'

print(f"Success: {result.success}")
# True if verification completed successfully (property proven or violated)

# Statistics
stats = result.stats
print(f"Total time: {stats['elapsed']:.2f} seconds")
print(f"PGD attack stats: {stats.get('pgd')}")
print(f"BaB iterations: {stats.get('bab')}")

# Access attack results if counterexample found
if stats.get('attack_examples') is not None:
    adv_examples = stats['attack_examples']
    adv_margins = stats['attack_margins']
    print(f"Adversarial example shape: {adv_examples.shape}")
    print(f"Margin to violation: {adv_margins}")

# Reference data (intermediate bounds, model state)
reference = result.reference
if 'model' in reference:
    bounded_model = reference['model']  # LiRPANet with computed bounds

# Serialize result to dictionary
result_dict = result.as_dict()
```

--------------------------------

### ABCrownSolver Initialization and Execution

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/docs/abcrown_api.md

Initializes the solver with a verification specification and model, then executes the solve method to determine property satisfaction.

```APIDOC
## ABCrownSolver

### Description
Initializes the solver with a verification specification and a computing graph (model) to verify neural network properties.

### Parameters
- **spec** (VerificationSpec) - Required - VerificationSpec object containing input/output constraints.
- **computing_graph** (torch.nn.Module/str) - Required - A PyTorch model instance or a path to an ONNX file.
- **config** (dict) - Optional - Configuration dictionary or builder result.
- **name** (str) - Optional - Identifier for logging purposes.

### Methods
- **solve()** - Executes the verification process and returns a SolveResult object.

### Response
#### SolveResult Object
- **status** (str) - The verification outcome (e.g., 'verified', 'unsafe-pgd', 'unsafe-bab', 'safe-incomplete', 'unknown').
- **success** (bool) - True if the property is satisfied or a counterexample is confirmed.
- **reference** (dict) - Optional intermediate data including bounds and attack traces.
- **stats** (dict) - Metadata including elapsed time, PGD iterations, and BaB splits.
```

--------------------------------

### Clone α,β-CROWN Repository with Submodules

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/README.md

Clone the main repository and its auto_LiRPA submodule to set up the project.

```bash
git clone --recursive https://github.com/Verified-Intelligence/alpha-beta-CROWN.git
```

--------------------------------

### Run α,β-CROWN Verifier with Configuration

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/docs/abcrown_usage.md

Basic command to run the verifier using a specified YAML configuration file. Ensure the path to the config file is correct.

```bash
python abcrown.py --config XXX.yaml
```

--------------------------------

### Run Verification via Command Line

Source: https://context7.com/verified-intelligence/alpha-beta-crown/llms.txt

Execute Alpha-Beta-CROWN verification using the command line interface with YAML configuration files. Parameters can be overridden directly on the command line.

```bash
# Basic verification command
python abcrown.py --config exp_configs/tutorial_examples/cifar_resnet_2b.yaml
```

```bash
# Run with ONNX model and VNNLIB specification
python abcrown.py --config exp_configs/tutorial_examples/onnx_with_one_vnnlib.yaml
```

```bash
# Override specific parameters via command line
python abcrown.py --config exp_configs/cifar_resnet_2b.yaml \
    --timeout 600 \
    --start 0 \
    --end 50 \
    --pgd_steps 200
```

--------------------------------

### Download and Extract CROWN-IBP Models

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/models/crown-ibp/README.md

Use wget to download the CROWN-IBP model archive and tar to extract its contents. Ensure you have sufficient disk space.

```bash
wget https://download.huan-zhang.com/models/crown-ibp/crown_ibp_cifar_2px.tar.gz
tar xf crown_ibp_cifar_2px.tar.gz
```

--------------------------------

### Run VNN-COMP Benchmarks with VNNCompBenchmark

Source: https://context7.com/verified-intelligence/alpha-beta-crown/llms.txt

Use VNNCompBenchmark to run verification on VNN-COMP instances. This class handles loading configurations, parsing instance files, and executing verification. Requires paths to config and benchmark roots.

```python
from abcrown import VNNCompBenchmark, load_vnncomp_instance, run_all_instances, run_specific_instance

# Load and run all instances from a VNN-COMP config
benchmark = VNNCompBenchmark(
    config_path="exp_configs/vnncomp23/cifar100.yaml",
    root="/path/to/vnncomp2023_benchmarks/cifar100"
)
```

```python
# Run all benchmark instances
results = benchmark.run_all_instances()
for idx, instance, result in results:
    print(f"Instance {idx}: {result.status} ({result.stats['elapsed']:.2f}s)")
```

```python
# Run a specific instance by index
idx, instance, result = benchmark.run_specific_instance(instance_id=5)
print(f"ONNX: {instance.onnx_path}")
print(f"VNNLIB: {instance.vnnlib_path}")
print(f"Result: {result.status}")
```

```python
# Load instance data for custom processing
spec, onnx_path, config, metadata = benchmark.load_instance(instance_id=0)
```

```python
# Functional API alternatives
all_results = run_all_instances("exp_configs/vnncomp23/cifar100.yaml")
single_result = run_specific_instance("exp_configs/vnncomp23/cifar100.yaml", instance_id=3)
```

```python
# Load a single instance for custom use
spec, model_path, config, meta = load_vnncomp_instance(
    "exp_configs/vnncomp23/cifar100.yaml",
    instance_id=0,
    root="/path/to/benchmarks"
)
```

--------------------------------

### Create Symbolic Variables with input_vars and output_vars

Source: https://context7.com/verified-intelligence/alpha-beta-crown/llms.txt

Define symbolic input and output variables for building verification specifications using the expression DSL. Supports indexing, comparisons, and arithmetic operations. Ensure torch is imported.

```python
from abcrown import input_vars, output_vars
import torch

# Create symbolic input variables with shape
x_1d = input_vars(784)              # Flattened MNIST (784 elements)
x_image = input_vars((1, 28, 28))   # MNIST with channel dimension
x_cifar = input_vars((3, 32, 32))   # CIFAR-10 image

# Create symbolic output variables
y = output_vars(10)  # 10-class classification
```

```python
# Indexing - access individual elements
first_input = x_1d[0]
first_output = y[0]
```

```python
# Build input constraints (conjunction of bounds)
epsilon = 0.1
base = torch.zeros(784)
input_constraint = (x_1d >= base - epsilon) & (x_1d <= base + epsilon)
```

```python
# Build output constraints using comparisons
# Robustness: class 3 has highest logit
robustness = (y[3] > y[0]) & (y[3] > y[1]) & (y[3] > y[2]) & (y[3] > y[4])
```

```python
# Linear inequalities on outputs
margin_constraint = (y[0] - y[1]) > 0.5  # Class 0 beats class 1 by margin 0.5
```

```python
# OR constraints (disjunction)
either_class = (y[0] > y[2]) | (y[1] > y[2])  # Either class 0 or 1 beats class 2
```

```python
# Complex mixed AND/OR expressions
complex_spec = ((y[0] > 0) & (y[1] < 0.5)) & ((y[2] > 0.1) | (y[0] - y[1] > -0.1))
```

--------------------------------

### Configure Scalar Reachability

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/examples_abcrown/demo.ipynb

Creates a default configuration for the scalar reachability verification demo.

```python
def build_robot_config():
    """Config for the scalar reachability demo."""
    return (
        ConfigBuilder.from_defaults()
    )
```

--------------------------------

### Build Configuration with Chainable API

Source: https://context7.com/verified-intelligence/alpha-beta-crown/llms.txt

Use ConfigBuilder to programmatically set various parameters for verification, including device, seed, attack settings, solver configurations, and branch and bound options. Updates can be applied using a dictionary.

```python
config = (
    ConfigBuilder.from_defaults()
    .set(
        general__device="cuda",              # Use GPU
        general__seed=42,                    # Set random seed
        attack__pgd_order="before",          # Run PGD attack before verification
        attack__pgd_steps=100,               # PGD attack iterations
        attack__pgd_restarts=30,             # Number of PGD restarts
        solver__batch_size=2048,             # Batch size for bound computation
        solver__alpha_crown__iteration=100,  # Alpha-CROWN iterations
        solver__beta_crown__iteration=50,    # Beta-CROWN iterations
        bab__timeout=360,                    # Branch and bound timeout (seconds)
        bab__branching__method="kfsb",       # Branching heuristic
    )
    .update({
        "bab": {
            "cut": {"enabled": True},        # Enable cutting planes (GCP-CROWN)
        }
    })
)
```

```python
# Load configuration from YAML file
config_from_yaml = ConfigBuilder.from_yaml("exp_configs/tutorial_examples/cifar_resnet_2b.yaml")
```

```python
# Clone and modify existing configuration
modified_config = config_from_yaml.copy().set(bab__timeout=600)
```

```python
# Get final configuration dictionary
final_config = config.to_dict()
```

--------------------------------

### Run VNN-COMP benchmark instances

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/docs/abcrown_usage.md

Executes multiple ONNX models and VNNLIB specifications in batch mode using the VNN-COMP benchmark format.

```bash
# To get the ONNX model and VNNLIB config file, first clone the vnncomp2022_benchmarks repository, put it at the same folder as the alpha-beta-CROWN repo folder.
# git clone https://github.com/VNN-COMP/vnncomp2022_benchmarks.git ../../vnncomp2022_benchmarks
# pushd ../../vnncomp2022_benchmarks; ./setup.sh; popd
python abcrown.py --config exp_configs/vnncomp22/tinyimagenet_2022.yaml
```

--------------------------------

### Run All Hard Instances from Index File

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/exp_configs/bab_attack/README.md

Launch BaB-Attack on multiple hard instances by providing a configuration file and a text file containing the indices of hard instances to process. This command is used for reproducing paper results.

```python
# MNIST model A
python abcrown.py --config exp_configs/bab_attack/mnist_MadryCNN_no_maxpool_tiny.yaml --data_idx_file exp_configs/bab_attack/attack_idx/mnist_MadryCNN_no_maxpool_tiny/mip_unsafe_idx.txt --start 0 --end 20
```

```python
python abcrown.py --config exp_configs/bab_attack/mnist_MadryCNN_no_maxpool_tiny.yaml --data_idx_file exp_configs/bab_attack/attack_idx/mnist_MadryCNN_no_maxpool_tiny/mip_unknown_idx.txt --start 0 --end 27
```

```python
# MNIST model B
python abcrown.py --config exp_configs/bab_attack/mnist_cnn_a_adv.yaml --data_idx_file exp_configs/bab_attack/attack_idx/mnist_cnn_a_adv/mip_unsafe_idx.txt --start 0 --end 20
```

```python
python abcrown.py --config exp_configs/bab_attack/mnist_cnn_a_adv.yaml --data_idx_file exp_configs/bab_attack/attack_idx/mnist_cnn_a_adv/mip_unknown_idx.txt --start 0 --end 50
```

```python
# CIFAR model C
python abcrown.py --config exp_configs/bab_attack/cifar_cnn_a_adv.yaml --data_idx_file exp_configs/bab_attack/attack_idx/cifar_cnn_a_adv/mip_unsafe_idx.txt --start 0 --end 3
```

```python
python abcrown.py --config exp_configs/bab_attack/cifar_cnn_a_adv.yaml --data_idx_file exp_configs/bab_attack/attack_idx/cifar_cnn_a_adv/mip_unknown_idx.txt --start 0 --end 50
```

--------------------------------

### Image Classification Demo

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/docs/abcrown_api.md

Demonstrates a typical workflow for image classification verification. Requires a PyTorch model and defines input/output constraints.

```python
def run_image_demo():
    base = torch.rand(1, 1, 28, 28); eps = 0.02
    x = input_vars((1, 28, 28)); y = output_vars(3)
    input_constraint = (x >= base - eps) & (x <= base + eps)
    output_constraint = (y[0] > y[1]) & (y[0] > y[2])
    spec = VerificationSpec.build_spec(x, y, input_constraint, output_constraint)

    model = SimpleConvClassifier()
    solver = ABCrownSolver(spec, model, config=demo_config())
    print(solver.solve().status)
```

--------------------------------

### Download and Organize DM-Large Models

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/models/crown-ibp/README.md

Download the DM-Large model archive, extract it, and then move specific model files to their designated locations. This step is crucial for setting up the correct model paths.

```bash
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
```

--------------------------------

### Execute Lyapunov Solver

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/examples_abcrown/demo.ipynb

Instantiates the ABCrownSolver with the model, spec, and config to perform verification and print the status.

```python
def solve_lyapunov_demo():
    spec = build_lyapunov_spec()
    model = build_lyapunov_model()
    solver = ABCrownSolver(spec, model, config=build_lyapunov_config())
    result = solver.solve()

    print("[lyapunov] verifying Van der Pol controller")

    print(f"status={result.status}, success={result.success}")
    return result

_ = solve_lyapunov_demo()
```

--------------------------------

### Load ONNX Model for Verification

Source: https://context7.com/verified-intelligence/alpha-beta-crown/llms.txt

Load an ONNX model and a VNNLIB specification for verification. Configure solver settings like device and timeout. Access verification results and counterexamples.

```python
from abcrown import ABCrownSolver, VerificationSpec, ConfigBuilder

# Load ONNX model with VNNLIB specification
spec = VerificationSpec.build_spec(
    vnnlib_path="/path/to/property.vnnlib"
)

config = ConfigBuilder.from_defaults().set(
    general__device="cuda",
    attack__pgd_order="before",
    bab__timeout=300
)

# Pass ONNX path directly as computing_graph
solver = ABCrownSolver(
    spec,
    computing_graph="/path/to/model.onnx",  # ONNX model path
    config=config,
    name="onnx_verification"
)

result = solver.solve()
print(f"Verification result: {result.status}")

# Access counterexample if found
if "unsafe" in result.status:
    attack_examples = result.stats.get("attack_examples")
    if attack_examples is not None:
        print(f"Counterexample found: {attack_examples.shape}")
```

--------------------------------

### Configure Lyapunov Verification

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/examples_abcrown/demo.ipynb

Creates a default configuration for the Lyapunov verification demo with Jacobian computation enabled.

```python
def build_lyapunov_config():
    """Config for the Lyapunov verification demo."""
    return (
        ConfigBuilder.from_defaults().set(model__with_jacobian=True)
    )
```

--------------------------------

### Execute image classification solver

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/examples_abcrown/demo.ipynb

Runs the solver with the specified model and configuration, printing the final verification status.

```python
# Step 4: solver + one-shot run
def solve_image_classification(base_image: torch.Tensor, eps: float = 0.0039):
    """Run ABCrown on the image classification spec."""
    spec = build_image_classification_spec(base_image, eps)
    model = SimpleConvClassifier()
    solver = ABCrownSolver(spec, model, config=build_demo_config())
    result = solver.solve()
    print("[image classification] base eps=", eps)
    print(f"status={result.status}, success={result.success}")
    return result

torch.manual_seed(40)
base_image = torch.rand(1, 3, 32, 32)
_ = solve_image_classification(base_image, eps=0.0039)
```

--------------------------------

### VerificationSpec.build_spec

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/docs/abcrown_api.md

Entry point for constructing verification specifications using the expression DSL or loading from VNNLIB.

```APIDOC
## VerificationSpec.build_spec

### Description
Constructs a specification object for the solver. Supports symbolic DSL expressions or loading from external VNNLIB files.

### Parameters
- **input_vars** (VariableVector) - Optional - Symbolic input variables.
- **output_vars** (VariableVector) - Optional - Symbolic output variables.
- **input_constraint** (Expression) - Optional - Boolean combination of input constraints.
- **output_constraint** (Expression) - Optional - Boolean combination of output constraints (strict inequalities only).
- **vnnlib_path** (str) - Optional - Path to a .vnnlib file.
- **force_simplify** (bool) - Optional - Override DNF simplification behavior.
```

--------------------------------

### Build VerificationSpec with Different Methods

Source: https://context7.com/verified-intelligence/alpha-beta-crown/llms.txt

Construct VerificationSpec objects using explicit bounds, center-epsilon boxes, symbolic DSL, or by loading from a VNNLIB file. Choose the method that best suits your property definition.

```python
import torch
from abcrown import VerificationSpec, input_vars, output_vars

# Method 1: Build from explicit bounds and clauses
lower = torch.zeros(1, 3, 32, 32)
upper = torch.ones(1, 3, 32, 32)
# Output constraint: y[0] - y[1] <= 0 (class 1 has higher logit than class 0)
C = torch.tensor([[1.0, -1.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0]])
rhs = torch.tensor([0.0])
clauses = [[(C, rhs)]]  # OR-of-AND structure

spec_bounds = VerificationSpec.build_spec(
    lower=lower,
    upper=upper,
    clauses=clauses
)

# Method 2: Build from center and epsilon (L-infinity box)
center = torch.rand(1, 3, 32, 32)
epsilon = 0.03
spec_center = VerificationSpec.build_spec(
    center=center,
    epsilon=epsilon,
    clauses=clauses
)

# Method 3: Build from symbolic expressions (DSL)
x = input_vars((3, 32, 32))
y = output_vars(10)
input_constraint = (x >= 0.0) & (x <= 1.0)
output_constraint = (y[0] > y[1]) & (y[0] > y[2])  # Class 0 beats classes 1 and 2

spec_dsl = VerificationSpec.build_spec(
    input_vars=x,
    output_vars=y,
    input_constraint=input_constraint,
    output_constraint=output_constraint,
)

# Method 4: Load from VNNLIB file
spec_vnnlib = VerificationSpec.build_spec(
    vnnlib_path="/path/to/specification.vnnlib",
    input_shape=(3, 32, 32)
)
```

--------------------------------

### Run CIFAR Model E Experiments

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/exp_configs/bab_attack/README.md

Executes verification or attack tasks for CIFAR model E using specified configuration and index files.

```bash
python abcrown.py --config exp_configs/bab_attack/cifar_cnn_a_mix.yaml --data_idx_file exp_configs/bab_attack/attack_idx/cifar_cnn_a_mix/mip_unsafe_idx.txt --start 0 --end 3
```

```bash
python abcrown.py --config exp_configs/bab_attack/cifar_cnn_a_mix.yaml --data_idx_file exp_configs/bab_attack/attack_idx/cifar_cnn_a_mix/mip_unknown_idx.txt --start 0 --end 150
```

--------------------------------

### Run VNN-COMP benchmark categories via shell script

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/docs/vnn_comp.md

Executes the full benchmark suite for a specific VNN-COMP year using the run_all_categories.sh script.

```bash
./run_all_categories.sh v1 ${HOME}/alpha-beta-CROWN/vnncomp_scripts $(pwd) all_results.csv ./counterexamples "acasxu cifar10_resnet cifar2020 eran marabou-cifar10 mnistfc nn4sys oval21 verivital" all 2>&1 | tee stdout.log
```

```bash
./run_all_categories.sh v1 ${HOME}/alpha-beta-CROWN/vnncomp_scripts $(pwd) all_results.csv ./counterexamples "oval21 tllverifybench carvana_unet_2022 cifar_biasfield collins_rul_cnn mnist_fc nn4sys reach_prob_density vggnet16_2022 rl_benchmarks sri_resnet_a sri_resnet_b cifar100_tinyimagenet_resnet acasxu cifar2020" all 2>&1 | tee stdout.log
```

```bash
./run_all_categories.sh v1 ${HOME}/alpha-beta-CROWN/vnncomp_scripts $(pwd) all_results.csv ./counterexamples "acasxu cgan collins_yolo_robustness metaroom nn4sys tllverifybench vggnet16 yolo cctsdb_yolo collins_rul_cnn dist_shift ml4acopf test traffic_signs_recognition vit" all 2>&1 | tee stdout.log
```

```bash
./run_all_categories.sh v1 ${HOME}/alpha-beta-CROWN/vnncomp_scripts $(pwd) all_results.csv ./counterexamples "acasxu_2023 cifar100 cora lsnc ml4acopf_2024 traffic_signs_recognition_2023 yolo_2023 cctsdb_yolo_2023 collins_aerospace_benchmark dist_shift_2023 metaroom_2023 nn4sys_2023 tinyimagenet vggnet16_2023 cgan_2023 collins_rul_cnn_2023 linearizenn ml4acopf_2023 safenlp tllverifybench_2023 vit_2023" all 2>&1 | tee stdout.log
```

```bash
./run_all_categories.sh v1 ${HOME}/alpha-beta-CROWN/vnncomp_scripts $(pwd) all_results.csv ./counterexamples "acasxu_2023 cctsdb_yolo_2023 cersyve cgan_2023 cifar100_2024 collins_aerospace_benchmark collins_rul_cnn_2022 cora_2024 dist_shift_2023 linearizenn_2024 lsnc_relu malbeware metaroom_2023 ml4acopf_2024 nn4sys relusplitter safenlp_2024 sat_relu soundnessbench tinyimagenet_2024 tllverifybench_2023 traffic_signs_recognition_2023 vggnet16_2022 vit_2023 yolo_2023" all 2>&1 | tee stdout.log
```

--------------------------------

### ConfigBuilder

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/docs/abcrown_api.md

Utility for managing and updating solver configuration parameters.

```APIDOC
## ConfigBuilder

### Description
Provides a chainable interface to manage configuration settings for the alpha-beta-CROWN solver.

### Methods
- **from_defaults()**: Returns a builder initialized with default values.
- **set(key, value)**: Sets a configuration parameter using a flat key path.
- **update(dict)**: Performs a deep merge of a dictionary into the configuration.
- **from_yaml(path)**: Loads configuration overrides from a YAML file.
```

--------------------------------

### Activate Conda Environment

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/README.md

Use this command to activate the 'alpha-beta-crown' Conda environment before running the verifier.

```bash
conda activate alpha-beta-crown
```

--------------------------------

### Run Verification with ABCrownSolver

Source: https://context7.com/verified-intelligence/alpha-beta-crown/llms.txt

Use ABCrownSolver to programmatically verify a neural network. Define the model, input/output variables, constraints, and configuration before calling solve().

```python
import torch
from abcrown import (
    ABCrownSolver, VerificationSpec, ConfigBuilder, input_vars, output_vars
)

# Define a simple neural network model
class SimpleClassifier(torch.nn.Module):
    def __init__(self):
        super().__init__()
        self.fc1 = torch.nn.Linear(784, 256)
        self.fc2 = torch.nn.Linear(256, 10)
        self.relu = torch.nn.ReLU()

    def forward(self, x):
        x = x.view(x.shape[0], -1)
        return self.fc2(self.relu(self.fc1(x)))

# Create symbolic variables for input and output
x = input_vars((1, 28, 28))  # MNIST image shape
y = output_vars(10)          # 10 output classes

# Define input bounds (L-infinity perturbation around a base point)
base_image = torch.rand(1, 28, 28)
epsilon = 0.02
input_constraint = (x >= base_image - epsilon) & (x <= base_image + epsilon)

# Define output constraint (class 0 should have highest logit)
output_constraint = (y[0] > y[1]) & (y[0] > y[2]) & (y[0] > y[3])

# Build verification specification
spec = VerificationSpec.build_spec(
    input_vars=x,
    output_vars=y,
    input_constraint=input_constraint,
    output_constraint=output_constraint,
)

# Configure and run solver
config = ConfigBuilder.from_defaults().set(
    attack__pgd_order="before",
    bab__timeout=120,
    solver__batch_size=2048
)

model = SimpleClassifier()
solver = ABCrownSolver(spec, model, config=config)
result = solver.solve()

print(f"Status: {result.status}")      # 'verified', 'unsafe-pgd', 'unsafe-bab', 'unknown'
print(f"Success: {result.success}")    # True if property proven or counterexample found
print(f"Elapsed: {result.stats['elapsed']:.2f}s")
```

--------------------------------

### Run CIFAR Model F Experiments

Source: https://github.com/verified-intelligence/alpha-beta-crown/blob/main/complete_verifier/exp_configs/bab_attack/README.md

Executes verification or attack tasks for CIFAR model F using specified configuration and index files.

```bash
python abcrown.py --config exp_configs/bab_attack/cifar_marabou_small.yaml --data_idx_file exp_configs/bab_attack/attack_idx/cifar_marabou_small/mip_unsafe_idx.txt --start 0 --end 9
```

```bash
python abcrown.py --config exp_configs/bab_attack/cifar_marabou_small.yaml --data_idx_file exp_configs/bab_attack/attack_idx/cifar_marabou_small/mip_unknown_idx.txt --start 0 --end 50
```

--------------------------------

### ConfigBuilder - Configuration Management

Source: https://context7.com/verified-intelligence/alpha-beta-crown/llms.txt

ConfigBuilder provides a fluent interface for creating and modifying verification configurations, supporting defaults, merging, and YAML loading.

```APIDOC
## ConfigBuilder - Configuration Management

### Description
`ConfigBuilder` provides a chainable interface for building verification configurations. It supports setting individual parameters, merging dictionaries, loading from YAML files, and creating configuration snapshots.

### Method
```python
from abcrown import ConfigBuilder, default_config

# Get default configuration as dictionary
config_dict = default_config()

# Example of using ConfigBuilder to set parameters
config = ConfigBuilder.from_defaults().set(
    attack__pgd_order="before",
    bab__timeout=120,
    solver__batch_size=2048
)

# You can also merge with an existing dictionary
merged_config = ConfigBuilder.from_dict(config_dict).merge_from_dict({
    "bab__timeout": 60
}).build()
```

### Parameters
#### Path Parameters
None

#### Query Parameters
None

#### Request Body
- **config_dict** (dict) - A dictionary containing configuration parameters to merge.

### Request Example
```json
{
  "attack__pgd_order": "before",
  "bab__timeout": 120
}
```

### Response
#### Success Response (200)
- **config** (object) - A configuration object or dictionary representing the built configuration.

#### Response Example
```json
{
  "config": {
    "attack__pgd_order": "before",
    "bab__timeout": 120,
    "solver__batch_size": 2048
  }
}
```
```