GPU GPT-2 Corpus Trainer

This command trains GPT-2-style models from text in TorchLean.

The model is initialized inside TorchLean and trained by the TorchLean runtime. It does not load a pretrained PyTorch/Hugging Face checkpoint:

• reusable tokenization lives under TorchLean.text,
• the compact GPT-2-style architecture lives under TorchLean.nn.models,
• the runnable corpus trainer enforces CUDA by default.

The default path keeps the byte-level model compact so the corpus trainer is quick to run. Passing --bpe-vocab and --bpe-merges switches to the Lean-native GPT-2 BPE tokenizer, using the standard 50,257-way GPT-2 token vocabulary. That BPE path still trains a randomly initialized model in TorchLean; it does not load a pretrained checkpoint.

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

Runner subcommand name. This subcommand trains a randomly initialized GPT-2-style model.

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

Default JSON loss-curve path for this command.

def NN.Examples.Models.Sequence.TextGpt2.minTrainingBytes : ℕ

Minimum corpus size for the default public training path: 100 MiB.

def NN.Examples.Models.Sequence.TextGpt2.byteSeqLen : ℕ

Default byte-level context window for the CUDA corpus trainer.

Keeping this near the file top lets corpus validation and the model architecture agree without depending on declaration order.

def NN.Examples.Models.Sequence.TextGpt2.readCorpusBytes (opts : API.text.CorpusLoggedPromptInteractiveOptions) : IO ByteArray

Read the primary raw text corpus.

def NN.Examples.Models.Sequence.TextGpt2.ByteGpt2.vocab : ℕ

Compact byte-level vocabulary for the default corpus path.

def NN.Examples.Models.Sequence.TextGpt2.ByteGpt2.batch : ℕ

Single-sequence batch for the byte-level corpus path.

def NN.Examples.Models.Sequence.TextGpt2.ByteGpt2.seqLen : ℕ

Interactive context window.

This shares the folder-level byte context constant so corpus validation, byte training, and BPE training use the same tensor layout. Larger windows require more allocator headroom, not something we should quietly make the default before allocator pressure is solved.

def NN.Examples.Models.Sequence.TextGpt2.ByteGpt2.numHeads : ℕ

Number of attention heads in the compact byte-level Transformer.

def NN.Examples.Models.Sequence.TextGpt2.ByteGpt2.headDim : ℕ

Per-head width.

def NN.Examples.Models.Sequence.TextGpt2.ByteGpt2.dModel : ℕ

Transformer embedding width.

def NN.Examples.Models.Sequence.TextGpt2.ByteGpt2.ffnHidden : ℕ

Feed-forward hidden width.

def NN.Examples.Models.Sequence.TextGpt2.ByteGpt2.layers : ℕ

Number of Transformer blocks.

theorem NN.Examples.Models.Sequence.TextGpt2.ByteGpt2.instNeZeroNatSeqLen : NeZero seqLen

theorem NN.Examples.Models.Sequence.TextGpt2.ByteGpt2.instNeZeroNatDModel : NeZero dModel

def NN.Examples.Models.Sequence.TextGpt2.ByteGpt2.cfg : TorchLean.nn.models.CausalOneHotConfig

Byte-level GPT configuration shared by shapes and the model constructor.

@[reducible, inline]

abbrev NN.Examples.Models.Sequence.TextGpt2.ByteGpt2.σ : Shape

Input shape: byte-level one-hot token sequence.

@[reducible, inline]

abbrev NN.Examples.Models.Sequence.TextGpt2.ByteGpt2.τ : Shape

Output shape: one byte-logit row per input position.

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

Runnable byte-level GPT-style model for corpus pretraining/fine-tuning.

The model is compact enough for the eager CUDA path while still exercising attention, feed-forward layers, byte tokenization, and the interactive prompt loop.

