DefinitionDefinition: Literature-sourcedProof: Not applicablePipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Stable summary of an attention key block

Definition

Let $n, d, v$ be positive integers, let $Q, K \in R^{n \times d}$ and $V \in R^{n \times v}$ , let $c \in R$ , and for each query row $i \in {1, \dots, n}$ let $A_{i} \subseteq {1, \dots, n}$ be a nonempty set of allowed keys. Write $q_{i}$ for row $i$ of $Q$ , $k_{j}$ for row $j$ of $K$ , $v_{j}$ for row $j$ of $V$ , and $s_{i j} = c \sum_{r = 1}^{d} Q_{i r} K_{j r}$ for $j \in A_{i}$ . For a nonempty finite set $S \subseteq A_{i}$ , its attention summary is

Σ_{i} (S) = (m_{i} (S), ℓ_{i} (S), z_{i} (S)), m_{i} (S) = \max_{j \in S} s_{i j}, ℓ_{i} (S) = \sum_{j \in S} e^{s_{i j} - m_{i} (S)}, z_{i} (S) = \sum_{j \in S} e^{s_{i j} - m_{i} (S)} v_{j} .

The empty set has the separate state $⊥$ and has no maximum or numeric summary coordinates. For disjoint nonempty $S, T \subseteq A_{i}$ , define their merge by

m^{'} = \max (m_{i} (S), m_{i} (T)), ℓ^{'} = e^{m_{i} (S) - m^{'}} ℓ_{i} (S) + e^{m_{i} (T) - m^{'}} ℓ_{i} (T), z^{'} = e^{m_{i} (S) - m^{'}} z_{i} (S) + e^{m_{i} (T) - m^{'}} z_{i} (T) .

and set $Σ_{i} (S) ⋆ Σ_{i} (T) = (m^{'}, ℓ^{'}, z^{'})$ . This summary stores the maximum score, a positive shifted normalizer, and the correspondingly shifted weighted value sum; dividing its third coordinate by its second gives the attention output on $S$ .

Definition references

Masked row-softmax attention and its nonempty-row convention

Dao et al., §3.1 and Appendix C: online maximum, normalizer, and weighted-value summaries

Milakov and Gimelshein, §3: online maximum and softmax normalizer

Depends on

Scaled dot-product attention

Used by

Dependency tree · one level

1 result within one dependency step of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Tri Dao et al., FlashAttention: Fast and Memory-Efficient Exact Attention with IO-Awareness, §3.1 and Appendix C (standard reference, not scraped)
Maxim Milakov and Natalia Gimelshein, Online normalizer calculation for softmax, §3 (standard reference, not scraped)