How to guides

To help you get up and running with ada-verona, we provide a tutorial notebook and a collection of example scripts:

Main Guide:
- The primary resource for learning how to use VERONA is the Jupyter notebook found in the notebooks folder. This tutorial notebook offers an overview of the package components, step-by-step instructions, and practical demonstrations of typical workflows. We highly recommend starting here to understand the core concepts and capabilities of the package.
Quick-Start Example Scripts:
- The scripts folder contains a variety of example scripts designed to help you get started quickly with ada-verona. These scripts cover common use cases and can be run directly (from within the scripts folder) to see how to perform tasks such as:
  - Running VERONA with a custom dataset and ab-crown (create_robustness_distribution_from_test_dataset.py).
  - Loading a PyTorch dataset and running VERONA with one-to-any or one-to-one verification (create_robustness_dist_on_pytorch_dataset.py).
  - Distributing jobs across multiple nodes using SLURM for large-scale experiments (multiple_jobs folder), including distributing tasks over CPU and GPU for different verifiers in the same experiment.
  - Using auto-verify integration (create_robustness_dist_with_auto_verify.py).

The notebook is your main entry point for learning and understanding the package, while the scripts serve as practical templates and quick-start resources for your own experiments.

Setting up the Experiment Directory

The experiment directory structure by default is expected as follows:

Note: You must provide ONNX or torch network files in the networks directory. ada-verona will create directories automatically, but you need to supply your own network models.

experiment/
|-- data/
|   |-- labels.csv
|   |-- images/
|       |-- mnist_0.npy
|       |-- mnist_1.npy
|       |-- ...
|-- networks/
|   |-- mnist-net_256x2.onnx
|   |-- mnist-net_256x4.onnx
|   |-- ...

Verification

Auto-Verify

VERONA features a plugin architecture through the AutoVerifyModule which allows integration with auto-verify when it's installed in the same environment. AutoVerify handles installation of various verifiers (see next section) as well as configuration and execution of the verifiers.

This design provides several benefits:

Independence: VERONA works perfectly without auto-verify, using attack-based verification methods for empirical upper bounds.
Automatic Detection: When auto-verify is installed in the same environment, its verifiers become automatically available
Interface: The same API works regardless of which verification backend is used

Auto-Verify can be installed in the following way:

Note: On macOS (and sometimes on Linux), you may need to install swig first with conda install -c conda-forge swig.

uv pip install auto-verify>=0.1.4

It is important to note that in order to use AutoVerify in VERONA, the pip version for AutoVerify must be >=0.1.4.

Available Verifiers

Currently, auto-verify supports nnenum, AB-Crown, VeriNet, and Oval-Bab. We thank the authors and maintainers of these projects for their contributions to the robustness research community.

We plan to add more verifiers to auto-verify in the future. For additional information about auto-verify, please refer to the official GitHub repository and documentation. Verifiers can be installed using the auto-verify command, e.g. to install nnenum and abcrown:

auto-verify install nnenum abcrown

To see the current configuration of auto-verify, you can use the auto-verify config show command.

auto-verify config show

Possible Extension: How to Add Your Own Verifier

Custom verifiers can be added to VERONA by using the VerificationModule interface.

Implement new verifiers using the VerificationModule class:

Create a new class that inherits from VerificationModule.
Implement the verify(self, verification_context: VerificationContext, epsilon: float) method. This method should return either a string (e.g., "SAT", "UNSAT", "ERR") or a CompleteVerificationData object.

Example:

from ada_verona.verification_module.verification_module import VerificationModule

class MyCustomVerifier(VerificationModule):
    def verify(self, verification_context, epsilon):
        # Your custom verification logic here
        # Return "SAT", "UNSAT", or a CompleteVerificationData object
        return "UNSAT"

Adversarial Attacks

VERONA implements the following adversarial attack methods:

Fast Gradient Sign Method (FGSM) - Goodfellow et al., 2015
Projected Gradient Descent (PGD) - Madry et al., 2018
AutoAttack - Croce and Hein, 2020

Optional: AutoAttack Installation

To use the AutoAttackWrapper class, you need to install AutoAttack separately from its GitHub repository:

uv pip install git+https://github.com/fra31/auto-attack

This package provides ensemble-based adversarial attacks for robustness evaluation. When installed, AutoAttackWrapper becomes automatically available in ada_verona.

Possible Extension: Custom Attacks

Custom attacks can be implemented by using the Attack interface.