User Guide

BoundLab computes sound [lower, upper] bounds on a network’s outputs over a set of inputs. Every page in this guide follows the same shape: first the idea behind a module, then a short tour of its API — enough to know what each method is for, with the full details left to the API Reference.

The pages build on one another:

• The Expression System
  • The idea
  • Groups, zeros, intersections
  • Error symbols
  • Conversion and concretization
• The Abstract Interpreter
  • The idea
  • The base interpreter
  • How a domain assembles its interpret
  • Using an interpreter
  • Export
• Intervals: boundlab.ibp
  • The idea
  • Handling Basic Operators
  • Handling Mul and Matmul
  • Handling Softmax
  • interpret
• Zonotopes: boundlab.zono
  • The idea
  • Handling Basic Operators
  • Handling Matmul
  • Handling Softmax
  • interpret
• Sparse Polynomials: boundlab.polysp
  • The idea
  • Handling Basic Operators
  • Handling Matmul
  • Handling Softmax
  • Compression
  • interpret
• Differential Verification: boundlab.diff
  • The idea
  • Handling Basic Operators
  • Handling ReLU
  • Handling exp, tanh, reciprocal
  • Handling Mul and MatMul
  • Handling Softmax and Pruning
  • Sharing and tightening
  • Building a paired model
  • interpret
  • Minimal example
• Future Plans for polysp
  • 1. Legendre Polynomial Concretization
  • 2. Polynomial Compression / Tensor Decomposition
  • 3. Polynomial Approximation of Non-linear Functions
  • Milestones

• The Expression System — the expression system every domain plugs into: typed components, groups, error symbols, conversion, and concretization.

• The Abstract Interpreter — the ONNX abstract interpreter: operator handlers, dispatch, and model export.

• Intervals: boundlab.ibp — the interval domain (Bias + Noise): the cheapest bounds.

• Zonotopes: boundlab.zono — the zonotope domain: affine forms over shared error symbols.

• Sparse Polynomials: boundlab.polysp — the sparse polynomial domain: higher-order monomials for products that intervals would destroy, and LAD-lasso compression that keeps the monomial count bounded at layer barriers.

• Differential Verification: boundlab.diff — differential verification: bounding the difference between two networks.

• Future Plans for polysp — research proposal: planned extensions of the sparse polynomial domain (Legendre concretization, compression — since implemented, see Sparse Polynomials: boundlab.polysp — and polynomial activation transfer).