Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.simulated-annealing

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/simulated_annealing.clj1 definitions, 3 theorems

AHoF Simulated Annealing: a global optimization metaheuristic that escapes local optima by sometimes accepting WORSE solutions -- with a probability that shrinks as a 'temperature' cools -- inspired by the annealing of metals. A downhill move (better objective) is always accepted; an uphill move to a worse candidate is accepted only when a random draw u falls under the Metropolis acceptance probability exp(-delta/T): accepts-uphill? u accept-probability = decide (u <= accept-probability) over exact-rational values. Proved native and axiom-free: the uphill-acceptance test, and worked instances -- a draw of 1/4 under probability 1/2 accepts the worse move; the certificate 1/4 <= 1/2 as a native nnrat/at-most; and a draw of 3/4 rejects the uphill move. No claim about the acceptance rate is proved. The cooling schedule, neighbor proposal, and exp/RNG are executable; what is proved is the acceptance decision at these instances. Requires nnrat/at-most, audit/decide-nnrat-at-most, nnrat/decide-at-most-true-sound (all in the D63 checkpoint). Scope (measured by the kernel): this module has 3 worked instances (statements about specific values). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.simulated-annealing` prints this classification.

simulated-annealing/accepts-uphill? :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

simulated-annealing/accepts-worse-move :
  → lis/extends? 1/4 1/2 = data/true

simulated-annealing/acceptance-within-probability :
  → 1/4 ≤ 1/2

simulated-annealing/rejects-worse-move :
  → lis/extends? 3/4 1/2 = data/false