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:

• Muon is an optimizer, but the public runtime constructor requires an explicit orthogonalization backend. The identity backend is available for proofs and fallback behavior.
• GaLore is exposed as gradient-projection machinery around a base update. The public name is therefore optim.galore.projectedSGD, which says exactly which update rule owns the state.

@[reducible, inline]

abbrev TorchLean.optim.Optimizer : Type

Optimizer algorithm and hyperparameters used by Trainer.

structure TorchLean.optim.SgdConfig : Type

Public SGD optimizer configuration.

• lr : Float

  Learning rate.

• momentum : Float

  Momentum coefficient.

def TorchLean.optim.instReprSgdConfig.repr : SgdConfig → ℕ → Std.Format

@[implicit_reducible]

instance TorchLean.optim.instReprSgdConfig : Repr SgdConfig

structure TorchLean.optim.AdaGradConfig : Type

Public AdaGrad optimizer configuration.

• lr : Float

  Learning rate.

• epsilon : Float

  Numerical stabilizer.

def TorchLean.optim.instReprAdaGradConfig.repr : AdaGradConfig → ℕ → Std.Format

@[implicit_reducible]

instance TorchLean.optim.instReprAdaGradConfig : Repr AdaGradConfig

structure TorchLean.optim.RMSPropConfig : Type

Public RMSProp optimizer configuration.

• lr : Float

  Learning rate.

• decay : Float

  Decay coefficient for the running average of squared gradients.

• epsilon : Float

  Numerical stabilizer.

@[implicit_reducible]

instance TorchLean.optim.instReprRMSPropConfig : Repr RMSPropConfig

def TorchLean.optim.instReprRMSPropConfig.repr : RMSPropConfig → ℕ → Std.Format

structure TorchLean.optim.AdamConfig : Type

Public Adam optimizer configuration.

• lr : Float

  Learning rate.

• beta1 : Float

  First moment coefficient.

• beta2 : Float

  Second moment coefficient.

• epsilon : Float

  Numerical stabilizer.

@[implicit_reducible]

instance TorchLean.optim.instReprAdamConfig : Repr AdamConfig

def TorchLean.optim.instReprAdamConfig.repr : AdamConfig → ℕ → Std.Format

structure TorchLean.optim.AdamWConfigextends TorchLean.optim.AdamConfig : Type

Public AdamW optimizer configuration.

• lr : Float
• beta1 : Float
• beta2 : Float
• epsilon : Float
• weightDecay : Float

  Decoupled weight decay.

def TorchLean.optim.instReprAdamWConfig.repr : AdamWConfig → ℕ → Std.Format

@[implicit_reducible]

instance TorchLean.optim.instReprAdamWConfig : Repr AdamWConfig

structure TorchLean.optim.AdadeltaConfig : Type

Public Adadelta optimizer configuration.

• lr : Float

  Learning rate.

• rho : Float

  Decay coefficient for gradient/update accumulators.

• epsilon : Float

  Numerical stabilizer.

@[implicit_reducible]

instance TorchLean.optim.instReprAdadeltaConfig : Repr AdadeltaConfig

def TorchLean.optim.instReprAdadeltaConfig.repr : AdadeltaConfig → ℕ → Std.Format

def TorchLean.optim.sgd (cfg : SgdConfig) : Optimizer

SGD optimizer config, written optim.sgd { lr := 0.05 }.

def TorchLean.optim.momentumSGD (cfg : SgdConfig) : Optimizer

Momentum SGD, using momentum 0.9 when the configuration leaves it at zero.

def TorchLean.optim.adagrad (cfg : AdaGradConfig) : Optimizer

AdaGrad optimizer config, written optim.adagrad { lr := 0.05 }.

def TorchLean.optim.rmsprop (cfg : RMSPropConfig) : Optimizer

RMSProp optimizer config, written optim.rmsprop { lr := 1e-3 }.

def TorchLean.optim.adam (cfg : AdamConfig) : Optimizer

Adam optimizer config, written optim.adam { lr := 1e-3 }.

def TorchLean.optim.adamw (cfg : AdamWConfig) : Optimizer

