Trainer Construction

Constructors for TorchLean.Trainer.

class TorchLean.Trainer.ToModel (Model : Type u) (input output : outParam Shape) : Type (max 1 u)

Values accepted by Trainer.new.

This class lets Trainer.new accept either a seedable model builder or an already-built checked model:

Trainer.new modelBuilder ...
Trainer.new alreadyBuiltModel ...

The seed is consumed only by the builder case. Already-built models pass through unchanged.

• build : ℕ → Model → nn.Sequential input output

  Materialize the model, using the seed only when the value still needs initialization.

@[instance_reducible]

instance TorchLean.Trainer.instToModelSequential {σ τ : Shape} : ToModel (nn.Sequential σ τ) σ τ

@[instance_reducible]

instance TorchLean.Trainer.instToModelBuilderSequential {σ τ : Shape} : ToModel (nn.Builder (nn.Sequential σ τ)) σ τ

def TorchLean.Trainer.new {Model : Type u} {σ τ : Shape} [ToModel Model σ τ] (model : Model) (config : Config σ τ := { }) : Trainer σ τ

Build a trainer from a sequential model or seedable model builder.

Example:

-- A trainer pairs a model with the loss, the optimizer, and the runtime it trains under.
def model : nn.Builder (nn.Sequential [2] [1]) :=
  nn.Sequential![nn.linear 2 8, nn.relu, nn.linear 8 1]

def trainer : TorchLean.Trainer [2] [1] :=
  Trainer.new model
    { objective := .meanSquaredError
      optimizer := optim.adam { learningRate := 0.03 }
      seed := 7 }

-- An already-built model is accepted too, and then the seed has nothing left to decide.
def fromBuiltModel : TorchLean.Trainer [2] [1] :=
  Trainer.new (nn.build 7 model)