Rounded scaled dot-product attention #
This module connects TorchLean's stable last-axis softmax theorem to the matrix operations used by attention. The forward theorem follows the actual unmasked computation
softmax(c * (Q Kᵀ)) V,
where c is normally 1 / sqrt(d). Both the matrices and c may be approximate. The result is a
single infinity-norm budget assembled from the existing transpose, matrix-multiplication,
coefficient-aware scaling, and row-softmax contracts.
The theorem keeps the rounded coefficient error explicit. A caller may obtain it from the concrete
construction of 1 / sqrt(d), from an interval certificate, or from a backend capsule. Hiding that
error would incorrectly treat a rounded normalization factor as an exact real constant.
References:
- A. Vaswani et al., "Attention Is All You Need," NeurIPS 2017.
- N. J. Higham, Accuracy and Stability of Numerical Algorithms, 2nd ed., SIAM, 2002.
- PyTorch,
torch.nn.functional.scaled_dot_product_attention, for the runtime operator and last-axis normalization convention.
The canonical 1 / sqrt(d) coefficient #
Rounding budget for embedding the positive feature dimension into NF.
Instances For
Error budget for the rounded square root of the embedded feature dimension.
Instances For
End-to-end error budget for constructing 1 / sqrt(d) in the rounded backend.
Instances For
The canonical rounded attention scale approximates the exact real 1 / sqrt(d).
The side condition is format-sensitive and executable: the accumulated square-root error must be smaller than the exact lower bound one. For IEEE binary32 and ordinary transformer dimensions it is tiny; keeping it explicit also makes the theorem valid for low-precision experimental formats.
Error after the rounded score product Q Kᵀ.
Instances For
Error after multiplying scores by an approximate runtime scale.
Instances For
Shared numerical certificate for the scaled score matrix scale * (Q Kᵀ).
Both masked and unmasked attention use this prefix. Keeping it as one theorem also identifies the natural contract boundary for fused score kernels: a provider may replace the implementation as long as it supplies this same approximation statement.
Error in the row-wise attention weights.
Instances For
End-to-end output error for unmasked scaled dot-product attention.
Instances For
Error in hard-masked attention weights, preserving one certificate record per query row.
Instances For
End-to-end output error for hard-masked scaled dot-product attention.
Instances For
Numerical forward theorem for hard-masked scaled dot-product attention.
Every query row must have an allowed key. This covers causal masks, where the diagonal is allowed; the all-blocked vector theorem remains available for APIs that intentionally permit empty rows. The selected allowed-row maxima and denominator margins are explicit certificate data, so no finite value is ever substituted for negative infinity.
Numerical forward theorem for the unmasked scaled-dot-product attention core.
hdenom is checked on each rounded score row after matrix multiplication and scaling. This is the
only nonlocal side condition introduced by stable softmax; it certifies that the accumulated
denominator error remains below the exact lower bound one.
Canonical TorchLean attention corollary for the unmasked branch.
This theorem is stated directly over Spec.AttentionContext, so model proofs do not need to
reconstruct the core expression by hand. The scale approximation and row-denominator checks are
the numerical evidence attached to the runtime context.
Canonical TorchLean attention corollary for a shared hard mask.
The row certificate is tied to the scaled score matrices in the two contexts. Thus a certificate cannot be replayed against a different mask, scale, or set of parameters merely because the tensor shapes happen to agree.
Fully instantiated unmasked attention theorem for a positive feature dimension.
This corollary discharges the scale-coefficient approximation with
approx_canonicalAttentionScale; callers provide only tensor approximation hypotheses and the two
checkable safety margins for square root and row normalization.