Training Reports

Training curves, metric histories, and logs produced by Trainer runs.

structure TorchLean.Training.LossProgress (α : Type) : Type

Loss measured before and after a training run.

• before : α

  Loss measured before any updates in the run.

• after : α

  Loss measured after all requested updates in the run.

def TorchLean.Training.instReprLossProgress.repr {α✝ : Type} [Repr α✝] : LossProgress α✝ → Nat → Std.Format

@[instance_reducible]

instance TorchLean.Training.instReprLossProgress {α✝ : Type} [Repr α✝] : Repr (LossProgress α✝)

def TorchLean.Training.shouldReport (every completed : Nat) : Bool

Return whether a completed step should emit a periodic report.

def TorchLean.Training.writeLog (destination : LogDestination) (log : TrainLog) : IO Unit

Write a training log to an enabled or disabled destination.

def TorchLean.Training.writeLossComparison (destination : LogDestination) (title : String) (steps : Nat) (lossBefore lossAfter : Float) (notes : Array String := #[]) : IO Unit

Write a before/after loss log to an enabled or disabled destination.

structure TorchLean.Training.CurveEndpoints : Type

First and last values of a nonempty scalar training curve.

• lastStep : Nat

  Step associated with the last value.

• firstValue : Float

  First recorded value.

• lastValue : Float

  Last recorded value.

def TorchLean.Training.instReprCurveEndpoints.repr : CurveEndpoints → Nat → Std.Format

@[instance_reducible]

instance TorchLean.Training.instReprCurveEndpoints : Repr CurveEndpoints

def TorchLean.Training.Curve.endpoints? (curve : Curve) : Option CurveEndpoints

Return the endpoints of a scalar curve, or none when it contains no values.

def TorchLean.Training.Curve.endpoints (curve : Curve) (context : String := "training curve") : IO CurveEndpoints

Return the endpoints of a scalar curve or raise a contextual error when it is empty.

def TorchLean.Training.Curve.printLossSummary (curve : Curve) (steps : Nat) : IO Unit

Print loss before and after the updates represented by a scalar training curve.

def TorchLean.Training.Curve.writeLog (curve : Curve) (destination : LogDestination) (title : String) (seriesName : String := "loss") (notes : Array String := #[]) (color : String := "#4e79a7") : IO Unit

Write a scalar curve to an enabled or disabled training-log destination.

def TorchLean.Training.MetricHistory.writeLog (history : MetricHistory) (destination : LogDestination) (title : String) (notes : Array String := #[]) : IO Unit

Write named metric series to an enabled or disabled training-log destination.