Trainer

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

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

trainer.train and trainer.open accept Tensor Float values and execute in the selected binary32 scalar: Float32 for native or FloatLib's ExecFloat.Binary 8 23 for ieee. Results record that selection and read the binary32 values back to Float.

For a different scalar, trainer.openTyped (α := α) keeps inputs, parameters, predictions, and losses in α throughout a CPU session. Supply initialState? with typed state when initialization must preserve digits beyond the model's stored seeded Float values. Both opening paths return a Trainer.Session for programs that drive the optimizer loop themselves.

structure TorchLean.Trainer.RunConfigextends Runtime.Autograd.Torch.Config : Type

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

The runtime fields (device, seed, backendProfile?, showBackend) are those of Runtime.Config, which this record extends, so { runtime with optimizer := ... } builds one from a runtime configuration.

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 { lr := 0.01, momentum := 0.9 }
    arithmetic := native
    device := cpu }

• device : NN.Backend.Device
• seed : ℕ
• backendProfile? : Option NN.Backend.BackendProfile
• showBackend : Bool
• optimizer : optim.Optimizer

  Optimizer used unless a training call supplies another run configuration.

• arithmetic : Runtime.Arithmetic

  Arithmetic semantics selected by trainer.open and the managed training methods.

  native trains in Lean's Float32 and ieee in FloatLib's ExecFloat.Binary 8 23. Both are binary32; Tensor Float values are converted at the boundary. These methods reject complex. trainer.openTyped instead uses its explicit scalar parameter.

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] := mse

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

• mse {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; nn.Mode.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. Managed training uses the binary32 scalar chosen by arithmetic, with Float data and result boundaries. trainer.openTyped uses an explicit scalar and preserves it in the session and its finished result.

• device : NN.Backend.Device
• seed : ℕ
• backendProfile? : Option NN.Backend.BackendProfile
• showBackend : Bool
• optimizer : optim.Optimizer
• arithmetic : Runtime.Arithmetic
• objective : Objective output

  Training objective attached to this trainer.

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. Its seed built the model when the model was a TorchLean.nn.Builder; changing it later does not rebuild it.

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.