Example: Verify an MLP with zono.interpret#

This example hands a whole model to the interpreter, which exports it to ONNX and replays the graph over the abstract input.

import torch
from torch import nn

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

torch.manual_seed(0)

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

center = torch.randn(4)
err = Error("input", ShapeDtype(center.shape, center.dtype))
x = Zono.error(err) * 0.1 + center

y = interpret(model)(x)
lb, ub = y.lbub()
print("lower:", lb)
print("upper:", ub)

# Monte-Carlo soundness check.
samples = center + 0.1 * (torch.rand(2000, 4) * 2 - 1)
with torch.no_grad():
    ys = model(samples)

assert (ys <= ub.unsqueeze(0) + 1e-5).all()
assert (ys >= lb.unsqueeze(0) - 1e-5).all()

What this demonstrates#

  • End-to-end bound propagation from an nn.Module in one call.

  • The interpreter exports once and evaluates operator by operator; only the abstract input flows differently from a concrete run.

  • A practical Monte-Carlo soundness check.