Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.f1-score

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

AHoF F1 Score: the standard single-number summary of a classifier's quality on imbalanced data -- the HARMONIC MEAN of precision and recall, f1 precision recall = 2 * precision * recall / (precision + recall). The harmonic mean is high only when BOTH precision and recall are high (it is dominated by the smaller of the two), unlike the arithmetic mean, which is why F1 resists being gamed by a classifier that trades one metric for the other. Proved native and axiom-free: the F1 combination (composing nnrat/multiply, nnrat/add, and exact rational division); a worked F1 (stated as rational equivalence via the cross-product certificate); and that a perfect classifier (precision = recall = 1) has F1 = 1. The confusion-matrix counts (TP, FP, FN) and precision/recall are executable; what is proved is the harmonic-mean combination. Requires nnrat/multiply, nnrat/add, nnrat/divide (division is the rational-division capability, composed here), nnrat/equivalent, and the D63 checkpoint. Scope (measured by the kernel): this module has 2 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.f1-score` prints this classification.

Depends onmath.rational.division

f1-score/f1 :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

f1-score/f1-example :
  → f1-score/f1 3/4 1/2 = 3/5

f1-score/perfect-classifier-f1-one :
  → f1-score/f1 1 1 = 1