Trainer Handle

Create a trainer from a checked model, choose its loss and optimizer, then train or predict:

let trainer := Trainer.new model
  { task := .regression
    optimizer := optim.adam { lr := 0.03 } }
let y0 ← trainer.predict x
let trained ← trainer.train data { steps := 200, batchSize := 16, logEvery := 25 }
trained.printSummary

Trainer.Manual provides direct access to runtime modules, tensor packs, and callbacks for custom loops.

structure TorchLean.Trainer.RuntimeSettings : Type

Runtime settings stored with a trainer.

• optimizer : optim.Optimizer

  Optimizer used unless a training call supplies another run configuration.

• dtype : Runtime.DType

  Scalar dtype used for the run.

• backend : Runtime.Backend

  Eager or compiled execution backend.

• executionProfile : NN.Backend.BackendProfile

  Contract profile controlling device, providers, assurance, and VJP ownership.

• showBackend : Bool

  Print each accepted backend capsule when it is first used.

inductive TorchLean.Trainer.Task (σ τ : Shape) : Type 1

Loss used to train a model.

The shape parameters belong to the model. The task only decides how (prediction, target) becomes a scalar objective.

• regression {σ τ : Shape} (reduction : Loss.Reduction := Loss.Reduction.mean) : Task σ τ

  Mean-squared-error supervised regression.

• classification {σ τ : Shape} (reduction : Loss.Reduction := Loss.Reduction.mean) : Task σ τ

  One-hot cross entropy over the model output tensor.

• crossEntropy {σ τ : Shape} (reduction : Loss.Reduction := Loss.Reduction.mean) : Task σ τ

  One-hot cross entropy for sequence or structured logit tensors.

• custom {σ τ : Shape} (loss : {α : Type} → [inst : Context α] → [inst_1 : DecidableEq Shape] → Runtime.Autograd.TorchLean.Program α [τ, τ] Shape.scalar) : Task σ τ

  A checked TorchLean loss program supplied by the caller.

structure TorchLean.Trainer.Config (σ τ : Shape) extends TorchLean.Trainer.RuntimeSettings : Type 1

Model-independent options accepted by Trainer.new.

• optimizer : optim.Optimizer
• dtype : Runtime.DType
• backend : Runtime.Backend
• executionProfile : NN.Backend.BackendProfile
• showBackend : Bool
• task : Task σ τ

  Task loss attached to this trainer.

• seed : ℕ

  Seed used when the model is still a seedable TorchLean.nn.M builder.

structure TorchLean.Trainer.Handle (σ τ : Shape) : Type 2

A checked model together with its loss, runtime settings, and initialization seed.

• model : nn.Sequential σ τ

  Checked TorchLean model.

• task : Task σ τ

  Supervised objective used by train.

• runtime : RuntimeSettings

  Runtime/backend/optimizer choices carried by this trainer.

• seed : ℕ

  Seed used to build this trainer when the input was an TorchLean.nn.M model builder.

def TorchLean.Trainer.Handle.info {σ τ : Shape} (trainer : Handle σ τ) : String

Checked model summary for this unified trainer.

def TorchLean.Trainer.Handle.printInfo {σ τ : Shape} (trainer : Handle σ τ) : IO Unit

Print the checked model summary under the heading model.

def TorchLean.Trainer.Handle.printInfoAs {σ τ : Shape} (trainer : Handle σ τ) (label : String) : IO Unit

Print the checked model summary with a caller-chosen heading.

structure TorchLean.Trainer.Implementation.Regression (σ τ : Shape) : Type 2

Typed dispatch record for supervised regression.

This record carries the equalities needed by the regression implementation. Users construct a Trainer.Handle rather than this task-specific record.

• model : nn.Sequential σ τ

  The checked TorchLean model used by this trainer.

• reduction : Loss.Reduction

  Mean vs sum loss reduction for the built regression task.

• runtime : RuntimeSettings

  Runtime/backend/optimizer choices carried by this trainer.

structure TorchLean.Trainer.Implementation.CrossEntropy (σ τ : Shape) : Type 2

Typed dispatch record for general one-hot cross-entropy training.

