Differential Verification: `boundlab.diff`#

The idea#

Differential verification bounds the difference between two structurally identical networks — the original and a quantized, pruned, or fine-tuned copy. Bounding each network separately and subtracting is hopeless: the two envelopes are treated as independent and their widths add. Instead BoundLab propagates the networks together as a triple

\[ (x,\; y,\; d), \qquad d \;\supseteq\; f_1(\nu) - f_2(\nu), \]

where d is a first-class abstract value over the same error symbols as the branches. Everything the networks share — the input region, common weights, shared linearization errors — cancels in d instead of accumulating, so f_1 - f_2 stays provably small at perturbation radii where independent bounds say nothing.

Handling Basic Operators#

Linear structure needs no special rules. A linear map \(W\) applies to all three components (\(W x\), \(W y\), \(W d\)); a shared bias \(b\) shifts both branches and cancels in the difference, \((Wx + b) - (Wy + b) = W(x - y)\). A paired constant — two networks’ weights joined by diff_pair — stays a DiffExpr2 of concrete tensors, so products against it are exact. Adding a plain expression to a differential one lands in an ExprGroup (the base Expr.__add__ has no differential rules); lift_diff folds it back after every node, adding the shared part to both branches where it cancels in d.

Handling `ReLU`#

Classify each neuron by the signs its two inputs can take (VeryDiff’s nine-case table). In eight cases at least one branch is stable, and the difference is recovered exactly from the two triangle relaxations: the error symbols \(\varepsilon_x, \varepsilon_y\) that the branch relaxations introduce are reused verbatim by the difference,

