Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.shap

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/shap.clj3 definitions, 4 theorems

AHoF V55 SHAP Values: attribute a prediction to features as a weighted sum of feature contributions (Shapley-weighted); attribution w0 c0 w1 c1 = w0*c0 + w1*c1. Proved native and axiom-free (worked values by cross-product equivalence). Scope (measured by the kernel): this module has 3 worked instances (statements about specific values) and 1 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.ahof.shap` prints this classification.

shap/attribution :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → ℚ≥0

shap/balanced :
  → ℚ≥0

shap/single :
  → ℚ≥0

shap/attribution-unfold :
  (w0 x0 w1 x1 : ℚ≥0)
  → qmdp/value w0 x0 w1 x1 = w0 · x0 + w1 · x1

shap/balanced-is-five-eighths :
  → shap/balanced = 5/8

shap/single-is-first :
  → shap/single = 1/2

shap/combined :
  → proposition/conjunction (shap/balanced = 5/8) (shap/single = 1/2)