Training Results

Regression, cross-entropy, and custom losses all return the same trained-model type. Capabilities that do not apply to every task, such as the current IBP verifier, are stored as optional operations.

structure TorchLean.Trainer.VerificationReport : Type

Result of checking an output box with the trained-model IBP verifier.

• 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.VerificationReport.summary (report : VerificationReport) : String

One-line verification summary.

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

Print the verification summary.

@[implicit_reducible]

instance TorchLean.Trainer.VerificationReport.instToString : ToString VerificationReport

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

A trained TorchLean model.

The handle owns the live runtime state through its closures. predict and predictBatch are available for every task. verifyRobustLInf? is present when the training path can compile the trained parameters to the checked IBP verifier.

• report : TrainSummary

  Before/after scalar summary for the completed run.

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

  Run one Float input through the trained model.

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

  Run several Float inputs through the trained model.

• verifyRobustLInf? : Option (Tensor.T Float σ → Float → IO VerificationReport)

  Optional verifier for a uniform $\ell_\infty$ input ball.

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

One-line summary for the completed training run.

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

Print the before/after training summary.

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

Print one prediction with a caller-supplied label.

def TorchLean.Trainer.TrainResult.verifyRobustLInf {σ τ : Shape} (result : TrainResult σ τ) (center : Tensor.T Float σ) (eps : Float) : IO VerificationReport

Verify a uniform $\ell_\infty$ ball around center.

The method fails explicitly when the training path did not attach the checked IBP capability.

def TorchLean.Trainer.TrainResult.printRobustLInf {σ τ : Shape} (result : TrainResult σ τ) (center : Tensor.T Float σ) (eps : Float) : IO Unit

Verify a uniform $\ell_\infty$ ball and print the resulting output interval.

@[implicit_reducible]

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

structure TorchLean.Trainer.StreamTrainResult (σ τ : 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 trained handle is paired with the evaluation curve collected from a caller-provided sample.

• result : TrainResult σ τ

  Trained model handle.

• curve : Training.Curve

  Evaluation loss curve recorded during stream training.

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

One-line summary for the trained stream run.

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

Print the stream training summary.

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

Run one prediction through the trained stream result.

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

Run several predictions through the trained stream result.

@[implicit_reducible]

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

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

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

• first : TrainResult σ₁ τ₁

  Trained handle for the first model.

• second : TrainResult σ₂ τ₂

  Trained handle for the second model.

• curve : Training.Curve

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

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

One-line summary for the two trained models.

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

Print the trained-handle summary for both models.

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

Print the endpoints of the coupled metric curve.

@[implicit_reducible]

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