boundlab.diff.zono3#
Triple-Zonotope-Based Abstract Interpretation for Differential Verification
This module provides zonotope transformations for computing over-approximations
of the difference f₁(x) − f₂(x) between two structurally identical networks,
achieving tighter bounds than verifying each network independently.
The interpreter operates on triples DiffExpr3
(x, y, d) where:
x: expression tracking network 1’s output zonotope,y: expression tracking network 2’s output zonotope,d: expression tracking the differencef₁(x) − f₂(x).
Affine operations (addition, scalar multiplication, linear layers, shape ops)
are handled directly: the bias cancels in the diff component, and weight
matrices are applied to all three components (without bias for d).
Non-linear operations (ReLU, …) use specialised differential linearisers derived from VeryDiff (Teuber et al., 2024).
Examples
Build a DiffExpr3 and propagate it through a model:
>>> import torch
>>> from torch import nn
>>> import boundlab.expr as expr
>>> from boundlab.diff.expr import DiffExpr3
>>> from boundlab.diff.zono3 import interpret
>>> model = nn.Sequential(nn.Linear(4, 5), nn.ReLU(), nn.Linear(5, 3))
>>> op = interpret(model)
>>> x = expr.ConstVal(torch.zeros(4)) + expr.LpEpsilon([4])
>>> y = expr.ConstVal(torch.ones(4)) + expr.LpEpsilon([4])
>>> d = x - y
>>> out = op(DiffExpr3(x, y, d))
>>> out.diff.ub().shape, out.diff.lb().shape
(torch.Size([3]), torch.Size([3]))
Module Attributes
Differential-verification interpreter. |
Functions
Return |