Runtime Supervised Training

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

inductive NN.API.TorchLean.Supervised.SeqLoss : Type

Built-in loss choices for SeqTask.

• mse (reduction : Loss.Reduction := Runtime.Autograd.TorchLean.Loss.Reduction.mean) : SeqLoss
• crossEntropyOneHot (reduction : Loss.Reduction := Runtime.Autograd.TorchLean.Loss.Reduction.mean) : SeqLoss

structure NN.API.TorchLean.Supervised.SeqTask (σ τ : Spec.Shape) : Type 2

A supervised task is just a model plus a choice of loss.

• model : NN.Seq σ τ

  Model to run.

• loss : SeqLoss

  Loss function.

def NN.API.TorchLean.Supervised.SeqTask.moduleDefWithMode {σ τ : Spec.Shape} (task : SeqTask σ τ) (mode : NN.Mode) : Runtime.Autograd.TorchLean.ScalarModuleDef task.model.paramShapes [σ, τ]

Build a ScalarModuleDef for a task, choosing an explicit model mode (train/eval).

This is the underlying "instantiate me as a runnable module" step for training.

def NN.API.TorchLean.Supervised.SeqTask.moduleDef {σ τ : Spec.Shape} (task : SeqTask σ τ) : Runtime.Autograd.TorchLean.ScalarModuleDef task.model.paramShapes [σ, τ]

Default module definition for a task (training mode).

def NN.API.TorchLean.Supervised.SeqTask.mse {σ τ : Spec.Shape} (model : NN.Seq σ τ) (reduction : Loss.Reduction := Runtime.Autograd.TorchLean.Loss.Reduction.mean) : SeqTask σ τ

Constructor: regression task (MSE loss).

def NN.API.TorchLean.Supervised.SeqTask.crossEntropyOneHot {σ τ : Spec.Shape} (model : NN.Seq σ τ) (reduction : Loss.Reduction := Runtime.Autograd.TorchLean.Loss.Reduction.mean) : SeqTask σ τ

Constructor: one-hot classification task (cross-entropy loss).

@[reducible, inline]

abbrev NN.API.TorchLean.Supervised.paramShapes {σ τ : Spec.Shape} (task : SeqTask σ τ) : List Spec.Shape

Parameter shapes for a task (delegates to Seq.paramShapes).

inductive NN.API.TorchLean.Supervised.OptimizerConfig : Type

Optimizer hyperparameter configuration for the supervised training helpers.

This configuration covers the optimizer choices exposed by the public training helpers. It mirrors a few common PyTorch optimizers by name/defaults, but it does not try to cover the full option surface of torch.optim.*.

• sgd (lr : Float) (momentum : Float := 0.0) : OptimizerConfig

  SGD optimizer config.

  PyTorch analogy: torch.optim.SGD(..., lr=..., momentum=...) when momentum > 0, and plain SGD when momentum = 0.

• adam (lr : Float) (beta1 : Float := 0.9) (beta2 : Float := 0.999) (epsilon : Float := 1e-8) : OptimizerConfig

  Adam optimizer config.

• adamw (lr : Float) (weightDecay : Float := 1e-2) (beta1 : Float := 0.9) (beta2 : Float := 0.999) (epsilon : Float := 1e-8) : OptimizerConfig

  AdamW optimizer config (decoupled weight decay).

def NN.API.TorchLean.Supervised.instReprOptimizerConfig.repr : OptimizerConfig → ℕ → Std.Format

@[implicit_reducible]

instance NN.API.TorchLean.Supervised.instReprOptimizerConfig : Repr OptimizerConfig

structure NN.API.TorchLean.Supervised.TrainConfig : Type

Step-based training configuration for trainSamples / trainDataset.

Fields:

• steps: number of parameter updates,
• batchSize: number of samples consumed by one public step for in-memory datasets,
• optimizer: optimizer hyperparameters,
• scheduler: optional learning-rate schedule (applied per step),
• logEvery: progress printing frequency (0 disables logging).

• steps : ℕ

  Number of training steps.

• batchSize : ℕ

  Number of samples consumed by one public training step.

  The in-memory supervised loop applies one optimizer update per sample in the group, while reporting/logging at the outer step cadence. Loader-backed training uses the loader batches directly.

• optimizer : OptimizerConfig

  Optimizer configuration.

• scheduler : Option Schedulers.Config

  Scheduler configuration.

• logEvery : ℕ

  Log once every this many steps.

def NN.API.TorchLean.Supervised.instReprTrainConfig.repr : TrainConfig → ℕ → Std.Format

@[implicit_reducible]

instance NN.API.TorchLean.Supervised.instReprTrainConfig : Repr TrainConfig

structure NN.API.TorchLean.Supervised.TrainReport (α : Type) : Type

Small summary returned by lower training helpers.

By default, before and after are mean loss values, but the type is polymorphic so callers can report other scalars in the same shape.

• before : α

  Metrics before training.

• after : α

  Metrics after training.

structure NN.API.TorchLean.Supervised.LoaderTrainConfig : Type

Epoch-based training configuration for trainLoader (data-loader training).

Fields:

• epochs: number of epochs (each epoch iterates once over the loader),
• optimizer: optimizer hyperparameters,
• scheduler: optional learning-rate schedule (applied per step/epoch depending on helper),
• logEvery: progress printing frequency (0 disables logging).

• epochs : ℕ

  Number of epochs to train for.

• optimizer : OptimizerConfig

  Optimizer configuration.

• scheduler : Option Schedulers.Config

  Scheduler configuration.

• logEvery : ℕ

  Log once every this many steps.

def NN.API.TorchLean.Supervised.instReprLoaderTrainConfig.repr : LoaderTrainConfig → ℕ → Std.Format

@[implicit_reducible]

