File size: 9,074 Bytes
63f41a6 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 | #!/usr/bin/env python
"""ETA model for the real P2 run, computed from MEASURED inputs (docs/P2.md section 6).
.venv/bin/python scripts/p2/eta.py # markdown table, low / central / high
.venv/bin/python scripts/p2/eta.py --json
Every input carries its source. Where an input is not measured for the quantity it is applied to
(pool completion length, pool verify time, 40,960-cap length), it is a BRACKET between two measured
anchors and the table says so; nothing here is fitted. All stages run strictly in series (one heavy
job at a time, /apps/CLAUDE.md), so the total is a sum.
generate(P, n, T) = P * n * T / r_gen (tokens / aggregate tok/s)
verify(P, n, f, t) = P * n * f * t (t = wall s per code-bearing sample at 8 workers)
corrections = U * n * k_fail * f_fb samples, U = P * (1 - solved@n) (lean_gen corrects only failed samples of
problems with NO accepted sample), each generated and verified like a round-0 sample
sft(rows, L, e) = rows * L * e / (r_tr * eff) + saves * 3.3 min
"""
from __future__ import annotations
import argparse
import json
# ---- measured inputs (value, source) ---------------------------------------------------------------------
M = {
# generation, vLLM TP=4 (P2-B; .tmp/p2/P2-B/probe_16k_seqs256_summary.json, probe_16k_summary.json)
"r_gen": {"low": 1043.0, "central": 1363.0, "high": 1602.0,
"src": "e2e 1,043 tok/s (256 samples, 64 problems); >=64 running 1,363 (256 seqs) / 1,602 (128 seqs)"},
"T16_minif2f": {"low": 4996.0, "central": 4996.0, "high": 5066.0,
"src": "mean completion tokens at cap 16,384, miniF2F, 256 / 128 samples; 8.2% / 7.8% hit the cap"},
"frac_len16": {"central": 0.082, "src": "finish_reason=length at cap 16,384 (21/256)"},
# verification (this session: B's 256 real Goedel samples through verify_generations, 8 workers)
"f_code_minif2f": {"central": 235 / 256, "src": "256 samples: 21 no_code (length), 235 sent to Lean"},
"t_v_minif2f": {"central": 722 / 235, "src": "722 s wall for 235 code-bearing samples at 8 workers, 7 timeouts (180 s) inside; mean per-proof 13.9 s, median 2.5 s"},
"t_v_easy": {"central": 9 / 51, "src": "tiny loop: 51 short pool proofs in 9 s at 8 workers (the 16 SHORTEST pool statements)"},
"acc_minif2f": {"central": 165 / 256, "src": "accepted/samples at cap 16,384, 64 miniF2F problems x 4"},
"solved4_minif2f": {"central": 52 / 64, "src": "solved@4 on those 64 problems"},
"ffb_minif2f": {"central": 62 / 91, "src": "compile_error share of failures (62/91); the rest: no_code 21, timeout 6, banned 2"},
# training (P2-A; configs/p2_sft.toml header, scripts/qwen3_sft_probe.py)
"r_tr": {"central": 2152.0, "src": "padded tokens/s on 4 GPUs at 16,384-token micro-batches (18,432: 2,146)"},
"save_min": {"central": 3.3, "src": "one checkpoint (16 GB merged + adapter/optimizer), measured twice (3.3 min; tiny loop 3.1 / 3.2)"},
}
def hours(s: float) -> float:
return s / 3600.0
def compute() -> dict:
P_pool, n, P_mf = 2000, 8, 244
rg = {k: M["r_gen"][k] for k in ("low", "central", "high")} # low = slowest tok/s
out = {}
def gen_h(samples, T, r):
return hours(samples * T / r)
# scenario columns: low = optimistic time, central, high = pessimistic time
def col(lo, ce, hi):
return {"low": lo, "central": ce, "high": hi}
# --- evaluation (miniF2F, n=8 -> 1,952 samples)
S_mf = P_mf * n
T16 = M["T16_minif2f"]
gen16 = col(gen_h(S_mf, T16["low"], rg["high"]), gen_h(S_mf, T16["central"], rg["central"]), gen_h(S_mf, T16["high"], rg["low"]))
t_v = M["t_v_minif2f"]["central"]
ver16 = hours(S_mf * M["f_code_minif2f"]["central"] * t_v)
out["eval_c16384_gen"] = gen16
out["eval_c16384_verify"] = col(ver16 * 0.6, ver16, ver16 * 1.4)
# --- 40,960 cap: lengths NOT measured at scale: bracket T16 (nobody continues) .. T16 + frac_len * (40,960 - 16,384 - prompt)
T40 = col(T16["central"], T16["central"] + M["frac_len16"]["central"] * 12000.0, T16["central"] + M["frac_len16"]["central"] * 24000.0)
out["eval_c40960_gen"] = col(gen_h(S_mf, T40["low"], rg["high"]), gen_h(S_mf, T40["central"], rg["central"]), gen_h(S_mf, T40["high"], rg["low"]))
ver40 = hours(S_mf * 0.99 * t_v)
out["eval_c40960_verify"] = col(ver40 * 0.6, ver40, ver40 * 1.4)
# --- pool round 0 (2,000 x 8 = 16,000 samples). T and t_v for POOL statements are bracketed, not measured.
S_pool = P_pool * n
Tp = col(1817.0, 3000.0, T16["central"]) # tiny loop (shortest statements, cap 4,096; 116,283 tok / 64) .. miniF2F
out["pool_r0_gen"] = col(gen_h(S_pool, Tp["low"], rg["high"]), gen_h(S_pool, Tp["central"], rg["central"]), gen_h(S_pool, Tp["high"], rg["low"]))
tvp = col(M["t_v_easy"]["central"], 1.0, t_v)
fcp = 0.9
out["pool_r0_verify"] = col(*(hours(S_pool * fcp * tvp[k]) for k in ("low", "central", "high")))
# --- correction round 1: failed samples of unsolved problems only
u = col(0.10, 0.20, 0.30) # unsolved@8 fraction of the pool: miniF2F unsolved@4 is 19%; pool statements are mostly easier
kfail = 8 * (1 - 0.0) # all 8 samples of an unsolved problem failed
ffb = M["ffb_minif2f"]["central"]
Nc = col(*(P_pool * u[k] * kfail * ffb for k in ("low", "central", "high")))
out["corr_samples"] = Nc
Tc = col(T16["central"], T16["central"], T16["central"]) # unsolved problems are hard: miniF2F-like lengths
out["corr_gen"] = col(gen_h(Nc["low"], Tc["low"], rg["high"]), gen_h(Nc["central"], Tc["central"], rg["central"]), gen_h(Nc["high"], Tc["high"], rg["low"]))
out["corr_verify"] = col(*(hours(Nc[k] * 0.9 * (t_v if k != "low" else tvp["central"])) for k in ("low", "central", "high")))
# --- SFT: rows x tokens x 2 epochs
rows = col(1000.0, 2500.0, 4500.0)
L = col(2800.0, 3300.0, 4000.0) # prompt ~0.25k + accepted completion mean 2.7k (measured); corrections are longer
eff = 0.9
ep = 2
sft = {}
for k in ("low", "central", "high"):
tok = rows[k] * L[k] * ep
steps = tok / eff / 18432 / 8
sft[k] = hours(tok / (M["r_tr"]["central"] * eff)) + (steps * 2 / 40) * M["save_min"]["central"] / 60.0
out["sft_rows"] = rows
out["sft_train"] = sft
out["sft_export"] = col(0.05, 0.1, 0.2)
# --- post-SFT re-evaluation at the primary cap
out["post_c16384_gen"] = out["eval_c16384_gen"]
out["post_c16384_verify"] = out["eval_c16384_verify"]
totals = {}
for k in ("low", "central", "high"):
totals[k] = {
"baseline_16k": out["eval_c16384_gen"][k] + out["eval_c16384_verify"][k],
"baseline_40k": out["eval_c40960_gen"][k] + out["eval_c40960_verify"][k],
"pool_r0": out["pool_r0_gen"][k] + out["pool_r0_verify"][k],
"correction": out["corr_gen"][k] + out["corr_verify"][k],
"sft": out["sft_train"][k] + out["sft_export"][k],
"reeval_16k": out["post_c16384_gen"][k] + out["post_c16384_verify"][k],
}
totals[k]["total_16k_only"] = sum(totals[k][x] for x in ("baseline_16k", "pool_r0", "correction", "sft", "reeval_16k"))
totals[k]["total_with_40k_baseline"] = totals[k]["total_16k_only"] + totals[k]["baseline_40k"]
out["totals"] = totals
out["T40_tokens"] = T40
out["T_pool_tokens"] = Tp
out["t_v_pool"] = tvp
out["unsolved_frac"] = u
return out
def markdown(o: dict) -> str:
rows = [
("baseline miniF2F, cap 16,384, n=8: generate", "eval_c16384_gen"), (" verify", "eval_c16384_verify"),
("baseline miniF2F, cap 40,960 (reference): generate", "eval_c40960_gen"), (" verify", "eval_c40960_verify"),
("pool round 0 (2,000 x 8 = 16,000): generate", "pool_r0_gen"), (" verify (--feedback)", "pool_r0_verify"),
("correction round 1: generate", "corr_gen"), (" verify", "corr_verify"),
("SFT (2 epochs, incl. saves)", "sft_train"), (" merge + export", "sft_export"),
("post-SFT miniF2F, cap 16,384, n=8: generate", "post_c16384_gen"), (" verify", "post_c16384_verify"),
]
t = ["| stage | low (h) | central (h) | high (h) |", "|---|---|---|---|"]
for name, key in rows:
t.append(f"| {name} | {o[key]['low']:.2f} | {o[key]['central']:.2f} | {o[key]['high']:.2f} |")
tt = o["totals"]
t.append(f"| **total, 16k baseline + loop + 16k re-eval** | **{tt['low']['total_16k_only']:.1f}** | **{tt['central']['total_16k_only']:.1f}** | **{tt['high']['total_16k_only']:.1f}** |")
t.append(f"| **total including the 40,960 baseline** | **{tt['low']['total_with_40k_baseline']:.1f}** | **{tt['central']['total_with_40k_baseline']:.1f}** | **{tt['high']['total_with_40k_baseline']:.1f}** |")
return "\n".join(t)
if __name__ == "__main__":
ap = argparse.ArgumentParser()
ap.add_argument("--json", action="store_true")
a = ap.parse_args()
o = compute()
print(json.dumps(o, indent=1) if a.json else markdown(o))
|