Reference · Algorithm guarantees

rainbow.algorithms.proofs.adadelta

Algorithm guaranteessrc/rainbow/algorithms/proofs/adadelta.clj2 definitions, 3 theorems

AHoF O23 Adadelta: the learning-rate-free update scale. Adadelta needs no base learning rate; instead it scales the gradient by the ratio of the root mean square of recent updates to the root mean square of recent gradients: scale = RMS[update] / RMS[gradient] = sqrt(accum-update) / sqrt(accum-grad) On perfect-square accumulators both roots are exact, so the scale is an exact rational division of the two roots (witnessed by root*root ~ accumulator). With an update accumulator of 4 (root 2) and a gradient accumulator of 9 (root 3) the scale is 2/3 -- a dimensionless step size derived entirely from the running statistics. The accumulator decay and the general irrational sqrt stay in the executable reference and are not claimed. Scope (measured by the kernel): this module has 3 worked instances (statements about specific values). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.adadelta` prints this classification.

adadelta/square-root? :
  (x₁ x₂ : ℚ≥0)
  → Prop

adadelta/scale :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

adadelta/three-is-root-of-nine :
  → adadelta/square-root? 9 3

adadelta/scale-example :
  → adadelta/scale 2 3 = 2/3

adadelta/scale-above-one-example :
  → adadelta/scale 3 2 = 3/2