The Observation Theory EncyclopediaFrom TSKAboutBy kindBy chapterBy Lean fileLedgerProvenance

attention concept

DefinitionThe operation inside a language model that lets each token look at earlier ones by comparing its query to their keys and averaging their values. Chapter 0 section 0.11.
ExampleScores 2, 1, and 0 against three keys give softmax weights 0.665, 0.245, and 0.090.
BookData Mining as Observation, draft 0.2, commit f3914f0; entry id attention, kind concept.
Statusno ledger row names this entry. Corrections: none recorded.
Defining equation

Book equation 0.23.

Assumptions and scope
  • A head weights each earlier token’s value by the softmax of its query-key score and sums. For scalar values the output lies between the smallest and largest value, and the head reads the keys only through their scores against the query, so a key change the query does not read leaves the output unchanged however large it is.
  • That is the head’s read subspace, a few query-weighted directions of each key, and the reason a key reconstruction at cosine 0.995 raised the perplexity by three orders of magnitude.
Prior artnone recorded
Evidencelean/DataMiningAsObservation/Attention.lean
Reviewednot yet reviewed; generated 2026-09-10 from records at the commits on the provenance page.
querykey 1key 2key 3key 4key 5key 6key 7key 8softmax weights, sum to one
A query against every key, and a softmax that turns the scores into weights.

Equation

Book equation 0.23.

\[\operatorname{softmax}(z)_i=\frac{e^{z_i}}{\sum_j e^{z_j}},\qquad \text{output}=\sum_i\operatorname{softmax}\!\Big(\frac{q\cdot k_i}{\sqrt{d}}\Big)_{\!i}\,v_i.\]

Conditions

Conditions are curated in entries.toml rather than read from a record.

Ledger

none

First stated

Chapter 0 section 0.11 and chapter 11 section 11.1 of Data Mining as Observation, with the program’s head-level measurements in turboquant-pro/docs/KV_KEYS_FINDING.md:1-49 and the serving-stack ledger row.

Measurements

none

Failures and corrections

none

Invariance envelope

none declared

Machine checked

lean/DataMiningAsObservation/Attention.lean, theorems output_le_max, min_le_output, output_congr, output_nuisance, at observation-data-mining f3914f0; what the check covers is stated in the book’s appendix C.

Used in

Data Mining as Observation chapters 0, 1, 2, 4, 6, 8, 11, 13.

Related

softmax; read subspace; nuisance; the flip.

See also

Book equations stated beside the entry’s terms, not defining it: 11.1.

Ledger rows that cite the entry’s records without naming it: GO-2/GO-12/GO-13 operational (KV serving, 077), NEG-2.

Sources-table rows that share a record with the entry without naming it: chapter 1 section 1.4, chapter 2 section 2.5, chapter 3 section 3.2, chapter 8 section 8.2, chapter 11 section 11.1, chapter 11 section 11.2.

Status

Generated 2026-09-10 by encyclopedia/generate.py; book at observation-data-mining f3914f0; the commit of every record is listed in the encyclopedia’s provenance.

← Apriori principleattribute type →