Getting Started#

This page walks through installation and a minimal end-to-end bound computation.

Core workflow: Expr (relaxed abstract value) -> transform (zono.interpret or expression ops) -> dual-norm concretization (ub / lb / ublb).

Install#

Install docs dependencies (optional)#

pip install -e ".[docs]"

Verify installation#

python -c "import boundlab as bl; print(bl.__version__)"

Quick Start: Bound a Simple ReLU Network#

import torch
from torch import nn

import boundlab.expr as expr
import boundlab.zono as zono

# A small model we want to verify under input perturbation.
model = nn.Sequential(
    nn.Linear(4, 6),
    nn.ReLU(),
    nn.Linear(6, 3),
)

# Nominal input center.
x_center = torch.randn(4)

# Build symbolic input: x = center + eps, where eps_i in [-1, 1].
x_expr = expr.ConstVal(x_center) + expr.LpEpsilon([4])

# Export first, then build an abstract interpreter and propagate bounds.
exported = torch.export.export(model, (x_center,))
op = zono.interpret(exported)
y_expr = op(x_expr)

ub, lb = y_expr.ublb()
print("Upper bound:", ub)
print("Lower bound:", lb)
print("Width:", ub - lb)

Next Steps#

  • Continue with the User Guide to learn the expression system and interpreter internals.

  • Explore runnable patterns in Examples.

  • Browse full APIs in API Reference.

Build This Documentation Locally#

cd docs
make html

The generated site is written to docs/_build/html.