Reference · Algorithm guarantees

rainbow.algorithms.proofs.adaptive-gradient

Algorithm guaranteessrc/rainbow/algorithms/proofs/adaptive_gradient.clj2 definitions, 4 theorems

AHoF O21 AdaGrad: the adaptive per-parameter learning rate. AdaGrad divides a base rate by the square root of the accumulated squared gradient: rate = base-rate / sqrt(accumulator) Exact square roots are not rational in general, so this is proved on the perfect-square instances that matter for worked trajectories: a root is witnessed by `square-root?` (root * root ~ accumulator, proven on the rational cross-product), and the adaptive rate is then the exact division base/root. With accumulator 4 the root is 2 and a base rate 1 gives adaptive rate 1/2. The general irrational sqrt stays unclaimed; the gradient step around the rate stays in the executable reference. Scope (measured by the kernel): this module has 3 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.adaptive-gradient` prints this classification.

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

adagrad/rate :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

adagrad/two-is-root-of-four :
  → adagrad/square-root? 4 2

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

adagrad/rate-unfold :
  (base-rate root : ℚ≥0)
  → adagrad/rate base-rate root = nnrat/divide base-rate root

adagrad/adaptive-rate-example :
  → adagrad/rate 1 2 = nnrat/half