TorchLean Public Trainer Methods

Unified trained result and public methods on Trainer.Handle.

def TorchLean.Trainer.Implementation.evalWithRunner {σ τ : Shape} {task : NN.API.TorchLean.Trainer.Task σ τ} {α : Type} [Runtime.SemanticScalar α] [DecidableEq Shape] [ToString α] [Runtime.Scalar α] [Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α] (runner : NN.API.train.Advanced.Runner α task) (x : Tensor.T Float σ) : IO (Tensor.T Float τ)

Evaluate one Float input through a runtime runner and return a Float output.

def TorchLean.Trainer.Implementation.evalCustomWithRunConfig {σ τ : Shape} (trainer : Custom σ τ) (run : RunConfig) (x : Tensor.T Float σ) : IO (Tensor.T Float τ)

Evaluate one input through a custom-loss trainer without first running training.

def TorchLean.Trainer.Implementation.regressionHandle {σ τ : Shape} (trainer : Handle σ τ) (reduction : Loss.Reduction := Runtime.Autograd.TorchLean.Loss.Reduction.mean) : Regression σ τ

Build the regression dispatch record used by Handle.train.

def TorchLean.Trainer.Implementation.crossEntropyHandle {σ τ : Shape} (trainer : Handle σ τ) (reduction : Loss.Reduction := Runtime.Autograd.TorchLean.Loss.Reduction.mean) : CrossEntropy σ τ

Build the cross-entropy dispatch record used by Handle.train.

def TorchLean.Trainer.Implementation.customHandle {σ τ : Shape} (trainer : Handle σ τ) (loss : {α : Type} → [inst : Runtime.TensorScalar α] → [inst_1 : DecidableEq Shape] → Runtime.Autograd.TorchLean.Program α [τ, τ] Shape.scalar) : Custom σ τ

Build the custom-loss dispatch record used by Handle.train.

def TorchLean.Trainer.Handle.eval {σ τ : Shape} (trainer : Handle σ τ) (x : Tensor.T Float σ) : IO (Tensor.T Float τ)

Evaluate one input using the trainer's current model and runtime settings.

Inference before any training call. After training, use the returned trained handle's trained.eval / trained.evalBatch methods to evaluate the trained parameters.

def TorchLean.Trainer.Handle.evalBatch {σ τ : Shape} (trainer : Handle σ τ) (xs : List (Tensor.T Float σ)) : IO (List (Tensor.T Float τ))

Evaluate a list of inputs using the trainer's current model and runtime settings.

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

Result returned by the unified public Trainer.train method.

• regression {σ τ : Shape} (result : Implementation.Regression.TrainResult σ τ) : TrainResult σ τ

  Trained regression model.

• crossEntropy {σ τ : Shape} (result : Implementation.CrossEntropy.TrainResult σ τ) : TrainResult σ τ

  Trained one-hot cross-entropy model.

• custom {σ τ : Shape} (result : Implementation.Custom.TrainResult σ τ) : TrainResult σ τ

  Trained custom-loss model.

def TorchLean.Trainer.TrainResult.report {σ τ : Shape} : TrainResult σ τ → TrainSummary

The before/after scalar summary for this training run.

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

One-line summary suitable for quickstarts and scripts.

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

Print the standard before/after training summary.

def TorchLean.Trainer.TrainResult.eval {σ τ : Shape} : TrainResult σ τ → Tensor.T Float σ → IO (Tensor.T Float τ)

Evaluate one input using the trained model.

def TorchLean.Trainer.TrainResult.evalBatch {σ τ : Shape} : TrainResult σ τ → List (Tensor.T Float σ) → IO (List (Tensor.T Float τ))

Evaluate a list of inputs using the trained model.

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

Print one prediction from a unified trained handle.

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

Verify an ℓ∞ input ball for a trained regression handle.

@[implicit_reducible]

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

def TorchLean.Trainer.Handle.train {σ τ : Shape} (trainer : Handle σ τ) (data : Dataset σ τ) (trainOptions : TrainOptions := { }) (probes : List (Probe σ) := []) : IO (TrainResult σ τ)

Train a unified public trainer.

Main user-facing training method: one trainer value, one task field, and one trained result.

def TorchLean.Trainer.Handle.trainStreamFloat {σ τ : Shape} (trainer : Handle σ τ) (opts : Options) (sampleAt : ℕ → SupervisedSample Float σ τ) (evalSample : SupervisedSample Float σ τ) (trainOptions : TrainOptions := { }) (curveEvery cudaMemWatch : ℕ := 0) (onEval : ℕ → String → (Tensor.T Float σ → IO (Tensor.T Float τ)) → IO Unit := fun (x : ℕ) (x_1 : String) (x_2 : Tensor.T Float σ → IO (Tensor.T Float τ)) => pure ()) : IO (Implementation.Regression.StreamTrainResult σ τ)

Train a unified regression trainer from a Float sample stream.

Generated-data examples use this when there is no fixed Dataset to hand to trainer.train.

def TorchLean.Trainer.Handle.trainPairStreamFloat {σ₁ τ₁ σ₂ τ₂ : Shape} (first : Handle σ₁ τ₁) (second : Handle σ₂ τ₂) (opts : Options) (firstSampleAt : ℕ → SupervisedSample Float σ₁ τ₁) (secondSamplesAt : ℕ → List (SupervisedSample Float σ₂ τ₂)) (evalTotal : (Tensor.T Float σ₁ → IO (Tensor.T Float τ₁)) → (Tensor.T Float σ₂ → IO (Tensor.T Float τ₂)) → IO Float) (trainOptions : TrainOptions := { }) (curveEvery : ℕ := 1) (cudaMemWatch : ℕ := 0) : IO (Implementation.Regression.PairStreamTrainResult σ₁ τ₁ σ₂ τ₂)

Train two unified regression trainers from coupled Float streams.

GAN-style examples use this path when two regression trainers have to step together, without opening the lower-level runtime modules directly.

def TorchLean.Trainer.Handle.trainSelectedCrossEntropy {σ τ : Shape} {α : Type} [Runtime.SemanticScalar α] [DecidableEq Shape] [ToString α] [Runtime.Scalar α] (trainer : Handle σ τ) (opts : Options) (data : Dataset σ τ) (trainOptions : TrainOptions := { }) (probes : List (Probe σ) := []) : IO (Implementation.CrossEntropy.TrainResult σ τ)

Train a unified cross-entropy trainer after the scalar type has already been selected.

Advanced scalar-selected cross-entropy training. Use this path from dispatchers such as ModelZoo.runAnyOrFloatNoCast, where the callback already has a concrete scalar α.