Runtime Supervised Training

Training loops for in-memory datasets and DataLoaders. A list-valued batch means gradient accumulation: every dataset item is differentiated at the same parameter point, the typed gradient packs are averaged, and the optimizer is applied once. An item may itself contain a fixed-size tensor minibatch; use a list batch of one for one vectorized pass in that case.

Gradient accumulation

def TorchLean.Trainer.Manual.Internal.addGradientPacks {α : Type} [Add α] {ss : List Spec.Shape} : Runtime.Autograd.Torch.TList α ss → Runtime.Autograd.Torch.TList α ss → Runtime.Autograd.Torch.TList α ss

Add two shape-aligned gradient packs and materialize every result tensor.

def TorchLean.Trainer.Manual.Internal.scaleGradientPack {α : Type} [Mul α] (c : α) {ss : List Spec.Shape} : Runtime.Autograd.Torch.TList α ss → Runtime.Autograd.Torch.TList α ss

Scale a shape-aligned gradient pack and materialize every result tensor.

def TorchLean.Trainer.Manual.Internal.meanGradients {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Context α] [DecidableEq Spec.Shape] (runner : Runner α task) (batch : List (Runtime.Autograd.Torch.TList α [σ, τ])) : IO (Runtime.Autograd.Torch.TList α (paramShapes task))

Compute mean parameter gradients for a nonempty sample batch at one parameter point.

Mutable model buffers advance before differentiation. Trainable parameters remain fixed until all sample gradients have been collected.

def TorchLean.Trainer.Manual.Internal.meanLossAndGradients {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Context α] [DecidableEq Spec.Shape] (runner : Runner α task) (batch : List (Runtime.Autograd.Torch.TList α [σ, τ])) : IO (α × Runtime.Autograd.Torch.TList α (paramShapes task))

Compute the mean loss and parameter gradients for a nonempty sample batch at one parameter point.

Use this form only when the caller needs the loss value. On CUDA, reading that scalar back to the host synchronizes the device.

def TorchLean.Trainer.Manual.Internal.stepBatch {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Context α] [DecidableEq Spec.Shape] (runner : Runner α task) (opt : Runtime.Autograd.TorchLean.Optimizer α (paramShapes task)) (state : opt.State) (useNativeSingleton : Bool) (batch : List (Runtime.Autograd.Torch.TList α [σ, τ])) : IO opt.State

Apply one optimizer update without reading a loss scalar.

useNativeSingleton is chosen once by the surrounding loop. Keeping it fixed prevents a final partial loader batch from switching between device-resident and host optimizer state.

def TorchLean.Trainer.Manual.Internal.stepBatchAndLoss {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Context α] [DecidableEq Spec.Shape] (runner : Runner α task) (opt : Runtime.Autograd.TorchLean.Optimizer α (paramShapes task)) (state : opt.State) (useNativeSingleton : Bool) (batch : List (Runtime.Autograd.Torch.TList α [σ, τ])) : IO (opt.State × α)

Apply one optimizer update and return the loss from the gradient-producing tapes.

def TorchLean.Trainer.Manual.Internal.runSampleSteps {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Context α] [DecidableEq Spec.Shape] [ToString α] (runner : Runner α task) (cfg : TrainConfig) (nextBatch : IO (List (Runtime.Autograd.Torch.TList α [σ, τ]))) (watchMemory : ℕ → IO Unit) (opt : Runtime.Autograd.TorchLean.Optimizer α (paramShapes task)) (initialState : opt.State) (scheduleState : ℕ → opt.State → opt.State) : IO Unit

Run the fixed-step in-memory loop for one concrete optimizer state type.

In-memory datasets

def TorchLean.Trainer.Manual.trainSamples {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Context α] [DecidableEq Spec.Shape] [ToString α] [Runtime.FromFloat α] (runner : Runner α task) (cfg : TrainConfig) (samples : List (Runtime.Autograd.Torch.TList α [σ, τ])) : IO (TrainReport α)

Train on an in-memory sample list for a fixed number of optimizer updates.

cfg.batchSize controls how many dataset items contribute to each update. It does not multiply the number of optimizer steps. If an item is already a vectorized tensor minibatch, use batchSize := 1 unless you intend to accumulate gradients across several such minibatches.

def TorchLean.Trainer.Manual.trainDataset {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Context α] [DecidableEq Spec.Shape] [ToString α] [Runtime.FromFloat α] (runner : Runner α task) (cfg : TrainConfig) (dataset : Runtime.Autograd.Train.Dataset (Runtime.Autograd.Torch.TList α [σ, τ])) : IO (TrainReport α)

Train over a dataset by materializing its sample list.

Data loaders

def TorchLean.Trainer.Manual.Internal.runLoaderEpochs {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Context α] [DecidableEq Spec.Shape] [ToString α] (runner : Runner α task) (cfg : LoaderTrainConfig) (initialLoader : Runtime.Autograd.Train.DataLoader (Runtime.Autograd.Torch.TList α [σ, τ])) (opt : Runtime.Autograd.TorchLean.Optimizer α (paramShapes task)) (initialState : opt.State) (scheduleState : ℕ → opt.State → opt.State) : IO (Runtime.Autograd.Train.DataLoader (Runtime.Autograd.Torch.TList α [σ, τ]))

Run all loader epochs for one concrete optimizer state type.

def TorchLean.Trainer.Manual.Internal.runLoaderEpochs.trainBatches {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Context α] [DecidableEq Spec.Shape] [ToString α] (runner : Runner α task) (cfg : LoaderTrainConfig) (opt : Runtime.Autograd.TorchLean.Optimizer α (paramShapes task)) (useNativeSingleton : Bool) (stepIdx : ℕ) (state : opt.State) (batches : List (List (Runtime.Autograd.Torch.TList α [σ, τ]))) : IO (ℕ × opt.State)

def TorchLean.Trainer.Manual.Internal.runLoaderEpochs.trainEpochs {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Context α] [DecidableEq Spec.Shape] [ToString α] (runner : Runner α task) (cfg : LoaderTrainConfig) (opt : Runtime.Autograd.TorchLean.Optimizer α (paramShapes task)) (scheduleState : ℕ → opt.State → opt.State) (useNativeSingleton : Bool) (epoch remaining stepIdx : ℕ) (loader : Runtime.Autograd.Train.DataLoader (Runtime.Autograd.Torch.TList α [σ, τ])) (state : opt.State) : IO (Runtime.Autograd.Train.DataLoader (Runtime.Autograd.Torch.TList α [σ, τ]))

def TorchLean.Trainer.Manual.trainLoader {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Context α] [DecidableEq Spec.Shape] [ToString α] [Runtime.FromFloat α] (runner : Runner α task) (cfg : LoaderTrainConfig) (dl : Runtime.Autograd.Train.DataLoader (Runtime.Autograd.Torch.TList α [σ, τ])) : IO (TrainReport α × Runtime.Autograd.Train.DataLoader (Runtime.Autograd.Torch.TList α [σ, τ]))

Train over a DataLoader.

Every loader batch contributes one averaged-gradient optimizer update. The scheduler advances once per epoch.