Training Sessions #
trainer.train owns the optimizer loop. A Session is the same trainer with the loop handed to
the caller:
let session ← trainer.open
for step in [0:steps] do
let loss ← session.step (sampleAt step) (loss := true)
if step % 100 = 0 then IO.println s!"step {step}: loss={loss}"
let after ← session.eval data
let trained ← session.finish { before, after }
Opening a session instantiates the model under the trainer's runtime settings and binds the
trainer's optimizer. step applies one update; set loss := true to read its loss. predict,
loss, and eval run the current parameters in evaluation mode; state, save, and load
read or replace the parameters; finish snapshots the current state as an ordinary Result.
trainer.open uses Float at the boundary and executes in the binary32 scalar selected by
RunConfig.arithmetic. trainer.openTyped (α := α) retains the selected scalar through inputs,
state, predictions, losses, reports, and checkpoints on CPU. Both use the same session and snapshot
implementation. Trainer.train is implemented as open, a loop, and finish.
A trainer with its model instantiated and the optimizer loop owned by the caller.
Obtain one with trainer.open or trainer.openTyped. The session type is indexed by the trainer it
runs, so the state layout nn.stateShapes trainer.model is available to state and load. Updates
run stateful layers in training mode, while predict, loss, and eval use evaluation mode.
- stepWithLossImpl : Array (TorchLean.Sample.Supervised α σ τ) → IO α
- stepImpl : Array (TorchLean.Sample.Supervised α σ τ) → IO Unit
- lossImpl : TorchLean.Sample.Supervised α σ τ → IO α
- predictImpl : TorchLean.Tensor α σ → IO (TorchLean.Tensor α τ)
- stateImpl : IO (TorchLean.nn.State α (Runtime.Autograd.Model.Layers.Seq.stateShapes trainer.model))
- setStateImpl : TorchLean.nn.State α (Runtime.Autograd.Model.Layers.Seq.stateShapes trainer.model) → IO Unit
- finishImpl : TorchLean.Training.LossProgress α → IO (TorchLean.Trainer.Result σ τ α)
Instances For
Construct a session at the trainer implementation boundary.
Replace the live parameters and buffers in the session's scalar.
Apply one optimizer update, optionally returning the loss.
Pass one sample, or use batch := true with a nonempty array. A batch averages
per-sample gradients at the same parameter point and counts as one update. loss := true
returns the mean loss from those forwards; the default avoids reading the loss back.
Example:
-- One update per call. Set `batch := true` to average several samples in one update.
def descend (trainer : TorchLean.Trainer [2] [1]) : IO (Trainer.Result [2] [1]) := do
let session ← trainer.open
let sample : Sample.Supervised Float [2] [1] := { input := [1.0, 0.0], target := [1.0] }
let before ← session.loss sample
for _ in List.range 100 do
session.step sample
let after ← session.loss sample
session.finish { before := before, after := after }
Evaluate samples in index order and combine their means pairwise.
Weights are cast from exact ratios, so a sample count need not fit in the model's scalar format. For IEEE scalars, finite partial means stay within the two child means' range. This prevents a large finite sum from overflowing, but does not guarantee accuracy under cancellation.
Evaluation-mode loss under the current parameters.
batch := true takes a lazy sample stream and returns its ordered mean, or zero when empty.
Evaluation-mode prediction under the current parameters.
With batch := true, map over the leading axis of length batchSize, including an empty axis.
Snapshot the current parameters as a trained Result.
The report records the number of updates applied so far, the runtime arithmetic, and the losses
supplied by the caller, typically from eval before and after the loop. Later session updates or
checkpoint loads do not change the result's parameters, predictions, or verification.
Example:
-- Keep a model snapshot with the losses measured for it. The session can continue training
-- without changing this result.
def package {trainer : TorchLean.Trainer [2] [1]}
(session : Trainer.Session trainer) (before after : Float) :
IO (Trainer.Result [2] [1]) :=
session.finish { before := before, after := after }
Write the current parameters with Checkpoint.State.save.
Instances For
Replace the current model state from a checkpoint written by save or Result.save.
Optimizer history and the completed-step count are retained. Open a new session before loading when training should restart with a fresh optimizer and schedule.
Instances For
Build a session for a runtime scalar α and a public scalar β.
The opening path supplies the conversions and an optional verifier. Typed opening uses identity conversions, preserving inputs, losses, and state without requiring bound-arithmetic instances.
nospecialize keeps this setup routine from generating a copy of the runner and stepper stack
for each runtime scalar. A session performs this setup once and reuses the bound optimizer.
Instances For
Instantiate the model under the trainer's runtime settings and hand the optimizer loop to the caller.
The trainer's optimizer is bound immediately; scheduler optionally adjusts its learning rate by
completed step. Optimizer and scheduler settings must remain valid after binary32 conversion and
are checked before the model is instantiated. CUDA execution requires native arithmetic, and
complex arithmetic is not supported by supervised training.
Example:
-- A session holds the instantiated model and the bound optimizer. `trainer.train` is exactly this
-- call, a loop of `step`, and a `finish`, so opening a session is how you take that loop over.
def stepOnce (trainer : TorchLean.Trainer [2] [1]) : IO Float := do
let session ← trainer.open
session.step { input := [1.0, 0.0], target := [1.0] } (loss := true)
Instances For
Open a CPU session whose inputs, state, predictions, and losses retain the scalar α.
initialState? supplies exact typed parameters and buffers. Without it, the model's existing seeded
Float initializers are converted into α; they do not acquire additional random precision.
Optimizer and scheduler coefficients are also configured in Float and converted into α.
The explicit scalar takes precedence over RunConfig.arithmetic. This path uses the maintained CPU
runtime and rejects other devices and custom backend profiles before instantiating state. It does
not narrow tensors for native kernels. Checkpoints use Checkpoint.Encoding α; finished results
carry no verifier, so Result.verify reports that verification is unavailable.