Regression Training

Regression dataset training for the trainer API.

This namespace contains the dependent runner machinery behind the public regression trainer. The public API 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 : Context α] → [inst_1 : DecidableEq Shape] → [ToString α] → [Runtime.FromFloat α] → [NN.MLTheory.CROWN.BoundOps α] → [Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α] → Manual.Runner α trainer.task → IO β) : IO β

Run a regression trainer directly from a public RunConfig.

Direct non-CLI execution path for the public training API. It deliberately avoids Manual.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} [Context α] [DecidableEq Shape] [ToString α] [Runtime.FromFloat α] [NN.MLTheory.CROWN.BoundOps α] [Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α] (trainer : Regression σ τ) (runner : Manual.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 API:

• 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 : Manual.TrainConfig) (probes : List (Probe σ) := []) (afterTrain : {α : Type} → [inst : Context α] → [inst_1 : DecidableEq Shape] → [ToString α] → [Runtime.FromFloat α] → Manual.Runner α trainer.task → IO β) : IO (TrainResult σ τ × β)

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

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.

For ordinary training:

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