Zonotopes: boundlab.zono#

The idea#

A zonotope tracks a value as an affine form over shared error symbols:

\[ x \;=\; c + \sum_k G_{\cdot k}\, \varepsilon_k, \qquad \varepsilon_k \in [-1, 1]. \]

Linear layers transform \(G\) exactly — no precision is lost until a non-linearity is met, and expressions built from the same symbols stay correlated (x - x is exactly zero). Non-linearities are handled by linearizers: sound enclosures f(x) ⊆ slope·x + bias ± error whose error term becomes a fresh Noise component.

In BoundLab a Zono couples a Generator — a tensor whose trailing axis holds the coefficients \(G\) — with a SpanTable mapping each Error symbol to its slice of that axis. Adding two zonotopes aligns their tables so shared symbols land in the same columns.

Handling Basic Operators#

Every linear operator — add, sub, neg, shape ops, reductions, and any product with a constant (Gemm, x @ W) — is one exact einsum on the generator: a linear map of an affine form is an affine form. Adding two zonotopes built over different symbols first merges their span tables (align_fill_zeros), so shared symbols land in the same columns and keep cancelling.

Non-linear activations use the linearizers below: a sound affine enclosure whose residual becomes fresh Noise, immediately promoted to a new error symbol by keep_zono so it participates in later cancellation.

Handling Matmul#

The product of two affine forms is quadratic in the symbols, so an estimate maps it to a center plus interval noise (Matmul in boundlab.zono.matmul):

  • basic_estimate / square_estimate — the box bound x.ub() @ y.ub().

  • precise_estimate — the DeepT bound: the diagonal terms \(\varepsilon_i^2 \in [0, 1]\) contribute a center of half their summed magnitude (half the naive width), cross terms are bounded by magnitude; computed blockwise so the m·n·errors² pair tensor is never materialized.

Transformer attention hits this handler twice per head (Q @ Kᵀ and attn @ V) — it is where the zonotope domain pays, and what Sparse Polynomials: boundlab.polysp improves on.

Handling Softmax#

Softmax2ExpReciprocal rewrites softmax shift-invariantly as \(\sigma_i = 1 / \sum_j e^{\nu_j - \nu_i}\): pairwise differences and the reduce-sum are exact, exp and reciprocal use the linearizers, and the denominator is intersected with its plain interval evaluation (Intersects) so the tighter enclosure wins per element. No product of two abstract values is needed.

interpret#

The zonotope interpreter, exactly as assembled in boundlab.zono:

from boundlab.ibp.matmul import MatmulBiased
from boundlab.ibp.softmax import Softmax2ExpReciprocal
from boundlab.interp import Interpreter, base
from boundlab.zono import keep_zono, linearizers, matmul

interpret = Interpreter(
    base.interpret,                    # shared exact operators
    MatmulBiased(),                    # peel Bias centers off matmul
    matmul.Matmul(),                   # zonotope x zonotope estimate
    linearizers.MaxWithConst2Relu(),
    linearizers.Relu(),                # affine enclosures (see above)
    linearizers.Exp(),
    linearizers.Tanh(),
    linearizers.Reciprocal(),
    Softmax2ExpReciprocal(),
    after_each=keep_zono,              # fresh Noise -> new error symbols
)

keep_zono is the important last line: every linearizer residual enters as Noise, and promoting it to a first-class Zono symbol right away is what lets later layers cancel against it. Abstract inputs are built with Zono.error(err) * radius + center; the Zono/Generator API details are in the API reference.