TorchLean Regression Trainer Implementation

Regression dataset training for the public trainer facade.

This namespace contains the dependent runner machinery behind the public regression trainer. The surface stays small: examples talk about models, datasets, and artifacts, while this file carries the shape-indexed runtime details.

def TorchLean.Trainer.Implementation.Regression.Internal.withRunnerFromRunConfig {σ τ : Shape} {β : Type} (trainer : Regression σ τ) (run : RunConfig) (k : {α : Type} → [inst : Runtime.SemanticScalar α] → [inst_1 : DecidableEq Shape] → [ToString α] → [Runtime.Scalar α] → [Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α] → NN.API.train.Advanced.Runner α trainer.task → IO β) : IO β

Run a regression trainer directly from a public RunConfig.

This is the non-CLI execution seam for the public facade. It deliberately avoids Advanced.run trainer.task run.toArgs, because that CLI-oriented path is designed for executable commands that parse and print runtime flags themselves. Public trainer methods already hold a RunConfig, so they can instantiate the runner directly and keep the user-facing output clean.

def TorchLean.Trainer.Implementation.Regression.Internal.trainedHandle {σ τ : Shape} {α : Type} [Runtime.SemanticScalar α] [DecidableEq Shape] [ToString α] [Runtime.Scalar α] [Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α] (trainer : Regression σ τ) (runner : NN.API.train.Advanced.Runner α trainer.task) (steps : ℕ) (before after : α) : TrainResult σ τ

Build the public trained regression result from an already-trained runner.

Both dataset and stream training end at the same place: a runner whose parameters have been updated. This operation packages that runner behind the stable public surface:

• predict casts ordinary Float tensors into the selected runtime scalar,
• predictBatch runs the same prediction path on a batched tensor,
• verify compiles the trained model into verifier IR and runs the public IBP request.

Keeping this here prevents every training variant from re-copying the same trained-model closures.

def TorchLean.Trainer.Implementation.Regression.Internal.trainDatasetWithRunConfigCore {σ τ : Shape} {β : Type} (trainer : Regression σ τ) (run : RunConfig) (data : Dataset σ τ) (cfg : NN.API.TorchLean.Trainer.TrainConfig) (probes : List (Probe σ) := []) (afterTrain : {α : Type} → [inst : Runtime.SemanticScalar α] → [inst_1 : DecidableEq Shape] → [ToString α] → [Runtime.Scalar α] → NN.API.train.Advanced.Runner α trainer.task → IO β) : IO (TrainResult σ τ × β)

Shared regression training core for already-parsed public runtime settings.

This is the path used by trainer.train and the regression implementation handle. It mirrors the CLI-backed trainer body, but starts from RunConfig instead of CLI strings, so public API calls do not print or parse runtime settings twice.

def TorchLean.Trainer.Implementation.Regression.trainWithRun {σ τ : Shape} (trainer : Regression σ τ) (data : Dataset σ τ) (run : RunConfig := trainer.runConfig) (opts : TrainOptions := { }) (probes : List (Probe σ) := []) : IO (TrainResult σ τ)

Train on an in-memory regression dataset using an explicit runtime override.

Use this when one call should temporarily override the optimizer/backend/dtype/device settings attached to the trainer.

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

Train on an in-memory regression dataset using the trainer's attached runtime settings.

This is the compact public entrypoint for ordinary user code:

• put persistent optimizer/backend/dtype/device choices on the trainer value itself,
• pass per-training-call knobs such as steps and logEvery here.