Reference · Algorithm guarantees

rainbow.algorithms.proofs.hypergradient

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

AHoF O25 Hypergradient Descent: the meta-optimizer that tunes its own learning rate by the gradient of the loss with respect to the learning rate. That hypergradient is the inner product of the current and previous gradients, so the learning-rate update is rate' = rate + beta * <gradient_current, gradient_previous> built from the vector dot product, signed scaling, and signed addition. When successive gradients agree (positive inner product) the rate grows; when they are orthogonal it is unchanged. This is the first algorithm to use `vector/dot`. The meta-step size beta is a concrete nonnegative rational in the worked instances; the base parameter update stays in the executable reference. Requires `signed/multiply` and `vector/dot` in the environment. 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.hypergradient` prints this classification.

Depends onalgorithms.proofs.inner-product

hypergrad/update-rate :
  (x₁ : ℚ) (x₂ : ℚ≥0) (x₃ x₄ : List ℚ)
  → ℚ

hypergrad/update-rate-unfold :
  (rate : ℚ) (beta : ℚ≥0) (g-current g-previous : List ℚ)
  → hypergrad/update-rate rate beta g-current g-previous = rate + signed/scale beta (vector/dot g-current g-previous)

hypergrad/aligned-example :
  → hypergrad/update-rate (signed/from-nnrat 1) 1 [signed/from-nnrat 1, signed/from-nnrat 1] [signed/from-nnrat 1, signed/from-nnrat 1] = signed/from-nnrat 3

hypergrad/orthogonal-example :
  → hypergrad/update-rate (signed/from-nnrat 2) 1 [signed/from-nnrat 1, signed/from-nnrat 0] [signed/from-nnrat 0, signed/from-nnrat 1] = signed/from-nnrat 2