A sound neural-network verifier that proves whether an image classifier's prediction stays constant under every L∞ perturbation of size ε — built on the DeepPoly convex relaxation with back-substitution and learnable ReLU bounds.
Team project for the Reliable & Trustworthy Artificial Intelligence course at ETH Zürich (2023).
Adversarial examples show that tiny, imperceptible pixel changes can flip a neural network's prediction. A verifier answers the opposite question with a mathematical guarantee: given an input image, a network, and a perturbation radius ε, is the prediction provably the same for every image inside the L∞ ε-ball?
The challenge is that the ε-ball contains infinitely many images, so they cannot be checked one by one. We instead propagate a symbolic over-approximation of the whole input region through the network and certify robustness on the output bounds. The verifier must be sound (never certify a network that is actually breakable) while being precise enough to certify as many genuinely-robust cases as possible.
Evaluated on the 70 provided test cases spanning all 13 networks
(9 fully-connected + 4 convolutional, on MNIST and CIFAR-10), against the
project's ground-truth labels (test_cases/gt.txt):
| Metric | Result |
|---|---|
| Cases correct | 69 / 70 |
| Unsound results (certified a non-robust case) | 0 |
| Networks with a perfect score | 12 / 13 |
| Only miss | conv_4 (4/5) — a conservative miss: declined to certify one robust case |
The single miss errs on the safe side — the verifier returned not verified on a case that is in fact robust (incompleteness), never the reverse. It never once certified a network that wasn't robust, which is the property that actually matters for a verifier.
Run from the repository root:
$ python code/verifier.py --net fc_1 --spec test_cases/fc_1/img2_mnist_0.0692.txt
verified
$ python code/verifier.py --net fc_1 --spec test_cases/fc_1/img0_mnist_0.1394.txt
not verifiedverified means the network's prediction is provably constant across the entire
ε-ball; not verified means the analysis could not prove it (the network may or
may not be robust there).
The verifier implements DeepPoly (Singh et al., 2019), an abstract interpretation that keeps, for every neuron, a relational pair of bounds — linear expressions in terms of the neurons of earlier layers — instead of a single interval. This relational information is what makes the analysis tight.
- Input region. The L∞ ε-ball around the image becomes per-pixel lower/upper
bounds, clamped to the valid
[0, 1]range. - Per-layer transformers (
code/transforms.py):- Linear and Conv2d layers propagate the relational bounds exactly (the convolution is unrolled into its equivalent affine map).
- ReLU / LeakyReLU layers are non-linear and must be relaxed: each activation is over-approximated by a linear lower/upper bound parameterised by a slope α.
- Back-substitution (
back(...)): to turn relational bounds into concrete numbers, the bounds are recursively substituted back through previous layers down to the input, then evaluated against the input box. This is far tighter than naive interval propagation. - Learnable α (slope) optimisation. The ReLU slopes α are made trainable and
tuned with Adam to maximise the certified output margin (loss
-Σ relu(lower_bound)), recovering cases that a fixed relaxation would miss — the "α-CROWN" idea. - Robustness property. A final affine layer encodes
logit(true) − logit(other)for every other class; the input is verified iff the lower bound of all these margins is ≥ 0.
The analysis runs entirely on CPU. Convolutional networks with α-optimisation are the slowest cases; fully-connected ones are near-instant.
- Python 3.10
- PyTorch 2.0 (CPU) — tensors, autograd for the α-optimisation, and model loading
No other runtime dependencies. (Verified to also run on PyTorch 2.2 / Python 3.12.)
code/
verifier.py # entry point: builds the abstract domain, runs analysis, prints verified / not verified
transforms.py # DeepPoly transformers (linear, conv2d, ReLU/LeakyReLU) + back-substitution
networks.py # the 13 network architectures
utils/loading.py # spec-file parsing
evaluate # bash helper: run the verifier over every test case
models/ # pretrained network weights (*.pt), one per architecture/dataset
test_cases/ # sample specs, grouped by network; gt.txt holds the ground-truth labels
preliminary_evaluation_test_cases/ # earlier sample specs from the course
The networks and specs needed to run are committed under models/ and
test_cases/. If you supply your own, the verifier expects:
- Weights at
models/{dataset}_{net}.pt(e.g.models/mnist_fc_1.pt), matching one of the architectures innetworks.py. - Specs as plain-text files whose first line is the true label and whose
second line is the comma-separated, row-major pixel vector in
[0, 1]({net}∈ MNIST 28×28 = 784 values, or CIFAR-10 3×32×32 = 3072 values). The filename encodes the perturbation:img{id}_{dataset}_{eps}.txt.
# 1. Environment (pick one)
python -m venv venv && source venv/bin/activate # or: venv\Scripts\activate on Windows
pip install -r requirements.txt
# — or with conda —
conda env create -f environment.yaml && conda activate rtai-project
# 2. Verify a single case (run from the repo root)
python code/verifier.py --net fc_1 --spec test_cases/fc_1/img2_mnist_0.0692.txt
# 3. Run the whole sample suite
bash code/evaluateThe --net argument is one of:
fc_base, fc_1 … fc_7, conv_base, conv_1 … conv_4.
- Incompleteness. Like any sound relaxation-based verifier, it cannot certify
every robust case —
conv_4shows one such conservative miss. Soundness is never traded for it. - Speed. Deep convolutional nets with α-optimisation are the slow path; the α-search is capped at a few Adam iterations rather than run to convergence.
- Scope. Targets the course's fully-connected and convolutional architectures with ReLU/LeakyReLU activations and L∞ specifications; other layer types or norms are out of scope.
This was a group project. The finished verifier lives on main; the Try-with-backsubstitution branch
keeps earlier performance experiments for reference.
Released under the MIT License.