Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.log-loss

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

AHoF Cross-Entropy / Log Loss: the standard loss for probabilistic classification and the maximum-likelihood objective for logistic regression and softmax networks. The per-example loss for the true class is -log(p_true): zero when the model is certain and correct, growing without bound as the predicted true-class probability goes to zero, so confident wrong predictions are strongly penalized. Because -log is strictly decreasing, a HIGHER true-class probability gives a LOWER loss; comparing two predictions' losses reduces to comparing their true-class probabilities: lower-loss? p-confident p-unsure = decide (p-unsure <= p-confident) (the more-confident correct prediction has the lower loss), over exact-rational probabilities. Proved native and axiom-free, as worked instances: the test says true for probability 3/4 against 1/4; the worked certificate 1/4 <= 3/4 (native nnrat/at-most); and the test says false for 1/4 against 3/4. That -log is strictly decreasing, so the test matches the loss order for all inputs, is classical and not proved here; the logarithm is executable. This is the LOSS FUNCTION, distinct from O41's cross-entropy optimization METHOD. 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.log-loss` prints this classification.

log-loss/lower-loss? :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

log-loss/confident-has-lower-loss :
  → bo/is-safe 3/4 1/4 = data/true

log-loss/lower-loss-more-probable :
  → 1/4 ≤ 3/4

log-loss/unsure-not-lower-loss :
  → bo/is-safe 1/4 3/4 = data/false