instance NN.API.TorchLean.Supervised.instReprLoaderTrainConfig : Repr LoaderTrainConfig

def NN.API.TorchLean.Supervised.optimizerLR : OptimizerConfig → Float

Extract the base learning rate encoded in an optimizer configuration.

def NN.API.TorchLean.Supervised.stepLR (scheduler : Option Schedulers.Config) (cfg : OptimizerConfig) (step : ℕ) : Float

Resolve the learning rate to use at a given training step.

If a scheduler is present, it takes precedence over the optimizer's baked-in base learning rate. Otherwise this simply returns optimizerLR cfg.

def NN.API.TorchLean.Supervised.mapStateList {State : Type → Spec.Shape → Type} {α : Type} {ss : List Spec.Shape} : ({s : Spec.Shape} → State α s → State α s) → Runtime.Autograd.TorchLean.StateList State α ss → Runtime.Autograd.TorchLean.StateList State α ss

Map a state update over every optimizer-state entry in a shape-indexed parameter list.

def NN.API.TorchLean.Supervised.adamStateWithLR {α : Type} (lr : α) {paramShapes : List Spec.Shape} : Runtime.Autograd.TorchLean.StateList Optim.Adam.State α paramShapes → Runtime.Autograd.TorchLean.StateList Optim.Adam.State α paramShapes

Set the learning rate field of every Adam optimizer state entry to lr.

def NN.API.TorchLean.Supervised.momentumSGDStateWithLR {α : Type} (lr : α) {paramShapes : List Spec.Shape} : Runtime.Autograd.TorchLean.StateList Optim.MomentumSGD.State α paramShapes → Runtime.Autograd.TorchLean.StateList Optim.MomentumSGD.State α paramShapes

Set the learning rate field of every momentum-SGD optimizer state entry to lr.

def NN.API.TorchLean.Supervised.adamwStateWithLR {α : Type} (lr : α) {paramShapes : List Spec.Shape} : Runtime.Autograd.TorchLean.StateList Optim.AdamW.State α paramShapes → Runtime.Autograd.TorchLean.StateList Optim.AdamW.State α paramShapes

Set the learning rate field of every AdamW optimizer state entry to lr.

structure NN.API.TorchLean.Supervised.Runner (α : Type) [Semantics.Scalar α] [DecidableEq Spec.Shape] {σ τ : Spec.Shape} (task : SeqTask σ τ) : Type

A fully instantiated supervised task runner.

This bundles:

• the imperative ScalarModule (parameters/buffers stored in refs),
• compiled predictors and loss functions for both .train and .eval modes (so switching mode is low-overhead),
• and the current mode stored in an IO.Ref.

The mode influences both operator behavior (e.g. dropout/batchnorm) and whether buffers are updated during training.

• module : Runtime.Autograd.TorchLean.ScalarModule α (paramShapes task) [σ, τ]

  Instantiated scalar module storing parameters/buffers in mutable refs.

• predictorTrain : CompiledOut α (paramShapes task ++ [σ]) τ

  Compiled forward predictor specialized to training-mode behavior.

• predictorEval : CompiledOut α (paramShapes task ++ [σ]) τ

  Compiled forward predictor specialized to eval-mode behavior.

• lossTrain : CompiledScalar α (paramShapes task ++ [σ, τ])

  Compiled loss function for training-mode behavior.

• lossEval : CompiledScalar α (paramShapes task ++ [σ, τ])

  Compiled loss function for eval-mode behavior.

• mode : IO.Ref NN.Mode

  Mutable mode flag (.train / .eval) used by stateful layers (e.g. dropout/batchnorm).

def NN.API.TorchLean.Supervised.instantiateWithOptions {σ τ : Spec.Shape} (task : SeqTask σ τ) {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] [Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α] (cast : Float → α) (opts : Options := { }) : IO (Runner α task)

Instantiate a Runner by explicitly providing a Float → α cast and backend.

Use this when you want to run the same task over different numeric backends (e.g. Float vs IEEE32Exec) or when you want custom literal injection.

def NN.API.TorchLean.Supervised.instantiateWith {σ τ : Spec.Shape} (task : SeqTask σ τ) {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] [Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α] (cast : Float → α) (backend : Backend := Runtime.Autograd.Torch.Backend.eager) : IO (Runner α task)

Instantiate a Runner by explicitly providing a Float → α cast and a backend selector.

Instantiate a module with explicit runtime options.

def NN.API.TorchLean.Supervised.instantiateWithRuntimeOptions {σ τ : Spec.Shape} (task : SeqTask σ τ) {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] [Runtime.Scalar α] [Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α] (opts : Options := { }) : IO (Runner α task)

Instantiate a Runner using the standard runtime literal injection API.Runtime.ofFloat.

This is the common entrypoint for executable examples.

def NN.API.TorchLean.Supervised.instantiate {σ τ : Spec.Shape} (task : SeqTask σ τ) {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] [Runtime.Scalar α] [Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α] (backend : Backend := Runtime.Autograd.Torch.Backend.eager) : IO (Runner α task)

Instantiate a Runner using the standard runtime literal injection API.Runtime.ofFloat and a backend selector.

Instantiate a module after parsing runtime options.

def NN.API.TorchLean.Supervised.run {σ τ : Spec.Shape} (task : SeqTask σ τ) (args : List String) (k : {α : Type} → [inst : Semantics.Scalar α] → [inst_1 : DecidableEq Spec.Shape] → [ToString α] → [Runtime.Scalar α] → Runner α task → List String → IO Unit) : IO Unit

Run a TorchLean task with CLI-style dtype/backend selection, then call k with a fully constructed runner.

This is used by lake exe entrypoints: run takes care of parsing dtype flags and instantiating the underlying module/compiled programs.

def NN.API.TorchLean.Supervised.params {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] (runner : Runner α task) : IO (TensorPack α (paramShapes task))

