Reference · Algorithm guarantees

rainbow.algorithms.proofs.rmsprop

Algorithm guaranteessrc/rainbow/algorithms/proofs/rmsprop.clj1 definitions, 3 theorems

AHoF O22 RMSProp: the decayed squared-gradient accumulator that adapts the learning rate. Where AdaGrad (O21) sums all squared gradients, RMSProp keeps an exponentially-weighted average, retaining a fraction of the old accumulator and mixing in a fraction of the new squared gradient: accumulator' = retain * accumulator + fresh * gradient^2 (with retain + fresh = 1). This is exact-rational multiplication and addition; the adaptive rate then divides a base rate by the square root of the accumulator, reusing the AdaGrad machinery. What is proved here is the decayed accumulator recurrence and a worked steady-state instance; the decay weights are supplied as concrete rationals. Scope (measured by the kernel): this module has 2 worked instances (statements about specific values) and 1 definitional unfoldings (true by unfolding a definition). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.rmsprop` prints this classification.

rmsprop/accumulate :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → ℚ≥0

rmsprop/accumulate-unfold :
  (retain fresh prev grad-squared : ℚ≥0)
  → adam/first-moment retain fresh prev grad-squared = retain · prev + fresh · grad-squared

rmsprop/steady-state-example :
  → adam/first-moment nnrat/half nnrat/half 4 4 = 4

rmsprop/rising-example :
  → adam/first-moment nnrat/half nnrat/half 4 16 = 10