Interval Bound Propagation in NCET¶
NCET groups operators by the rule used to propagate their tensor bounds. This avoids overlapping mathematical labels: for example, AveragePool2d is both linear and monotone, but its bounds are most simply propagated by monotonicity.
For one operation over an independent input box, the formulas below give exact elementwise output ranges. Across a deeper network, IBP can become conservative because it does not preserve correlations between tensor elements or graph branches.
1. Signed affine propagation¶
Linear, Conv2d, BatchNorm, and ElementwiseAffine may contain both positive and negative fixed coefficients, so their bounds require a positive/negative coefficient split.
Linear layer¶
Consider a linear layer
where \(x \in \mathbb{R}^{n}\), \(W \in \mathbb{R}^{m \times n}\), \(b \in \mathbb{R}^{m}\), and the input is bounded elementwise by
Split the weight matrix into its positive and negative parts:
The propagated bounds are then
Conv2d layer¶
A Conv2d layer is affine with respect to its input:
where the input bounds satisfy
As for a Linear layer, split the fixed kernel into positive and negative parts:
Using the same stride, padding, dilation, and groups settings as the original layer, the propagated bounds are
The bound propagation exactly follows the above formulas and uses torch.nn.functional.conv2d
directly.
NCET applies these formulas to per-sample tensors of shape (C, H, W); a
temporary batch dimension is used only for the PyTorch call and is removed
from the returned bounds. Padded positions are fixed at zero rather than
treated as uncertain inputs.
See Exact Conv2d encoding in NCET for the corresponding optimization constraint and sparse-matrix construction.
BatchNorm layer¶
In evaluation mode, BatchNorm is a fixed per-channel affine map:
where
Here, \(\mu_c\) and \(\sigma_c^2\) are the stored running statistics. For a non-affine module, \(\gamma_c=1\) and \(\beta_c=0\). Define \(a_c^+=\max(a_c,0)\) and \(a_c^-=\min(a_c,0)\). The propagated bounds are
with the channel vectors broadcast over spatial or sequence dimensions. See Exact BatchNorm encoding in NCET for the normalization and exact equality.
ElementwiseAffine¶
Tensor arithmetic with one fixed constant is normalized to
where the fixed arrays \(A\) and \(D\) may be broadcast without changing the shape of \(X\). Define
The propagated bounds are
This covers fixed-constant Add/Sub/Mul and division by a nonzero fixed constant. It gives the exact elementwise range of this operation over its input box.
2. Order-preserving unary operations¶
ReLU, LeakyReLU with a nonnegative slope, ReduceMean, AvgPool2d, AdaptiveAvgPool2d, and MaxPool2d are order-preserving unary operations. Let \(f\) denote any one of them. Given
monotonicity gives
Therefore, these operators use the same IBP rule:
ReLU¶
ReLU is elementwise and nondecreasing:
Its bounds are
LeakyReLU¶
For \(0<\alpha<1\), LeakyReLU is also elementwise and nondecreasing:
Therefore,
ReduceMean¶
For a fixed set of sample axes \(\mathcal D\), ReduceMean assigns every reduced element the nonnegative coefficient \(1/K\), where \(K\) is the number of reduced elements. Its bounds are therefore
See Exact ReduceMean encoding in NCET for the dimension convention and linear equality.
AveragePool2d layer¶
AveragePool2d is a linear operation whose averaging coefficients are all nonnegative. Consequently, there is no need to split its coefficients into positive and negative parts.
NCET uses the original kernel size, stride, padding, and
count_include_pad setting. Zero-padded positions are fixed constants, and
count_include_pad determines whether they contribute to the divisor.
See Exact AveragePool2d encoding in NCET for the corresponding averaging-matrix construction.
AdaptiveAvgPool2d layer¶
AdaptiveAvgPool2d also averages with nonnegative coefficients, but computes each pooling window from the input shape and requested output shape. Its bounds are therefore
See Exact AdaptiveAvgPool2d encoding in NCET for the window boundaries and sparse averaging matrix.
MaxPool2d layer¶
MaxPool2d is nonlinear but monotone: increasing any candidate in a pooling window cannot decrease the window maximum. Its bounds are therefore
NCET uses the original kernel size, stride, and padding. Padded positions are not valid maximum candidates, matching PyTorch's implicit negative-infinity padding.
For both pooling operators, an omitted stride defaults to the kernel size. NCET temporarily adds a batch-size-one dimension for the corresponding PyTorch functional call and removes it from the returned bounds.
See Exact MaxPool2d encoding in NCET for the corresponding one-hot exact formulation.
3. Multi-input arithmetic operations¶
These rules combine the bounds of two input tensors. Given
Write both scaled Add and Sub as
where \(\beta=\alpha\) for Add and \(\beta=-\alpha\) for Sub. Define
\(\beta^+=\max(\beta,0)\) and \(\beta^-=\min(\beta,0)\). Then
For the default \(\alpha=1\), these reduce to the usual \(L_X+L_Z, U_X+U_Z\) rule for Add and \(L_X-U_Z, U_X-L_Z\) rule for Sub. The ranges are exact when \(X\) and \(Z\) independently span their input boxes. If they are correlated graph branches, as in a residual connection, the formulas remain sound but can be conservative.
4. Structural operations¶
Structural operators only assemble, select, or reorder tensor elements, so NCET applies the same structural transformation to the lower and upper bounds.
For Concat,
For Identity, Flatten, Reshape/View/Squeeze/Unsqueeze, Permute, Transpose, GetItem, and Slice,
where \(g\) is the same shape transformation, axis reordering, or static index operation recorded in the GraphIR node. These operations do not introduce additional interval relaxation.
For Identity specifically,
Evaluation-mode Dropout is normalized to Identity because PyTorch disables its random mask during inference.