Reference · Algorithm guarantees

rainbow.algorithms.proofs.counterfactual

Algorithm guaranteessrc/rainbow/algorithms/proofs/counterfactual.clj1 definitions, 2 theorems

AHoF V57 Counterfactual Explanation: the proximity term of the counterfactual search objective. A counterfactual for an input is the nearest point that flips the model's decision, found by minimizing distance-to-original plus a penalty for not achieving the desired class. The distinctive proximity measure is the squared distance between the original and the candidate: distance-squared = <original - candidate, original - candidate> the inner product of the difference with itself. Because the difference is a non-origin subtraction (Grothendieck pairs), the worked value is proven on the signed equivalence: the counterfactual [1,0] is squared-distance 9 from the original [4,0]. The desired-class penalty and the outer minimization stay in the executable reference. Requires signed multiplication and the vector dot product. 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.counterfactual` prints this classification.

Depends onmath.finite.vectoralgorithms.proofs.inner-product

counterfactual/distance-squared :
  (x₁ x₂ : List ℚ)
  → ℚ

counterfactual/distance-example :
  → counterfactual/distance-squared [signed/from-nnrat 4, signed/from-nnrat 0] [signed/from-nnrat 1, signed/from-nnrat 0] = signed/from-nnrat 9

counterfactual/closer-example :
  → counterfactual/distance-squared [signed/from-nnrat 4, signed/from-nnrat 5] [signed/from-nnrat 3, signed/from-nnrat 4] = signed/from-nnrat 2