boundlab.diff.zono3#

Triple-zonotope abstract interpretation for differential verification.

Two structurally identical networks are propagated together as a triple DiffExpr3 (x, y, d), where x and y bound each network’s activations and d bounds their difference. Because d is tracked as a first-class zonotope over the same error symbols as the branches, everything the two networks share cancels instead of accumulating — which is what makes f₁(x) − f₂(x) provable at perturbation radii where bounding each network separately gives nothing.

Affine operations need no special handling: the four Expr primitives map over the components, biases cancel in d, and the base ONNX operators work unchanged. Non-linearities use the differential linearisers in this package — a nine-case ReLU split following VeryDiff (Teuber et al., 2024), and hexagon-Chebyshev envelopes for exp / tanh / reciprocal that bound the divided difference over the feasible region rather than over a merged interval.

Examples

>>> import torch
>>> from torch import nn
>>> from boundlab import Error
>>> from boundlab.utils import ShapeDtype
>>> from boundlab.zono import Zono
>>> from boundlab.diff.expr import DiffExpr3
>>> from boundlab.diff.zono3 import interpret
>>> err = Error("input", ShapeDtype((4,), torch.float32))
>>> x = Zono.error(err) * 0.05 + torch.zeros(4)
>>> triple = DiffExpr3(x, x, torch.zeros(4))
>>> model = nn.Sequential(nn.Linear(4, 5), nn.ReLU(), nn.Linear(5, 3))
>>> out = interpret(model)(triple)
>>> tuple(out.diff.ub().shape)
(3,)

Module Attributes

interpret

Differential interpreter over dense zonotopes.

Functions

`apply_diff_bounds`	Realise bounds against the input triple in the given `domain`.
`diff_bilinear`	Apply `interp_op` (`mul` or `matmul`) to a differential pair.
`diff_interpreter`	Assemble a differential interpreter over `domain`.
`diff_linearizer_fn`	Turn a differential lineariser into an `OpHandler`.
`diff_pairwise`	Apply `interp_op` to two branch pairs, keeping them independent.
`keep_diff`	Lift a domain's `after_each` normaliser over differential components.
`tighten_diff`	Pick, per element, the narrower of two sound enclosures of the difference.

Classes

`DiffBounds`	Affine enclosures for both branches and for their difference.
`DiffExp`	Differential exp bounds for a `(x, y, d)` triple.
`DiffHeavisidePruning`	Exact handler for `boundlab::HeavisidePruning` with concrete scores.
`DiffMatmul`	Matrix product of differential expressions.
`DiffMul`	Element-wise product of differential expressions.
`DiffReciprocal`	Differential `1/x` bounds for a `(x, y, d)` triple.
`DiffRelu`	Differential ReLU bounds for a `(x, y, d)` triple.
`DiffSoftmax`	Differential softmax over the last axis.
`DiffSoftmaxPruning`	Differential handler for `boundlab::SoftmaxPruning` over the last axis.
`DiffTanh`	Differential tanh bounds for a `(x, y, d)` triple.
`DiffTopKPruning`	Exact handler for `boundlab::TopKPruning` with concrete scores.