boundlab.zono#

Zonotope-Based Abstract Interpretation for Neural Networks

This module provides zonotope transformations for computing over-approximations of neural network outputs under bounded input perturbations.

Examples

>>> import torch
>>> from torch import nn
>>> import boundlab.expr as expr
>>> import boundlab.zono as zono
>>> model = nn.Sequential(nn.Linear(4, 5), nn.ReLU(), nn.Linear(5, 3))
>>> op = zono.interpret(model)
>>> x = expr.ConstVal(torch.zeros(4)) + expr.LpEpsilon([4])
>>> y = op(x)
>>> y.ub().shape
torch.Size([3])

Module Attributes

interpret

Zonotope-based interpreter.

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 (DeepT, Section 4.6).
`tanh_linearizer`	Minimal-area tanh relaxation (DeepT, Section 4.4).
`bilinear_matmul`	Linearize `A @ B` when both operands are symbolic expressions.
`bilinear_elementwise`	Linearize element-wise product of two symbolic expressions.
`matmul_handler`	Dispatcher implementation for `torch.matmul`.
`softmax_handler`	Zonotope softmax transformer built from primitive handlers.

Classes

ZonoBounds

Data class representing zonotope bounds for a neural network layer.