Min Wu, Xiaofu Li, Haoze Wu, Clark Barrett.
The accompanying paper Efficiently Computing Compact Formal Explanations is accepted by AAAI 2026. VeriX+ builds on VeriX (NeurIPS 2023) and significantly improves both the size and the generation time of formal explanations, through a bound propagation-based traversal order, a binary search-based traversal, a confidence ranking strategy, and an adaptation of QuickXplain.
@inproceedings{VeriXplus,
author = {Wu, Min and Li, Xiaofu and Wu, Haoze and Barrett, Clark},
title = {Efficiently Computing Compact Formal Explanations},
booktitle = {Proceedings of the AAAI Conference on Artificial Intelligence},
volume = {40},
number = {42},
pages = {35857--35866},
year = {2026},
doi = {10.1609/aaai.v40i42.40900}
}
For the MNIST dataset, to compute the VeriX+ explanation for the 10th image in the test set x_test, using the fully-connected network models/mnist-fc:
from train_mnist import MNISTFC
verix = VeriX(
dataset="mnist",
image=x_test[10],
model_path="models/mnist-fc",
directory="results/",
model_class=MNISTFC,
)
verix.traversal_order(traverse="bounds", epsilon=0.05)
verix.compute_explanation(epsilon=0.05, procedure="sequential")traversal_order sets a traversal order over the input features, and compute_explanation then generates the explanation under perturbation magnitude epsilon. By default, the original image, the sensitivity map, and the explanation are plotted and saved to directory.
The choices for each variable:
traversal_order(traverse=...)
├── "bounds" bound propagation, smaller explanations
├── "saliency" feature-level saliency, the original VeriX
└── "random" random shuffle, a baseline
compute_explanation(procedure=..., use_confidence_ranking=...)
├── procedure
│ ├── "sequential" naive, one feature at a time
│ ├── "binary-search" same explanation as sequential, faster
│ └── "QuickXplain" smaller explanation, size–time trade-off
└── use_confidence_ranking
├── True (default) order the checks by confidence, faster
└── False check the classes in their default order
model_path points to a model stem: VeriX+ loads models/mnist-fc.onnx for inference and verification (Marabou), and models/mnist-fc.pt (a PyTorch state_dict, instantiated into model_class) for bound propagation.
See mnist.py for a full example on the MNIST dataset, and gtsrb.py for the GTSRB dataset. To train your own models — saved as a state_dict .pt for bound propagation and exported to .onnx for verification (simplified with onnxsim so Marabou is more likely to support all its operations) — see train_mnist.py and train_gtsrb.py.
Create the Python environment from verix.yml:
conda env create -f verix.yml
conda activate verix
VeriX+ uses the neural network verification tool Marabou (with the Gurobi LP solver) as its verification backend. Clone and build it into a Marabou/ folder at the repository root:
git clone https://github.com/NeuralNetworkVerification/Marabou.git
cd Marabou
mkdir build && cd build
cmake .. -DENABLE_GUROBI=ON -DBUILD_PYTHON=ON
cmake --build . -j 12
More details on installing Marabou with Gurobi enabled can be found here.
VeriX+ computes its sensitivity maps with two bound propagation libraries: bound_propagation for fully-connected models and auto_LiRPA for convolutional models. Install bound_propagation from PyPI, and auto_LiRPA from source as recommended in its repository:
pip install bound-propagation
git clone https://github.com/Verified-Intelligence/auto_LiRPA
cd auto_LiRPA
pip install .
This is for reference only — feel free to set up your own environment (see verix.yml for the full specification).
python 3.8.18
torch 2.2.2
tensorflow 2.13.1
keras 2.13.1
onnx 1.15.0
onnxruntime 1.17.1
onnxsim 0.5.0
auto_LiRPA 0.5.0
bound-propagation 0.4.3
Thanks a lot for your interest in our work. Any questions please feel free to contact us: minwu@cs.stanford.edu.