1 # mlbend-metrics: the evaluation surface of machine learning, natively in Bend 2. 2 # 3 # import mlbend-metrics@0.1.0.0/main.bend as M 4 # 5 # A metric compares two sequences of the same length. The length is not 6 # trusted: every metric answers a Result, and a mismatch of lengths (or 7 # an empty input) is a value, never a crash. 8 # 9 # What is proved: the counts. What is tested: the F32 numbers, against 10 # NumPy and scikit-learn (reference/test_metrics.py). F32 is not a real 11 # number, so a metric's value is never proved, only its shape. 12 13 import Base 14 import bend-ml-nat-lemmas@0.1.1.0/main.bend as NL 15 16 # Bad 17 # --- 18 # 19 # Why a metric could not answer. 20 21 type Bad is Data: 22 Mismatch{expected: Nat, got: Nat} 23 Empty{} 24 25 # Counts 26 # ------ 27 # 28 # The counting core, over Nat, so that it can be proved. A count walks 29 # the labels; the walks over two sequences stop at the shorter one (the 30 # metrics check the lengths first). 31 32 # 1 when a and b are the same label, 0 otherwise 33 def same_of(s: Bool) -> Nat: 34 match s: 35 case True{}: 36 1n 37 case False{}: 38 0n 39 40 def same(a: Nat, b: Nat) -> Nat: 41 same_of(Nat.is_eq(a, b)) 42 43 # the number of samples 44 def count(ys: List<&2, Nat>) -> Nat: 45 match ys: 46 case Nil{}: 47 0n 48 case Con{h, t}: 49 (1n + count(t) : Nat) 50 51 # the number of samples whose true label is k 52 def count_true.go(ys: List<&2, Nat>, +k: Nat, n: Nat) -> Nat: 53 match ys: 54 case Nil{}: 55 n 56 case Con{y, yt}: 57 count_true.go(yt, k, (n + same(y, k) : Nat)) 58 59 def count_true(ys: List<&2, Nat>, k: Nat) -> Nat: 60 count_true.go(ys, k, 0n) 61 62 # the number of samples whose predicted label is k 63 def count_pred.go(ps: List<&2, Nat>, +k: Nat, n: Nat) -> Nat: 64 match ps: 65 case Nil{}: 66 n 67 case Con{p, pt}: 68 count_pred.go(pt, k, (n + same(p, k) : Nat)) 69 70 def count_pred(ps: List<&2, Nat>, k: Nat) -> Nat: 71 count_pred.go(ps, k, 0n) 72 73 # the number of samples whose true label is k and whose predicted label 74 # is k too: the true positives of the class k 75 def count_both.go(ys: List<&2, Nat>, ps: List<&2, Nat>, +k: Nat, n: Nat) -> Nat: 76 match ys ps: 77 case Con{y, yt} Con{p, pt}: 78 count_both.go(yt, pt, k, (n + same(y, k) * same(p, k) : Nat)) 79 case _ _: 80 n 81 82 def count_both(ys: List<&2, Nat>, ps: List<&2, Nat>, k: Nat) -> Nat: 83 count_both.go(ys, ps, k, 0n) 84 85 # the number of samples predicted right 86 def count_right.go(ys: List<&2, Nat>, ps: List<&2, Nat>, n: Nat) -> Nat: 87 match ys ps: 88 case Con{y, yt} Con{p, pt}: 89 count_right.go(yt, pt, (n + same(y, p) : Nat)) 90 case _ _: 91 n 92 93 def count_right(ys: List<&2, Nat>, ps: List<&2, Nat>) -> Nat: 94 count_right.go(ys, ps, 0n) 95 96 # LAW 1 (count_length): the number of samples is the length of the list 97 # of labels. (The count is this package's own walk, so the law pins it 98 # to the length Base counts.) 99 law count_length: 100 for ys: List<&2, Nat> 101 {count(ys) == List.length(&2, Nat, ys) : Nat} 102 103 # the number of samples is the length of the list of labels 104 def count_length(ys): 105 match ys: 106 case Nil{}: 107 {==} 108 case Con{h, t}: 109 %count_length(t) : {1n+count(t) == 1n+_ : Nat} 110 {==} 111 112 # Sums 113 # ----- 114 # 115 # The sums the error metrics need: the walk over the two sequences, with 116 # the number of pairs walked beside the sum. 117 118 type Sum is Data: 119 Sum{n: Nat, s: F32} 120 121 def sum_add(a: Sum, x: F32) -> Sum: 122 match a: 123 case Sum{n, s}: 124 Sum{(1n + n : Nat), (s + x : F32)} 125 126 # the sum of the squared differences of the pairs walked 127 def sq_sum.go(ys: List<&2, F32>, ps: List<&2, F32>, acc: Sum) -> Sum: 128 match ys ps: 129 case Con{y, yt} Con{p, pt}: 130 +d = (y - p : F32); 131 sum_add(sq_sum.go(yt, pt, acc), (d * d : F32)) 132 case _ _: 133 acc 134 135 # the sum of the absolute differences of the pairs walked 136 def abs_sum.go(ys: List<&2, F32>, ps: List<&2, F32>, acc: Sum) -> Sum: 137 match ys ps: 138 case Con{y, yt} Con{p, pt}: 139 d = F32.abs((y - p : F32)); 140 sum_add(abs_sum.go(yt, pt, acc), d) 141 case _ _: 142 acc 143 144 # Ratios 145 # ------ 146 # 147 # A metric that divides: the ratio of two counts, and the mean of a sum 148 # over a number of pairs. A zero denominator answers 0.0, the 149 # convention scikit-learn uses (zero_division=0). 150 151 # the ratio a over b, or 0.0 when b is zero 152 def ratio_of(z: Bool, +a: Nat, +b: Nat) -> F32: 153 match z: 154 case True{}: 155 0.0 156 case False{}: 157 (F32.from_nat(a) / F32.from_nat(b) : F32) 158 159 def ratio(+a: Nat, +b: Nat) -> F32: 160 ratio_of(Nat.is_eq(b, 0n), a, b) 161 162 # the mean of a sum over n pairs 163 def mean(s: Sum, n: Nat) -> F32: 164 match s: 165 case Sum{n0, s0}: 166 (s0 / F32.from_nat(n) : F32) 167 168 # Metrics 169 # ------- 170 # 171 # Every metric answers a Result: the value, or why it could not answer. 172 173 # the number of pairs to walk, or why the two sequences do not agree 174 def same_len_of(s: Bool, +n: Nat, +m: Nat) -> Result<&1, &1, Bad, Nat>: 175 match s: 176 case True{}: 177 Done{n} 178 case False{}: 179 Fail{Mismatch{n, m}} 180 181 def same_len(+n: Nat, +m: Nat) -> Result<&1, &1, Bad, Nat>: 182 same_len_of(Nat.is_eq(n, m), n, m) 183 184 # the number of pairs to walk, or why there are none 185 def not_empty_of(z: Bool, n: Nat) -> Result<&1, &1, Bad, Nat>: 186 match z: 187 case True{}: 188 Fail{Empty{}} 189 case False{}: 190 Done{n} 191 192 # the number of pairs, or why there is no answer 193 def not_empty(r: Result<&1, &1, Bad, Nat>) -> Result<&1, &1, Bad, Nat>: 194 match r: 195 case Done{+n}: 196 not_empty_of(Nat.is_eq(n, 0n), n) 197 case Fail{Mismatch{expected, got}}: 198 Fail{Mismatch{expected, got}} 199 case Fail{Empty{}}: 200 Fail{Empty{}} 201 202 # the number of pairs the two sequences hold, or why there is no answer 203 def pairs(a, -A: Kind(a), ys: List, ps: List) -> Result<&1, &1, Bad, Nat>: 204 not_empty(same_len(List.length(a, A, ys), List.length(a, A, ps))) 205 206 # the mean squared error between the targets and the predictions 207 def mse.go(r: Result<&1, &1, Bad, Nat>, +ys: List<&2, F32>, +ps: List<&2, F32>) -> Result<&1, &1, Bad, F32>: 208 match r: 209 case Done{n}: 210 Done{mean(sq_sum.go(ys, ps, Sum{0n, 0.0}), n)} 211 case Fail{Mismatch{expected, got}}: 212 Fail{Mismatch{expected, got}} 213 case Fail{Empty{}}: 214 Fail{Empty{}} 215 216 def mse(+ys: List<&2, F32>, +ps: List<&2, F32>) -> Result<&1, &1, Bad, F32>: 217 mse.go(pairs(&2, F32, ys, ps), ys, ps) 218 219 # the mean absolute error between the targets and the predictions 220 def mae.go(r: Result<&1, &1, Bad, Nat>, +ys: List<&2, F32>, +ps: List<&2, F32>) -> Result<&1, &1, Bad, F32>: 221 match r: 222 case Done{n}: 223 Done{mean(abs_sum.go(ys, ps, Sum{0n, 0.0}), n)} 224 case Fail{Mismatch{expected, got}}: 225 Fail{Mismatch{expected, got}} 226 case Fail{Empty{}}: 227 Fail{Empty{}} 228 229 def mae(+ys: List<&2, F32>, +ps: List<&2, F32>) -> Result<&1, &1, Bad, F32>: 230 mae.go(pairs(&2, F32, ys, ps), ys, ps) 231 232 # the root mean squared error between the targets and the predictions 233 def rmse.go(r: Result<&1, &1, Bad, Nat>, +ys: List<&2, F32>, +ps: List<&2, F32>) -> Result<&1, &1, Bad, F32>: 234 match r: 235 case Done{n}: 236 Done{F32.sqrt(mean(sq_sum.go(ys, ps, Sum{0n, 0.0}), n))} 237 case Fail{Mismatch{expected, got}}: 238 Fail{Mismatch{expected, got}} 239 case Fail{Empty{}}: 240 Fail{Empty{}} 241 242 def rmse(+ys: List<&2, F32>, +ps: List<&2, F32>) -> Result<&1, &1, Bad, F32>: 243 rmse.go(pairs(&2, F32, ys, ps), ys, ps) 244 245 # the fraction of the samples predicted right 246 def accuracy.go(r: Result<&1, &1, Bad, Nat>, +ys: List<&2, Nat>, +ps: List<&2, Nat>) -> Result<&1, &1, Bad, F32>: 247 match r: 248 case Done{n}: 249 Done{ratio(count_right(ys, ps), n)} 250 case Fail{Mismatch{expected, got}}: 251 Fail{Mismatch{expected, got}} 252 case Fail{Empty{}}: 253 Fail{Empty{}} 254 255 def accuracy(+ys: List<&2, Nat>, +ps: List<&2, Nat>) -> Result<&1, &1, Bad, F32>: 256 accuracy.go(pairs(&2, Nat, ys, ps), ys, ps) 257 258 # the fraction of the samples predicted as k that are really k: the 259 # precision of the class k 260 def precision.go(r: Result<&1, &1, Bad, Nat>, +ys: List<&2, Nat>, +ps: List<&2, Nat>, +k: Nat) -> Result<&1, &1, Bad, F32>: 261 match r: 262 case Done{n}: 263 Done{ratio(count_both(ys, ps, k), count_pred(ps, k))} 264 case Fail{Mismatch{expected, got}}: 265 Fail{Mismatch{expected, got}} 266 case Fail{Empty{}}: 267 Fail{Empty{}} 268 269 def precision(+ys: List<&2, Nat>, +ps: List<&2, Nat>, +k: Nat) -> Result<&1, &1, Bad, F32>: 270 precision.go(pairs(&2, Nat, ys, ps), ys, ps, k) 271 272 # the fraction of the samples really k that are predicted as k: the 273 # recall of the class k 274 def recall.go(r: Result<&1, &1, Bad, Nat>, +ys: List<&2, Nat>, +ps: List<&2, Nat>, +k: Nat) -> Result<&1, &1, Bad, F32>: 275 match r: 276 case Done{n}: 277 Done{ratio(count_both(ys, ps, k), count_true(ys, k))} 278 case Fail{Mismatch{expected, got}}: 279 Fail{Mismatch{expected, got}} 280 case Fail{Empty{}}: 281 Fail{Empty{}} 282 283 def recall(+ys: List<&2, Nat>, +ps: List<&2, Nat>, +k: Nat) -> Result<&1, &1, Bad, F32>: 284 recall.go(pairs(&2, Nat, ys, ps), ys, ps, k) 285 286 # the harmonic mean of two scores 287 def f1_num_of(z: Bool, +p: F32, +r: F32) -> F32: 288 match z: 289 case True{}: 290 0.0 291 case False{}: 292 ((2.0 * p * r / (p + r) : F32)) 293 294 def f1_num(+p: F32, +r: F32) -> F32: 295 f1_num_of(F32.is_eq((p + r : F32), 0.0), p, r) 296 297 # the harmonic mean of a precision and a recall 298 def f1_of(p: Result<&1, &1, Bad, F32>, r: Result<&1, &1, Bad, F32>) -> Result<&1, &1, Bad, F32>: 299 match p: 300 case Done{pv}: 301 match r: 302 case Done{rv}: 303 Done{f1_num(pv, rv)} 304 case Fail{Mismatch{expected, got}}: 305 Fail{Mismatch{expected, got}} 306 case Fail{Empty{}}: 307 Fail{Empty{}} 308 case Fail{Mismatch{expected, got}}: 309 Fail{Mismatch{expected, got}} 310 case Fail{Empty{}}: 311 Fail{Empty{}} 312 313 # the harmonic mean of the precision and the recall of the class k 314 def f1.go(r: Result<&1, &1, Bad, Nat>, +ys: List<&2, Nat>, +ps: List<&2, Nat>, +k: Nat) -> Result<&1, &1, Bad, F32>: 315 match r: 316 case Done{+n}: 317 f1_of(precision.go(Done{n}, ys, ps, k), recall.go(Done{n}, ys, ps, k)) 318 case Fail{Mismatch{expected, got}}: 319 Fail{Mismatch{expected, got}} 320 case Fail{Empty{}}: 321 Fail{Empty{}} 322 323 def f1(+ys: List<&2, Nat>, +ps: List<&2, Nat>, +k: Nat) -> Result<&1, &1, Bad, F32>: 324 f1.go(pairs(&2, Nat, ys, ps), ys, ps, k) 325