Seq2Seq (spec model) #

Encoder-decoder models for sequence generation.

This file supports both bounded token indices and differentiable token distributions. A bounded index has type Fin vocabularySize, so embedding lookup cannot silently substitute a value for an invalid token. A token distribution uses a vector of length vocabularySize and realizes embedding as a matrix multiplication.

PyTorch analogue:

encoder: nn.RNN / nn.LSTM (or nn.TransformerEncoder) over source token embeddings
decoder: nn.RNN over target embeddings (teacher forcing in training), then a final nn.linear to vocabulary logits

Scope of this baseline:

the optional attention in Seq2SeqDecoderSpec is causal self-attention over decoder inputs. Training and inference use the same attention parameters and RNN recurrence. The baseline receives the encoder's final hidden state; it does not attend to the encoder's output sequence.
for cross-attention style mechanisms, we include a small additive/Bahdanau-style attention at the bottom of the file (computeAttentionWeightsSpec / applyAttentionSpec).

The transformer encoder blocks used by the transformer variant come from NN/Spec/Models/Transformer.lean.

References:

Sutskever et al., "Sequence to Sequence Learning with Neural Networks" (NeurIPS 2014).
Bahdanau et al., "Neural Machine Translation by Jointly Learning to Align and Translate" (2015).
Hochreiter and Schmidhuber, "Long Short-Term Memory" (1997).
Cho et al., "Learning Phrase Representations using RNN Encoder-Decoder for Statistical Machine Translation" (2014).
Vaswani et al., "Attention Is All You Need" (2017) for the transformer encoder variant.

PyTorch docs (for API intuition, not semantics):

torch.nn.Embedding: https://pytorch.org/docs/stable/generated/torch.nn.Embedding.html
torch.nn.RNN: https://pytorch.org/docs/stable/generated/torch.nn.RNN.html
torch.nn.LSTM: https://pytorch.org/docs/stable/generated/torch.nn.LSTM.html
torch.nn.Linear: https://pytorch.org/docs/stable/generated/torch.nn.Linear.html
torch.nn.MultiheadAttention: https://pytorch.org/docs/stable/generated/torch.nn.MultiheadAttention.html
torch.nn.TransformerEncoderLayer: https://pytorch.org/docs/stable/generated/torch.nn.TransformerEncoderLayer.html

Implementation status #

No API builder implements an encoder-decoder model. nn.rnn, nn.lstm, and nn.gru build single recurrent layers and NN/API/Models/Recurrent.lean builds sequence models with a per-step linear head, neither of which is this architecture. NN/Spec/Module/Seq2seq.lean wraps this file as a Spec.Module. No theorem is proved about it.

Training + gradients (one-hot inputs) #

Most of this file focuses on architecture variants and forward passes (teacher-forcing, inference-time decoding, optional self-attention in the decoder, etc.).

To make Seq2Seq usable as a first-class baseline, we also provide an explicit training objective and reverse-mode gradients for the differentiable path:

inputs are one-hot / token distributions (so embedding lookup is a matrix multiply),
teacher forcing is used in the decoder,
the loss is per-timestep cross-entropy between softmax(logits) and the target distribution,
gradients flow through embeddings, encoder RNN, decoder RNN, output projection, and (optionally) the decoder self-attention block.

Bounded token indices are intentionally treated as non-differentiable.

Seq2Seq (spec model) #

Implementation status #

Training + gradients (one-hot inputs) #

Small gradient records #

Decoder backward (teacher forcing) #

Differentiable training + backward (one-hot inputs) #