Optimizers

Optimizer configuration records and runtime optimizer constructors.

The default trainer config exposes self-contained core update rules for SGD, momentum SGD, AdaGrad, RMSProp, Adam, AdamW, and Adadelta. Runtime-only extension points live here too:

• optim.muon.optimizer accepts an orthogonalization backend and defaults to the identity backend for proofs and fallback behavior.
• GaLore is exposed as gradient-projection machinery around a base update. The public name is therefore optim.galore.sgd, which says exactly which update rule owns the state.

def TorchLean.optim.Optimizer.validateFor {α : Type} [Runtime.FromFloat α] (optimizer : Optimizer) (scalarName : String := "the runtime scalar") : Except String Unit

Check the supplied configuration and its representation in the selected runtime scalar.

Float32 and IEEE32 reject overflow, positive stabilizers rounded to zero, and averaging coefficients rounded to one. Float retains binary64 domains. Custom scalar instances may supply Runtime.FromFloat.roundForValidation; its default retains the input-domain checks. scalarName labels conversion errors when an execution boundary selects a specific format.

inductive TorchLean.optim.Algorithm : Type

Optimizer algorithms accepted by model-training commands.

• sgd : Algorithm
• adaGrad : Algorithm
• rmsProp : Algorithm
• adam : Algorithm
• adamW : Algorithm
• adaDelta : Algorithm

@[instance_reducible]

instance TorchLean.optim.instDecidableEqAlgorithm : DecidableEq Algorithm

def TorchLean.optim.instReprAlgorithm.repr : Algorithm → ℕ → Std.Format

@[instance_reducible]

instance TorchLean.optim.instReprAlgorithm : Repr Algorithm

def TorchLean.optim.Algorithm.parse (value : String) : Except String Algorithm

Parse an optimizer name used by --optim.

def TorchLean.optim.Algorithm.displayName : Algorithm → String

Name written to logs and summaries.

def TorchLean.optim.Algorithm.configure (algorithm : Algorithm) (lr : Float) : Optimizer

Configure the selected algorithm with its command-line learning rate and defaults.

def TorchLean.optim.muon.optimizer {α : Type} [Storage α] [Context α] (lr momentum : α) (orthogonalizer : {s : Shape} → Orthogonalizer α s := fun {s : Shape} => Optim.Muon.identityOrthogonalizer) {paramShapes : List Shape} : Runtime.Autograd.Model.Optim.Optimizer α paramShapes

Runtime Muon-style optimizer for module-level training.

Muon is public at the runtime layer because a meaningful Muon run needs an orthogonalization backend. The default identity backend supports proofs and fallback behavior; production Muon should pass a matrix-shaped orthogonalizer.

def TorchLean.optim.galore.sgd {α : Type} [Storage α] [Context α] (lr : α) (projector : {s : Shape} → Projector α s s := fun {s : Shape} => Optim.GaLore.identityProjector) {paramShapes : List Shape} : Runtime.Autograd.Model.Optim.Optimizer α paramShapes

Projected-SGD runtime constructor for GaLore-style gradient projection.

This is a projection strategy wrapped around an SGD update. Full GaLore also needs a policy that constructs and refreshes low-rank projectors for matrix parameters; this constructor exposes the verified update boundary once a same-shape projector is supplied.