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 byte path uses one output class for each of the 256 UTF-8 byte values. Passing --bpe-vocab and --bpe-merges loads the GPT-2 tokenizer files, then projects observed token IDs into a local vocabulary of at most 512 entries. IDs outside that local vocabulary map to entry zero. The model therefore does not have a 50,257-way GPT-2 output head. Both paths train randomly initialized models with four-token contexts; generated text is a runtime demonstration.

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.defaultLogPath : 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.contextLength : ℕ

Default context window for both corpus trainers.

Keeping this near the file top lets corpus validation and the model architecture agree without depending on declaration order. Four positions are enough to exercise causal attention while keeping this command a compact runtime check.

structure NN.Examples.Models.Sequence.TextGpt2.Options : Type

Command-local corpus, training, tokenization, generation, and prompt-loop controls.

• training : TorchLean.CLI.Training.RunOptions

  Step, batching, logging, and allocator controls.

• generation : TorchLean.text.PromptGenerationOptions

  Prompt and continuation-length settings.

• interaction : TorchLean.text.InteractiveOptions

  Terminal prompt-loop policy.

• corpus : TorchLean.text.CorpusFileOptions

  Primary corpus and explicit small-data override.

• finetune : TorchLean.text.FinetuneOptions

  Optional second corpus pass.

• bpe : TorchLean.text.BpeCorpusOptions

  Optional GPT-2 BPE tokenizer bundle.

@[instance_reducible]

instance NN.Examples.Models.Sequence.TextGpt2.instReprOptions : Repr Options

def NN.Examples.Models.Sequence.TextGpt2.instReprOptions.repr : Options → ℕ → Std.Format

def NN.Examples.Models.Sequence.TextGpt2.Options.usage : String

Help text for corpus training, optional GPT-2 tokenization, and generation.

def NN.Examples.Models.Sequence.TextGpt2.Options.parse (args : List String) : Except String (Options × List String)

Parse the complete option surface owned by the text_gpt2 executable.

def NN.Examples.Models.Sequence.TextGpt2.readCorpusBytes (corpusOptions : Options) : IO ByteArray

Read the primary raw text corpus.

def NN.Examples.Models.Sequence.TextGpt2.ByteModel.vocabularySize : ℕ

Compact byte-level vocabulary for the default corpus path.

theorem NN.Examples.Models.Sequence.TextGpt2.ByteModel.instNeZeroNatVocabularySize : NeZero vocabularySize

def NN.Examples.Models.Sequence.TextGpt2.ByteModel.byteIndex (id : ℕ) : Fin vocabularySize

Embed a byte id in the complete 256-entry byte vocabulary.

def NN.Examples.Models.Sequence.TextGpt2.ByteModel.batchSize : ℕ

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

instance NN.Examples.Models.Sequence.TextGpt2.ByteModel.instNeZeroNatBatchSize : NeZero batchSize

def NN.Examples.Models.Sequence.TextGpt2.ByteModel.contextLength : ℕ

Context window shared by corpus validation, byte training, BPE training, and generation.

def NN.Examples.Models.Sequence.TextGpt2.ByteModel.attentionHeads : ℕ

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

def NN.Examples.Models.Sequence.TextGpt2.ByteModel.attentionHeadWidth : ℕ

Per-head width.

def NN.Examples.Models.Sequence.TextGpt2.ByteModel.modelWidth : ℕ

Transformer embedding width.

def NN.Examples.Models.Sequence.TextGpt2.ByteModel.feedForwardWidth : ℕ

Feed-forward hidden width.

def NN.Examples.Models.Sequence.TextGpt2.ByteModel.transformerLayers : ℕ

Number of Transformer blocks.

theorem NN.Examples.Models.Sequence.TextGpt2.ByteModel.instNeZeroNatContextLength : NeZero contextLength

theorem NN.Examples.Models.Sequence.TextGpt2.ByteModel.instNeZeroNatModelWidth : NeZero modelWidth

@[reducible, inline]

abbrev NN.Examples.Models.Sequence.TextGpt2.ByteModel.modelConfig : TorchLean.nn.models.CausalTransformer.Config

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

@[reducible, inline]

abbrev NN.Examples.Models.Sequence.TextGpt2.ByteModel.input : Spec.Shape

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

@[reducible, inline]