def NN.Examples.Models.Sequence.TextGpt2.mkByteCorpusSample (bytes : ByteArray) (i : ℕ) : TorchLean.SupervisedSample Float ByteGpt2.σ ByteGpt2.τ

Build one byte-level training sample from a corpus byte offset.

def NN.Examples.Models.Sequence.TextGpt2.mkBytePromptSample (prompt : String) : TorchLean.SupervisedSample Float ByteGpt2.σ ByteGpt2.τ

Build one byte-level prompt sample for before/after generation reports.

def NN.Examples.Models.Sequence.TextGpt2.generateByteGreedy (predict : TorchLean.Tensor.T Float ByteGpt2.σ → IO (TorchLean.Tensor.T Float ByteGpt2.τ)) (prompt : String) (steps : ℕ) : IO String

Greedy byte-level generation from the trained model.

def NN.Examples.Models.Sequence.TextGpt2.interactiveByteLoop (predict : TorchLean.Tensor.T Float ByteGpt2.σ → IO (TorchLean.Tensor.T Float ByteGpt2.τ)) (generate : ℕ) : IO Unit

Terminal prompt loop for the trained byte-level model.

partial def NN.Examples.Models.Sequence.TextGpt2.interactiveByteLoop.loop (predict : TorchLean.Tensor.T Float ByteGpt2.σ → IO (TorchLean.Tensor.T Float ByteGpt2.τ)) (generate : ℕ) (stdin : IO.FS.Stream) : IO Unit

def NN.Examples.Models.Sequence.TextGpt2.BpeGpt2.vocab : ℕ

Compact vocabulary used by the runnable BPE training path.

The tokenizer still uses GPT-2's real 50,257-token BPE files. For this Lean/CUDA model we project the corpus tokens into a local vocabulary of the first observed BPE ids. A full 50k-way output head is a much larger training run; this example focuses on the tokenizer/data path.

def NN.Examples.Models.Sequence.TextGpt2.BpeGpt2.batch : ℕ

Batch size for the BPE corpus path.

def NN.Examples.Models.Sequence.TextGpt2.BpeGpt2.seqLen : ℕ

Short context window used by the trainer.

def NN.Examples.Models.Sequence.TextGpt2.BpeGpt2.numHeads : ℕ

Number of attention heads in the miniature BPE Transformer.

def NN.Examples.Models.Sequence.TextGpt2.BpeGpt2.headDim : ℕ

Per-head width for the BPE Transformer.

def NN.Examples.Models.Sequence.TextGpt2.BpeGpt2.dModel : ℕ

Transformer embedding width.

def NN.Examples.Models.Sequence.TextGpt2.BpeGpt2.ffnHidden : ℕ

Feed-forward hidden width.

def NN.Examples.Models.Sequence.TextGpt2.BpeGpt2.layers : ℕ

Number of Transformer blocks.

theorem NN.Examples.Models.Sequence.TextGpt2.BpeGpt2.instNeZeroNatSeqLen : NeZero seqLen

theorem NN.Examples.Models.Sequence.TextGpt2.BpeGpt2.instNeZeroNatDModel : NeZero dModel

def NN.Examples.Models.Sequence.TextGpt2.BpeGpt2.cfg : TorchLean.nn.models.CausalOneHotConfig

BPE GPT configuration shared by shapes and the model constructor.

@[reducible, inline]

abbrev NN.Examples.Models.Sequence.TextGpt2.BpeGpt2.σ : Shape

Input shape: local-BPE one-hot token batch.

@[reducible, inline]

abbrev NN.Examples.Models.Sequence.TextGpt2.BpeGpt2.τ : Shape

Output shape: one local-BPE logit row per input position.

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

Compact GPT-2-style model with the real GPT-2 BPE tokenizer path.

This is not OpenAI GPT-2-small. It is a TorchLean-native Transformer whose tokenizer comes from GPT-2 BPE files and whose output head uses a local projection of the observed corpus ids.

