code/scripts/p2/eta.py · viai957/align at main

Add files using upload-large-folder tool

63f41a6 verified 15 days ago

9.07 kB

#!/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))

	#!/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))