Rounded scaled dot-product attention #
This module composes rounded-real NF bounds for attention's matrix operations and stable last-axis softmax. The unmasked forward theorem follows
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 transpose, sequential matrix multiplication,
coefficient-aware scaling, and row-softmax contracts. The current statements use the same feature
width for queries, keys, and values; they do not prove a native or fused attention kernel.
NF keeps the ordinary rounded-real expression. Finite IEEE carriers can additionally replay
scaled contractions and pullbacks from their original coefficients after range loss or absorption.
The statements here do not establish that separate finite-codec execution path.
The theorem keeps the rounded coefficient error explicit. A caller may obtain it from the concrete
construction of 1 / sqrt(d) or another proved coefficient bound. Backend metadata alone does
not establish this hypothesis. Hiding the error would treat a rounded scale as an exact 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 #
Half-ULP budget for embedding feature dimension d + 1 into NF.
Instances For
Error budget for the rounded square root of the embedded feature dimension.
Instances For
Error budget for constructing 1 / sqrt(d + 1) in the rounded-real model.
Instances For
The canonical rounded attention scale approximates the exact real 1 / sqrt(d + 1).
The accumulated square-root error must be smaller than one. This is a hypothesis about a noncomputable real-valued bound; the theorem does not automatically discharge it for a format.
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 supplies a bound for each rounded score row after matrix multiplication and scaling:
the accumulated denominator error must remain below the exact lower bound one. It is a
mathematical hypothesis, not an executable check performed by this theorem.
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 supply tensor approximation hypotheses and the two
error-margin proofs for square root and row normalization.