NF Reduction Operators #
NF (rounded) backend: approximation lemmas for matrix reductions used by LayerNorm and attention.
The row and column lemmas use explicit Shape.NonemptyAxis evidence derived from positivity of the
matrix dimensions.
PyTorch correspondence / citations #
This file targets reduction patterns used by normalization/attention (sums and means along an
axis), analogous to torch.sum and torch.mean.
https://pytorch.org/docs/stable/generated/torch.sum.html
https://pytorch.org/docs/stable/generated/torch.mean.html
Current scope: row and column reductions on matrices, with sequential addition along the selected axis. Extending this proof through a matrix view requires a bridge preserving the element order and rounding schedule, not only the exact real sum.
Mean bound #
The row mean divides the rounded row sum by the rounded row length n. Its budget meanRowBound
is derived from the conditioned division bound divPosErrorBound: the exact denominator is n,
the denominator rounding error is natCastError n = |n̂ - n|, and the certificate natCastError n < n keeps the rounded denominator positive. When n is exactly representable the budget is
ulp(Σ̂ / n) / 2 + sumBound eps row / n (mean_row_bound_of_exact); if the certificate fails
the budget falls back to an always valid triangle-inequality bound. The rounded-real division
is total even when the rounded length is zero; this is not native NaN or infinity behavior.
Per-row sequential summation budgets for an m × n NF matrix.
Instances For
Row-wise reduceSum along axis 1 approximates the exact row sums within
linfNorm (sumRowBoundVec eps xR).
Rounding error of the runtime row length. The natural number n is embedded into NF by
rounding, and natCastError n is exactly how far that rounded value sits from n. It vanishes
whenever n is representable in the format.
Instances For
Per-row forward error budget for reduceMean along the last axis of a matrix.
The runtime mean divides the sequentially rounded row sum Σ̂ by the rounded row length n̂.
When the row-length rounding error is below n, the budget is the conditioned division bound
divPosErrorBound with exact denominator lower bound n, numerator error sumBound eps rowR, and
denominator error natCastError n. For an exactly represented n this is
ulp(Σ̂ / n) / 2 + sumBound eps rowR / n (see mean_row_bound_of_exact). If the certificate fails
the budget falls back to the always valid |Σ̂ / n̂| + (|Σ̂| + sumBound eps rowR) / n.
Instances For
Row-wise mean budget vector for an m × n runtime matrix.
Instances For
Scalar certificate for one row mean: the rounded quotient Σ̂ / n̂ approximates Σ / n within
meanRowBound.
Regression: when the row length is exactly representable, the mean budget is precisely one
output half ulp plus the row-sum budget divided by n.
Under the half-margin certificate natCastError n ≤ n / 2, the mean budget is controlled by
the row-sum budget, the row-length rounding error, their product, and one output rounding. The
hypothesis hsum records that the row-sum budget is nonnegative, which holds for every budget
produced by approxTensor_sum_spec.
Row-wise reduceMean along axis 1 of an m × n matrix approximates the exact row means
within linfNorm (meanRowBoundVec eps xR). Each entry is the certified division budget
meanRowBound for its row.
Extract column j from a runtime m×n tensor.
Instances For
Extract column j from a spec m×n tensor.
Instances For
Column-wise budget vector for an m × n runtime matrix, the axis-0 mirror of
sumRowBoundVec: entry j is the accumulated rounding budget of runtime column j.
Instances For
Column-wise reduceSum along axis 0 approximates the exact column sums within
linfNorm (sumColumnBoundVec eps xR). Note that this is not the row statement with the arguments
renamed: the budget reads columns, so a caller cannot reuse one bound for the other reduction.