Reference · Algorithm guarantees

rainbow.algorithms.proofs.feature-importance

Algorithm guaranteessrc/rainbow/algorithms/proofs/feature_importance.clj1 definitions, 3 theorems

AHoF V54 Permutation Feature Importance: the drop in model score when a feature's values are permuted, measuring how much the model relies on it: importance(feature) = baseline-score - permuted-score a signed subtraction (the drop is usually positive but can be negative for a harmful feature). Worked instances prove the drop on the signed equivalence. The scoring function, the permutation, and the averaging over repetitions are the executable concern. Requires the signed rationals in the environment. Scope (measured by the kernel): this module has 2 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.feature-importance` prints this classification.

importance/importance :
  (x₁ x₂ : ℚ)
  → ℚ

importance/importance-unfold :
  (baseline permuted : ℚ)
  → importance/importance baseline permuted = baseline - permuted

importance/relied-on-example :
  → importance/importance (signed/from-nnrat 5) (signed/from-nnrat 3) = signed/from-nnrat 2

importance/unused-example :
  → importance/importance (signed/from-nnrat 4) (signed/from-nnrat 4) = signed/from-nnrat 0