Optimizer Configuration

Optimizer algorithms and hyperparameters shared by the public training and runtime APIs.

inductive TorchLean.optim.Optimizer.Internal.View : Type

Closed optimizer representation used only when lowering the public configuration to a runtime.

• sgd (learningRate momentum : Float) : View
• adaGrad (learningRate epsilon : Float) : View
• rmsProp (learningRate decay epsilon : Float) : View
• adam (learningRate beta1 beta2 epsilon : Float) : View
• adamW (learningRate weightDecay beta1 beta2 epsilon : Float) : View
• adaDelta (learningRate rho epsilon : Float) : View

def TorchLean.optim.Optimizer.Internal.instReprView.repr : View → ℕ → Std.Format

@[instance_reducible]

instance TorchLean.optim.Optimizer.Internal.instReprView : Repr View

structure TorchLean.optim.Optimizer : Type

An optimizer configuration accepted by the trainer and manual-module APIs.

Construct values with optim.sgd, optim.adam, and the other record-based helpers. The sealed representation prevents positional runtime constructors from leaking into user code.

• representation : TorchLean.optim.Optimizer.Internal.View

structure TorchLean.optim.SGD.Config : Type

Public SGD optimizer configuration.

• learningRate : Float

  Learning rate.

• momentum : Float

  Momentum coefficient.

@[instance_reducible]

instance TorchLean.optim.SGD.instReprConfig : Repr Config

def TorchLean.optim.SGD.instReprConfig.repr : Config → ℕ → Std.Format

structure TorchLean.optim.AdaGrad.Config : Type

Public AdaGrad optimizer configuration.

• learningRate : Float

  Learning rate.

• epsilon : Float

  Numerical stabilizer.

@[instance_reducible]

instance TorchLean.optim.AdaGrad.instReprConfig : Repr Config

def TorchLean.optim.AdaGrad.instReprConfig.repr : Config → ℕ → Std.Format

structure TorchLean.optim.RMSProp.Config : Type

Public RMSProp optimizer configuration.

• learningRate : Float

  Learning rate.

• decay : Float

  Decay coefficient for the running average of squared gradients.

• epsilon : Float

  Numerical stabilizer.

@[instance_reducible]

instance TorchLean.optim.RMSProp.instReprConfig : Repr Config

def TorchLean.optim.RMSProp.instReprConfig.repr : Config → ℕ → Std.Format

structure TorchLean.optim.Adam.Config : Type

Public Adam optimizer configuration.

• learningRate : Float

  Learning rate.

• beta1 : Float

  First moment coefficient.

• beta2 : Float

  Second moment coefficient.

• epsilon : Float

  Numerical stabilizer.

def TorchLean.optim.Adam.instReprConfig.repr : Config → ℕ → Std.Format

@[instance_reducible]

instance TorchLean.optim.Adam.instReprConfig : Repr Config

structure TorchLean.optim.AdamW.Config : Type

Public AdamW optimizer configuration.

• learningRate : Float

  Learning rate.

• beta1 : Float

  First moment coefficient.

• beta2 : Float

  Second moment coefficient.

• epsilon : Float

  Numerical stabilizer.

• weightDecay : Float

  Decoupled weight decay.

def TorchLean.optim.AdamW.instReprConfig.repr : Config → ℕ → Std.Format

@[instance_reducible]

instance TorchLean.optim.AdamW.instReprConfig : Repr Config

structure TorchLean.optim.AdaDelta.Config : Type

Public Adadelta optimizer configuration.

• learningRate : Float

  Learning rate.

• rho : Float

  Decay coefficient for gradient/update accumulators.

• epsilon : Float

  Numerical stabilizer.

def TorchLean.optim.AdaDelta.instReprConfig.repr : Config → ℕ → Std.Format

@[instance_reducible]

instance TorchLean.optim.AdaDelta.instReprConfig : Repr Config

opaque TorchLean.optim.Optimizer.Internal.create (representation : View) : Optimizer

Build the sealed public optimizer value at the API boundary.

opaque TorchLean.optim.Optimizer.Internal.view (optimizer : Optimizer) : View

Reveal an optimizer only at the runtime-lowering boundary.

def TorchLean.optim.Optimizer.Internal.formatScalar (value : Float) : String

Render a hyperparameter as a Lean expression, preserving every finite binary64 bit.

