Training Results

Regression, cross-entropy, and custom losses all return the same trained-model type.

A Result keeps a parameter snapshot of the trained model. Prediction and verification use it directly. Result.state retains the session's public scalar and Result.save writes its exact encoding with Checkpoint.State.save. Results are produced by Session.finish; verification is available when the opening path supplies a verifier for its runtime scalar.

structure TorchLean.Trainer.Result (σ τ : Shape) (α : Type := Float) [Storage α] : Type

A trained TorchLean model.

The result retains its parameter snapshot through prediction, state-reading, and verification closures. Continued training of the source session does not change the result.

The default public scalar is Float: ordinary sessions read binary32 state back exactly. Typed sessions retain their selected scalar through state, prediction, reporting, and checkpoint encoding.

• reportValue : TorchLean.Trainer.Report α
• stateShapes : List Shape

  Shapes of the trained parameters and buffers, in the order used by state and save.

• readState : IO (TorchLean.nn.State α self.stateShapes)
• saveState : System.FilePath → IO Unit
• predictOne : TorchLean.Tensor α σ → IO (TorchLean.Tensor α τ)
• runVerification? : Option (TorchLean.Tensor Float σ → Float → TorchLean.Verification.Norm → TorchLean.Verification.Property → TorchLean.Verification.Algorithm → IO TorchLean.Verification.Report)

opaque TorchLean.Trainer.Result.Internal.create {α : Type} [Storage α] {σ τ : Shape} (report : Report α) (stateShapes : List Shape) (readState : IO (nn.State α stateShapes)) (saveState : System.FilePath → IO Unit) (predict : Tensor α σ → IO (Tensor α τ)) (verify? : Option (Tensor Float σ → Float → Verification.Norm → Verification.Property → Verification.Algorithm → IO Verification.Report) := none) : Result σ τ α

Construct an opaque trained-model result at the trainer implementation boundary.

opaque TorchLean.Trainer.Result.report {α : Type} [Storage α] {σ τ : Shape} (result : Result σ τ α) : Report α

Loss progress, step count, and runtime arithmetic for the completed run.

opaque TorchLean.Trainer.Result.state {α : Type} [Storage α] {σ τ : Shape} (result : Result σ τ α) : IO (nn.State α result.stateShapes)

Read the trained parameters and persistent buffers in the session's public scalar.

Ordinary sessions read binary32 state back to Float exactly; typed sessions preserve α. The layout result.stateShapes equals nn.stateShapes of the trained model, which is what Checkpoint.State.save and Checkpoint.State.load expect.

opaque TorchLean.Trainer.Result.save {α : Type} [Storage α] {σ τ : Shape} (result : Result σ τ α) (path : System.FilePath) : IO Unit

Save the trained state with Checkpoint.State.save.

Restore it with Session.load on a session using the same scalar. For typed state, open that session with trainer.openTyped (α := α) before loading the checkpoint.

opaque TorchLean.Trainer.Result.predict {α : Type} [Storage α] {σ τ inputShape : Shape} (result : Result σ τ α) (input : Tensor α inputShape) (batch : Bool := false) (batchSize : ℕ := 1) [Internal.BatchInput (Tensor α σ) (Tensor α (σ.prependDim batchSize)) batch (Tensor α inputShape)] : IO (Tensor α (match batch with | false => τ | true => τ.prependDim batchSize))

Run evaluation-mode prediction through the trained snapshot.

batch := true maps over a leading axis of length batchSize, including an empty axis.

opaque TorchLean.Trainer.Result.verify {α : Type} [Storage α] {σ τ : Shape} (result : Result σ τ α) (center : Tensor Float σ) (radius : Float) (norm : Verification.Norm := linf) (property : Verification.Property := outputBounds) (algorithm : Verification.Algorithm := alphaCrown) : IO Verification.Report

Verify the trained model over a region around center.

property and algorithm have defaults, so checking output bounds needs only center and radius. This fails explicitly if the opening path supplied no verifier, including openTyped.

