Runtime Supervised Training

Supervised tasks, runners, steppers, optimizer configs, trainer aliases, and the low-level session exports that back executable examples.

Stateful training steps

structure TorchLean.Trainer.Manual.Stepper (α : Type) [Context α] [DecidableEq Spec.Shape] {σ τ : Spec.Shape} (task : SeqTask σ τ) : Type

Stateful training loop object: a Runner plus an optimizer state and a step counter. It packages the model runner with the state needed to step on successive batches.

• runner : Runner α task

  Underlying task runner (module + compiled forward artifacts/losses).

• stepSample : Runtime.Autograd.Torch.TList α [σ, τ] → IO α

  Run a single optimization step on one supervised sample, returning the loss value.

• epochSamples : List (Runtime.Autograd.Torch.TList α [σ, τ]) → IO (List α)

  Run an epoch over an explicit list of samples, returning the per-step loss values.

• stepCount : IO ℕ

  Read the total number of stepSample calls performed so far.

def TorchLean.Trainer.Manual.stepper {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Context α] [DecidableEq Spec.Shape] [ToString α] [Runtime.FromFloat α] (runner : Runner α task) (optimizer : OptimizerConfig) (scheduler : Option Scheduler.Config := none) : IO (Stepper α task)

Construct a Stepper for a runner, optimizer config, and optional scheduler.

This is the recommended way to build custom training loops without reimplementing the optimizer logic: call stepper, then choose stepSample for single batches or epochSamples for explicit sample lists.

def TorchLean.Trainer.Manual.step {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Context α] [DecidableEq Spec.Shape] (loop : Stepper α task) (sample : Runtime.Autograd.Torch.TList α [σ, τ]) : IO α

Run one optimization step on a single supervised sample.

def TorchLean.Trainer.Manual.epoch {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Context α] [DecidableEq Spec.Shape] (loop : Stepper α task) (samples : List (Runtime.Autograd.Torch.TList α [σ, τ])) : IO (List α)

Run one epoch over a list of supervised samples, returning the per-step losses.