AdamW optimizer config, written optim.adamw { lr := 1e-3, weightDecay := 0.01 }.

def TorchLean.optim.adadelta (cfg : AdadeltaConfig) : Optimizer

Adadelta optimizer config, written optim.adadelta {}.

inductive TorchLean.optim.Kind : Type

Optimizer names accepted by model-training commands.

• sgd : Kind
• adagrad : Kind
• rmsprop : Kind
• adam : Kind
• adamw : Kind
• adadelta : Kind

@[implicit_reducible]

instance TorchLean.optim.instDecidableEqKind : DecidableEq Kind

@[implicit_reducible]

instance TorchLean.optim.instReprKind : Repr Kind

def TorchLean.optim.instReprKind.repr : Kind → ℕ → Std.Format

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

Parse an optimizer name used by --optim.

def TorchLean.optim.Kind.name : Kind → String

Name written to logs and summaries.

def TorchLean.optim.Kind.toOptimizer (kind : Kind) (lr : Float) : Optimizer

Build the selected optimizer with the defaults used by training commands.

def TorchLean.optim.runtimeAdam {α : Type} [Context α] (lr beta1 beta2 epsilon : α) {paramShapes : List Shape} : Runtime.Autograd.TorchLean.Optimizer α paramShapes

Runtime Adam optimizer for module-level training.

def TorchLean.optim.runtimeAdamW {α : Type} [Context α] (lr weightDecay beta1 beta2 epsilon : α) {paramShapes : List Shape} : Runtime.Autograd.TorchLean.Optimizer α paramShapes

Runtime AdamW optimizer for module-level training.

def TorchLean.optim.runtimeSGD {α : Type} [Context α] (lr : α) {paramShapes : List Shape} : Runtime.Autograd.TorchLean.Optimizer α paramShapes

Runtime SGD optimizer for module-level training.

def TorchLean.optim.runtimeMomentumSGD {α : Type} [Context α] (lr momentum : α) {paramShapes : List Shape} : Runtime.Autograd.TorchLean.Optimizer α paramShapes

Runtime momentum-SGD optimizer for module-level training.

def TorchLean.optim.runtimeAdaGrad {α : Type} [Context α] (lr epsilon : α) {paramShapes : List Shape} : Runtime.Autograd.TorchLean.Optimizer α paramShapes

Runtime AdaGrad optimizer for module-level training.

def TorchLean.optim.runtimeRMSProp {α : Type} [Context α] (lr decay epsilon : α) {paramShapes : List Shape} : Runtime.Autograd.TorchLean.Optimizer α paramShapes

Runtime RMSProp optimizer for module-level training.

def TorchLean.optim.runtimeAdadelta {α : Type} [Context α] (lr rho epsilon : α) {paramShapes : List Shape} : Runtime.Autograd.TorchLean.Optimizer α paramShapes

Runtime Adadelta optimizer for module-level training.

@[reducible, inline]

abbrev TorchLean.optim.MuonOrthogonalizer (α : Type) (s : Shape) : Type

Orthogonalization backend for a matrix-shaped update.

Muon uses a momentum buffer and then replaces the raw momentum direction by an approximately orthogonalized update, commonly via Newton-Schulz iterations. TorchLean keeps this as an explicit backend so the pure update rule is testable before CUDA kernels are introduced.

def TorchLean.optim.identityMuonOrthogonalizer {α : Type} {s : Shape} : MuonOrthogonalizer α s

The identity orthogonalizer, used when Muon is requested without a matrix backend.

def TorchLean.optim.runtimeMuon {α : Type} [Context α] (lr momentum : α) (orthogonalizer : {s : Shape} → MuonOrthogonalizer α s := fun {s : Shape} => identityMuonOrthogonalizer) {paramShapes : List Shape} : Runtime.Autograd.TorchLean.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.identityProjector {α : Type} {s : Shape} : Projector α s s

Identity projector, used when projected SGD is requested without a projection backend.

def TorchLean.optim.galore.projectedSGD {α : Type} [Context α] (lr : α) (projector : {s : Shape} → Projector α s s := fun {s : Shape} => identityProjector) {paramShapes : List Shape} : Runtime.Autograd.TorchLean.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.