boundlab.diff.expr#
Paired and tripled expressions for differential verification.
Two structurally identical networks f₁ and f₂ are propagated at the
same time so that their difference f₁(x) − f₂(x) can be bounded far more
tightly than by bounding each network on its own and subtracting.
Two carriers implement that:
DiffExpr2A pair
(x, y). Every linear operator applies to both components independently; no difference is tracked. Produced byboundlab.diff.ops.diff_pair()for paired weights, and by the interpreter for values that have not yet met a non-linearity.DiffExpr3A triple
(x, y, diff)wherediffover-approximatesx − y. Constant biases cancel indiff; a shared sub-expression (a value both networks compute identically) also cancels exactly.
Both are boundlab.Expr subclasses, so every base ONNX operator
(reshape, transpose, reduce, cast, …) works on them unchanged: the four
Expr primitives simply map over the components.
Examples
>>> import torch
>>> from boundlab import Error
>>> from boundlab.utils import ShapeDtype
>>> from boundlab.zono import Zono
>>> from boundlab.diff.expr import DiffExpr3
>>> err = Error("input", ShapeDtype((2,), torch.float32))
>>> x = Zono.error(err) * 0.1 + torch.tensor([1.0, 2.0])
>>> y = Zono.error(err) * 0.1 + torch.tensor([1.0, 2.5])
>>> triple = DiffExpr3(x, y, x - y)
>>> [round(v, 4) for v in triple.diff.ub().tolist()]
[0.0, -0.5]
Functions
Fold the shared part of a mixed sum into its differential component. |
Classes