Custom-Loss Training

Custom checked supervised-loss training for the trainer API.

def TorchLean.Trainer.Implementation.Custom.Internal.meanModuleLoss {σ τ : Shape} {α : Type} [Context α] [DecidableEq Shape] [Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α] (model : nn.Sequential σ τ) (m : Runtime.Autograd.TorchLean.ScalarModule α (Runtime.Autograd.TorchLean.NN.Seq.paramShapes model) [σ, τ]) (samples : List (SupervisedSample α σ τ)) : IO α

Mean loss for the custom trainer's concrete runtime module.

def TorchLean.Trainer.Implementation.Custom.Internal.trainDatasetWithRunConfigCore {σ τ : Shape} {β : Type} (trainer : Custom σ τ) (run : RunConfig) (data : Dataset σ τ) (trainOpts : TrainOptions) (afterTrain : {α : Type} → [inst : Context α] → [inst_1 : DecidableEq Shape] → [ToString α] → [Runtime.FromFloat α] → (model : nn.Sequential σ τ) → Runtime.Autograd.TorchLean.ScalarModule α (Runtime.Autograd.TorchLean.NN.Seq.paramShapes model) [σ, τ] → IO β) : IO (TrainResult σ τ × β)

Shared custom-loss training core for already-parsed public runtime settings.

This opens a ScalarModule for a custom supervised objective. The unified Trainer.new ... { task := .custom ... } path uses the same checked module/loss/optimizer machinery as the runtime trainer.

def TorchLean.Trainer.Implementation.Custom.trainWithRun {σ τ : Shape} (trainer : Custom σ τ) (data : Dataset σ τ) (run : RunConfig := trainer.runConfig) (opts : TrainOptions := { }) : IO (TrainResult σ τ)

Train on an in-memory dataset with a custom checked supervised loss and an explicit runtime override.

The shape matches the canned trainers: runtime choices come from RunConfig, training/logging choices come from TrainOptions, and the returned handle owns the trained model for prediction.

def TorchLean.Trainer.Implementation.Custom.train {σ τ : Shape} (trainer : Custom σ τ) (data : Dataset σ τ) (opts : TrainOptions := { }) : IO (TrainResult σ τ)

Train on an in-memory dataset using this custom trainer's attached runtime settings.