TorchLean Custom-Loss Trainer Implementation

Custom checked supervised-loss training for the public trainer facade.

def TorchLean.Trainer.Implementation.Custom.Internal.meanModuleLoss {σ τ : Shape} {α : Type} [Runtime.TensorScalar α] [DecidableEq Shape] [Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α] (model : nn.Sequential σ τ) (m : Module.ScalarModule α (nn.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 : Runtime.SemanticScalar α] → [inst_1 : DecidableEq Shape] → [ToString α] → [Runtime.Scalar α] → (model : nn.Sequential σ τ) → Module.ScalarModule α (nn.paramShapes model) [σ, τ] → IO β) : IO (TrainResult σ τ × β)

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

This is the public facade seam that 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.