\[ d' = \bar\lambda\, d + (\lambda_x - \bar\lambda) x + (\bar\lambda - \lambda_y) y + (\mu_x - \mu_y) + \mu_x \varepsilon_x - \mu_y \varepsilon_y , \]

which equals \(\mathrm{relu}(x)' - \mathrm{relu}(y)'\) symbol for symbol — no fresh approximation error. Only the ninth case (both branches crossing zero) relaxes \(d\) directly, with the tighter triangle \(\lambda_d = \mathrm{clamp}(d_u / (d_u - d_l), 0, 1)\) and half-width \(\mu_d = \tfrac12 \max(d_u, -d_l)\), introducing one fresh symbol for exactly those neurons.

Handling `exp`, `tanh`, `reciprocal`#

For a unary \(f\), the difference factors through the divided difference:

\[ f(x) - f(y) = S(x, y)\,(x - y), \qquad S(x, y) = \frac{f(x) - f(y)}{x - y}, \]

so bounding \(S\) over the feasible region gives \(d' \in \lambda_d\, d \pm \beta_d\) with \(\lambda_d = (S_{\min} + S_{\max})/2\) and \(\beta_d = \tfrac12 (S_{\max} - S_{\min}) \cdot \max(|d_l|, |d_u|)\). VeryDiff bounds \(S\) by the range of \(f'\) over the merged interval \([\min(l_x, l_y), \max(u_x, u_y)]\); BoundLab instead bounds it over the hexagon

\[ P = \{ (x, y) : x \in [l_x, u_x],\; y \in [l_y, u_y],\; x - y \in [d_l, d_u] \}, \]

a strict subset once the strip constraint bites. \(P\) has at most six vertices drawn from twelve closed-form candidates (rectangle corners plus strip/edge intersections); for exp and reciprocal the divided difference is monotone so vertex evaluation is exact, while tanh adds its interior and edge critical points analytically. In the saturation regime this shrinks \(\beta_d\) by orders of magnitude over the merged-interval bound.

Handling `Mul` and `MatMul`#

The difference of two products is linear in the tracked differences:

\[ a_1 b_1 - a_2 b_2 = a_1\, \Delta b + \Delta a\, b_2 , \qquad A_1 B_1 - A_2 B_2 = A_1\, \Delta B + \Delta A\, B_2 . \]

Each sub-product is delegated back to the enclosing domain, so whatever relaxation it uses for abstract products (the zonotope estimate, the sparse polynomial pair product) applies unchanged — and when one factor is a paired constant (the diff_pair case), every sub-product is exact and the difference carries no relaxation error at all. Two pairs with no non-linearity between them stay a DiffExpr2: nothing is materialized until a handler actually needs \(d\).

Handling `Softmax` and Pruning#

Softmax uses the shared decomposition \(\sigma_i = 1/\sum_j e^{\nu_j - \nu_i}\) with the differential exp and reciprocal handlers, wrapped in two soundness guards: the denominator’s propagated lower bound is raised to the provable floor \(\sum_j e^{\nu_j - \nu_i} \ge \max(1, e^{\max_j \nu^{lb}_j - \nu^{ub}_i})\) (the \(j = i\) term is \(e^0 = 1\)), and the outputs are intersected with their known ranges — probabilities in \([0, 1]\), their difference in \([-1, 1]\).

The pruning operators apply a concrete 0/1 mask \(m\) to the second network only, which is exact — no relaxation error:

\[ \text{out}_x = x, \qquad \text{out}_y = m \odot y, \qquad \text{out}_d = m \odot d + (1 - m) \odot x . \]

Symbolic (input-dependent) scores are rejected rather than approximated: a single fixed mask cannot enclose an input-varying kept-set; such models are handled one level up by enumerating the reachable kept-sets.

Building a paired model#

Differential structure is marked inside the model itself. diff_pair(x, y) joins two tensors (a weight and its quantized copy, say) into one differential value — a no-op returning x when run eagerly, a custom boundlab::DiffPair node under export, lifted to a DiffExpr2 by the interpreter. DiffLinear(fc1, fc2) packages two parallel linear layers that way, and the mock pruning operators (heaviside_pruning, topk_pruning, softmax_pruning in boundlab.diff.ops) mark score-based masking of the second network while running eagerly as the pruned network, so the same module supports Monte-Carlo checking. When the two networks exist as separate ONNX files instead, diff_net(net1, net2) merges them: wherever both graphs read an initializer, the merged graph pairs the two through a shared DiffPair node.

`interpret`#

A differential interpreter is assembled by diff_interpreter: the base handlers, the differential handlers for products and non-linearities, and the pruning/pairing operators. Each differential handler owns its operator and carries the domain’s standard handler as its fallback for plain expressions, so no operator ever has two ready handlers:

from boundlab.ibp.matmul import MatmulBiased
from boundlab.ibp.softmax import Softmax2ExpReciprocal
from boundlab.interp import Interpreter, base
from boundlab.zono import Zono, keep_zono, linearizers, matmul
from boundlab.diff import ops
from boundlab.diff.zono3 import (
    DiffMatmul, DiffMul, DiffRelu, DiffExp, DiffTanh, DiffReciprocal,
    DiffSoftmax, DiffSoftmaxPruning, DiffHeavisidePruning, DiffTopKPruning,
    keep_diff,
)

interpret = Interpreter(
    base.interpret,
    ops.DiffPair(),                       # boundlab::DiffPair -> DiffExpr2
    DiffMul(), DiffMatmul(),              # differential products
    DiffRelu(domain=Zono, fallback=linearizers.Relu()),
    DiffExp(domain=Zono, fallback=linearizers.Exp()),
    DiffTanh(domain=Zono, fallback=linearizers.Tanh()),
    DiffReciprocal(domain=Zono, fallback=linearizers.Reciprocal()),
    DiffSoftmax(fallback=Softmax2ExpReciprocal()),
    DiffSoftmaxPruning(), DiffHeavisidePruning(), DiffTopKPruning(),
    MatmulBiased(), matmul.Matmul(),      # plain-zonotope handlers
    linearizers.MaxWithConst2Relu(),
    after_each=keep_diff(keep_zono),      # lift groups, normalize components
)

boundlab.diff.zono3.interpret is exactly this assembly; boundlab.diff.polysp3.interpret is the same call with domain=PolySp and the polynomial matmul — the differential linearizers are shared, only the domain for fresh error symbols changes. Either accepts a DiffExpr3 triple, a DiffExpr2 pair, or a plain Expr (which falls through to the standard domain); out.diff.lbub() reads the certified difference bounds. New activations plug in through diff_linearizer_fn, which wraps a bounds function (x_lbub, y_lbub, d_lbub) -> DiffBounds with the fallback plumbing included.

Minimal example#

import torch
from torch import nn

from boundlab import Error
from boundlab.utils import ShapeDtype
from boundlab.zono import Zono
from boundlab.diff.ops import DiffLinear
from boundlab.diff.zono3 import interpret

fc1 = nn.Linear(4, 3)
fc2 = nn.Linear(4, 3)          # e.g. a quantized copy of fc1
model = nn.Sequential(DiffLinear(fc1, fc2), nn.ReLU()).eval()

center = torch.zeros(4)
err = Error("input", ShapeDtype(center.shape, center.dtype))
x = Zono.error(err) * 0.1 + center

out = interpret(model)(x)
lb, ub = out.diff.lbub()       # bounds on fc-net1 minus fc-net2, after ReLU

Differential Verification: boundlab.diff#

The idea#

Handling Basic Operators#

Handling ReLU#

Handling exp, tanh, reciprocal#

Handling Mul and MatMul#

Handling Softmax and Pruning#

Sharing and tightening#