GPT-2 style sequence model example.

The runnable causal language-model path includes training, generation, and infoview support. It uses the same public TorchLean model API that the command-line example uses.

GPT-2-Style Causal Language Model Example

Runnable torchlean gpt2 example. It builds a GPT-2-style causal transformer over byte-level tokens, with optional real text input from tiny-shakespeare or --data-file PATH.

If you are looking for the simplest "Karpathy-style single text file" path, start with torchlean chargpt (character-level tokenizer). This gpt2 command is byte-level and is meant to show the Transformer block wiring and save/reload loop.

python3 scripts/datasets/download_example_data.py --tiny-shakespeare
lake build -R -K cuda=true && lake exe torchlean gpt2 --cuda --tiny-shakespeare --steps 1 --windows 1 --generate 0

def NN.Examples.Models.Sequence.Gpt2.exeName : String

CLI subcommand name used in terminal banners and error messages.

def NN.Examples.Models.Sequence.Gpt2.defaultLogJson : System.FilePath

Default JSON loss-curve path for this command.

def NN.Examples.Models.Sequence.Gpt2.batch : ℕ

Batch size for the byte-level causal Transformer.

def NN.Examples.Models.Sequence.Gpt2.seqLen : ℕ

Prompt/target window length for the runnable GPT example.

def NN.Examples.Models.Sequence.Gpt2.vocab : ℕ

Byte vocabulary width used by the one-hot tokenizer.

def NN.Examples.Models.Sequence.Gpt2.numHeads : ℕ

Number of attention heads in the miniature Transformer block.

def NN.Examples.Models.Sequence.Gpt2.headDim : ℕ

Per-head embedding width. The model dimension is numHeads * headDim.

def NN.Examples.Models.Sequence.Gpt2.dModel : ℕ

Transformer embedding width.

def NN.Examples.Models.Sequence.Gpt2.ffnHidden : ℕ

Hidden width of the feed-forward sublayer.

def NN.Examples.Models.Sequence.Gpt2.layers : ℕ

Number of Transformer encoder blocks.

theorem NN.Examples.Models.Sequence.Gpt2.instNeZeroNatSeqLen : NeZero seqLen

theorem NN.Examples.Models.Sequence.Gpt2.instNeZeroNatDModel : NeZero dModel

@[reducible, inline]

abbrev NN.Examples.Models.Sequence.Gpt2.σ : Shape

Input shape: batched byte-level one-hot token windows.

@[reducible, inline]

abbrev NN.Examples.Models.Sequence.Gpt2.τ : Shape

Output shape: one vocabulary-logit row for every input token position.

def NN.Examples.Models.Sequence.Gpt2.model : TorchLean.nn.M (TorchLean.nn.Sequential σ τ)

Public GPT-style causal Transformer constructor specialized to the byte-level config.

def NN.Examples.Models.Sequence.Gpt2.mkSampleFromTokenIds (toks : List ℕ) : TorchLean.SupervisedSample Float σ τ

Build a batched causal-LM sample by repeating one token window across all rows.

def NN.Examples.Models.Sequence.Gpt2.mkSampleBatchFromTokenIds (idsByBatch : Array (List ℕ)) : TorchLean.SupervisedSample Float σ τ

Build a batch sample from per-row token windows.

idsByBatch[i] is the (seqLen + 1)-token window for batch row i. If fewer than batch windows are provided, the final window is repeated to fill the batch.

def NN.Examples.Models.Sequence.Gpt2.takeInputText (args : List String) : IO (String × List String)

Parse GPT-2-specific data flags and return the training corpus plus remaining runtime flags.

def NN.Examples.Models.Sequence.Gpt2.tokenWindowIds (input : String) (offset : ℕ) : List ℕ

Byte-token window used for reporting prompt/target text.

def NN.Examples.Models.Sequence.Gpt2.printPredictionReport (label input : String) (logits : TorchLean.Tensor.T Float σ) : IO Unit

Print a compact before/after language-model report for the first batch row.

def NN.Examples.Models.Sequence.Gpt2.inputTensorFromIds (ids : List ℕ) : TorchLean.Tensor.T Float σ

Convert byte ids into the typed batched one-hot input tensor used for generation.

@[reducible, inline]

abbrev NN.Examples.Models.Sequence.Gpt2.Predictor : Type

Fitted byte-level GPT predictor.

Training, saved-checkpoint inference, and future compiled runners all provide this one closure. Generation only needs a logit-producing function; it does not depend on where the logits came from.

def NN.Examples.Models.Sequence.Gpt2.generateSampledFromIds (predict : Predictor) (promptIds : List ℕ) (steps : ℕ) (temperature : Float) (topK seed repeatWindow : ℕ) (repeatPenalty : Float) (asciiOnly : Bool) : IO (List ℕ)

Autoregressively extend byte token ids using a trained byte-level GPT model.

def NN.Examples.Models.Sequence.Gpt2.generateSampled (predict : Predictor) (prompt : String) (steps : ℕ) (temperature : Float) (topK seed repeatWindow : ℕ) (repeatPenalty : Float) (asciiOnly : Bool) : IO (List ℕ)

Encode a string prompt and autoregressively extend it.

def NN.Examples.Models.Sequence.Gpt2.samplesFromCorpus (input _prompt : String) (windows : ℕ) : Array (TorchLean.SupervisedSample Float σ τ)

Build a finite cyclic training set from corpus text, biased toward the prompt when present.

def NN.Examples.Models.Sequence.Gpt2.interactiveLoopFloat (predict : Predictor) (train : API.text.InteractiveCheckpointedWindowedTrainGenerationOptions) : IO Unit

Interactive prompt loop for the in-memory Float model.

Each line is appended to the current byte context, decoded through the trained local model, and then kept as context for the next prompt unless the user clears it.

partial def NN.Examples.Models.Sequence.Gpt2.interactiveLoopFloat.loop (predict : Predictor) (train : API.text.InteractiveCheckpointedWindowedTrainGenerationOptions) (stdin : IO.FS.Stream) (ctx : List ℕ) : IO Unit

def NN.Examples.Models.Sequence.Gpt2.unitTrainStepsFloat (opts : TorchLean.Options) (input : String) (train : API.text.InteractiveCheckpointedWindowedTrainGenerationOptions) : IO (Float × Float × String)

Float-specialized training path with decoded prediction reports.

The CUDA executable uses Lean Float tensors, so this branch can show actual prompt, target, and predicted text before and after training. The polymorphic path above remains useful for checking the same training loop over other scalar backends.

def NN.Examples.Models.Sequence.Gpt2.main (args : List String) : IO UInt32

CLI entrypoint for byte-level GPT training, sampling, logging, and checkpointing.