Prediction and Training

Prediction and training methods on Trainer.Handle.

def TorchLean.Trainer.Implementation.predictWithRunner {σ τ : Shape} {task : Manual.SeqTask σ τ} {α : Type} [Context α] [DecidableEq Shape] [ToString α] [Runtime.FromFloat α] [Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α] (runner : Manual.Runner α task) (x : Tensor.T Float σ) : IO (Tensor.T Float τ)

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

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

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

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

Build the regression dispatch record used by Handle.train.

def TorchLean.Trainer.Implementation.crossEntropyHandle {σ τ : Shape} (trainer : Handle σ τ) (reduction : Loss.Reduction := 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 : Context α] → [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.predict {σ τ : Shape} (trainer : Handle σ τ) (x : Tensor.T Float σ) : IO (Tensor.T Float τ)

Predict 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.predict / trained.predictBatch methods to predict with the trained parameters.

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

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

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

Train the model with the loss and runtime settings stored in trainer.

The result stores the trained parameters together with prediction and reporting methods.

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 (StreamTrainResult σ τ)

Train a regression model 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 (PairStreamTrainResult σ₁ τ₁ σ₂ τ₂)

Train two regression models 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} [Context α] [DecidableEq Shape] [ToString α] [Runtime.FromFloat α] (trainer : Handle σ τ) (opts : Options) (data : Dataset σ τ) (trainOptions : TrainOptions := { }) (probes : List (Probe σ) := []) : IO (TrainResult σ τ)

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

Use this path from a runtime callback where Lean has already selected a concrete scalar α.