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 reads the parameters back as Float tensors and Result.save writes them with Checkpoint.State.save, so a trained model can be stored and later restored with Trainer.load. Results are produced by Session.finish.

structure TorchLean.Trainer.Result (σ τ : Shape) : 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 runtime state lives in the binary32 scalar selected by RunConfig.arithmetic (Float32 or ExecFloat.Binary 8 23). state and save read it back as Float, which is exact because every binary32 value is a binary64 value.

• 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 Float self.stateShapes)
• saveState : System.FilePath → IO Unit
• predictOne : TorchLean.Tensor Float σ → IO (TorchLean.Tensor Float τ)
• runVerification (center : TorchLean.Tensor Float σ) (radius : Float) : TorchLean.Verification.Norm → TorchLean.Verification.Property → TorchLean.Verification.Algorithm → IO TorchLean.Verification.Report

def TorchLean.Trainer.Result.Internal.verificationUnavailable {σ : Shape} : Tensor Float σ → Float → Verification.Norm → Verification.Property → Verification.Algorithm → IO Verification.Report

Verification implementation used by training paths that cannot lower a verifier.

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

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

opaque TorchLean.Trainer.Result.report {σ τ : Shape} (result : Result σ τ) : Report

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

opaque TorchLean.Trainer.Result.state {σ τ : Shape} (result : Result σ τ) : IO (nn.State Float result.stateShapes)

Read the trained parameters and persistent buffers as Float tensors.

The runtime holds them in binary32 (Float32 or ExecFloat.Binary 8 23); reading them back to binary64 is exact. 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 {σ τ : Shape} (result : Result σ τ) (path : System.FilePath) : IO Unit

Save the trained state with Checkpoint.State.save; restore it with Trainer.load.

opaque TorchLean.Trainer.Result.predict {σ τ : Shape} (result : Result σ τ) (input : Tensor Float σ) : IO (Tensor Float τ)

Run one Float input through the trained model.

opaque TorchLean.Trainer.Result.predictMany {σ τ : Shape} {batch : ℕ} (result : Result σ τ) (inputs : Tensor Float (σ.prependDim batch)) : IO (Tensor Float (τ.prependDim batch))

Run several Float inputs through the trained model.

opaque TorchLean.Trainer.Result.verify {σ τ : Shape} (result : Result σ τ) (center : Tensor Float σ) (radius : Float) (norm : Verification.Norm := Verification.Norm.inf) (property : Verification.Property := Verification.Property.bounds) (algorithm : Verification.Algorithm := Verification.Algorithm.alphaBetaCrown) : 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.

def TorchLean.Trainer.Result.summary {σ τ : Shape} (result : Result σ τ) : String

One-line summary for the completed training run.

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

Print the before/after training summary.

def TorchLean.Trainer.Result.printPrediction {σ τ : Shape} (result : Result σ τ) (label : String) (input : Tensor Float σ) : IO Unit

Print one prediction with a caller-supplied label.

@[instance_reducible]

instance TorchLean.Trainer.Result.instToString {σ τ : Shape} : ToString (Result σ τ)

structure TorchLean.Trainer.StreamResult (σ τ : Shape) : 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.

• trained : Result σ τ

  Trained model result.

• curve : Training.Curve

  Evaluation loss curve recorded during stream training.

def TorchLean.Trainer.StreamResult.summary {σ τ : Shape} (result : StreamResult σ τ) : String

One-line summary for the trained stream run.

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

Print the stream training summary.

def TorchLean.Trainer.StreamResult.predict {σ τ : Shape} (result : StreamResult σ τ) (input : Tensor Float σ) : IO (Tensor Float τ)

Run one prediction through the trained stream result.

def TorchLean.Trainer.StreamResult.predictMany {σ τ : Shape} {batch : ℕ} (result : StreamResult σ τ) (inputs : Tensor Float (σ.prependDim batch)) : IO (Tensor Float (τ.prependDim batch))

Run several predictions through the trained stream result.

@[instance_reducible]

instance TorchLean.Trainer.StreamResult.instToString {σ τ : Shape} : ToString (StreamResult σ τ)

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

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

• first : Result σ₁ τ₁

  Trained result for the first model.

• second : Result σ₂ τ₂

  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 σ₁ τ₁ σ₂ τ₂)