Cross-Entropy Training

One-hot cross-entropy training for classifiers, text windows, and structured logit tensors.

def TorchLean.Trainer.Implementation.CrossEntropy.Internal.castParamBits {α : Type} [Context α] [Runtime.FromFloat α] {ss : List Shape} : TensorPack Float ss → TensorPack α ss

Cast a Float checkpoint payload to the runtime scalar selected for the current run.

def TorchLean.Trainer.Implementation.CrossEntropy.Internal.paramsToFloatIO {α : Type} [Context α] [Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α] {ss : List Shape} : TensorPack α ss → IO (TensorPack Float ss)

Convert a runtime parameter payload back to the public Float checkpoint format.

def TorchLean.Trainer.Implementation.CrossEntropy.Internal.loadCheckpointIfSome {σ τ : Shape} {α : Type} [Context α] [Runtime.FromFloat α] [DecidableEq Shape] (trainer : CrossEntropy σ τ) (runner : Manual.Runner α trainer.task) (path? : Option System.FilePath) : IO Unit

Load optional checkpoint bits into a cross-entropy runner before training.

The saved file is checked against the model's parameter shapes first, then cast into the selected runtime scalar. That means stale checkpoints fail at the boundary instead of silently perturbing a training run.

def TorchLean.Trainer.Implementation.CrossEntropy.Internal.saveCheckpointIfSome {σ τ : Shape} {α : Type} [Context α] [Runtime.FromFloat α] [DecidableEq Shape] [Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α] (trainer : CrossEntropy σ τ) (runner : Manual.Runner α trainer.task) (path? : Option System.FilePath) : IO Unit

Save optional trained checkpoint bits from a cross-entropy runner.

def TorchLean.Trainer.Implementation.CrossEntropy.Internal.withRunnerFromRunConfig {σ τ : Shape} {β : Type} (trainer : CrossEntropy σ τ) (run : RunConfig) (k : {α : Type} → [inst : Context α] → [inst_1 : DecidableEq Shape] → [ToString α] → [Runtime.FromFloat α] → [Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α] → Manual.Runner α trainer.task → IO β) : IO β

Run a general cross-entropy trainer directly from a public RunConfig.

Same direct runtime path used by regression/classifier trainers. It does not serialize the config back into CLI flags or expose a Runner callback to ordinary examples.

def TorchLean.Trainer.Implementation.CrossEntropy.Internal.trainDatasetWithSelectedRunnerCore {σ τ : Shape} {β α : Type} [Context α] [DecidableEq Shape] [ToString α] [Runtime.FromFloat α] [Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α] (trainer : CrossEntropy σ τ) (runner : Manual.Runner α trainer.task) (run : RunConfig) (data : Dataset σ τ) (opts : TrainOptions) (probes : List (Probe σ) := []) (afterTrain : {α : Type} → [inst : Context α] → [inst_1 : DecidableEq Shape] → [ToString α] → [Runtime.FromFloat α] → Manual.Runner α trainer.task → IO β) : IO (TrainResult σ τ × β)

Shared cross-entropy training core for already-parsed public runtime settings.

This core is generic over shapes. It works for byte-level language-model windows, sequence-to-sequence one-hot targets, and other supervised tasks whose target is already encoded as a one-hot tensor with the same shape expected by the model loss.

def TorchLean.Trainer.Implementation.CrossEntropy.Internal.trainDatasetWithRunConfigCore {σ τ : Shape} {β : Type} (trainer : CrossEntropy σ τ) (run : RunConfig) (data : Dataset σ τ) (opts : TrainOptions) (probes : List (Probe σ) := []) (afterTrain : {α : Type} → [inst : Context α] → [inst_1 : DecidableEq Shape] → [ToString α] → [Runtime.FromFloat α] → Manual.Runner α trainer.task → IO β) : IO (TrainResult σ τ × β)

Shared cross-entropy training core for already-parsed runtime settings.

CLI commands may select the scalar type before calling into the public trainer. This entrypoint keeps that path inside the trainer API instead of exposing manual module calls to examples.

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

Train on an in-memory one-hot cross-entropy 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.CrossEntropy.trainSelected {σ τ : Shape} {α : Type} [Context α] [DecidableEq Shape] [ToString α] [Runtime.FromFloat α] (trainer : CrossEntropy σ τ) (runtimeOpts : Options) (data : Dataset σ τ) (trainOpts : TrainOptions := { }) (probes : List (Probe σ) := []) : IO (TrainResult σ τ)

Train with a runtime scalar that has already been selected by the caller.

Call trainer.train when the scalar should be chosen from trainer.runConfig.dtype. This method exists for model-zoo dispatchers that already run inside a runtime callback. At that point Lean has a concrete scalar type α, not merely a Runtime.DType tag. Even these deep-dive examples still use the public trainer API, so they do not have to open-code module creation, loss calls, or optimizer steps.

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

Train on an in-memory one-hot cross-entropy dataset using the trainer's attached runtime settings.

Sequence-model implementation behind trainer.train: persistent runtime choices live on the trainer, while step/logging choices live on TrainOptions.