Trainer

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

let trainer := Trainer.new model
  { objective := .meanSquaredError
    optimizer := optim.adam { learningRate := 0.03 } }
let y0 ← trainer.predict x
let trained ← trainer.train data { steps := 200, samplesPerStep := 16, logEvery := 25 }
trained.printSummary
trained.save "model.state"

Inputs, targets, and predictions cross the API as Tensor Float. Training itself never runs in binary64: .native arithmetic uses Float32 and .ieee uses ExecFloat.Binary 8 23, both binary32. The Float values are converted at the boundary, and Result.report records which scalar ran.

trainer.open returns a Trainer.Session for programs that drive the optimizer loop themselves.

structure TorchLean.Trainer.RunConfig : Type

Runtime, device, arithmetic, and optimizer settings for a trainer or one training call.

Example:

-- The defaults train on the CPU in Lean's `Float32`. `.ieee` swaps in the bit-level reference
-- semantics, which is the setting to reach for when a result looks like a rounding artifact.
def settings : Trainer.RunConfig :=
  { optimizer := optim.sgd { learningRate := 0.01, momentum := 0.9 }
    arithmetic := .native
    execution := .eager
    device := .cpu }

• optimizer : optim.Optimizer

  Optimizer used unless a training call supplies another run configuration.

• arithmetic : Runtime.Arithmetic

  Arithmetic semantics used for the run.

  .native trains in Lean's Float32 and .ieee in the bit-level ExecFloat.Binary 8 23 reference. Both are binary32; the Tensor Float values in the public signatures are converted at the boundary. Supervised training rejects .complex.

• execution : Runtime.Autograd.Torch.ExecutionMode

  Immediate tape execution or reusable typed-graph execution.

• device : NN.Backend.Device

  Device used for execution.

• backendProfile? : Option NN.Backend.BackendProfile

  Optional advanced override for provider, assurance, and VJP policy.

• showBackend : Bool

  Print each accepted backend capsule when it is first used.

inductive TorchLean.Trainer.Objective (output : Shape) : Type 1

Loss used to train a model.

The output shape belongs to the model. The objective only decides how (prediction, target) becomes a scalar objective; it does not need a separate input-shape index.

Example:

-- Regression scores a prediction against a target tensor.
def regression : Trainer.Objective [1] := .meanSquaredError

-- Classification needs the axis the logits live on, here the only axis of a ten-class output.
def classification : Trainer.Objective [10] := .oneHotCrossEntropy 0

• meanSquaredError {output : Shape} (reduction : Loss.Reduction := Loss.Reduction.mean) : Objective output

  Mean-squared-error supervised regression.

• oneHotCrossEntropy {output : Shape} (axis : ℕ) (reduction : Loss.Reduction := Loss.Reduction.mean) : Objective output

  One-hot cross entropy over a class or structured logit tensor.

• custom {output : Shape} (loss : {α : Type} → [inst : Storage α] → [inst_1 : Context α] → Runtime.Autograd.Model.Program α [output, output] []) : Objective output

  A checked TorchLean loss program supplied by the caller.

def TorchLean.Trainer.Objective.definition {σ τ : Shape} (objective : Objective τ) (model : nn.Sequential σ τ) (mode : nn.Mode := Runtime.Autograd.Model.Layers.Mode.train) : Module.ObjectiveDefinition Unit (Runtime.Autograd.Model.Layers.Seq.stateShapes model) [σ, τ]

Lower an objective for a checked model into the runtime module definition that the trainer instantiates.

Training mode is the default; .eval builds the graph that stateful layers use for inference.

structure TorchLean.Trainer.Config (input output : Shape) extends TorchLean.Trainer.RunConfig : Type 1

Model-independent options accepted by Trainer.new.

The RunConfig fields select the optimizer and runtime. Although the trainer's public signatures use Tensor Float, training runs in the binary32 scalar chosen by arithmetic: Float32 for .native and ExecFloat.Binary 8 23 for .ieee. Trained parameters are read back to Float exactly.

• optimizer : optim.Optimizer
• arithmetic : Runtime.Arithmetic
• execution : Runtime.Autograd.Torch.ExecutionMode
• device : NN.Backend.Device
• backendProfile? : Option NN.Backend.BackendProfile
• showBackend : Bool
• objective : Objective output

  Training objective attached to this trainer.

• seed : ℕ

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

structure TorchLean.Trainer (input output : Shape) : Type 1

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

Construct trainers with Trainer.new. The resulting value supports prediction, training, and model inspection directly through dot notation.

• model : nn.Sequential input output

  Checked TorchLean model.

• objective : Objective output

  Supervised objective used by train.

• runtime : RunConfig

  Runtime, backend-contract, and optimizer choices carried by this trainer.

• seed : ℕ

  Seed used to build this trainer when the input was a TorchLean.nn.Builder model builder.

def TorchLean.Trainer.summary {σ τ : Shape} (trainer : Trainer σ τ) : Except String nn.ModelSummary

Structured checked-model summary for this trainer.

def TorchLean.Trainer.printSummary {σ τ : Shape} (trainer : Trainer σ τ) (label : String := "model") : IO Unit

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