Reference · Algorithm guarantees

rainbow.algorithms.proofs.momentum

Algorithm guaranteessrc/rainbow/algorithms/proofs/momentum.clj3 definitions, 4 theorems

Polyak momentum descent over signed rationals with pair-valued state. The state is a Product of a signed position and a signed velocity. Each step updates the velocity `v' = beta * v - alpha * gradient(position)` (the momentum term `beta * v` accumulates past steps, which plain gradient descent lacks) and then the position `x' = x + v'`. Velocity carry uses signed scaling and subtraction; the state is read and rebuilt through the Product projections. This is the first optimizer that evolves paired state (AHoF O19), wrapping the signed-descent gradient with velocity accumulation.

optimization/momentum-velocity :
  (beta rate : ℚ≥0) (gradient : ℚ → ℚ≥0) (x v : ℚ)
  → ℚ

optimization/momentum-step :
  (beta rate : ℚ≥0) (gradient : ℚ → ℚ≥0) (s : data/Product ℚ ℚ)
  → data/Product ℚ ℚ

optimization/momentum-iterate :
  (beta rate : ℚ≥0) (gradient : ℚ → ℚ≥0) (x₁ : ℕ) (x₂ : data/Product ℚ ℚ)
  → data/Product ℚ ℚ

optimization/momentum-velocity-unfold :
  (beta rate : ℚ≥0) (gradient : ℚ → ℚ≥0) (x v : ℚ)
  → optimization/momentum-velocity beta rate gradient x v = signed/scale beta v - signed/from-nnrat (rate · gradient x)

optimization/momentum-step-unfold :
  (beta rate : ℚ≥0) (gradient : ℚ → ℚ≥0) (s : data/Product ℚ ℚ)
  → optimization/momentum-step beta rate gradient s = data/pair ℚ ℚ (product/first ℚ ℚ s + velocity) (velocity)
  where velocity := optimization/momentum-velocity beta rate gradient (product/first ℚ ℚ s) (product/second ℚ ℚ s)

optimization/momentum-iterate-zero :
  (beta rate : ℚ≥0) (gradient : ℚ → ℚ≥0) (initial : data/Product ℚ ℚ)
  → optimization/momentum-iterate beta rate gradient 0 initial = initial

optimization/momentum-iterate-successor :
  (beta rate : ℚ≥0) (gradient : ℚ → ℚ≥0) (steps : ℕ) (initial : data/Product ℚ ℚ)
  → iterate (data/succ steps) initial = (fun x₁ => fun previous => optimization/momentum-step beta rate gradient previous) steps (iterate steps initial)
  where iterate := optimization/momentum-iterate beta rate gradient