Learning-Rate Schedules

Pure learning-rate schedules used by TorchLean training loops and examples. A Config describes a schedule, and Config.rate evaluates it at an optimizer step.

References

• PyTorch schedulers: torch.optim.lr_scheduler.* (https://pytorch.org/docs/stable/optim.html#how-to-adjust-learning-rate)

inductive TorchLean.Trainer.Scheduler.Annealing : Type

Interpolation between the endpoints of a one-cycle phase.

• linear : Annealing

  Constant slope between the endpoints.

• cosine : Annealing

  A half cosine, with zero slope at both endpoints.

def TorchLean.Trainer.Scheduler.instReprAnnealing.repr : Annealing → Nat → Std.Format

@[instance_reducible]

instance TorchLean.Trainer.Scheduler.instReprAnnealing : Repr Annealing

inductive TorchLean.Trainer.Scheduler.Config : Type

Small learning-rate scheduler surface for higher-level training code.

This file keeps the interface compact: a Config is just a description of a schedule, and config.rate stepIndex computes the learning rate after that many optimizer updates.

PyTorch mapping

Config.step and Config.exponential correspond to the schedule math of:

• torch.optim.lr_scheduler.StepLR
• torch.optim.lr_scheduler.ExponentialLR

Config.warmupCosine is the schedule commonly used for Transformer pretraining: a short linear warm-up followed by cosine decay to a nonzero floor.

All indices count completed optimizer updates, starting at zero. oneCycle uses explicit integer phase lengths; it does not reproduce PyTorch's fractional pct_start * total_steps - 1 boundaries.

• constant (lr : Float) : Config
• step (baseLr : Float) (stepSize : Nat) (decayFactor : Float := 0.1) : Config
• exponential (baseLr decayFactor : Float) : Config
• linearWarmup (startLr peakLr : Float) (warmupSteps : Nat) : Config

  Increase from startLr at step zero to peakLr at warmupSteps, then hold the peak. Zero warm-up steps select the peak immediately.

• cosine (baseLr minLr : Float) (halfCycleSteps : Nat) (periodic : Bool := false) : Config

  Decay from baseLr to minLr over halfCycleSteps, then hold the minimum. With periodic := true, continue back to the base rate and repeat every 2 * halfCycleSteps. A zero half-cycle selects the minimum immediately.

• cyclic (baseLr peakLr : Float) (halfCycleSteps : Nat) (cycleDecay : Float := 1.0) : Config

  Repeated linear rises and falls, each lasting halfCycleSteps. The first cycle runs from baseLr to peakLr and back. cycleDecay scales the amplitude once per completed cycle: 1 gives fixed triangles and 0.5 halves each successive peak's distance above the base. A zero half-cycle is invalid.

• oneCycle (initialLr peakLr finalLr : Float) (riseSteps totalSteps : Nat) (annealing : Annealing := Annealing.cosine) : Config

  Rise from initialLr to peakLr at riseSteps, then fall to finalLr at totalSteps and hold it. Both phases use annealing; only the learning rate changes. Validation requires 0 < riseSteps < totalSteps and both endpoints at or below the peak.

• warmupCosine (peakLr minLr : Float) (warmupSteps totalSteps : Nat) : Config

  Linearly warm up to peakLr, then follow a cosine curve down to minLr.

  warmupSteps counts optimizer updates. The first update uses peakLr / warmupSteps, and the last warm-up update reaches peakLr. Once totalSteps updates have been scheduled, the learning rate remains at minLr. A warm-up longer than the run is clamped to totalSteps. When totalSteps = 0, no update belongs to the schedule and Config.rate returns minLr.

@[instance_reducible]

instance TorchLean.Trainer.Scheduler.instReprConfig : Repr Config

def TorchLean.Trainer.Scheduler.instReprConfig.repr : Config → Nat → Std.Format

def TorchLean.Trainer.Scheduler.Internal.requireRate (name : String) (value : Float) : Except String Unit

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

def TorchLean.Trainer.Scheduler.Internal.requireDecay (name : String) (value : Float) : Except String Unit

Reject a decay factor outside [0, 1]. A factor above one grows the learning rate instead of decaying it, which in practice is a typo rather than an intention.

def TorchLean.Trainer.Scheduler.Internal.requireRange (lowerName upperName : String) (lower upper : Float) : Except String Unit

Check an interpolation's ordered, nonnegative endpoints.

def TorchLean.Trainer.Scheduler.Internal.requireDuration (name : String) (steps : Nat) : Except String Unit

Reject a duration that would overflow the binary64 interpolation arithmetic.

def TorchLean.Trainer.Scheduler.Internal.interpolate (annealing : Annealing) (start finish : Float) (elapsed duration : Nat) : Float

Interpolate inside a phase, returning its exact endpoints at the boundaries. Roundoff near an endpoint must not exceed the range checked by Config.validate, even near overflow.

def TorchLean.Trainer.Scheduler.Internal.validate : Config → Except String Unit

Validate a learning-rate schedule before it is attached to optimizer state.

The checks keep every scheduled rate finite and nonnegative. Step and exponential schedules use decay factors in [0, 1]; a zero step size is rejected instead of silently changing the schedule to a constant rate.

def TorchLean.Trainer.Scheduler.Config.validate (config : Config) (round : Float → Float := id) : Except String Unit

Validate a schedule, optionally checking its largest rate after scalar conversion.

round reports the converted value in binary64. Its default leaves rates unchanged; a runtime supplies its scalar conversion to catch overflow before training. Schedule arithmetic remains binary64; each resulting rate is converted when the optimizer state is updated.

def TorchLean.Trainer.Scheduler.Config.rate : Config → Nat → Float

Learning rate after the given number of completed optimizer updates.