Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.adaboost

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

AHoF AdaBoost (Adaptive Boosting): combine many weak classifiers into a strong one by a weighted majority vote, where each weak learner's vote weight alpha = (1/2) ln((1 - err)/err) DECREASES with its weighted error err -- more accurate learners get larger votes, and after each round the misclassified examples are up-weighted so the next learner focuses on them. The ordering of vote weights by error is: earns-more-weight? err-a err-b = decide (err-a <= err-b) (the lower-error learner earns at least as much weight), over exact-rational errors. Defined: the weight-ordering test. Proved native and axiom-free, as worked instances: error 1/4 earns more weight than error 1/2, error 1/2 does not earn more weight than error 1/4, and the worked certificate 1/4 <= 1/2 (native nnrat/at-most). That alpha is monotone decreasing in error, and AdaBoost's classical training-error bound, are not proved here. The alpha computation (a log), the reweighting, and the final vote are executable. 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.adaboost` prints this classification.

adaboost/earns-more-weight? :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

adaboost/lower-error-earns-more :
  → search/poll-improves 1/4 1/2 = data/true

adaboost/more-weight-means-lower-error :
  → 1/4 ≤ 1/2

adaboost/higher-error-earns-less :
  → search/poll-improves 1/2 1/4 = data/false