Reference · Algorithm guarantees

rainbow.algorithms.proofs.adam

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

AHoF O24 Adam: the first-moment (momentum) estimate and the preconditioned step direction. Adam keeps a decayed average of the gradient (the first moment) alongside RMSProp's decayed average of the squared gradient (the second moment), then steps in the direction of the first moment divided by the square root of the second moment: first-moment' = retain * first-moment + fresh * gradient direction = first-moment / sqrt(second-moment) This composes exact-rational multiplication/addition (the moment update) with exact division (the preconditioning), reusing the perfect-square root witness from AdaGrad. Bias correction (dividing by 1 - beta^t) needs powers and subtraction and stays in the executable reference, as does the epsilon term; what is proved is the first-moment recurrence and a worked preconditioned direction. 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.adam` prints this classification.

adam/first-moment :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → ℚ≥0

adam/direction :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

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

adam/first-moment-example :
  → adam/first-moment nnrat/half nnrat/half 0 2 = 1

adam/direction-example :
  → adadelta/scale 1 2 = nnrat/half