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.
Positional encodings and causal masks
Definition
For a sequence of length with -dimensional token representations, a positional encoding is a fixed or trainable matrix added rowwise to the token matrix , giving . One fixed choice, with positions and coordinates indexed from , is and whenever the indicated coordinate is less than .
For decoder self-attention on positions indexed by , the causal mask is with when and when . Thus query position can use keys at positions and cannot use a future position; every row has an allowed key because .
Definition references
Vaswani et al., §3.5: positional encodings added to embeddings and sinusoidal formula
Vaswani et al., §3.2.3: masking illegal decoder connections before softmax
Dive into Deep Learning, §11.6.3: absolute and relative positional information
Dive into Deep Learning, §11.7.5: autoregressive decoder mask
Used by
Dependency tree · 0 levels
Nothing. This result depends on no other item in the library.
Sources
- Vaswani et al., Attention Is All You Need, §§3.2.3 and 3.5 (standard reference, not scraped)
- Dive into Deep Learning, §§11.6.3 and 11.7.5 (standard reference, not scraped)