FaVeX: Faster Verified Explanations for Neural Networks

This repository contains the code for FaVeX, an algorithm to compute Faster Verified Explanations for Neural Networks.

If you use FaVeX in your research, please cite:

@inproceedings{DePalma2026,
    title={Faster Verified Explanations for Neural Networks},
    author={De Palma, Alessandro and Dolcetti, Greta and Urban, Caterina},
    booktitle={European Conference on Object-Oriented Programming (ECOOP)},
    year={2026},
}

Running FaVeX

FaVeX can be run on a user-provided PyTorch network and dataset through the following command:

python explanations/single_image_runner.py --dataset <dataset> --idx <input_idx> --gpu --model <network_architecture> --load <checkpoint_path> --eps <eps> --traversal alpha-favex --explanation_type v-optimal --algorithm favex --query_timeout <timeout> --max_leaves <max_leaves> --bab_config <bab_config> 

Where:

• <dataset> denotes the chosen dataset: in order to support additional datasets, please add them to the dataset_loading in explanations/utils.py;
• <input_idx> is the input index on which to compute the explanation;
• <network_architecture> is the PyTorch architecture to employ: it must be implemented as a function with the same name within explanations/models.py;
• <checkpoint_path> the path to the PyTorch checkpoint with the saved network weights for the network;
• <eps> the perturbation radius to employ for the explanation;
• <query_timeout> the branch-and-bound time per query to the verifier: we recommend 60 in general;
• <max_leaves> the maximum number of leaves from previous verifier queries to store: we recommend 500;
• <bab_config> the branch and bound configuration: we recommend verix_tinynet.json on small networks, expconfig_cnn7_cheap.json on larger networks, reducing max_solver_batch and batch_size in case of GPU OOM errors;
• --gpu can be removed to run FaVeX on CPU (not recommended for larger networks).

Reproducing the experiments

A python script to run the paper's experiments is provided in scripts/evaluation_script.py, which accepts a single argument indicating the network-dataset combination to run. By default, the script runs both the main experiments and the ablations at once. Depending on the network this may take considerable time (see average runtimes reported in the paper).

Running the CNN-7 experiments requires downloading the respective networks associated to Expressive Losses for Verified Robustness via Convex Combinations and placing them within trained_models, which already contains the other models used in the evaluation. This can be done by running the following commands:

cd trained_models
wget https://sail.doc.ic.ac.uk/data/expressive-losses-models-iclr24/mnist-0.1-ccibp.pt
wget https://sail.doc.ic.ac.uk/data/expressive-losses-models-iclr24/cifar10-2-255-ccibp.pt
cd ..

Code setup and dependencies

We suggest installing the code into a custom conda environment, created as follows:

conda create -y -n favex python=3.13
conda activate favex

OVAL BaB (incremental branch)

The verifier used in the paper is the incremental branch of the OVAL branch-and-bound framework. Clone the relative repository, switch to the relative branch (incremental), and please follow its relative installation instructions. These will also install other dependencies for this codebase (e.g., PyTorch).

Gurobi

Gurobi is required to reproduce the experiments in the paper: installation instructions are provided within those for the OVAL framework.

Installing this repository

Once the above requirements are met, this code can be installed as follows:

pip install .