Read the current parameter list from a runner.

def NN.API.TorchLean.Supervised.mode {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] (runner : Runner α task) : IO NN.Mode

Read the runner's current mode (.train or .eval).

def NN.API.TorchLean.Supervised.setMode {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] (runner : Runner α task) (value : NN.Mode) : IO Unit

Set the runner mode (.train or .eval).

def NN.API.TorchLean.Supervised.trainMode {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] (runner : Runner α task) : IO Unit

Convenience: setMode runner .train.

def NN.API.TorchLean.Supervised.evalMode {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] (runner : Runner α task) : IO Unit

Convenience: setMode runner .eval.

def NN.API.TorchLean.Supervised.isTraining {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] (runner : Runner α task) : IO Bool

Predicate: are we in training mode?

def NN.API.TorchLean.Supervised.activePredictor {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] (runner : Runner α task) : IO (CompiledOut α (paramShapes task ++ [σ]) τ)

Pick the predictor compiled for the runner's current mode (.train or .eval).

def NN.API.TorchLean.Supervised.activeLoss {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] (runner : Runner α task) : IO (CompiledScalar α (paramShapes task ++ [σ, τ]))

Pick the loss program compiled for the runner's current mode (.train or .eval).

def NN.API.TorchLean.Supervised.updateRunnerBuffers {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] (runner : Runner α task) (sample : TensorPack α [σ, τ]) : IO Unit

Refresh mode-dependent runner buffers using one supervised sample.

This mutates the module parameters only in .train mode, mirroring PyTorch-style buffer updates for layers such as normalization. In .eval mode it is a no-op.

def NN.API.TorchLean.Supervised.backward {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] (runner : Runner α task) (sample : TensorPack α [σ, τ]) : IO (TensorPack α (paramShapes task))

Run one forward/backward pass on a single supervised sample and return gradients for all parameters.

This is the TorchLean analogue of the loss.backward() payload in PyTorch, except TorchLean returns the gradients explicitly instead of storing them in .grad fields.

def NN.API.TorchLean.Supervised.predict {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] (runner : Runner α task) (x : Spec.Tensor α σ) : IO (Spec.Tensor α τ)

Predict on one input tensor using the runner's active mode (.train or .eval).

def NN.API.TorchLean.Supervised.predictBatch {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] (runner : Runner α task) (xs : List (Spec.Tensor α σ)) : IO (List (Spec.Tensor α τ))

Predict on a list of inputs by repeatedly calling predict.

def NN.API.TorchLean.Supervised.predictClass? {σ : Spec.Shape} {n : ℕ} {task : SeqTask σ (Spec.Shape.dim n Spec.Shape.scalar)} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] (runner : Runner α task) (x : Spec.Tensor α σ) : IO (Option (Fin n))

For classification heads: run predict, then take argmax over the logits (if defined).

def NN.API.TorchLean.Supervised.accuracyOneHot {σ : Spec.Shape} {n : ℕ} {task : SeqTask σ (Spec.Shape.dim n Spec.Shape.scalar)} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] (runner : Runner α task) (samples : List (TensorPack α [σ, Spec.Shape.dim n Spec.Shape.scalar])) : IO (ℕ × ℕ)

Compute (correct, total) for a one-hot classification dataset.

def NN.API.TorchLean.Supervised.accuracyOneHot.go {σ : Spec.Shape} {n : ℕ} {task : SeqTask σ (Spec.Shape.dim n Spec.Shape.scalar)} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] (runner : Runner α task) (correct total : ℕ) : List (TensorPack α [σ, Spec.Shape.dim n Spec.Shape.scalar]) → IO (ℕ × ℕ)

def NN.API.TorchLean.Supervised.meanLoss {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] [ToString α] (runner : Runner α task) (samples : List (TensorPack α [σ, τ])) : IO α