FloatLib rounds the exact value to seventeen significant decimal digits. The candidate is decoded with Lean's scientific-literal decoder and OfScientific Float; it is used only if the resulting bits match. Otherwise an explicit Float.ofBits expression retains the original finite value. Negative zero and nonfinite values use Float.ofBits directly. NaNs follow Lean's canonicalization.

def TorchLean.optim.sgd (config : SGD.Config) : Optimizer

SGD optimizer config, optionally with momentum.

Example:

-- `torch.optim.SGD(params, lr=0.01)`, then the same with heavy-ball momentum.
def plain : optim.Optimizer := optim.sgd { learningRate := 0.01 }

def withMomentum : optim.Optimizer :=
  optim.sgd { learningRate := 0.01, momentum := 0.9 }

def TorchLean.optim.adaGrad (config : AdaGrad.Config) : Optimizer

AdaGrad optimizer config, written optim.adaGrad { learningRate := 0.05 }.

def TorchLean.optim.rmsProp (config : RMSProp.Config) : Optimizer

RMSProp optimizer config, written optim.rmsProp { learningRate := 1e-3 }.

def TorchLean.optim.adam (config : Adam.Config) : Optimizer

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

Example:

-- `torch.optim.Adam(params, lr=1e-3)`: same default moments, same stabilizer
-- (Kingma and Ba, "Adam: A Method for Stochastic Optimization", ICLR 2015).
def optimizer : optim.Optimizer := optim.adam { learningRate := 1e-3 }

def TorchLean.optim.adamW (config : AdamW.Config) : Optimizer

AdamW optimizer config, written optim.adamW { learningRate := 1e-3 }.

Example:

-- Decoupled weight decay, so the penalty does not travel through the adaptive moments
-- (Loshchilov and Hutter, "Decoupled Weight Decay Regularization", ICLR 2019).
def optimizer : optim.Optimizer :=
  optim.adamW { learningRate := 1e-3, weightDecay := 0.01 }

def TorchLean.optim.adaDelta (config : AdaDelta.Config) : Optimizer

AdaDelta optimizer config, written optim.adaDelta {}.

def TorchLean.optim.Optimizer.describe (optimizer : Optimizer) : String

Render an optimizer in the record-based syntax used to construct it. Finite fields retain their binary64 bits through Internal.formatScalar, including coefficients close to one and subnormal stabilizers. Negative zero and nonfinite fields use explicit Float.ofBits expressions; NaNs follow Lean's canonicalization.

@[instance_reducible]

instance TorchLean.optim.Optimizer.instToString : ToString Optimizer

@[instance_reducible]

instance TorchLean.optim.Optimizer.instRepr : Repr Optimizer

def TorchLean.optim.Optimizer.learningRate (optimizer : Optimizer) : Float

Return the base learning rate encoded in an optimizer configuration.

def TorchLean.optim.Optimizer.Internal.requireFiniteNonnegative (name : String) (value : Float) : Except String Unit

Reject a hyperparameter that is not a finite number at or above zero.

isFinite is the load-bearing half of the test: 0.0 <= value alone would accept +∞, and an infinite learning rate or weight decay poisons every later update instead of failing where it was configured.

def TorchLean.optim.Optimizer.Internal.requireUnitInterval (name : String) (value : Float) : Except String Unit

Reject a coefficient that is not a finite number in [0, 1).

Exponential-average coefficients such as Adam's beta1 and beta2 belong in the half-open interval: at exactly 1.0 the running average never forgets its initial value, so the optimizer would ignore the gradient forever rather than merely converge slowly.

def TorchLean.optim.Optimizer.Internal.requireFinitePositive (name : String) (value : Float) : Except String Unit

Reject a hyperparameter that is not a finite number strictly above zero. This is the check for quantities that end up in a denominator, such as Adam's epsilon.

def TorchLean.optim.Optimizer.validate (optimizer : Optimizer) : Except String Unit

Check the numerical domain of an optimizer configuration before allocating optimizer state.

The checks rule out undefined bias corrections and non-finite updates. They are shared by the trainer, manual-module, and reinforcement-learning entry points.

def TorchLean.optim.Optimizer.Internal.mapScalars (cast : Float → Float) (optimizer : Optimizer) : Optimizer

Transform every scalar in a configuration for validation after conversion.

def TorchLean.optim.Optimizer.validateFloat32 (optimizer : Optimizer) : Except String Unit

Check both the supplied configuration and its binary32 representation.

Training must reject coefficients that round to one, stabilizers that round to zero, and finite binary64 rates that overflow binary32. validate remains available for binary64 callers.