IBP Verifier
Interval & symbolic bound propagation for neural networks, from scratch
A from-scratch neural network verifier that computes sound output bounds for ONNX models under L∞ perturbations, using interval and symbolic bound propagation.
Overview
Verifiers like α,β-CROWN answer a precise question: for every input within ε of x, can the network's output ever cross a decision boundary? To understand how they answer it, I implemented the core technique — Interval Bound Propagation (IBP) — from scratch in Python and NumPy.
The verifier parses Gemm and ReLU layers straight from ONNX graph initializers, then pushes an input box through the network. Linear layers split their weights into positive and negative parts so bounds stay sound in one vectorized pass; ReLU layers clamp the bounds at zero.
Plain IBP is fast but loose, so I extended it with symbolic interval propagation: each neuron is tracked as an affine function of the input, with a linear relaxation at unstable ReLUs, to tighten the resulting bounds. A unit-test suite checks linear and ReLU propagation and compares symbolic against interval bounds.