Mean scalar loss over a list of supervised samples (uses the runner's active mode).

def NN.API.TorchLean.Supervised.meanLossDataset {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] [ToString α] (runner : Runner α task) (dataset : Runtime.Autograd.Train.Dataset (TensorPack α [σ, τ])) : IO α

Mean scalar loss over a dataset (materialized via dataset.toList).

def NN.API.TorchLean.Supervised.moduleLoss {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] (runner : Runner α task) (sample : TensorPack α [σ, τ]) : IO α

Scalar loss for one sample through the instantiated runtime module.

def NN.API.TorchLean.Supervised.effectiveTrainBatchSize (n : ℕ) : ℕ

Treat 0 as the conservative single-sample step size.

def NN.API.TorchLean.Supervised.nextCyclicBatch {α : Type} (context : String) (samples : List α) (restRef : IO.Ref (List α)) (batchSize : ℕ) : IO (List α)

Take the next cyclic group of samples from an in-memory training set.

def NN.API.TorchLean.Supervised.trainSamples {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] [ToString α] [Runtime.Scalar α] (runner : Runner α task) (cfg : TrainConfig) (samples : List (TensorPack α [σ, τ])) : IO (TrainReport α)

Train on a small in-memory list of supervised samples for a fixed number of steps.

This is the simplest training-loop helper: it is intended for examples and small synthetic datasets. For loader-based training, see trainLoader.

def NN.API.TorchLean.Supervised.trainDataset {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] [ToString α] [Runtime.Scalar α] (runner : Runner α task) (cfg : TrainConfig) (dataset : Runtime.Autograd.Train.Dataset (TensorPack α [σ, τ])) : IO (TrainReport α)

Train over a dataset by materializing it as a list.

def NN.API.TorchLean.Supervised.trainLoader {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] [ToString α] [Runtime.Scalar α] (runner : Runner α task) (cfg : LoaderTrainConfig) (dl : Runtime.Autograd.Train.DataLoader (TensorPack α [σ, τ])) : IO (TrainReport α × Runtime.Autograd.Train.DataLoader (TensorPack α [σ, τ]))

Train over a DataLoader for cfg.epochs epochs, returning the final report and updated loader.

This corresponds to the common PyTorch pattern: for epoch in ...: for batch in loader: step(batch).

def NN.API.TorchLean.Supervised.trainLoader.trainSgdBatches {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] [Runtime.Scalar α] (runner : Runner α task) (cfg : LoaderTrainConfig) (epoch : ℕ) (batches : List (List (TensorPack α [σ, τ]))) : IO Unit

def NN.API.TorchLean.Supervised.trainLoader.runSgdEpochs {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] [Runtime.Scalar α] (runner : Runner α task) (cfg : LoaderTrainConfig) (nextEpoch : Runtime.Autograd.Train.DataLoader (TensorPack α [σ, τ]) → IO (Runtime.Autograd.Train.DataLoader (TensorPack α [σ, τ]) × List (List (TensorPack α [σ, τ])))) (remaining epoch : ℕ) (loader : Runtime.Autograd.Train.DataLoader (TensorPack α [σ, τ])) : IO (Runtime.Autograd.Train.DataLoader (TensorPack α [σ, τ]))

def NN.API.TorchLean.Supervised.trainLoader.trainMomSamples {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] [ToString α] [Runtime.Scalar α] (runner : Runner α task) (cfg : LoaderTrainConfig) (lr momentum : Float) (epoch stepIdx : ℕ) (state : (Runtime.Autograd.TorchLean.momentumSGD (Runtime.ofFloat lr) (Runtime.ofFloat momentum)).State) (samples : List (TensorPack α [σ, τ])) : have opt := Runtime.Autograd.TorchLean.momentumSGD (Runtime.ofFloat lr) (Runtime.ofFloat momentum); IO (opt.State × ℕ)

def NN.API.TorchLean.Supervised.trainLoader.trainMomBatches {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] [ToString α] [Runtime.Scalar α] (runner : Runner α task) (cfg : LoaderTrainConfig) (lr momentum : Float) (epoch stepIdx : ℕ) (state : (Runtime.Autograd.TorchLean.momentumSGD (Runtime.ofFloat lr) (Runtime.ofFloat momentum)).State) (batches : List (List (TensorPack α [σ, τ]))) : have opt := Runtime.Autograd.TorchLean.momentumSGD (Runtime.ofFloat lr) (Runtime.ofFloat momentum); IO (opt.State × ℕ)

def NN.API.TorchLean.Supervised.trainLoader.runMomEpochs {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] [ToString α] [Runtime.Scalar α] (runner : Runner α task) (cfg : LoaderTrainConfig) (nextEpoch : Runtime.Autograd.Train.DataLoader (TensorPack α [σ, τ]) → IO (Runtime.Autograd.Train.DataLoader (TensorPack α [σ, τ]) × List (List (TensorPack α [σ, τ])))) (lr momentum : Float) (epoch remaining : ℕ) (loader : Runtime.Autograd.Train.DataLoader (TensorPack α [σ, τ])) (st : (Runtime.Autograd.TorchLean.momentumSGD (Runtime.ofFloat lr) (Runtime.ofFloat momentum)).State) : have opt := Runtime.Autograd.TorchLean.momentumSGD (Runtime.ofFloat lr) (Runtime.ofFloat momentum); IO (Runtime.Autograd.Train.DataLoader (TensorPack α [σ, τ]) × opt.State)

def NN.API.TorchLean.Supervised.trainLoader.trainAdamSamples {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] [ToString α] [Runtime.Scalar α] (runner : Runner α task) (cfg : LoaderTrainConfig) (lr beta1 beta2 epsilon : Float) (epoch stepIdx : ℕ) (state : (Runtime.Autograd.TorchLean.adam (Runtime.ofFloat lr) (Runtime.ofFloat beta1) (Runtime.ofFloat beta2) (Runtime.ofFloat epsilon)).State) (samples : List (TensorPack α [σ, τ])) : have opt := Runtime.Autograd.TorchLean.adam (Runtime.ofFloat lr) (Runtime.ofFloat beta1) (Runtime.ofFloat beta2) (Runtime.ofFloat epsilon); IO (opt.State × ℕ)

def NN.API.TorchLean.Supervised.trainLoader.trainAdamBatches {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] [ToString α] [Runtime.Scalar α] (runner : Runner α task) (cfg : LoaderTrainConfig) (lr beta1 beta2 epsilon : Float) (epoch stepIdx : ℕ) (state : (Runtime.Autograd.TorchLean.adam (Runtime.ofFloat lr) (Runtime.ofFloat beta1) (Runtime.ofFloat beta2) (Runtime.ofFloat epsilon)).State) (batches : List (List (TensorPack α [σ, τ]))) : have opt := Runtime.Autograd.TorchLean.adam (Runtime.ofFloat lr) (Runtime.ofFloat beta1) (Runtime.ofFloat beta2) (Runtime.ofFloat epsilon); IO (opt.State × ℕ)

def NN.API.TorchLean.Supervised.trainLoader.runAdamEpochs {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] [ToString α] [Runtime.Scalar α] (runner : Runner α task) (cfg : LoaderTrainConfig) (nextEpoch : Runtime.Autograd.Train.DataLoader (TensorPack α [σ, τ]) → IO (Runtime.Autograd.Train.DataLoader (TensorPack α [σ, τ]) × List (List (TensorPack α [σ, τ])))) (lr beta1 beta2 epsilon : Float) (epoch remaining : ℕ) (loader : Runtime.Autograd.Train.DataLoader (TensorPack α [σ, τ])) (st : (Runtime.Autograd.TorchLean.adam (Runtime.ofFloat lr) (Runtime.ofFloat beta1) (Runtime.ofFloat beta2) (Runtime.ofFloat epsilon)).State) : have opt := Runtime.Autograd.TorchLean.adam (Runtime.ofFloat lr) (Runtime.ofFloat beta1) (Runtime.ofFloat beta2) (Runtime.ofFloat epsilon); IO (Runtime.Autograd.Train.DataLoader (TensorPack α [σ, τ]) × opt.State)

def NN.API.TorchLean.Supervised.trainLoader.trainAdamWSamples {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] [ToString α] [Runtime.Scalar α] (runner : Runner α task) (cfg : LoaderTrainConfig) (lr weightDecay beta1 beta2 epsilon : Float) (epoch stepIdx : ℕ) (state : (Runtime.Autograd.TorchLean.adamw (Runtime.ofFloat lr) (Runtime.ofFloat weightDecay) (Runtime.ofFloat beta1) (Runtime.ofFloat beta2) (Runtime.ofFloat epsilon)).State) (samples : List (TensorPack α [σ, τ])) : have opt := Runtime.Autograd.TorchLean.adamw (Runtime.ofFloat lr) (Runtime.ofFloat weightDecay) (Runtime.ofFloat beta1) (Runtime.ofFloat beta2) (Runtime.ofFloat epsilon); IO (opt.State × ℕ)

def NN.API.TorchLean.Supervised.trainLoader.trainAdamWBatches {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] [ToString α] [Runtime.Scalar α] (runner : Runner α task) (cfg : LoaderTrainConfig) (lr weightDecay beta1 beta2 epsilon : Float) (epoch stepIdx : ℕ) (state : (Runtime.Autograd.TorchLean.adamw (Runtime.ofFloat lr) (Runtime.ofFloat weightDecay) (Runtime.ofFloat beta1) (Runtime.ofFloat beta2) (Runtime.ofFloat epsilon)).State) (batches : List (List (TensorPack α [σ, τ]))) : have opt := Runtime.Autograd.TorchLean.adamw (Runtime.ofFloat lr) (Runtime.ofFloat weightDecay) (Runtime.ofFloat beta1) (Runtime.ofFloat beta2) (Runtime.ofFloat epsilon); IO (opt.State × ℕ)

def NN.API.TorchLean.Supervised.trainLoader.runAdamWEpochs {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] [ToString α] [Runtime.Scalar α] (runner : Runner α task) (cfg : LoaderTrainConfig) (nextEpoch : Runtime.Autograd.Train.DataLoader (TensorPack α [σ, τ]) → IO (Runtime.Autograd.Train.DataLoader (TensorPack α [σ, τ]) × List (List (TensorPack α [σ, τ])))) (lr weightDecay beta1 beta2 epsilon : Float) (epoch remaining : ℕ) (loader : Runtime.Autograd.Train.DataLoader (TensorPack α [σ, τ])) (st : (Runtime.Autograd.TorchLean.adamw (Runtime.ofFloat lr) (Runtime.ofFloat weightDecay) (Runtime.ofFloat beta1) (Runtime.ofFloat beta2) (Runtime.ofFloat epsilon)).State) : have opt := Runtime.Autograd.TorchLean.adamw (Runtime.ofFloat lr) (Runtime.ofFloat weightDecay) (Runtime.ofFloat beta1) (Runtime.ofFloat beta2) (Runtime.ofFloat epsilon); IO (Runtime.Autograd.Train.DataLoader (TensorPack α [σ, τ]) × opt.State)

structure NN.API.TorchLean.Supervised.Stepper (α : Type) [Semantics.Scalar α] [DecidableEq Spec.Shape] {σ τ : Spec.Shape} (task : SeqTask σ τ) : Type

Stateful training loop object: a Runner plus an optimizer state and a step counter.

This is the TorchLean analogue of holding a PyTorch optimizer object plus the model, ready to step() on batches.

• runner : Runner α task

  Underlying task runner (module + compiled predictors/losses).

• stepSample : TensorPack α [σ, τ] → IO α

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

• epochSamples : List (TensorPack α [σ, τ]) → 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 NN.API.TorchLean.Supervised.stepper {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] [ToString α] [Runtime.Scalar α] (runner : Runner α task) (optimizer : OptimizerConfig) (scheduler : Option Schedulers.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 NN.API.TorchLean.Supervised.step {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] (loop : Stepper α task) (sample : TensorPack α [σ, τ]) : IO α

Run one optimization step on a single supervised sample.

def NN.API.TorchLean.Supervised.epoch {σ τ : Spec.Shape} {task : SeqTask σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] (loop : Stepper α task) (samples : List (TensorPack α [σ, τ])) : IO (List α)

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

NN.API.TorchLean.Trainer is the stable public namespace for supervised training machinery.

Usage note:

If you are writing ordinary model code, prefer the NN umbrella: import NN; open TorchLean; Trainer.new .... This namespace is the lower runtime layer underneath that facade, and it exposes lower-level controls for custom training loops.

The intended workflow is:

• pick a Task (regression / classification),
• call instantiate to get a Runner (parameters + buffers + backend state),
• call trainSamples / trainDataset / trainLoader, or build a Stepper for custom loops.

This API is backend-agnostic: the same code can run in .eager mode or via a compiled backend, depending on the backend argument passed to instantiate.

@[reducible, inline]

abbrev NN.API.TorchLean.Trainer.Task (σ τ : Spec.Shape) : Type 2

A supervised task is just a model plus a choice of loss.

@[reducible, inline]

abbrev NN.API.TorchLean.Trainer.Runner (α : Type) [Semantics.Scalar α] [DecidableEq Spec.Shape] {σ τ : Spec.Shape} (task : Supervised.SeqTask σ τ) : Type

A fully instantiated supervised task runner.

This bundles:

• the imperative ScalarModule (parameters/buffers stored in refs),
• compiled predictors and loss functions for both .train and .eval modes (so switching mode is low-overhead),
• and the current mode stored in an IO.Ref.

The mode influences both operator behavior (e.g. dropout/batchnorm) and whether buffers are updated during training.

@[reducible, inline]

abbrev NN.API.TorchLean.Trainer.Optimizer : Type

Optimizer hyperparameter configuration for the supervised training helpers.

This configuration covers the optimizer choices exposed by the public training helpers. It mirrors a few common PyTorch optimizers by name/defaults, but it does not try to cover the full option surface of torch.optim.*.

@[reducible, inline]

abbrev NN.API.TorchLean.Trainer.TrainConfig : Type

Step-based training configuration for trainSamples / trainDataset.

Fields:

• steps: number of parameter updates,
• batchSize: number of samples consumed by one public step for in-memory datasets,
• optimizer: optimizer hyperparameters,
• scheduler: optional learning-rate schedule (applied per step),
• logEvery: progress printing frequency (0 disables logging).

@[reducible, inline]

abbrev NN.API.TorchLean.Trainer.LoaderTrainConfig : Type

Epoch-based training configuration for trainLoader (data-loader training).

Fields:

• epochs: number of epochs (each epoch iterates once over the loader),
• optimizer: optimizer hyperparameters,
• scheduler: optional learning-rate schedule (applied per step/epoch depending on helper),
• logEvery: progress printing frequency (0 disables logging).

@[reducible, inline]

abbrev NN.API.TorchLean.Trainer.TrainReport (α : Type) : Type

Small summary returned by lower training helpers.

By default, before and after are mean loss values, but the type is polymorphic so callers can report other scalars in the same shape.

@[reducible, inline]

abbrev NN.API.TorchLean.Trainer.Stepper (α : Type) [Semantics.Scalar α] [DecidableEq Spec.Shape] {σ τ : Spec.Shape} (task : Supervised.SeqTask σ τ) : Type

Stateful training loop object: a Runner plus an optimizer state and a step counter.

This is the TorchLean analogue of holding a PyTorch optimizer object plus the model, ready to step() on batches.

def NN.API.TorchLean.Trainer.runtimeRegressionTask {σ τ : Spec.Shape} (model : NN.Seq σ τ) (reduction : Loss.Reduction := Runtime.Autograd.TorchLean.Loss.Reduction.mean) : Task σ τ

Lower-runtime regression task with mean-squared error loss by default.

def NN.API.TorchLean.Trainer.runtimeClassifierTask {σ τ : Spec.Shape} (model : NN.Seq σ τ) (reduction : Loss.Reduction := Runtime.Autograd.TorchLean.Loss.Reduction.mean) : Task σ τ

Lower-runtime classifier task with cross-entropy loss by default.

def NN.API.TorchLean.Trainer.sgd (lr : Float) (momentum : Float := 0.0) : Optimizer

SGD optimizer config.

PyTorch analogue: torch.optim.SGD (https://pytorch.org/docs/stable/generated/torch.optim.SGD.html).

def NN.API.TorchLean.Trainer.momentumSGD (lr : Float) (momentum : Float := 0.9) : Optimizer

Momentum SGD optimizer config. Pass lr and optionally override momentum.

def NN.API.TorchLean.Trainer.adam (lr : Float) (beta1 : Float := 0.9) (beta2 : Float := 0.999) (epsilon : Float := 1e-8) : Optimizer

Adam optimizer config. Pass lr; override beta1, beta2, or epsilon when the run needs it.

PyTorch analogue: torch.optim.Adam (https://pytorch.org/docs/stable/generated/torch.optim.Adam.html).

def NN.API.TorchLean.Trainer.adamw (lr : Float) (weightDecay : Float := 1e-2) (beta1 : Float := 0.9) (beta2 : Float := 0.999) (epsilon : Float := 1e-8) : Optimizer

AdamW optimizer config. Pass lr; override weight decay or moment parameters when the run needs it.

PyTorch analogue: torch.optim.AdamW (https://pytorch.org/docs/stable/generated/torch.optim.AdamW.html).

inductive NN.API.TorchLean.Trainer.OptimizerKind : Type

Optimizer algorithm accepted by simple CLI commands that expose a --optim flag.

• sgd : OptimizerKind

  Stochastic gradient descent.

• adam : OptimizerKind

  Adam with TorchLean's usual public defaults.

• adamw : OptimizerKind

  AdamW with decoupled weight decay.

@[implicit_reducible]

instance NN.API.TorchLean.Trainer.instDecidableEqOptimizerKind : DecidableEq OptimizerKind

@[implicit_reducible]

instance NN.API.TorchLean.Trainer.instReprOptimizerKind : Repr OptimizerKind

def NN.API.TorchLean.Trainer.instReprOptimizerKind.repr : OptimizerKind → ℕ → Std.Format

def NN.API.TorchLean.Trainer.OptimizerKind.parse (s : String) : Except String OptimizerKind

Parse an optimizer name accepted by a command-line --optim flag.

def NN.API.TorchLean.Trainer.OptimizerKind.name : OptimizerKind → String

Human-readable optimizer name used in logs.

def NN.API.TorchLean.Trainer.OptimizerKind.toOptimizer (kind : OptimizerKind) (lr : Float) : Optimizer

Build a public optimizer config for this optimizer kind and learning rate.

def NN.API.TorchLean.Trainer.steps (count : ℕ) (optimizer : Optimizer := sgd 1e-2) (logEvery : ℕ := 1) : TrainConfig

Fixed-step training config over an in-memory sample list or dataset.

def NN.API.TorchLean.Trainer.epochs (count : ℕ) (optimizer : Optimizer := sgd 1e-2) (logEvery : ℕ := 1) : LoaderTrainConfig

Epoch-based training config over a data loader.

def NN.API.TorchLean.Trainer.withScheduler (cfg : TrainConfig) (scheduler : Schedulers.Config) : TrainConfig

Attach a scheduler to a step-based training config.

def NN.API.TorchLean.Trainer.withEpochScheduler (cfg : LoaderTrainConfig) (scheduler : Schedulers.Config) : LoaderTrainConfig

Attach a scheduler to an epoch-based loader training config.

def NN.API.TorchLean.Trainer.constantLR (cfg : TrainConfig) (lr : Float) : TrainConfig

Step-based constant learning-rate schedule.

def NN.API.TorchLean.Trainer.stepLR (cfg : TrainConfig) (base : Float) (stepSize : ℕ) (gamma : Float := 0.1) : TrainConfig

Step-based step-decay schedule.

def NN.API.TorchLean.Trainer.exponentialLR (cfg : TrainConfig) (base gamma : Float) : TrainConfig

Step-based exponential-decay schedule.

def NN.API.TorchLean.Trainer.constantEpochLR (cfg : LoaderTrainConfig) (lr : Float) : LoaderTrainConfig

Epoch-based constant learning-rate schedule.

def NN.API.TorchLean.Trainer.stepEpochLR (cfg : LoaderTrainConfig) (base : Float) (stepSize : ℕ) (gamma : Float := 0.1) : LoaderTrainConfig

Epoch-based step-decay schedule.

def NN.API.TorchLean.Trainer.exponentialEpochLR (cfg : LoaderTrainConfig) (base gamma : Float) : LoaderTrainConfig

Epoch-based exponential-decay schedule.

def NN.API.TorchLean.Trainer.instantiateWithOptions {σ τ : Spec.Shape} (task : Task σ τ) {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] [Runtime.Scalar α] [Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α] (opts : Options := { }) : IO (Runner α task)

Instantiate a runner under explicit Torch options (backend, useGpu, fastKernels, ...).

This is the recommended entrypoint when you want CUDA eager execution from the training helpers without dropping down to TorchLean.Module directly.

def NN.API.TorchLean.Trainer.instantiate {σ τ : Spec.Shape} (task : Task σ τ) {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] [Runtime.Scalar α] [Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α] (backend : Backend := Runtime.Autograd.Torch.Backend.eager) : IO (Runner α task)

Instantiate a runner (parameters + buffers + backend state) for the given task.

This allocates and initializes model parameters (via Seq.initParams) and sets up the chosen execution backend (.eager vs .compiled).

def NN.API.TorchLean.Trainer.run {σ τ : Spec.Shape} (task : Task σ τ) (args : List String) (k : {α : Type} → [inst : Semantics.Scalar α] → [inst_1 : DecidableEq Spec.Shape] → [ToString α] → [Runtime.Scalar α] → Runner α task → List String → IO Unit) : IO Unit

CLI-oriented runner entry point.

This parses dtype/backend flags (via NN.API.DType / Module.ExecConfig) and then calls the continuation k under the selected scalar backend.

def NN.API.TorchLean.Trainer.params {σ τ : Spec.Shape} {task : Task σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] (runner : Runner α task) : IO (TensorPack α (Supervised.paramShapes task))

Get the current model parameters from a runner.

def NN.API.TorchLean.Trainer.mode {σ τ : Spec.Shape} {task : Task σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] (runner : Runner α task) : IO NN.Mode

Read the current mode (train vs eval).

def NN.API.TorchLean.Trainer.setMode {σ τ : Spec.Shape} {task : Task σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] (runner : Runner α task) (value : NN.Mode) : IO Unit

Set the mode (train vs eval).

def NN.API.TorchLean.Trainer.trainMode {σ τ : Spec.Shape} {task : Task σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] (runner : Runner α task) : IO Unit

Put the runner in training mode so layers such as dropout/batchnorm use training behavior.

def NN.API.TorchLean.Trainer.evalMode {σ τ : Spec.Shape} {task : Task σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] (runner : Runner α task) : IO Unit

Put the runner in evaluation mode so stateful layers use inference behavior.

def NN.API.TorchLean.Trainer.isTraining {σ τ : Spec.Shape} {task : Task σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] (runner : Runner α task) : IO Bool

Check whether the runner is in training mode.

def NN.API.TorchLean.Trainer.backward {σ τ : Spec.Shape} {task : Task σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] (runner : Runner α task) (sample : TensorPack α [σ, τ]) : IO (TensorPack α (Supervised.paramShapes task))

Run forward+backward on one supervised sample and return gradients for all parameters.

def NN.API.TorchLean.Trainer.predict {σ τ : Spec.Shape} {task : Task σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] (runner : Runner α task) (x : Spec.Tensor α σ) : IO (Spec.Tensor α τ)

Predict on a single input tensor.

This runs the forward pass under the runner's current mode.

def NN.API.TorchLean.Trainer.predictBatch {σ τ : Spec.Shape} {task : Task σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] (runner : Runner α task) (xs : List (Spec.Tensor α σ)) : IO (List (Spec.Tensor α τ))

Predict on a list of inputs (runs the forward pass repeatedly).

def NN.API.TorchLean.Trainer.predictClass? {σ : Spec.Shape} {n : ℕ} {task : Task σ (Spec.Shape.dim n Spec.Shape.scalar)} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] (runner : Runner α task) (x : Spec.Tensor α σ) : IO (Option (Fin n))

Predict the argmax class for a classification task, if argmax is well-defined for α.

It runs predict and then applies Metrics.argmax? to the output vector.

def NN.API.TorchLean.Trainer.accuracyOneHot {σ : Spec.Shape} {n : ℕ} {task : Task σ (Spec.Shape.dim n Spec.Shape.scalar)} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] (runner : Runner α task) (samples : List (TensorPack α [σ, Spec.Shape.dim n Spec.Shape.scalar])) : IO (ℕ × ℕ)

Count correct predictions in a one-hot labeled sample list (returns (correct, total)).

def NN.API.TorchLean.Trainer.meanLoss {σ τ : Spec.Shape} {task : Task σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] [ToString α] (runner : Runner α task) (samples : List (TensorPack α [σ, τ])) : IO α

Mean loss over an explicit list of samples.

def NN.API.TorchLean.Trainer.meanLossDataset {σ τ : Spec.Shape} {task : Task σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] [ToString α] (runner : Runner α task) (dataset : Runtime.Autograd.Train.Dataset (TensorPack α [σ, τ])) : IO α

Mean loss over an entire Dataset.

def NN.API.TorchLean.Trainer.trainSamples {σ τ : Spec.Shape} {task : Task σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] [ToString α] [Runtime.Scalar α] (runner : Runner α task) (cfg : TrainConfig) (samples : List (TensorPack α [σ, τ])) : IO (TrainReport α)

Train on an explicit list of samples for a fixed number of steps.

Returns a small report with mean loss before/after.

def NN.API.TorchLean.Trainer.trainDataset {σ τ : Spec.Shape} {task : Task σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] [ToString α] [Runtime.Scalar α] (runner : Runner α task) (cfg : TrainConfig) (dataset : Runtime.Autograd.Train.Dataset (TensorPack α [σ, τ])) : IO (TrainReport α)

Train on a Dataset for a fixed number of steps.

def NN.API.TorchLean.Trainer.trainLoader {σ τ : Spec.Shape} {task : Task σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] [ToString α] [Runtime.Scalar α] (runner : Runner α task) (cfg : LoaderTrainConfig) (loader : Runtime.Autograd.Train.DataLoader (TensorPack α [σ, τ])) : IO (TrainReport α × Runtime.Autograd.Train.DataLoader (TensorPack α [σ, τ]))

Train using a DataLoader for a fixed number of epochs.

def NN.API.TorchLean.Trainer.stepper {σ τ : Spec.Shape} {task : Task σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] [ToString α] [Runtime.Scalar α] (runner : Runner α task) (optimizer : Optimizer) (scheduler : Option Schedulers.Config := none) : IO (Stepper α task)

Construct a stateful stepper for custom loops.

This is useful if you want to control:

• evaluation cadence,
• logging,
• validation, early stopping, etc.

The returned Stepper still uses TorchLean's optimizer/scheduler implementations.

def NN.API.TorchLean.Trainer.step {σ τ : Spec.Shape} {task : Task σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] (loop : Stepper α task) (sample : TensorPack α [σ, τ]) : IO α

Run a single training step on one sample using a Stepper.

def NN.API.TorchLean.Trainer.epoch {σ τ : Spec.Shape} {task : Task σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] (loop : Stepper α task) (samples : List (TensorPack α [σ, τ])) : IO (List α)

Run an epoch over a list of samples using a Stepper (returns the per-step losses).

def NN.API.TorchLean.Trainer.train {σ τ : Spec.Shape} {_task : Task σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] [ToString α] [Runtime.Scalar α] (task : Task σ τ) (cfg : TrainConfig) (samples : List (TensorPack α [σ, τ])) (backend : Backend := Runtime.Autograd.Torch.Backend.eager) : IO (Runner α task × TrainReport α)

Convenience: instantiate + train on a list of samples.

Returns both the Runner (so you can keep using the trained parameters) and the train report.

def NN.API.TorchLean.Trainer.trainDatasetTask {σ τ : Spec.Shape} {_task : Task σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] [ToString α] [Runtime.Scalar α] (task : Task σ τ) (cfg : TrainConfig) (dataset : Runtime.Autograd.Train.Dataset (TensorPack α [σ, τ])) (backend : Backend := Runtime.Autograd.Torch.Backend.eager) : IO (Runner α task × TrainReport α)

Convenience: instantiate a task and train on a Dataset.

Returns both the Runner and the train report.

def NN.API.TorchLean.Trainer.trainLoaderTask {σ τ : Spec.Shape} {_task : Task σ τ} {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] [ToString α] [Runtime.Scalar α] (task : Task σ τ) (cfg : LoaderTrainConfig) (loader : Runtime.Autograd.Train.DataLoader (TensorPack α [σ, τ])) (backend : Backend := Runtime.Autograd.Torch.Backend.eager) : IO (Runner α task × TrainReport α × Runtime.Autograd.Train.DataLoader (TensorPack α [σ, τ]))

Convenience: instantiate a task and train using a DataLoader.

Returns the Runner, the train report, and the updated loader state (shuffled epoch cursor).

@[reducible, inline]

abbrev NN.API.TorchLean.ExecConfig : Type

Execution config parsed from CLI flags (dtype/backend/fast-kernels).

@[reducible, inline]

abbrev NN.API.TorchLean.ExecConfig.parseAndStrip (args : List String) : Except String (Module.ExecConfig × List String)

Parse and strip execution flags, returning (config, remainingArgs).

@[reducible, inline]

abbrev NN.API.TorchLean.ExecConfig.log (cfg : Module.ExecConfig) : IO Unit

Log the chosen execution config to stdout for reproducible runs.

Re-export of the low-level imperative scalar trainer interface.

This exposes forwardT/backwardT/stepT from Runtime.Autograd.TorchLean.ScalarTrainer. Use the higher-level TorchLean.Trainer facade unless a file needs these lower-level training hooks.

Imperative session API: a tape-backed interface that can run in eager or compiled mode.

This is approximately analogous to using PyTorch "eager tensors", except TorchLean makes the tape/session explicit. The Session surface is useful for:

• interactive experiments in IO,
• debugging (inspect intermediate values),
• building higher-level runners.