boundlab.zono.bilinear_matmul#

boundlab.zono.bilinear_matmul(A, B)[source]#

Linearize A @ B when both operands are symbolic expressions.

A: (m, k), B: (k, n) → result: (m, n)

The method uses a first-order expansion around expression centers:

\[A B \approx c_A B + A c_B - c_A c_B + E\]

where \(E\) is bounded by interval half-widths:

\[|E| \le \mathrm{hw}(A)\,\mathrm{hw}(B)\]

and represented using fresh noise symbols.

Parameters:
  • A (Expr) – Left expression with shape (m, k).

  • B (Expr) – Right expression with shape (k, n).

Returns:

An expression over-approximating A @ B.

Return type:

Expr

Examples

>>> import torch
>>> import boundlab.expr as expr
>>> from boundlab.zono.bilinear import bilinear_matmul
>>> A = expr.ConstVal(torch.ones(2, 3)) + 0.1 * expr.LpEpsilon([2, 3])
>>> B = expr.ConstVal(torch.ones(3, 4)) + 0.1 * expr.LpEpsilon([3, 4])
>>> C = bilinear_matmul(A, B)
>>> C.shape
torch.Size([2, 4])