boundlab.poly#

Polytope-Based Abstract Interpretation for Neural Networks.

This module provides CROWN-style abstract interpretation using linear polytope relaxations of nonlinear activations. Each neuron is bounded by a pair of linear envelopes:

\[\lambda_\ell \odot x + b_\ell \;\le\; f(x) \;\le\; \lambda_u \odot x + b_u\]

The central PolyBoundGate expression represents an abstract function with fixed \(\pm 1\) offsets; general CROWN-style bounds are wrapped by rescaling around their midpoint.

Examples

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

Module Attributes

interpret

Polytope-based interpreter.

Functions

`relu_linearizer`	CROWN relaxation of ReLU.
`exp_linearizer`	CROWN relaxation of \(\exp\).
`reciprocal_linearizer`	CROWN relaxation of \(1/x\) on a strictly positive domain.
`tanh_linearizer`	CROWN relaxation of \(\tanh\).
`square_linearizer`	CROWN relaxation of \(x^2\).
`softmax_handler`	Polytope softmax transformer via the DeepT decomposition.
`matmul_handler`	Dispatcher implementation for `torch.matmul`.
`mul_handler`	Dispatcher implementation for element-wise multiplication.

Classes

`PolyBoundGate`	Abstract gate bounded pointwise by a pair of linear polytopes on its child.
`PolyBounds`	CROWN-style linear relaxation bounds for a unary nonlinearity.