def TorchLean.Trainer.Result.summary {α : Type} [Storage α] {σ τ : Shape} [ToString α] (result : Result σ τ α) : String

One-line summary for the completed training run.

def TorchLean.Trainer.Result.printSummary {α : Type} [Storage α] {σ τ : Shape} [ToString α] (result : Result σ τ α) : IO Unit

Print the before/after training summary.

def TorchLean.Trainer.Result.printPrediction {α : Type} [Storage α] {σ τ : Shape} [Repr α] (result : Result σ τ α) (label : String) (input : Tensor α σ) : IO Unit

Print one prediction with a caller-supplied label.

@[instance_reducible]

instance TorchLean.Trainer.Result.instToString {α : Type} [Storage α] {σ τ : Shape} [ToString α] : ToString (Result σ τ α)

structure TorchLean.Trainer.StreamResult (σ τ : Shape) (α : Type := Float) [Storage α] : Type

A trained model returned by step-indexed stream training.

Generated or resampled workloads may not have one static dataset to summarize. The ordinary training result is paired with the evaluation curve collected from a caller-provided sample. Predictions retain the result's scalar α; the recorded curve uses Float metrics.

• trained : Result σ τ α

  Trained model result.

• curve : Training.Curve

  Evaluation loss curve recorded during stream training.

def TorchLean.Trainer.StreamResult.summary {α : Type} [Storage α] {σ τ : Shape} [ToString α] (result : StreamResult σ τ α) : String

One-line summary for the trained stream run.

def TorchLean.Trainer.StreamResult.printSummary {α : Type} [Storage α] {σ τ : Shape} [ToString α] (result : StreamResult σ τ α) : IO Unit

Print the stream training summary.

def TorchLean.Trainer.StreamResult.predict {α : Type} [Storage α] {σ τ inputShape : Shape} (result : StreamResult σ τ α) (input : Tensor α inputShape) (batch : Bool := false) (batchSize : ℕ := 1) [Internal.BatchInput (Tensor α σ) (Tensor α (σ.prependDim batchSize)) batch (Tensor α inputShape)] : IO (Tensor α (match batch with | false => τ | true => τ.prependDim batchSize))

Predict one input, or map a leading tensor batch, through the trained stream result.

@[instance_reducible]

instance TorchLean.Trainer.StreamResult.instToString {α : Type} [Storage α] {σ τ : Shape} [ToString α] : ToString (StreamResult σ τ α)

structure TorchLean.Trainer.AlternatingResult (σ₁ τ₁ σ₂ τ₂ : Shape) : Type

Two trained regression models and the coupled metric recorded by alternating updates.

• first : Result σ₁ τ₁ Float

  Trained result for the first model.

• second : Result σ₂ τ₂ Float

  Trained result for the second model.

• curve : Training.Curve

  Task-specific curve recorded by the caller-provided evaluation function.

def TorchLean.Trainer.AlternatingResult.summary {σ₁ τ₁ σ₂ τ₂ : Shape} (result : AlternatingResult σ₁ τ₁ σ₂ τ₂) : String

One-line summary for the two trained models.

def TorchLean.Trainer.AlternatingResult.printSummary {σ₁ τ₁ σ₂ τ₂ : Shape} (result : AlternatingResult σ₁ τ₁ σ₂ τ₂) : IO Unit

Print the training summary for both models.

def TorchLean.Trainer.AlternatingResult.printCurveSummary {σ₁ τ₁ σ₂ τ₂ : Shape} (result : AlternatingResult σ₁ τ₁ σ₂ τ₂) (metric : String := "loss") : IO Unit

Print the endpoints of the coupled metric curve.

@[instance_reducible]

instance TorchLean.Trainer.AlternatingResult.instToString {σ₁ τ₁ σ₂ τ₂ : Shape} : ToString (AlternatingResult σ₁ τ₁ σ₂ τ₂)