Classification and sequence models use the same checked one-hot cross-entropy runtime path. Image examples usually batch their dataset first with Data.batchDataset; text examples often train on a whole matrix of one-hot next-token rows:

let trainer := Trainer.new model { task := .crossEntropy, optimizer := optim.adam { lr := 1e-3 } }
let trained ← trainer.train tokenWindows { steps := 200 }

The output handle exposes prediction tensors, not class labels, because token decoding is model-specific and belongs in the text example.

• model : nn.Sequential σ τ

  The checked TorchLean model used by this trainer.

• reduction : Loss.Reduction

  Mean vs sum loss reduction for the one-hot cross-entropy task.

• runtime : RuntimeSettings

  Runtime/backend/optimizer choices carried by this trainer.

structure TorchLean.Trainer.Implementation.Custom (σ τ : Shape) : Type 2

Typed dispatch record for a checked custom scalar loss.

Custom losses cover masked language-model objectives, physics residuals, and algorithmic tasks where the model is still an ordinary TorchLean.nn.Sequential, but the loss has task logic that does not fit a canned reduction. The boundary stays precise: the loss is a TorchLean program over (prediction, target), so module construction and optimizer wiring remain inside the trainer API.

• model : nn.Sequential σ τ

  The checked TorchLean model used by this trainer.

• loss {α : Type} [Context α] [DecidableEq Shape] : Runtime.Autograd.TorchLean.Program α [τ, τ] Shape.scalar

  Checked scalar loss program applied to (modelOutput, target).

• runtime : RuntimeSettings

  Runtime/backend/optimizer choices carried by this trainer.

def TorchLean.Trainer.Implementation.Regression.task {σ τ : Shape} (trainer : Regression σ τ) : Manual.SeqTask σ τ

Checked TorchLean task induced by this regression dispatch record.

def TorchLean.Trainer.Implementation.Regression.info {σ τ : Shape} (trainer : Regression σ τ) : String

Checked model summary for this trainer.

def TorchLean.Trainer.Implementation.Regression.printInfo {σ τ : Shape} (trainer : Regression σ τ) : IO Unit

Print the checked model summary with the standard public-example heading.

Examples use this instead of open-coding IO.println "model:"; IO.println trainer.info, so the first thing users see is consistent across regression, classifier, sequence, and custom trainers.

def TorchLean.Trainer.Implementation.Regression.printInfoAs {σ τ : Shape} (trainer : Regression σ τ) (label : String) : IO Unit

Print this trainer's checked model summary with a caller-chosen heading.

Most examples should use trainer.printInfo; paired-model examples such as GANs use this labeled variant so both summaries still go through the same formatting path.

theorem TorchLean.Trainer.Implementation.Regression.taskParamShapes_eq {σ τ : Shape} (trainer : Regression σ τ) : Manual.paramShapes trainer.task = Runtime.Autograd.TorchLean.NN.Seq.paramShapes trainer.model

The runtime task induced by this handle has exactly the model's parameter shapes.

def TorchLean.Trainer.Implementation.CrossEntropy.task {σ τ : Shape} (trainer : CrossEntropy σ τ) : Manual.SeqTask σ τ

Checked TorchLean task induced by this cross-entropy dispatch record.

def TorchLean.Trainer.Implementation.CrossEntropy.info {σ τ : Shape} (trainer : CrossEntropy σ τ) : String

Checked model summary for this trainer.

def TorchLean.Trainer.Implementation.CrossEntropy.printInfo {σ τ : Shape} (trainer : CrossEntropy σ τ) : IO Unit

Print the checked model summary with the standard public-example heading.

theorem TorchLean.Trainer.Implementation.CrossEntropy.taskParamShapes_eq {σ τ : Shape} (trainer : CrossEntropy σ τ) : Manual.paramShapes trainer.task = Runtime.Autograd.TorchLean.NN.Seq.paramShapes trainer.model

The runtime task induced by this handle has exactly the model's parameter shapes.

def TorchLean.Trainer.Implementation.Custom.info {σ τ : Shape} (trainer : Custom σ τ) : String

Checked model summary for this custom-loss trainer.

def TorchLean.Trainer.Implementation.Custom.printInfo {σ τ : Shape} (trainer : Custom σ τ) : IO Unit

Print the checked model summary with the standard public-example heading.