boundlab.diff

Differential verification: bounding f₁(x) − f₂(x) for two networks.

Verifying two structurally identical networks separately and subtracting the results is hopeless — the two error envelopes are treated as independent, so the difference inherits the sum of both. Propagating them together, with an explicit third component tracking the difference over shared error symbols, lets everything the networks have in common cancel.

The pieces:

expr

DiffExpr2 (a branch pair) and DiffExpr3 (a pair plus its difference).

ops

Operators that mark differential structure inside a model — diff_pair(), DiffLinear, and mock pruning ops.

onnx

diff_net(), which merges two ONNX models into one paired graph.

zono3 / polysp3

The interpreters, over dense zonotopes and sparse polynomials respectively.

Examples

>>> from boundlab.diff import zono3, polysp3
>>> callable(zono3.interpret) and callable(polysp3.interpret)
True

Functions

diff_net	Pair the initializers of two structurally identical ONNX models.
diff_pair	Mark x and y as the two branches of one differential value.
heaviside_pruning	Mock score-based pruning: network 1 keeps data, network 2 masks it.
softmax_pruning	Mock softmax pruning: network 1 is softmax(data), network 2 masks it.
topk_pruning	Mock top-k pruning: network 2 keeps the k highest-scoring positions.

Classes

DiffExpr2	A pair of expressions (x, y), one per network.
DiffExpr3	A triple (x, y, diff) where diff over-approximates x − y.
DiffLinear	Two parallel linear layers paired through diff_pair().

Modules

expr	Paired and tripled expressions for differential verification.
onnx	Merge two ONNX models into one paired graph for differential interpretation.
ops	Custom operators that mark differential structure inside a model.
polysp3	Triple-sparse-polynomial abstract interpretation for differential verification.
zono3	Triple-zonotope abstract interpretation for differential verification.