boundlab.diff.polysp3#
Triple-sparse-polynomial abstract interpretation for differential verification.
Same differential algebra as boundlab.diff.zono3 — a triple
DiffExpr3 (x, y, d) with d tracking the
difference over shared error symbols — but each component is a
PolySp instead of a Zono.
That matters wherever the network multiplies two abstract values (attention scores, gating): the sparse-polynomial domain keeps second-order monomials instead of collapsing them to interval noise, so the products that dominate a transformer’s error budget stay correlated — and the differential difference inherits that precision directly.
The linearisers are shared with zono3: they work on plain
tensors and only the domain used for fresh error symbols differs.
Examples
>>> import torch
>>> from torch import nn
>>> from boundlab import Error
>>> from boundlab.utils import ShapeDtype
>>> from boundlab.polysp import PolySp
>>> from boundlab.diff.expr import DiffExpr3
>>> from boundlab.diff.polysp3 import interpret
>>> err = Error("input", ShapeDtype((4,), torch.float32))
>>> x = PolySp.error(err) * 0.05 + torch.zeros(4)
>>> triple = DiffExpr3(x, x, torch.zeros(4))
>>> out = interpret(nn.Sequential(nn.Linear(4, 5), nn.ReLU()))(triple)
>>> tuple(out.diff.ub().shape)
(5,)
Module Attributes
Differential interpreter over sparse polynomial expressions. |