TorchLean Trainer Results

Public trained-result handles and verification reports for the unified trainer facade.

structure TorchLean.Trainer.Implementation.Regression.LInfIBPRequest (σ : Shape) : Type

Uniform ℓ∞ verification request for a trained regression model.

The request is deliberately small: one center input and one radius. It maps cleanly to TorchLean's existing verifier stack:

1. compile the trained forward model to verifier IR,
2. seed the distinguished input node with an ℓ∞ box,
3. run IBP,
4. report the certified output interval.

The report is not a replacement for richer robustness specifications; it is the compact public door into the checked verifier path.

• center : Tensor.T Float σ

  Center of the input perturbation box, written as a normal Float tensor.

• eps : Float

  Uniform ℓ∞ radius around center.

structure TorchLean.Trainer.Implementation.Regression.VerificationReport : Type

Public result of an ℓ∞ IBP verification run.

Bounds are rendered as strings because the trained handle hides the runtime-selected scalar type inside a closure. That keeps the API usable from ordinary scripts while still running the verifier over the same scalar backend used for training.

• nodes : ℕ

  Number of IR nodes in the compiled verifier graph.

• outputDim : ℕ

  Flattened output dimension reported by the verifier.

• lo : String

  Lower bound on the flattened output box.

• hi : String

  Upper bound on the flattened output box.

def TorchLean.Trainer.Implementation.Regression.VerificationReport.summary (report : VerificationReport) : String

One-line verification summary.

def TorchLean.Trainer.Implementation.Regression.VerificationReport.printSummary (report : VerificationReport) : IO Unit

Print the verification summary to stdout.

@[implicit_reducible]

instance TorchLean.Trainer.Implementation.Regression.VerificationReport.instToString : ToString VerificationReport

structure TorchLean.Trainer.Implementation.Regression.TrainResult (σ τ : Shape) : Type

Result of training a regression trainer.

The trained runner stays alive behind the returned closures, so callers can immediately reuse the trained model for inference without reopening the runtime API directly.

• report : TrainSummary

  Before/after loss summary for the completed training run.

• predict : Tensor.T Float σ → IO (Tensor.T Float τ)

  Run one Float input through the trained model and return the output tensor.

• predictBatch : List (Tensor.T Float σ) → IO (List (Tensor.T Float τ))

  Run several Float inputs through the trained model and return their output tensors.

• verify : LInfIBPRequest σ → IO VerificationReport

  Run a public robustness check against the trained model.

structure TorchLean.Trainer.Implementation.Regression.StreamTrainResult (σ τ : Shape) : Type

Result of training from a step-indexed regression stream.

Generated or resampled workloads may not have one static dataset to summarize: diffusion noising schedules, PDE collocation batches, RL replay-style batches, and similar loops. The trained model handle is the same one returned by ordinary training; the extra field is the explicit loss curve collected from a caller-provided evaluation sample.

• result : TrainResult σ τ

  Trained model handle with prediction and verification closures.

• curve : Training.Curve

  Evaluation loss curve recorded during stream training.

structure TorchLean.Trainer.Implementation.Regression.PairStreamTrainResult (σ₁ τ₁ σ₂ τ₂ : Shape) : Type

Result of training two regression trainers in one alternating stream.

GAN-style examples need this shape: one checked model is stepped on one stream, another checked model is stepped on a related stream, and the report is a task-specific scalar such as total generator/discriminator loss. The public result still returns ordinary trained handles for both models, so post-training code uses predict instead of touching module state directly.

• first : TrainResult σ₁ τ₁

  Trained handle for the first trainer.

• second : TrainResult σ₂ τ₂

  Trained handle for the second trainer.

• curve : Training.Curve

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

def TorchLean.Trainer.Implementation.Regression.TrainResult.summary {σ τ : Shape} (result : TrainResult σ τ) : String

One-line summary for the completed training run.

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

Print the before/after training summary to stdout.

def TorchLean.Trainer.Implementation.Regression.TrainResult.printPrediction {σ τ : Shape} (result : TrainResult σ τ) (label : String) (x : Tensor.T Float σ) : IO Unit

Run one regression prediction and print it with a user-provided label.

This is the small "train, then inspect one heldout example" helper used by tutorials.

@[implicit_reducible]

