Reference · Algorithm guarantees

rainbow.algorithms.proofs.noisy-descent

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

AHoF O38 Noisy Descent: the WRAP pattern that perturbs a base descent step with additive noise. Given whatever step a base optimizer produced, the noisy wrapper adds a perturbation vector: wrapped = step + noise This is a finite-vector addition; the base step and the noise draw are the wrapped optimizer's and the sampler's concern (executable), and the textbook Gaussian perturbation is supplied as a concrete vector in the worked instance. What is proved here is the wrap recurrence and worked instances. 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.noisy-descent` prints this classification.

Depends onmath.finite.vector

noisy/wrap :
  (x₁ x₂ : List ℚ)
  → List ℚ

noisy/wrap-unfold :
  (step noise : List ℚ)
  → noisy/wrap step noise = vector/add step noise

noisy/wrap-example :
  → noisy/wrap [signed/from-nnrat 1, signed/from-nnrat 2] [signed/from-nnrat 1, signed/from-nnrat 1] = [signed/from-nnrat 2, signed/from-nnrat 3]

noisy/wrap-3d-example :
  → noisy/wrap [signed/from-nnrat 1, signed/from-nnrat 2, signed/from-nnrat 3] [signed/from-nnrat 1, signed/from-nnrat 1, signed/from-nnrat 1] = [signed/from-nnrat 2, signed/from-nnrat 3, signed/from-nnrat 4]