TorchLean Public Trainer Facade

Public training starts from one handle:

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

Runtime modules, tensor packs, and callback runners remain available under Trainer.Advanced. Application code should usually construct one Trainer value, call trainer.eval for initial inference, and call trainer.train to get a trained handle.

Advanced training hooks.

Runtime trainer hooks for code that needs direct control.

Use this namespace for manual callbacks, explicit runtime mode changes, custom streams, or verification bridges. Model examples should stay on Trainer.new and trainer.train.

structure TorchLean.Trainer.RuntimeSettings : Type

Runtime settings carried by a public trainer.

• optimizer : optim.Optimizer

  Optimizer used by public trainer training runs unless a call supplies another run config.

• dtype : Runtime.DType

  Scalar dtype used for the run.

• backend : Runtime.Backend

  Eager or compiled execution backend.

• device : Runtime.Device

  CPU or CUDA execution device.

• fastKernels : Bool

  Enable runtime-only fast kernels where available.

• fastGpuMatmulPrecision : Runtime.Autograd.FastKernels.GpuMatmulPrecision

  CUDA matmul precision for fast kernels.

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

Task carried by the unified public trainer.

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

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

  Mean-squared-error supervised regression.

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

  One-hot cross entropy over the model output tensor.

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

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

• custom {σ τ : Shape} (loss : {α : Type} → [inst : Runtime.TensorScalar α] → [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

Construction options for the unified public trainer.

• optimizer : optim.Optimizer
• dtype : Runtime.DType
• backend : Runtime.Backend
• device : Runtime.Device
• fastKernels : Bool
• fastGpuMatmulPrecision : Runtime.Autograd.FastKernels.GpuMatmulPrecision
• task : Task σ τ

  Task loss attached to this trainer.

• seed : ℕ

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

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

One public trainer handle.

The main public trainer handle: a checked model, one task description, runtime choices, and a seed for model builders.

• 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 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 with the standard public-example heading.

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.

The exported API still has one trainer handle. This record exists so the runtime implementation can carry task-specific equalities without splitting the public surface into separate trainer classes.

• 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 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 facade.

• model : nn.Sequential σ τ

  The checked TorchLean model used by this trainer.

• loss {α : Type} [Runtime.TensorScalar α] [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 σ τ) : NN.API.train.Advanced.Task σ τ

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 σ τ) : Supervised.paramShapes trainer.task = nn.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 σ τ) : NN.API.train.Advanced.Task σ τ

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 σ τ) : Supervised.paramShapes trainer.task = nn.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.