abbrev NN.Examples.Models.Sequence.TextGpt2.ByteModel.output : Spec.Shape

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

def NN.Examples.Models.Sequence.TextGpt2.ByteModel.model : TorchLean.nn.Builder (TorchLean.nn.Sequential input output)

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

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

def NN.Examples.Models.Sequence.TextGpt2.byteCorpusSampleAt (bytes : ByteArray) (i : ℕ) : TorchLean.Sample.Supervised Float ByteModel.input ByteModel.output

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

def NN.Examples.Models.Sequence.TextGpt2.generateByteGreedy (predict : TorchLean.Tensor Float ByteModel.input → IO (TorchLean.Tensor Float ByteModel.output)) (prompt : String) (steps : ℕ) : IO String

Greedy byte-level generation from the trained model.

def NN.Examples.Models.Sequence.TextGpt2.interactiveByteLoop (predict : TorchLean.Tensor Float ByteModel.input → IO (TorchLean.Tensor Float ByteModel.output)) (newTokenCount : ℕ) : IO Unit

Terminal prompt loop for the trained byte-level model.

partial def NN.Examples.Models.Sequence.TextGpt2.interactiveByteLoop.loop (predict : TorchLean.Tensor Float ByteModel.input → IO (TorchLean.Tensor Float ByteModel.output)) (newTokenCount : ℕ) (stdin : IO.FS.Stream) : IO Unit

def NN.Examples.Models.Sequence.TextGpt2.BpeModel.vocabularySize : ℕ

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.

instance NN.Examples.Models.Sequence.TextGpt2.BpeModel.instNeZeroNatVocabularySize : NeZero vocabularySize

def NN.Examples.Models.Sequence.TextGpt2.BpeModel.batchSize : ℕ

Batch size for the BPE corpus path.

instance NN.Examples.Models.Sequence.TextGpt2.BpeModel.instNeZeroNatBatchSize : NeZero batchSize

def NN.Examples.Models.Sequence.TextGpt2.BpeModel.contextLength : ℕ

Short context window used by the trainer.

def NN.Examples.Models.Sequence.TextGpt2.BpeModel.attentionHeads : ℕ

Number of attention heads in the miniature BPE Transformer.

def NN.Examples.Models.Sequence.TextGpt2.BpeModel.attentionHeadWidth : ℕ

Per-head width for the BPE Transformer.

def NN.Examples.Models.Sequence.TextGpt2.BpeModel.modelWidth : ℕ

Transformer embedding width.

def NN.Examples.Models.Sequence.TextGpt2.BpeModel.feedForwardWidth : ℕ

Feed-forward hidden width.

def NN.Examples.Models.Sequence.TextGpt2.BpeModel.transformerLayers : ℕ

Number of Transformer blocks.

theorem NN.Examples.Models.Sequence.TextGpt2.BpeModel.instNeZeroNatContextLength : NeZero contextLength

theorem NN.Examples.Models.Sequence.TextGpt2.BpeModel.instNeZeroNatModelWidth : NeZero modelWidth

@[reducible, inline]

abbrev NN.Examples.Models.Sequence.TextGpt2.BpeModel.modelConfig : TorchLean.nn.models.CausalTransformer.Config

BPE GPT configuration shared by shapes and the model constructor.

@[reducible, inline]

abbrev NN.Examples.Models.Sequence.TextGpt2.BpeModel.input : Spec.Shape

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

@[reducible, inline]

abbrev NN.Examples.Models.Sequence.TextGpt2.BpeModel.output : Spec.Shape

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

def NN.Examples.Models.Sequence.TextGpt2.BpeModel.model : TorchLean.nn.Builder (TorchLean.nn.Sequential input output)

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

This TorchLean-native Transformer reads GPT-2 BPE tokenizer files and uses a local output projection over the corpus ids it observes. Its architecture and scale differ from OpenAI GPT-2-small.

Example-local compact vocabulary

def NN.Examples.Models.Sequence.TextGpt2.bpeCorpusSampleAt {tokenCount : ℕ} (tokens : TorchLean.Tensor (Fin BpeModel.vocabularySize) [tokenCount]) (i : ℕ) : TorchLean.Sample.Supervised Float BpeModel.input BpeModel.output

Build one BPE training sample from a tokenized corpus.

