boundlab.zonosq

Quadratic-zonotope abstract interpretation.

Most operators mirror boundlab.zono; MatMul uses the QuadraticEpsilon square-term relaxation from this package.

Functions

relu_linearizer	Triangle relaxation of ReLU for zonotope abstract interpretation.
exp_linearizer	Minimal-area exp relaxation (DeepT, Section 4.5).
reciprocal_linearizer	Minimal-area reciprocal relaxation with positive-output constraint.
tanh_linearizer	Minimal-area tanh relaxation (DeepT, Section 4.4).
bilinear_elementwise	Linearize element-wise product of two symbolic expressions.
bilinear_matmul
matmul_handler
zonosq_matmul
zonosq_matmuls	Abstract the sum of matmuls Σ_i A_i @ B_i as a single zonosq expression.
softmax_handler	Zonotope softmax transformer using the DeepT decomposition.
softmax2_handler
softmax2_linearizer	Gradlin-based linearizer for x / (1 + x * exp(y)).

Classes

QuadraticEpsilon	Tuple of (eps, eps^2, eps' * eps^2) for eps, eps' in [-1, 1].
ZonosqExpr
ZonoBounds	Data class representing zonotope bounds for a neural network layer.