Reference · Algorithm guarantees

rainbow.algorithms.proofs.nesterov

Algorithm guaranteessrc/rainbow/algorithms/proofs/nesterov.clj4 definitions, 4 theorems

Nesterov accelerated momentum over signed rationals with pair-valued state. Nesterov differs from Polyak momentum by evaluating the gradient at a look-ahead point `x + beta * v` rather than at `x`: the velocity update is `v' = beta * v - rate * gradient(x + beta * v)` and the position moves `x' = x + v'`. When the gradient depends on position the look-ahead genuinely changes the trajectory. This wraps the momentum pair-state engine (AHoF O20) with the look-ahead evaluation. Scope (measured by the kernel): this module has 4 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.nesterov` prints this classification.

optimization/nesterov-lookahead :
  (beta : ℚ≥0) (x v : ℚ)
  → ℚ

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

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

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

optimization/nesterov-lookahead-unfold :
  (beta : ℚ≥0) (x v : ℚ)
  → optimization/nesterov-lookahead beta x v = x + signed/scale beta v

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

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

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