instance TorchLean.Trainer.Implementation.Regression.TrainResult.instToString {σ τ : Shape} : ToString (TrainResult σ τ)

def TorchLean.Trainer.Implementation.Regression.StreamTrainResult.summary {σ τ : Shape} (result : StreamTrainResult σ τ) : String

One-line summary for the trained stream run.

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

Print the stream training summary to stdout.

def TorchLean.Trainer.Implementation.Regression.StreamTrainResult.predict {σ τ : Shape} (result : StreamTrainResult σ τ) (x : Tensor.T Float σ) : IO (Tensor.T Float τ)

Run one prediction through the trained model produced by stream training.

Stream training carries an extra loss curve. This forwarding method keeps stream examples concise: call stream.predict x on the stream result instead of reaching through the trained handle field.

def TorchLean.Trainer.Implementation.Regression.StreamTrainResult.predictBatch {σ τ : Shape} (result : StreamTrainResult σ τ) (xs : List (Tensor.T Float σ)) : IO (List (Tensor.T Float τ))

Run several predictions through the trained model produced by stream training.

@[implicit_reducible]

instance TorchLean.Trainer.Implementation.Regression.StreamTrainResult.instToString {σ τ : Shape} : ToString (StreamTrainResult σ τ)

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

One-line summary for the two trained models.

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

Print the trained-handle summary for both models.

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

Print a before/after summary for the paired task curve.

Paired-model examples usually care about a coupled metric such as total GAN loss. That metric lives in result.curve, not in either trained handle alone, so this operation gives examples one standard before/after line without peeking at curve.values.

@[implicit_reducible]

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

structure TorchLean.Trainer.Implementation.CrossEntropy.TrainResult (σ τ : Shape) : Type

Result of training a general one-hot cross-entropy trainer.

Sequence-model friendly trained handle: it owns the trained runner and gives callers ordinary Float prediction tensors. Text examples can then decode logits however they like without threading runtime runner/module state through the example.

• report : TrainSummary

  Before/after loss summary for the completed training run.

• predict : Tensor.T Float σ → IO (Tensor.T Float τ)

  Run one Float input through the trained model and return logits/output tensor.

• predictBatch : List (Tensor.T Float σ) → IO (List (Tensor.T Float τ))

  Run several Float inputs through the trained model.

def TorchLean.Trainer.Implementation.CrossEntropy.TrainResult.summary {σ τ : Shape} (result : TrainResult σ τ) : String

One-line summary for the completed training run.

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

Print the before/after training summary to stdout.

def TorchLean.Trainer.Implementation.CrossEntropy.TrainResult.printPrediction {σ τ : Shape} (result : TrainResult σ τ) (label : String) (x : Tensor.T Float σ) : IO Unit

Run one prediction and print it with a user-provided label.

@[implicit_reducible]

instance TorchLean.Trainer.Implementation.CrossEntropy.TrainResult.instToString {σ τ : Shape} : ToString (TrainResult σ τ)

structure TorchLean.Trainer.Implementation.Custom.TrainResult (σ τ : Shape) : Type

Result of training a custom supervised trainer.

The trained handle mirrors CrossEntropy.TrainResult: custom objectives affect training, but inference is still just "run the checked model on a Float tensor". Keeping that surface identical means examples can switch from a canned loss to a task-specific loss without rewriting their prediction/reporting code.

• report : TrainSummary

  Before/after loss summary for the completed training run.

• predict : Tensor.T Float σ → IO (Tensor.T Float τ)

  Run one Float input through the trained model and return its output tensor.

• predictBatch : List (Tensor.T Float σ) → IO (List (Tensor.T Float τ))

  Run several Float inputs through the trained model.

def TorchLean.Trainer.Implementation.Custom.TrainResult.summary {σ τ : Shape} (result : TrainResult σ τ) : String

One-line summary for the completed training run.

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

Print the before/after training summary to stdout.

def TorchLean.Trainer.Implementation.Custom.TrainResult.printPrediction {σ τ : Shape} (result : TrainResult σ τ) (label : String) (x : Tensor.T Float σ) : IO Unit

Run one prediction and print it with a user-provided label.

@[implicit_reducible]

instance TorchLean.Trainer.Implementation.Custom.TrainResult.instToString {σ τ : Shape} : ToString (TrainResult σ τ)