User Guide

This guide explains how BoundLab represents symbolic computations and computes sound bounds.

Start with the BoundLab User Guide for the core mental model and usage patterns, then dive into specific APIs as needed.

• BoundLab User Guide
  • Mental Model
  • Core Building Blocks
  • Working Patterns
  • Inspecting Expressions and Operators
  • Supported Operations
  • Internals
  • Limitations and Notes
  • Extending BoundLab
  • Differential Verification (boundlab.diff.zono3)
  • Where To Go Next
• API Deep Dive: Expr, backward, AffineSum, TupleExpr
  • Expr
  • Expr.backward(...)
  • AffineSum
  • TupleExpr and GetTupleItem
  • Minimal Example
• API Deep Dive: LinearOp
  • Why LinearOp Exists
  • Core API
  • Most Important Implementations
  • Shape and Indexing LinearOps
  • Jacobian Utility APIs
  • Minimal Example
• API Deep Dive: ub, lb, ublb
  • ub and lb
  • ublb
  • Caching and Practical Notes
  • Minimal Example
• API Deep Dive: zono.interpret and Linearizers
  • zono.interpret(program_or_graph_module)
  • Linearizer Contract
  • Registration and Execution
  • Built-in Zonotope Handlers
  • Minimal Example
  • Notes
• Differential Verification with diff.zono3
  • Why Differential Verification?
  • Core Abstractions
  • diff.zono3.interpret
  • ReLU Differential Linearizer
  • Registering Custom Differential Linearizers
  • Comparing Differential vs. Independent Bounds
  • Limitations
  • Where To Go Next