Training Configuration

Probes, run-configuration helpers, and per-training options for the trainer API. Command-line parsing is available separately from NN.API.CLI.Trainer, keeping process flags out of these configuration records.

structure TorchLean.Trainer.Probe (σ : Shape) : Type

A small input probe evaluated at the start and end of training.

• name : String

  Human-facing probe name.

• inputText : String

  Human-facing input description.

• input : Tensor Float σ

  Concrete input converted to the selected runtime arithmetic when the probe runs.

• expected : Option String

  Optional expected value shown beside the prediction.

def TorchLean.Trainer.Probe.tensor {σ : Shape} (name : String) (input : Tensor Float σ) (inputText : String := "") (expected : Option String := none) : Probe σ

Build a named prediction probe from a tensor.

Example:

-- Probes print a named prediction before and after the run, so training shows its movement
-- without a separate evaluation script.
def probes : Array (Trainer.Probe [2]) :=
  #[Trainer.Probe.tensor "heldout" [0.25, -0.75] (inputText := "x = (0.25, -0.75)")]

def TorchLean.Trainer.RunConfig.withDevice (run : RunConfig) (device : NN.Backend.Device) : Except String RunConfig

Override the execution device using a maintained backend profile.

def TorchLean.Trainer.RunConfig.withBackendProfile (run : RunConfig) (profile : NN.Backend.BackendProfile) : RunConfig

Select a complete backend contract profile.

The profile carries the device, provider preference, assurance policy, VJP ownership, and capsule registry together. It can select, for example, LibTorch forward execution with a TorchLean-owned backward pass.

def TorchLean.Trainer.RunConfig.withBackendReport (run : RunConfig) (enabled : Bool := true) : RunConfig

Enable or disable first-use backend capsule reporting.

def TorchLean.Trainer.RunConfig.withRuntime (run : RunConfig) (runtime : Runtime.Config) : RunConfig

Apply runtime execution settings to a persistent trainer run configuration.

def TorchLean.Trainer.RunConfig.fromRuntime (runtime : Runtime.Config) (base : RunConfig := { }) : RunConfig

Build a trainer run configuration from a runtime configuration and trainer choices.

def TorchLean.Trainer.RunConfig.executionSettings (run : RunConfig) : Runtime.Config

Execution settings carried by this trainer configuration.

def TorchLean.Trainer.RunConfig.forObjective {σ τ : Shape} (run : RunConfig) (objective : Objective τ := Objective.meanSquaredError) (seed : ℕ := 0) : Config σ τ

Attach a training objective and initialization seed to these run settings.

structure TorchLean.Trainer.TrainOptions : Type

Per-training-call options for the trainer API.

steps has no default so that trainer.train data {} cannot silently perform a single update.

Example:

-- `steps` has no default on purpose: how long to train is not a library's decision.
def options : Trainer.TrainOptions :=
  { steps := 200
    logEvery := 25
    saveCheckpoint? := some "checkpoints/mlp.state" }

• steps : ℕ

  Number of optimizer updates.

• samplesPerStep : ℕ

  Number of dataset items whose gradients are accumulated into one optimizer update.

  The items are processed one after another and their gradients are averaged at the same parameter point; this is gradient accumulation, not a vectorized minibatch. To run a vectorized minibatch, give the model an explicit batch axis and build the dataset with Data.batch, whose items are already fixed-size tensor minibatches, then keep this option at 1.

• scheduler : Option Scheduler.Config

  Optional learning-rate schedule, indexed by completed optimizer updates.

• logEvery : ℕ

  Print step losses every logEvery updates; 0 disables stdout step logging.

• cudaMemorySampleEvery : ℕ

  Sample CUDA allocator state every this many completed updates; 0 disables sampling.

• logDestination : Training.LogDestination

  Optional TrainLog artifact destination. Use .disabled for stdout-only runs.

• logTitle : String

  Title used when writing a TrainLog artifact.

• logNotes : Array String

  Free-form notes attached to the TrainLog artifact.

• loadCheckpoint? : Option System.FilePath

  Optional model-state checkpoint loaded before training; optimizer and schedule start fresh.

• saveCheckpoint? : Option System.FilePath

  Optional model-state checkpoint written after training.

def TorchLean.Trainer.TrainOptions.validate (options : TrainOptions) : Except String Unit

Reject option combinations that cannot describe a training run.