def NN.Examples.Models.Sequence.TextGpt2.bpePromptSample (tok : TorchLean.text.GPT2BPE.Tokenizer) (lv : TorchLean.text.VocabularyProjection BpeModel.vocabularySize) (prompt : String) : Except String (TorchLean.Sample.Supervised Float BpeModel.input BpeModel.output)

Turn a BPE prompt into one model input window.

def NN.Examples.Models.Sequence.TextGpt2.decodeLocalBPE {count : ℕ} (tok : TorchLean.text.GPT2BPE.Tokenizer) (lv : TorchLean.text.VocabularyProjection BpeModel.vocabularySize) (ids : TorchLean.Tensor ℕ [count]) : Except String String

Decode projected BPE ids at the tokenizer's serialization boundary.

def NN.Examples.Models.Sequence.TextGpt2.isLocalBPEId (lv : TorchLean.text.VocabularyProjection BpeModel.vocabularySize) (token : Fin BpeModel.vocabularySize) : Bool

Whether a model output id belongs to the compact vocabulary built for this run.

def NN.Examples.Models.Sequence.TextGpt2.argmaxLocalBPETokens (lv : TorchLean.text.VocabularyProjection BpeModel.vocabularySize) (logits : TorchLean.Tensor Float BpeModel.output) : Except String (TorchLean.Tensor ℕ [BpeModel.contextLength])

Decode one batch row while excluding unassigned compact-vocabulary output slots.

def NN.Examples.Models.Sequence.TextGpt2.printBpePredictionProbe (tok : TorchLean.text.GPT2BPE.Tokenizer) (lv : TorchLean.text.VocabularyProjection BpeModel.vocabularySize) (predict : TorchLean.Tensor Float BpeModel.input → IO (TorchLean.Tensor Float BpeModel.output)) (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 : TorchLean.text.GPT2BPE.Tokenizer) (lv : TorchLean.text.VocabularyProjection BpeModel.vocabularySize) (predict : TorchLean.Tensor Float BpeModel.input → IO (TorchLean.Tensor Float BpeModel.output)) (prompt : String) (steps : ℕ) : IO String

Greedy BPE generation by repeatedly feeding the last contextLength 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.interactiveBpeLoop (tok : TorchLean.text.GPT2BPE.Tokenizer) (lv : TorchLean.text.VocabularyProjection BpeModel.vocabularySize) (predict : TorchLean.Tensor Float BpeModel.input → IO (TorchLean.Tensor Float BpeModel.output)) (newTokenCount : ℕ) : IO Unit

Terminal prompt loop for the trained BPE model.

partial def NN.Examples.Models.Sequence.TextGpt2.interactiveBpeLoop.loop (tok : TorchLean.text.GPT2BPE.Tokenizer) (lv : TorchLean.text.VocabularyProjection BpeModel.vocabularySize) (predict : TorchLean.Tensor Float BpeModel.input → IO (TorchLean.Tensor Float BpeModel.output)) (newTokenCount : ℕ) (stdin : IO.FS.Stream) : IO Unit

def NN.Examples.Models.Sequence.TextGpt2.trainCorpus (runtime : TorchLean.Runtime.Config) (trainOpts : Options) (bytes : ByteArray) : IO Unit

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

This materializes only the requested deterministic training schedule, rather than every possible corpus window. 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.loadBpeFileTokens (trainOpts : Options) (tok : TorchLean.text.GPT2BPE.Tokenizer) (path : System.FilePath) : IO (Array ℕ)

Validate, optionally cap, and tokenize one UTF-8 corpus file with GPT-2 BPE.

def NN.Examples.Models.Sequence.TextGpt2.printBpeCorpusPreview {tokenCount : ℕ} (tok : TorchLean.text.GPT2BPE.Tokenizer) (lv : TorchLean.text.VocabularyProjection BpeModel.vocabularySize) (tokens : TorchLean.Tensor ℕ [tokenCount]) : IO Unit

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

def NN.Examples.Models.Sequence.TextGpt2.trainBpeCorpus {tokenCount : ℕ} (runtime : TorchLean.Runtime.Config) (trainOpts : Options) (tok : TorchLean.text.GPT2BPE.Tokenizer) (lv : TorchLean.text.VocabularyProjection BpeModel.vocabularySize) (tokens : TorchLean.Tensor ℕ [tokenCount]) (finetuneTokens? : Option ((count : ℕ) × TorchLean.Tensor ℕ [count])) : 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.