Reference · Algorithm guarantees

rainbow.algorithms.proofs.trust-region

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

Trust region step acceptance over exact rationals. A trust region method computes the ratio of the actual reduction to the predicted reduction, and accepts the candidate step only when that ratio clears a threshold; otherwise it rejects the step and keeps the current point (and would shrink the region). The accept-or-reject branch is the distinctive control flow of trust region methods (AHoF O16): `reduction-ratio` uses exact rational division, `trust-accept?` decides the threshold comparison, and `trust-region-update` selects the candidate or the current point by that decision. 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.trust-region` prints this classification.

decision/reduction-ratio :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

decision/trust-accept :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

decision/trust-region-update :
  (x₁ : data/Bool) (x₂ x₃ : ℚ)
  → ℚ

decision/reduction-ratio-unfold :
  (actual predicted : ℚ≥0)
  → adagrad/rate actual predicted = nnrat/divide actual predicted

decision/trust-accept-unfold :
  (threshold ratio : ℚ≥0)
  → failmon/safe? threshold ratio = audit/decide-nnrat-at-most threshold ratio

decision/trust-region-update-accepts :
  (candidate current : ℚ)
  (accepted : data/true = data/true)
  → decision/trust-region-update data/true candidate current = candidate

decision/trust-region-update-rejects :
  (candidate current : ℚ)
  (rejected : data/false = data/false)
  → decision/trust-region-update data/false candidate current = current