Getting Started#

BoundLab’s workflow is three steps: build an abstract input (an Expr describing a set of inputs), run it through an abstract interpreter (which replays a model’s ONNX graph over expressions), and concretize the result into sound bounds with lbub().

Install#

git clone https://github.com/YuantianDing/BoundLab.git
cd BoundLab
pixi install          # or: pip install -e ".[dev]"

Requires Python ≥ 3.11 and PyTorch. Run the test suite with pixi run test.

Quick start: bound a ReLU network#

import torch
from torch import nn

from boundlab import Error
from boundlab.utils import ShapeDtype
from boundlab.zono import Zono, interpret

model = nn.Sequential(nn.Linear(4, 8), nn.ReLU(), nn.Linear(8, 3)).eval()

# An L-inf ball of radius 0.1 around `center`:
# x = center + 0.1 * eps, with each eps_i ranging over [-1, 1].
center = torch.randn(4)
err = Error("input", ShapeDtype(center.shape, center.dtype))
x = Zono.error(err) * 0.1 + center

# Interpret the model over the abstract input and concretize.
output = interpret(model)(x)
lb, ub = output.lbub()
print("lower:", lb)
print("upper:", ub)

interpret(model) exports the model to ONNX once and returns a callable that evaluates the graph operator by operator — concrete tensors stay concrete, abstract expressions are transformed by the registered handlers.

A quick Monte-Carlo sanity check:

samples = center + 0.1 * (torch.rand(2000, 4) * 2 - 1)
with torch.no_grad():
    outputs = model(samples)
assert (outputs >= lb - 1e-5).all() and (outputs <= ub + 1e-5).all()

Choosing a domain#

Domain

Import

Use when

Intervals

boundlab.ibp

speed matters more than precision

Zonotopes

boundlab.zono

the default: linear layers are exact

Sparse polynomials

boundlab.polysp

products (attention) dominate the error

Differential

boundlab.diff

bounding f1(x) - f2(x) for two networks

All domains share the same three-step workflow; only the expression class behind x and the interpret object change.

Next steps#