AlgorithmAlgorithm: 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.

Transformer encoder-decoder forward pass

Definition

Inputs: A nonempty source token sequence $(x_{1}, \dots, x_{n})$ , a target prefix $(y_{0}, \dots, y_{m - 1})$ with $m \geq 1$ and a start token $y_{0}$ , source and target embedding maps into $R^{d}$ , positional encoding matrices of compatible shapes, a finite encoder stack, a finite decoder stack, and a linear output map to a finite vocabulary of logits. Each layer has the parameters and conventions in the transformer encoder/decoder definition. All self-attention and cross-attention masks must leave at least one allowed key in every query row.

Procedure:

Embed each source token and add its positional vector to form $X \in R^{n \times d}$ .
Apply the encoder layers in order to $X$ and call the final matrix $E \in R^{n \times d}$ .
Embed each target-prefix token and add its positional vector to form $U \in R^{m \times d}$ .
Apply each decoder layer in order. In every decoder layer, use the causal mask on decoder self-attention, use the current decoder rows as queries and $E$ as keys and values for cross-attention, and then apply the positionwise feedforward sublayer.
Apply the output linear map to each final decoder row and apply softmax over vocabulary coordinates. Return the encoder matrix $E$ , the final decoder hidden matrix, and the rowwise next-token probability matrix.

Outputs: The source representations, decoder representations, and one probability vector for each target-prefix position. At position $i$ , the decoder self-attention calculation uses only target-prefix positions $j \leq i$ ; the encoder cross-attention may use every source position.

Definition references

Vaswani et al., §3.1: encoder/decoder stacks and shifted autoregressive targets

Vaswani et al., §§3.2.3–3.5: cross-attention, causal mask, feedforward maps, and positional encodings

Dive into Deep Learning, §§11.7.1–11.7.7: encoder-decoder model and forward computation

Transformer encoder, decoder, and fixed-width expressivity blocks: exact residual, normalization, attention, and feedforward layer conventions.

Depends on

Transformer encoder, decoder, and fixed-width expressivity blocks

Used by

Dependency tree · two levels

4 results within two dependency steps 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

Vaswani et al., Attention Is All You Need, §§3.1–3.5 (standard reference, not scraped)
Dive into Deep Learning, §§11.7.1–11.7.7 (standard reference, not scraped)