def NN.Examples.Models.Sequence.TextGpt2.mkBpeCorpusSample (tokens : Array ℕ) (i : ℕ) : TorchLean.SupervisedSample Float BpeGpt2.σ BpeGpt2.τ

Build one BPE training sample from a tokenized corpus.

def NN.Examples.Models.Sequence.TextGpt2.mkBpePromptSample (tok : API.text.Gpt2Bpe.Tokenizer) (lv : API.text.LocalBpeVocab) (prompt : String) : Except String (TorchLean.SupervisedSample Float BpeGpt2.σ BpeGpt2.τ)

Turn a BPE prompt into one model input window.

def NN.Examples.Models.Sequence.TextGpt2.decodeBpeD (tok : API.text.Gpt2Bpe.Tokenizer) (ids : List ℕ) : String

Decode original GPT-2 BPE ids with the loaded tokenizer.

def NN.Examples.Models.Sequence.TextGpt2.decodeLocalBpeD (tok : API.text.Gpt2Bpe.Tokenizer) (lv : API.text.LocalBpeVocab) (ids : List ℕ) : String

Decode local BPE ids by mapping them back to original GPT-2 ids first.

def NN.Examples.Models.Sequence.TextGpt2.printBpePredictionProbe (tok : API.text.Gpt2Bpe.Tokenizer) (lv : API.text.LocalBpeVocab) (predict : TorchLean.Tensor.T Float BpeGpt2.σ → IO (TorchLean.Tensor.T Float BpeGpt2.τ)) (label prompt : String) : IO Unit

Print an argmax prediction report for a prompt under the BPE model.

def NN.Examples.Models.Sequence.TextGpt2.generateBpeGreedy (tok : API.text.Gpt2Bpe.Tokenizer) (lv : API.text.LocalBpeVocab) (predict : TorchLean.Tensor.T Float BpeGpt2.σ → IO (TorchLean.Tensor.T Float BpeGpt2.τ)) (prompt : String) (steps : ℕ) : IO String

Greedy BPE generation by repeatedly feeding the last seqLen tokens and appending the final-position argmax. This is a deterministic sampling path for inspecting the trained next-token model.

def NN.Examples.Models.Sequence.TextGpt2.trainCorpusFloat (opts : TorchLean.Options) (trainOpts : API.text.CorpusLoggedPromptInteractiveOptions) (bytes : ByteArray) : IO Unit

Train the GPT-2-style model over a text corpus using CUDA.

This performs one optimizer step per corpus window, rather than materializing the entire dataset in memory. The example is compact by GPT-2 standards, but the data path is real: file bytes → token windows → one-hot tensors → TorchLean CUDA training.

def NN.Examples.Models.Sequence.TextGpt2.loadBpeCorpusTokens (trainOpts : API.text.CorpusLoggedPromptInteractiveOptions) (tok : API.text.Gpt2Bpe.Tokenizer) : IO (Array ℕ)

Load and tokenize the text corpus with GPT-2 BPE.

def NN.Examples.Models.Sequence.TextGpt2.printBpeCorpusPreview (tok : API.text.Gpt2Bpe.Tokenizer) (lv : API.text.LocalBpeVocab) (tokens : Array ℕ) : IO Unit

Print the first BPE training window for inspecting tokenization and windowing.

def NN.Examples.Models.Sequence.TextGpt2.trainBpeCorpusFloat (opts : TorchLean.Options) (trainOpts : API.text.CorpusLoggedPromptInteractiveOptions) (tok : API.text.Gpt2Bpe.Tokenizer) (lv : API.text.LocalBpeVocab) (tokens : Array ℕ) : IO Unit

Train the compact GPT-2-style model with the real GPT-2 BPE tokenizer.

This exercises the GPT-2 tokenizer/vocabulary path and can overfit local windows. It is not a pretrained GPT-2 checkpoint; it is a randomly initialized TorchLean model trained by this command.

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

CLI entrypoint for CUDA byte/BPE corpus training.