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, means, maxes along an
axis), analogous to operations like torch.sum, torch.mean, and torch.max.
https://pytorch.org/docs/stable/generated/torch.sum.html
https://pytorch.org/docs/stable/generated/torch.mean.html
https://pytorch.org/docs/stable/generated/torch.max.html
Current scope: row and column reductions on matrices. Broader-rank reductions can reuse the same argument after moving the selected axis into a matrix view.
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.
Row-wise budget vector for an m × n runtime matrix: entry i is the accumulated rounding
budget of runtime row i, so a row of large magnitudes is allowed a larger error than a row of
small ones. This is the sum-side counterpart of meanRowBoundVec below, and naming it keeps the
theorem statement readable instead of inlining the whole vector into the tolerance slot.
Instances For
Row-wise reduceSum along axis 1 approximates the exact row sums within
linfNorm (sumRowBoundVec eps xR). The reduction's own nonempty-axis evidence is the hypothesis, so
the statement asks for exactly what reduceSum needs and nothing more.
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.
Regression: under the half-margin certificate natCastError n ≤ n / 2, the mean budget is
linear in the row-sum budget, the row-length rounding error, 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.