| # P2: SFT of Goedel-Prover-V2-8B with the strict Lean verifier in the loop (data, verification, evaluation) |
|
|
| Scope of this document: the **data + verification + evaluation** side of experiment P2 (owner |
| P2-C). Generation (vLLM, `extras/vllm_rollout/lean_gen.py`) and the Qwen3 model / trainer belong |
| to P2-A and P2-B; the contract between the three is in section 2. Everything under "Measured" |
| is copied from a run recorded in `.tmp/p2/c/` (paths given); nothing is estimated unless it is |
| labelled as a model. |
|
|
| Code: `scripts/p2/{build_problems,verify_generations,build_sft_data,eval_report}.py`, |
| `scripts/p2/p2_common.py`, `scripts/p2/run_round.sh`, `align/eval/proof_stats.py`. |
| Tests: `tests/test_p2_*.py` (run `uv run pytest tests/test_p2_*.py -m "not slow"`; `-m slow` drives |
| the real Lean toolchain with one worker). |
|
|
| ## 1. Pre-registration |
|
|
| Registered 2026-10-12 22:51 IST. At registration **no generation or verification record of the |
| experiment exists** (`find .tmp -name 'gen*.jsonl' -o -name 'ver*.jsonl'` is empty), and the |
| verifier, the problem files and the statistics code are already frozen by the hashes below. The |
| text between the two markers is hashed; edit nothing between them after registration. Changes go |
| in section 1.3 (amendments), which is outside the hash. |
|
|
| <!-- PREREG:BEGIN --> |
| **Question.** Does one round of expert-iteration SFT (accepted self-generated proofs plus |
| accepted self-correction examples, from a decontaminated 2,000-problem pool) improve |
| Goedel-Prover-V2-8B on miniF2F under the strict Lean verifier? |
|
|
| **Primary endpoint (the only confirmatory test).** |
|
|
| | | | |
| |---|---| |
| | Problem set | miniF2F, the 244 problems of `Goedel-Prover-V2/dataset/minif2f.jsonl` (statement text normalised exactly as Goedel's `split(":= by")[0] + ":= by sorry"`), no exclusions | |
| | Systems | baseline = `Goedel-LM/Goedel-Prover-V2-8B` revision `dfd02e6271a58375dfbf3ece0175277cf6b6a89a`; candidate = that model after the P2 SFT | |
| | Generation | handler `dpskcot`, temperature 1.0, top_p 0.95, no top_k, 8 samples per problem (`sample_idx` 0..7; if more exist the first 8 are used), completion cap **16,384** tokens (nominal cap; the effective `max_tokens` is recorded per sample and reported) | |
| | Verifier | `align.verify.lean` StrictVerifier, `statement_mode="strict"`, kernel recheck on, lexical gate on, 180 s per-proof budget, Lean 4.9.0-rc1 / Mathlib `d1d1e4b7` (pins recorded in every verification row); identical pins, config and budget for both systems | |
| | Outcome per problem | **solved@8** = at least one of samples 0..7 accepted | |
| | Test | paired **exact two-sided McNemar** on solved@8 (binomial on the discordant problems, `align.eval.proof_stats.mcnemar_exact`), alpha = 0.05 | |
| | Success | p < 0.05 **and** candidate solves more problems than baseline. p < 0.05 with the candidate lower is reported as a significant degradation. Anything else is reported as "no detectable improvement" | |
|
|
| **Secondary endpoints** (descriptive; not multiplicity-corrected; none can rescue a failed primary): |
| S1 miniF2F solved@8 at cap 40,960 (reference baseline only unless both systems are run at it); |
| S2 MOBench on the verifier-supported subset, solved@8, same test; S3 pass@1 (mean over samples, |
| unbiased pass@k estimator) with cluster-bootstrap CIs and a paired bootstrap difference; |
| S4 pass@k for k in {2, 4, 8}; S5 the correction-round lift table (conversion of round-0-unsolved |
| problems per correction round, with samples and tokens spent). |
|
|
| **Validity conditions.** A run pair is *invalid* (not "negative") and is repeated or discarded if |
| any of: the verifier pins / config / budget differ between the two systems; fewer than 8 samples |
| exist for any problem; any training problem shares a statement with miniF2F or MOBench (the SFT |
| builder raises); more than half of any verification chunk dies for infrastructure reasons; the SFT |
| data build fails its read-back check. There is **no optional stopping**: 8 samples per problem is |
| fixed in advance; the only permitted re-runs are resumes of the same sample keys after a crash. |
|
|
| **Statistical power (exact McNemar, 244 problems; computed with `mcnemar_power`).** The test can |
| only fire for a given number of discordant problems at a minimum split: 10 discordant needs 1:9, |
| 20 needs 5:15, 30 needs 9:21, 40 needs 13:27, 60 needs 21:39. Unconditional power, if a fraction |
| d of problems is discordant and the net gain is delta: |
| |
| | discordant fraction d | delta = +2 pp | +4 pp | +6 pp | +8 pp | |
| |---|---|---|---|---| |
| | 0.10 | 0.12 | 0.43 | 0.82 | 0.99 | |
| | 0.15 | 0.09 | 0.30 | 0.63 | 0.89 | |
| | 0.20 | 0.08 | 0.24 | 0.51 | 0.78 | |
| |
| So the primary test has about 80 % power only for a gain of roughly 6 pp at d = 0.10 and 8 pp at |
| d = 0.15. **A null result means "no gain of about 6 pp or more was detectable", not "no effect".** |
| <!-- PREREG:END --> |
| |
| PREREG_SHA256: `adc28ebedf2581777edc67ce843dbadc7c56b6b25bdf3e2e8e5424e75458eb58` |
| |
| (`eval_report.py` recomputes the hash of the block and prints whether it equals the recorded value.) |
| |
| ### 1.1 What the report will and will not claim |
| |
| * pass@k with k > n is not computed (`null`, never 0). Samples within a problem are correlated, so |
| the pass@1 interval is a **cluster bootstrap over problems**; a Wilson interval over pooled samples |
| is also printed and labelled anti-conservative. Wilson intervals on solved@k are valid (problems |
| are the independent unit). |
| * Caps are never pooled and every row names its cap. At cap 40,960 in a 40,960-token window every |
| sample is clipped by its prompt length; the table prints the mean effective `max_tokens`. |
| * Statement fidelity, trust base and soundness limits are those of `docs/LEAN_VERIFIER.md` |
| section 6; in particular a rejected proof can be a policy rejection (banned `def`, `native_decide`) |
| of a valid proof, and a 180 s wall budget makes borderline `nlinarith` proofs flaky in both |
| directions. |
| |
| ### 1.2 Known restrictions on the evaluation sets (measured, section 3) |
| |
| * miniF2F: all 244 problems enter the verifier. |
| * MOBench: **only the verifier-supported subset can be scored.** The strict verifier supports |
| "header, then ONE theorem"; MOBench statements often carry `def` / `abbrev` / `structure` / |
| `variable` blocks. Those problems are listed in `mobench_unsupported.json` with a reason and are |
| not part of any MOBench number. MOBench results are therefore "MOBench-verifiable subset (n = see |
| section 3)", an easier-looking subset by construction, and say nothing about the other problems. |
|
|
| ### 1.3 Amendments (outside the hash) |
|
|
| Any change after registration is listed here with date, reason and the pre-amendment |
| result kept. Nothing below alters the registered question, endpoint, test, alpha or validity conditions. |
|
|
| **A1. Disclosure of baseline data that existed or was seen (reviewer R1, 2026-10-13 03:00 IST; factual, no analysis changed).** |
|
|
| * The sentence "at registration no generation or verification record of the experiment exists" was checked with a file-name |
| pattern (`gen*.jsonl`, `ver*.jsonl`) and is imprecise. At 22:51 real **generations** of the baseline model on miniF2F |
| already existed under other names: `.tmp/p2/P2-B/probe_16k.jsonl` (128 samples, 32 problems x 4, cap 16,384, written 22:49:57) |
| and `smoke.jsonl` (6 samples, cap 256). They had **not** been verified: no accepted/rejected verdict for any |
| baseline sample existed at registration. |
| * After registration the integrator verified 256 baseline samples at the registered cap (miniF2F, 64 problems x 4 samples, |
| `.tmp/p2/p2i/eta/{gen,ver}_probe256.jsonl`, verdicts written 2026-10-13 02:32 IST): 165 / 256 accepted, solved@4 = 52 / 64, and |
| published them in section 6 (ETA). So the experimenters have seen a partial baseline pass rate on 64 of the 244 |
| primary problems **before any registered baseline run**. It informed only the time estimate. These samples are not |
| reused as baseline samples (the registered baseline is regenerated by `launch_baseline.py` into its own run directory, all |
| 244 problems, `sample_idx` 0..7), and no part of the analysis plan was changed in response. The registered test is paired |
| (baseline vs candidate), so knowing the baseline rate does not bias it, but the record should say it. |
| * The evaluation problem files (`minif2f.jsonl`, written 22:34), `align/eval/proof_stats.py` (22:31), `align/verify/lean/*` (<= 20:03) |
| and `scripts/p2/eval_report.py` (22:50) precede the registration. The training pool (`train_pool.jsonl`, 23:03) does **not**: it |
| was built 12 minutes after registration, still before any pool generation. "Already frozen by the hashes below" is true for the |
| evaluation files and the verifier only. |
| * `scripts/p2/eval_report.py` was edited after registration (R1 review) to make the PRIMARY label stricter: it is printed only for |
| the registered test (all 244 problems, baseline = the registered revision, temperature 1.0 / top_p 0.95 / no top_k, identical |
| sampling and round-0 prompts in both runs). No statistic changed (`proof_stats.py` untouched). |
|
|
| **Proposed, NOT in force until the user confirms (R1).** "Candidate = the post-SFT model" leaves the SFT configuration unregistered |
| (epochs, LR, rows kept, checkpoint). To close that fork: the candidate is ONE SFT run, configuration fixed (`configs/p2_sft.toml`, |
| the `build_sft_data.py` arguments recorded in its manifest) before the baseline result is read, evaluated at its final |
| checkpoint; any further SFT variant evaluated on miniF2F is reported in full and carries the secondary label. |
|
|
| ## 2. Contract and what this side adds to it |
|
|
| JSONL files, one object per line (field names as in the shared contract; additions are marked +). |
|
|
| | File | Fields | |
| |---|---| |
| | Problem | `problem_id, source, split, formal_statement` (full header + theorem, ends `:= by sorry`), `informal_prefix, statement_sha` | |
| | Generation | `problem_id, sample_idx, round, cap_tokens, prompt_ids, completion_ids, prompt_text, completion_text, finish_reason, lean_code, messages, model_path, model_rev, sampling, parent` (+ `lean_code_error`, `context_clipped` written by lean_gen.py) | |
| | Verification | key `(problem_id, sample_idx, round, cap_tokens)` + `accepted, reasons, verify_s, budget_s, verifier{pins,config,workers}` + **`code_sha256`**, `stage`, `diagnostics`; with `--feedback` also **`repl_errors`, `repl_code`** | |
| |
| Definitions and rules enforced by the readers (every one raises, none skips silently): |
| |
| * `statement_sha` = sha256 of the lexer-normalised signature tokens (comments and whitespace |
| removed, **theorem name excluded**) of the statement the verifier parses. Alpha-renaming-invariant |
| hash and name matching are separate decontamination layers (section 4). |
| * `finish_reason == "length"` implies `len(completion_ids) == sampling.max_tokens`; `sampling.max_tokens <= cap_tokens`; |
| `len(completion_ids) <= sampling.max_tokens`. `max_tokens < cap_tokens` is legitimate only as context clipping and is reported. |
| * `code_sha256` pins a verdict to the exact code it was computed for. A verification whose hash differs from the generation |
| now on disk (the generation file was regenerated under the same keys) raises in `verify_generations`, |
| `build_sft_data` and `eval_report`. |
| * `repl_errors` / `repl_code` are what `extras/vllm_rollout/lean_gen.py --corrections-from` joins on: `repl_code` is Goedel's |
| `compile_view(lean_code)` (import / set_option / open lines dropped) and `repl_errors` are the REPL's error dicts, whose |
| `pos.line` index that text (`tests/test_p2_verify.py::test_compile_view_is_identical_to_the_generators_copy` pins the two copies of |
| `compile_view` together). |
| * SFT rows: `input_ids = prompt_ids + completion_ids` exactly as sampled; the store extra `prompt_len = len(prompt_ids)` makes |
| `collate_sft` label positions `[prompt_len, L)` and nothing else. Extras per row: `kind` (first | correction), `round`, `sample_idx`, |
| `cap_tokens`, `n_completion`, `proof_sha`, `model_rev`. |
|
|
| ## 3. Measured: problem sets |
|
|
| Files: `.tmp/p2/problems/` (copied from the build in `.tmp/p2/c/problems/`; `problems_manifest.json` holds every number below). |
| Commands: section 5, step 1. Build seed 20261012. Verifier pins recorded in the manifest: Lean 4.9.0-rc1, Mathlib `d1d1e4b7`, REPL `7df77c0a`. |
|
|
| **Evaluation sets** (from `reference-repos/Goedel-Prover-V2/dataset/`, input sha256 `47ca505c...` and `f286b894...`): |
|
|
| | Set | In the file | Enter the verifier | Excluded, listed in `mobench_unsupported.json` | |
| |---|---|---|---| |
| | miniF2F (`split: test`) | 244 | **244** (sha256 `d5da8ea6...`) | 0 | |
| | MOBench (`split: test`) | 360 | **135** (sha256 `419d5377...`) | **225**: 220 whose first command after the header is `def` / `abbrev` / `structure` / `inductive` / `variable` / `instance` / `notation`... (the strict verifier supports "header, then ONE theorem"), 5 with `:= by` not occurring exactly once | |
|
|
| Statement text is normalised as Goedel does (`split(":= by")[0] + ":= by sorry"`), made safe: a statement with an earlier `:= by` |
| raises instead of being truncated, and the line-broken form `:=\n by sorry` (which Goedel's literal split cannot parse) is accepted. |
| `test_eval_statement_matches_goedels_own_prompt_normalisation_bytewise` asserts byte equality with Goedel's rule on all 244 miniF2F problems. |
| Elaboration under the pin (the verifier's own reference command `theorem _align_ref <sig> := by sorry`): **244/244** miniF2F and **135/135** MOBench elaborate. |
|
|
| **Training pool.** |
|
|
| | | | |
| |---|---| |
| | Source | `Goedel-LM/Goedel-Pset-v1`, 1,732,594 Lean 4 statements (4 parquet shards, 827 MB, sha256 checked against the hub's LFS oids) | |
| | Pinned revision | `79fc4fbe87b4c694a941bc63ad92dc38d39d41db` (2025-04-18) | |
| | Licence | the repo's `LICENSE` file: "licensed under the MIT License". The dataset card has **no** `license:` metadata; informal problems are "from Numina" (Apache-2.0 on the hub for `AI-MO/NuminaMath-CoT` and `-1.5`; the README does not say which). Alternative considered: `internlm/Lean-Workbook` (apache-2.0, about 140k statements; the Pset README calls itself ten times larger): smaller, so not used | |
| | Why this source | it is the statement set released with Goedel-Prover-V1 (its README: expert iteration was run on it; use in V2 not verified here), with the `import Mathlib ... open BigOperators Real Nat Topology Rat` header the extraction and `problem_check` steps re-insert; every row passed its authors' compile test | |
| | Sampling | rank by `sha256("20261012|problem_id")`, keep the 5,000 smallest hashes among rows that survive the filters (bounded heap, O(5,000) memory, independent of row order), then take the first 2,000 that elaborate | |
|
|
| | Stage | Rows | |
| |---|---| |
| | in the pinned dataset | 1,732,594 | |
| | dropped: not a bare statement (`:= by` count != 1, or text after `:= by sorry`; mostly full proofs stored as statements) | 270,325 | |
| | dropped: shape the verifier cannot use (`def`/`variable`/second theorem in the file) | 29,086 | |
| | dropped: longer than 4,000 characters | 712 | |
| | **decontaminated out** against miniF2F + the 135 verifier-supported MOBench problems (379 statements, 377 distinct signatures; **not** the 225 unsupported MOBench problems, see section 4): signature sha 48, alpha-renamed sha 18, name 3 | **69** | |
| | eligible | 1,432,402 | |
| | ranked candidates kept (seeded hash) | 5,000 | |
| | dropped from candidates: informal text 13-gram overlap 27, >= 3 distinct 8-gram overlaps 31, duplicate statement 5 | 63 | |
| | candidates for the elaboration check | 4,937 | |
| | checked in rank order until 2,000 passed | 2,000 | |
| | **failed to elaborate** | **0** (0 timeouts, 0 crashes) | |
| | **final pool** (`train_pool.jsonl`, sha256 `9e8a9fbc...`) | **2,000**, all `split=train`, unique ids and statement shas; median 445 characters; 21 have a non-standard header (kept: `problem_check` re-inserts the statement's own header) | |
|
|
| Note the layers are counted in the order shown, so "alpha 18" means 18 rows caught by layer 2 that layer 1 missed. |
| The elaboration filter removed nothing because the source already passed a compile test at (essentially) this Lean version. That is a measured |
| outcome, not an assumption, and the instrument is not vacuous: its start-up self-test requires a known-good statement to pass and a known-bad one to fail, and a |
| separate run on 30 random pool statements gave **30/30 accepted when clean, 30/30 rejected after appending an unknown-lemma conjunct** |
| (`.tmp/p2/problems/elab_ceiling.json`). The final pool, re-checked with all four layers plus an independent raw-text comparison (comments and whitespace |
| stripped, theorem name removed), has 0 collisions; 28 of 2,000 pool problems still share one or two (never more than two) 8-word informal windows with an eval problem, |
| all generic phrasing in the samples inspected. |
|
|
| Development history, kept because it changed the pool: the first build used only the 13-gram informal layer. An audit of the finished pool found problems sharing up to 7 distinct 8-grams |
| with an eval problem (an IMO 1965 problem with different LaTeX spacing, no shared 13-gram); layer 4b (>= 3 distinct 8-grams) was added and the pool rebuilt (first pool sha256 `0f3e4914...`, candidates `7ce868f0...`; now `9e8a9fbc...`, `8e0c886e...`). |
|
|
| ## 4. Decontamination (what is removed, how) |
|
|
| Against miniF2F (244) + the verifier-supported MOBench problems (135): **379 statements, 377 distinct signatures** |
| (`problems_manifest.json`: `decontamination_sets.statement_sha = 377`). *Correction (R1, 2026-10-13): an earlier version of this section said |
| "all 604 statements before the verifier-support filter". That was wrong: `phase_pool_sample` builds the `Decontaminator` from the two |
| files that contain only problems the verifier can score, so the 225 unsupported MOBench problems are in none of the four layers, not even the |
| informal-text one.* Measured consequence (`.tmp/p2/r1rev/check_d*.py`, TF-IDF cosine of informal text + eyeballing the top pairs against all 604 |
| problems): no pool problem is a formalisation of a **scored** problem, but three pool problems are the same olympiad problem as an |
| **unsupported** MOBench problem (`Goedel-Pset-1628009` = IMO 1971 P5 / `Imo1971P5`, `Goedel-Pset-290458` = IMO 2003 P2 / `Imo2003P2`, |
| `Goedel-Pset-361555` = IMO 1962 P4 / `Imo1962P4`; different informal wording and formalisation, so no layer could catch them). They affect no |
| number in this experiment (those MOBench problems are never scored). They WOULD contaminate a MOBench result once the verifier supports |
| definitions (open item 1): decontaminate against all 360 informal texts before that. |
|
|
| | Layer | Catches | Where counted | |
| |---|---|---| |
| | 1. `statement_sha` | identical signature up to whitespace / comments / theorem name | `contaminated_statement_sha` | |
| | 2. `alpha_sha` | the same signature with consistently renamed local variables | `contaminated_alpha_sha` | |
| | 3. normalised name | `lowercase, alphanumerics only` equality, or an eval name of >= 8 characters as a substring of the pool theorem name or `problem_id` | `contaminated_name` | |
| | 4. informal 13-gram | any 13-word window of the pool's informal problem text also in an eval informal text | `contaminated_informal_13gram_among_ranked` (checked on the ranked candidates, not all 1.7 M rows) | |
|
|
| Layers 1-3 are run on **every** row of the pinned dataset; layer 4 on the 5,000 ranked candidates. |
| Every layer is tested alone (`tests/test_p2_problems.py`) and each has a mutant that the tests kill (section 8). |
| `build_sft_data.py` repeats a cheap version of the check as a hard gate (any training problem whose `statement_sha` is in an |
| eval file raises) and refuses generations for problems outside the training pool. |
|
|
| What this does **not** cover: a different formalisation of the same olympiad problem whose informal text is paraphrased |
| (layer 4 is a 13-gram test), and contamination inside the base model's own pre-training (not addressable here). |
|
|
| Measured by R1 (`.tmp/p2/r1rev/check_d4.py`, 80 random miniF2F statements, theorem name replaced by `lean_workbook_123`, then one meaning-preserving |
| rewrite each): layers 1-3 catch a pure theorem rename (80/80, sha) and consistent hypothesis/variable renaming (67/67, alpha) and **nothing |
| else**: `Real`/`Nat`/`Int` for `ℝ`/`ℕ`/`ℤ` (0/67), `∑ x in` -> `∑ x ∈` (0/7), numeral type ascriptions `(2 : ℝ)` (0/35), two hypotheses swapped |
| (0/44), an extra trivial hypothesis (0/70). Such a copy is stopped only by the informal-text layer, and only if its informal text matches. |
| An independent check of the FINAL pool against the scored sets (NFKC + alpha-renamed 4-gram shingles of the signature: max Jaccard 0.42, no exact hit; |
| TF-IDF cosine of the informal texts: the closest scored-set pairs are the same problem TEMPLATE with different numbers, e.g. `mathd_numbertheory_99` |
| vs `Goedel-Pset-732880`, never the same instance) found no contamination of miniF2F or the 135 supported MOBench problems. It is a negative result from |
| three heuristics, not a proof. |
|
|
| ## 5. Command sequence for a full round |
|
|
| `scripts/p2/run_round.sh print` lists every command; `RUN=<name> scripts/p2/run_round.sh all` runs them in order, stopping at the first |
| failure. Each step is one process that takes and releases the repo heavy-job lock itself, so **never wrap the sequence in a lock** and never |
| run two steps concurrently. Every step is resumable: re-run the same command. |
|
|
| ```bash |
| cd /apps/development/rlhf/align && export RUN=r1 TMPDIR=$PWD/.tmp/p2/r1/scratch HF_HOME=/apps/development/rlhf/hf_cache HF_HUB_DISABLE_XET=1 |
| D=$PWD/.tmp/p2/$RUN; mkdir -p $D/scratch |
| # 1 problems (CPU; the Lean check takes the lock for 8 workers) |
| .venv/bin/python scripts/p2/build_problems.py --phase eval --out-dir $D/problems |
| .venv-rollout/bin/python scripts/p2/build_problems.py --phase pool-sample --out-dir $D/problems # needs pyarrow |
| .venv/bin/python scripts/p2/build_problems.py --phase check --out-dir $D/problems --workers 8 |
| # 2 baseline, cap 16384, 8 samples (GPU, then Lean) |
| .venv-rollout/bin/python extras/vllm_rollout/lean_gen.py --problems $D/problems/minif2f.jsonl --out $D/base/gen_minif2f_c16384.jsonl --n 8 --cap-tokens 16384 --round 0 --tp 4 --wait-lock |
| .venv/bin/python scripts/p2/verify_generations.py --generations $D/base/gen_minif2f_c16384.jsonl --problems $D/problems/minif2f.jsonl --out $D/base/ver_minif2f_c16384.jsonl --workers 8 |
| # (same two commands for mobench.jsonl, and for --cap-tokens 40960 as the reference baseline) |
| # 3 training pool: round 0, verify with feedback, correction round 1, verify |
| .venv-rollout/bin/python extras/vllm_rollout/lean_gen.py --problems $D/problems/train_pool.jsonl --out $D/pool/gen_r0.jsonl --n 8 --cap-tokens 16384 --round 0 --tp 4 --wait-lock |
| .venv/bin/python scripts/p2/verify_generations.py --generations $D/pool/gen_r0.jsonl --problems $D/problems/train_pool.jsonl --out $D/pool/ver_r0.jsonl --workers 8 --feedback |
| .venv-rollout/bin/python extras/vllm_rollout/lean_gen.py --problems $D/problems/train_pool.jsonl --out $D/pool/gen_r1.jsonl --n 1 --cap-tokens 16384 --round 1 --tp 4 --wait-lock --corrections-from $D/pool/ver_r0.jsonl $D/pool/gen_r0.jsonl |
| .venv/bin/python scripts/p2/verify_generations.py --generations $D/pool/gen_r1.jsonl --problems $D/problems/train_pool.jsonl --out $D/pool/ver_r1.jsonl --workers 8 |
| # 4 SFT shards (CPU, seconds), then P2-B's train + HF export (commands supplied by P2-B) |
| .venv/bin/python scripts/p2/build_sft_data.py --generations $D/pool/gen_r0.jsonl $D/pool/gen_r1.jsonl --verifications $D/pool/ver_r0.jsonl $D/pool/ver_r1.jsonl --problems $D/problems/train_pool.jsonl --eval-problems $D/problems/minif2f.jsonl $D/problems/mobench.jsonl --cap-tokens 16384 --max-seq-len $MAX_SEQ_LEN --out-dir $D/sft_data # MAX_SEQ_LEN: longest row the trainer fits (P2-B probe); rows over it are dropped, never truncated |
| # 5 post-SFT evaluation = step 2 with --model $D/export and --out under $D/sft/, then the report |
| .venv/bin/python scripts/p2/eval_report.py --problems $D/problems/minif2f.jsonl $D/problems/mobench.jsonl --run base:G,..:V,.. --run sft:G,..:V,.. --baseline base --candidate sft --out-dir $D/report |
| ``` |
|
|
| ## 6. ETA for the real P2 (measured inputs; integrator) |
|
|
| Computed by `.venv/bin/python scripts/p2/eta.py` (every input and its source is in the `M` dict of that file; `--json` prints the |
| intermediate numbers). All stages run in series (one heavy job at a time), so the total is a sum. **Columns are brackets, not |
| confidence intervals:** *low* = optimistic end of every input, *central* = the measured value, *high* = pessimistic end. Where an |
| input was measured for a DIFFERENT quantity than the one it is applied to, the table says "bracket" below and the pilot in 6.3 |
| collapses it. |
|
|
| ### 6.1 Formulas and inputs |
|
|
| | Quantity | Formula | Inputs (value; where measured) | |
| |---|---|---| |
| | generate | `samples * T / r_gen` | `r_gen` = 1,363 tok/s central (>= 64 sequences running, 256 seqs), 1,602 (128 seqs), 1,043 end-to-end including ramp-up and tail (P2-B, TP=4, `.tmp/p2/P2-B/probe_16k_seqs256_summary.json`). `T` miniF2F at cap 16,384 = **4,996** mean tokens (256 samples; median 3,033, p90 13,641; **8.2 %** hit the cap) | |
| | verify | `samples * f_code * t_v` | `f_code` = 235/256 = **0.918** at cap 16,384 (the rest are length-capped = `no_code`); `t_v` = **3.07 s per code-bearing sample** at 8 workers: 722 s wall for 235 real Goedel samples on 64 miniF2F problems (this session, `.tmp/p2/p2i/eta/ver_probe256.jsonl`); mean per-proof 13.9 s, median 2.5 s, p90 38.6 s, 7 timeouts at 180 s; worker utilisation 57 % (chunk barriers + timeouts). Accepted 165/256 = 64.5 %, solved@4 = 52/64; failures: compile_error 62, no_code 21, timeout 6, banned 2 | |
| | corrections | `U * k * f_fb` samples, `U = P * (1 - solved@8)` | `lean_gen` corrects only the failed samples of problems with **no** accepted sample (`load_parents`), so the count scales with unsolved problems, not with all failures; `f_fb` = 62/91 = 0.68 (only `compile_error` carries Lean errors); k = 8 failed samples per unsolved problem | |
| | SFT | `rows * L * epochs / (r_tr * eff) + saves` | `r_tr` = 2,152 padded tok/s at 16,384-token micro-batches (P2-A); `eff` = 0.9 packing efficiency (assumed; the tiny loop's was 0.68 at seq_len 4,096 with 45 rows); a save = 3.3 min per 40 micro-steps (measured three times) | |
| |
| ### 6.2 Table (hours) |
| |
| | stage | low (h) | central (h) | high (h) | |
| |---|---|---|---| |
| | baseline miniF2F, cap 16,384, n=8: generate | 1.69 | 1.99 | 2.63 | |
| | verify | 0.92 | 1.53 | 2.14 | |
| | baseline miniF2F, cap 40,960 (reference): generate | 1.69 | 2.38 | 3.62 | |
| | verify | 0.99 | 1.65 | 2.31 | |
| | pool round 0 (2,000 x 8 = 16,000): generate | 5.04 | 9.78 | 21.29 | |
| | verify (--feedback) | 0.71 | 4.00 | 12.29 | |
| | correction round 1: generate | 0.94 | 2.22 | 4.35 | |
| | verify | 0.27 | 1.67 | 2.51 | |
| | SFT (2 epochs, incl. saves) | 0.92 | 2.71 | 5.91 | |
| | merge + export | 0.05 | 0.10 | 0.20 | |
| | post-SFT miniF2F, cap 16,384, n=8: generate | 1.69 | 1.99 | 2.63 | |
| | verify | 0.92 | 1.53 | 2.14 | |
| | **total, 16k baseline + loop + 16k re-eval** | **13.1** | **27.5** | **56.1** | |
| | **total including the 40,960 baseline** | **15.8** | **31.5** | **62.0** | |
| |
| |
| Bracketed (NOT measured for the quantity they are applied to) inputs: |
| |
| * **Pool completion length `T_pool`**: 1,817 / 3,000 / 4,996 tokens. Anchors: the tiny loop's 16 shortest pool statements (116,283 tokens / 64 samples at cap 4,096, 20 % of them capped, so this understates) and miniF2F's 4,996. Pool statements are from Lean-Workbook-style sources and are probably easier than miniF2F, but this is not measured. |
| * **Pool verification time `t_v_pool`**: 0.18 / 1.0 / 3.07 s per sample. Anchors: 9 s for 51 samples of the shortest pool statements (tiny loop) and the miniF2F figure above. |
| * **40,960-cap length**: 4,996 / 5,980 / 6,964 tokens = `T16 + 8.2 % * {0, 12k, 24k}`: the share of samples that hit 16,384 and how far they continue is unmeasured at scale (B's 16-sample 40k probe had mean 4,450, 0 capped, on different problems). 40,960 is a context window: the prompt (about 220-600 tokens) comes out of it. |
| * **Unsolved@8 fraction of the pool** 10 / 20 / 30 %; **SFT rows** 1,000 / 2,500 / 4,500 and **row length** 2.8k / 3.3k / 4.0k tokens (`--max-per-problem 4`, problems solved 8/8 are excluded by default, accepted completions average 2,681 tokens + 219 prompt). |
| |
| Reading the table: the pool generation (round 0, 16,000 samples) is the dominant and least certain cost; the evaluation legs (about 3.5 h per cap-16,384 pass) are tight. Everything in the first four rows is a direct extrapolation of measured numbers. |
| |
| ### 6.3 Collapsing the brackets before committing 10-25 hours |
| |
| A 100-problem pilot of the real pool gives `T_pool`, `t_v_pool`, `f_code`, solved@8 and `f_fb` in about 40 minutes (the numbers it prints replace the bracketed rows): |
|
|
| ```bash |
| cd /apps/development/rlhf/align && D=.tmp/p2/r1 && mkdir -p $D/pilot $D/scratch && export TMPDIR=$PWD/$D/scratch HF_HOME=/apps/development/rlhf/hf_cache HF_HUB_DISABLE_XET=1 |
| head -100 .tmp/p2/problems/train_pool.jsonl > $D/pilot/pool100.jsonl |
| .venv-rollout/bin/python extras/vllm_rollout/lean_gen.py --problems $D/pilot/pool100.jsonl --out $D/pilot/gen.jsonl --n 8 --cap-tokens 16384 --round 0 --tp 4 --seed 0 --max-num-seqs 128 --wait-lock |
| .venv/bin/python scripts/p2/verify_generations.py --generations $D/pilot/gen.jsonl --problems $D/pilot/pool100.jsonl --out $D/pilot/ver.jsonl --workers 8 --feedback |
| ``` |
|
|
| ### 6.4 Measured in the tiny loop (section 9), for scale only |
|
|
| generate 64 samples / 116,283 tokens in 114.6 s (1,015 tok/s end to end; engine load 26.8 s warm); verify 51 samples in 9 s; LoRA SFT at |
| seq_len 4,096: about 10.8 s per micro-step (comm-bound, as P2-A measured 11.75 s), about 1.0k real tok/s; a checkpoint save 3.1-3.3 min; |
| merge + export 36.8 s; vLLM reload of the export 14 s. |
| |
| ## 7. Measured: tests and verification of the tooling |
| |
| | Suite | Tests | Result | |
| |---|---|---| |
| | `test_p2_proof_stats.py` | 28 | pass; pass@k equals subset enumeration for every (n <= 8, c, k); exact McNemar equals brute-force summation for every split up to 40 discordant pairs and the independent `align.eval.metrics.mcnemar_exact`; Wilson reproduces the published 177/178 interval | |
| | `test_p2_problems.py` | 25 + 1 slow | pass; each decontamination layer alone; sampler determinism / row-order independence / bounded memory; elaboration filter with a fake pool; real eval files; slow: filter verdict equals "StrictVerifier does not say `reference_invalid`" on the real toolchain | |
| | `test_p2_verify.py` | 19 + 1 slow | pass; kill-and-resume re-verifies nothing, torn tail dropped, stale verdicts raise, dead-verifier chunk not written; slow: real toolchain accept / reject / `no_code` / feedback / resume | |
| | `test_p2_sft_data.py` | 25 | pass; (+4 by R1: displayed-theorem fidelity filter) tokens and mask checked through the real `ShardDataset` + `collate_sft`; stage gate `assert_build_is_current` and shard discovery `resolve_split_dir` accept the build | |
| | `test_p2_eval_report.py` | 23 | pass; hand-built truth tables for pass@k, McNemar cells, correction lift; (+6 by R1: the PRIMARY label requires the registered design, runs with different sampling / prompts are refused, the registered decision rule is applied by the code) | |
| | **total** | **112** (110 + 2 slow) | `tests/test_dependency_firewall.py` still passes (2) | |
|
|
| Mutation check: **64 hand-written mutants, 64 killed, 0 survivors** (53 by P2-C, +11 by R1: M48, M49, M51-M58; the first R1 run had 2 survivors, M54b (a test that mixed sampling in ONE run only) and a stale M43 pattern, both fixed) (`.venv/bin/python scripts/p2/mutation_check.py`; result `.tmp/p2/mutants_result.json`). |
|
|
| | Group | Mutants (each removes one fix in a private copy; `scripts/p2/mutation_check.py`) | Killed by | |
| |---|---|---| |
| | statistics (9) | M01 plug-in pass@k; M02 k > n allowed; M03 McNemar tail off by one; M04 one-sided; M05 p not capped at 1; M06 solved@k over all samples not the prefix; M07 unpaired problem sets; M08 wrong z; M09 unpaired bootstrap | `test_p2_proof_stats.py` | |
| | problems / decontamination (13) | M10 name inside `statement_sha`; M11 no alpha-renaming; M12 name layer off; M13 substring layer off; M14 / M14b / M14c 13-gram off, 8-gram off, a single 8-gram triggers; M15 sampler keeps the largest hashes; M16 sampler skips decontamination; M17 failures counted beyond the cutoff; M18 instrument not ceiling-tested; M19 several `:= by` accepted | `test_p2_problems.py` | |
| | verification (11) | M20 length-capped sent to Lean; M21 stale verdict accepted; M22 resume ignores existing rows; M23 dead-verifier chunk written; M24 feedback on the full file; M24b `endPos` null handling; M25 / M25b torn tail kept; M25c atomic write leaves a temp file; M25d parent unchecked | `test_p2_verify.py` | |
| | SFT data (14 + 2) | M48 statement-fidelity filter removed; M49 displayed theorem compared by presence only; M26 `prompt_len` + 1 (readback off); M27 last completion token dropped (readback off); M28 `prompt_len` - 1 (readback ON); M29 easy problems kept; M30 n < 8 counted easy; M31 other-cap samples mixed in; M32 correction of an accepted parent kept; M33 correction prompt not checked; M34 duplicates kept; M35 EOS not required; M36 eval-leak check off; M37 foreign problems allowed; M38 stale verdict accepted; M39 per-problem cap ignored | `test_p2_sft_data.py` | |
| | report (8 + 9) | M51 PRIMARY without the registered problem count; M52 ... baseline revision; M53 ... sampling settings; M54 / M54b different or mixed sampling compared; M55 differently prompted runs compared; M56 design mismatch without the flag; M57 / M58 decision rule ignores direction / alpha 0.5; M40 caps pooled; M41 missing problems scored as failures; M42 verifier mismatch allowed; M43 primary endpoint unflagged; M44 correction of an accepted parent allowed; M45 stale verdict accepted; M46 McNemar on any-of-all instead of the first-k prefix; M47 pre-registration hash never mismatches | `test_p2_eval_report.py` | |
|
|
| One mutant survived the first run and was fixed by adding a test, not by editing the mutant: M46 (every fixture had n = k = 8, so the prefix rule was unobservable; `test_solved_at_k_is_the_prefix_of_length_k_when_more_samples_exist` was added). |
|
|
| Other runs, all from this session: |
|
|
| * `verify_generations.py` CLI on the real toolchain, 2 workers (5 synthetic generations of a trivial theorem): proof accepted (4.85 s), `linarith [nonexistent]` rejected as |
| `compile_error` with `repl_errors[0].pos = {line 6, column 12}` indexing `repl_code`, `sorry` rejected statically (`banned:sorry`, 0.0001 s), length-capped and code-less samples `no_code` |
| without Lean; a rerun verified 0 and skipped 5. |
| * `build_sft_data.py` on a synthetic 3,200-sample / 106 MB generation file: 6.0 s wall, 671 MB peak RSS, 749 rows, readback check passed on every row. |
| * Full elaboration check: 2,000 pool + 244 + 135 eval statements, 8 workers, 31 s from lock acquisition to manifest (both builds); the first build waited 3 min 9 s for another job's heavy-job lock (waited, not skipped). |
|
|
| What was **not** run by P2-C alone: `scripts/sft.py`, a real vLLM generation, real Goedel-Prover output through the verifier. The integrator ran all three (section 9); the |
| verification throughput in section 6 is now measured on real Goedel output (256 samples, 722 s at 8 workers). |
|
|
| ## 8. Open items |
|
|
| 1. **MOBench covers 135 of 360 problems** (section 3). The other 225 need definitions in the reference statement, which `parse_statement` rejects (`unsupported_statement`). |
| Supporting them means a verifier change (reference header containing `def` / `abbrev` / `structure`, with the candidate required to leave them untouched); not done here, owner of |
| `align/verify/lean/`. Until then every MOBench number is "verifier-supported subset". |
| 2. **Correction examples are long.** A round-1 row's prompt carries the failed attempt (up to the cap) plus the error text, so prompt + completion can approach 2 x cap. `build_sft_data.py --max-seq-len` |
| drops (never truncates) rows over the limit and counts them; the right value is the longest sequence P2-B's trainer fits on an A10G, which this side cannot measure. `run_round.sh` has no default for it on purpose. |
| 3. **The SFT manifest reuses the MATH-corpus gate fields** (`build_version: 2`, `pins_verified: true`, `pin_violations: []`) so `assert_build_is_current` passes. `pins_verified` here means "row accounting reconciled" |
| (selected = written = receipts = read back); P2 has no corpus pins. The trainer config must point `data.shard_dir` at `<out>/shards`, `data.manifest_path` at `<out>/manifest.json`, `data.sft_split` at `sft-train` |
| and `data.pad_token_id` at the Qwen3 pad id (151643): the defaults are the Mistral ones. `evaluate_and_gate` / the entry gates were written for the MATH pipeline and were not exercised. |
| 4. **Feedback exists only for `compile_error` rejections.** Rejections by the static gate (`banned:*`, `statement_mismatch`, `header_mismatch`), timeouts and axiom findings carry no Lean error list, so |
| `lean_gen.py` skips and counts them as `no_repl_errors`; Goedel's own flow would have shown the compiler's (possibly empty) output for them. The correction loop therefore sees a subset of failures. |
| 5. **`--fill-duplicates` is off.** "Prefer distinct proofs" is implemented as "distinct only, unless asked"; with fewer distinct accepted proofs than the cap a problem contributes fewer rows. Pass the flag to fill with repeats. |
| 6. **Heavy-lock duration.** `verify_generations.py` with more than 2 workers holds the exclusive lock for the whole run (for the pool, hours), which blocks GPU jobs; run verification and generation strictly in turn. |
| 7. **Informal-text decontamination is heuristic** (13-gram or >= 3 8-grams); a paraphrased duplicate of an olympiad problem under a different formalisation can pass. 28 of 2,000 pool problems share one or two 8-word windows with an eval |
| problem (listed by the audit, generic in the samples inspected). It does not address contamination in the base model's pre-training. |
| 8. **Statistical power is modest** (section 1): about 80 % for a 6 pp gain at 10 % discordance on 244 problems. A larger n per problem does not help the McNemar test much (the unit is the problem); only more problems would, and miniF2F has 244. |
| 9. **40,960-cap baseline is clipped by the prompt** (about 250-600 tokens per sample); the report prints the effective `max_tokens` next to the nominal cap and the comparison is never made across caps. |
| 10. The `PREREG` time stamp is the time this file was frozen, not an external timestamp; its integrity guarantee is the recorded hash plus `eval_report.py --verify-prereg`, not a notarised clock. |
|
|
| ## 8b. Open items from the integration (continues section 8) |
|
|
| 11. **Correction rows are unexercised on real data** (section 9: 0 accepted of 18). Whether round 1 adds anything on the real pool is unknown until the pool run; the SFT builder and trainer handle the kind, tested synthetically. |
| 12. **Correction rows can exceed the trainer's row limit.** `configs/p2_sft.toml` fits `seq_len` 18,432 (P2-A); a correction prompt carries the failed attempt (up to 16,384 tokens) plus errors plus the completion, so many will be dropped by `--max-seq-len 18432`; `build_sft_data.py` counts them (`over_max_seq_len`). Read that counter before trusting the correction share. |
| 13. **Fused CE builds an fp32 `d_weight` even for a frozen head** (P2-A, from reading `align/kernels/fused_ce.py`, not measured). Only matters if `seq_len` above 18,432 is ever wanted. |
| 14. **MOBench is 135/360** (item 1) and is not part of the baseline job in section 10; the registered primary is miniF2F only. |
| 15. **The heavy lock is held for the whole baseline job (about 7-8 h)**. That is the design (GPU and Lean never overlap, nothing slips in between phases), but other agents' jobs wait that long. |
| 16. **~1.4 % of the pool elaborates numerals as `Float`** (28/2,000 by regex). A cheap extra filter (`Float` in the elaborated statement type) would remove them; not done. |
| 17. **`t_v` is a wall figure with 57 % worker utilisation** (chunk barriers and 180 s timeouts). A larger `--chunk` may recover part of it; not tuned or tested. |
|
|
| ### 8c. Open items from the R1 review (fidelity and statistics; 2026-10-13) |
|
|
| 18. **Verification credits a rewritten statement; training no longer does.** `problem_check` (Goedel's, ported byte-for-byte) swaps the original statement |
| in, so a completion whose displayed theorem is false or different is ACCEPTED whenever its tactics prove the original (constructed and run end to |
| end: displayed `v = 66`, tactics prove `v = 65`: accepted by the real verifier). Evaluation keeps that rule (it is Goedel's protocol and the registered |
| primary must stay comparable); `build_sft_data.py` now drops such samples (`drop_statement_not_faithful`; compares signature tokens, theorem name ignored). |
| On the real data available (230 accepted samples: 165 Goedel miniF2F + 46 + 19) the count is 0, so the SFT rows of the tiny loop are unchanged (45 rows, |
| identical shard hash); the filter is insurance, not a measured effect. The report does not yet count accepted-but-rewritten samples per system: add that |
| if the candidate's rate could differ from the baseline's. |
| 19. **`Goedel-Pset-1662008` is unwinnable and should be removed from the pool.** Its statement contains `sorry` twice inside the signature (Fin-bound proofs); |
| Goedel's `problem_check` does `.replace("sorry", "")` on the statement, which deletes them, so the re-inserted statement never matches the reference |
| (`statement_mismatch`, shown by running every pool / eval statement through `lean_code_for_record` + `static_check`: 2,378 of 2,379 pass, this is the one). |
| It elaborated, so the elaboration filter kept it. Cost: 8 wasted samples; fix: drop it (`grep -v '"Goedel-Pset-1662008"'`) or add "exactly one `sorry`" to |
| the pool filter at the next rebuild (not done: the parquet cache is gone and a rebuild changes every recorded pool hash). |
| 20. **Decontamination covers 379 scored statements, not 604** (corrected in section 4). Three unscored-MOBench olympiad problems are in the pool. |
| 21. **Registered-design guard in `eval_report.py`.** A subset run (e.g. 64 problems) at cap 16,384 / k = 8 used to print `PRIMARY`; it is now `secondary` with the reason. |
| The report also refuses two runs with different sampling settings or round-0 prompts (`--allow-design-mismatch` records the override). |
| 22. **Candidate definition is not registered** (SFT configuration / checkpoint): see the proposed (not in force) amendment in section 1.3. |
| 23. **Timeouts are the one verifier outcome that depends on host load** (180 s wall; 6 / 256 in the probe). Baseline and candidate are verified in different sessions; |
| the report prints `reason_histogram` per run, read the `timeout` counts before interpreting a small difference. Not controlled. |
| 24. **Training run-to-run variance is outside the McNemar p-value** (review R2, 2026-10-13). The paired test covers problem and |
| sampling noise for ONE trained candidate; two LoRA runs on identical data order already differ (adapter rel_B 0.10-0.38, |
| 8-bit optimizer rounding and kernel nondeterminism). Report the primary result with this caveat, and train a second seed |
| (about 2.7 h central) before reading a borderline difference as an effect of the method. |
| 25. **Memory headroom at seq_len 18,432 is 1.9 GiB (8.5%)** on 23 GiB cards (R2, mixed 1k-18.4k rows, peak 21,077 MiB). |
| `align/kernels/fused_ce.py` builds an fp32 frozen-head `d_weight` it does not need under LoRA; drop it before raising seq_len. |
| 26. **Sampling settings follow Goedel's `src/inference.py` (temperature 1.0, top_p 0.95), not the model's |
| `generation_config.json` (0.6 / top_k 20)**, which vLLM 0.26 does not apply on this path. Deliberate, and recorded per sample. |
| |
| ## 9. Integration: one tiny end-to-end loop on the real model (integrator) |
|
|
| `scripts/p2/smoke_loop.sh` (steps `problems gen_r0 ver_r0 gen_r1 ver_r1 sft_data seams train_a train_resume export gen_post gen_base ver_eval report cleanup`; `smoke_loop.sh print` |
| lists every command). Every heavy step runs `waitfree` (poll the repo flock until free) and a strict `preflight` first, then the entry point takes the lock itself. Run dir `.tmp/p2/p2i/`. |
| It uses **16 training problems** (the 16 shortest statements of the 2,000-problem pool, so that some proofs are accepted) and **8 miniF2F problems**, cap **4,096**. The numbers mean nothing; the plumbing is what is tested. |
|
|
| | Step | What ran | Result | |
| |---|---|---| |
| | 1 problems | slice of the built pool + miniF2F | `train16.jsonl`, `minif2f8.jsonl` (`build_problems.py` is not re-run: its parquet cache was deleted; the slice is of the already-built, already-decontaminated files) | |
| | 2 gen round 0 | `lean_gen.py`, n=4, cap 4,096, TP=4 | 64 samples, 116,283 tokens, 114.6 s, 1,015 tok/s end to end; 13 length-capped (`no_code`) | |
| | 3 verify | `verify_generations.py --feedback`, 8 workers | 51 sent to Lean in 9 s: **46 accepted**, 5 `compile_error`, 13 `no_code` | |
| | 4 correction round 1 | `--corrections-from`, cap 4,096 | n=1 per failed parent: 4 samples, **0/4 accepted**. Repeated with n=4: 16 samples (4 parents; the fifth compile error belongs to a problem that has accepted samples and is skipped by design), 2 `no_code`, **0/14 accepted**. The prompts are right (failed attempt + Goedel error block + "provide a detailed analysis"); the unsolved problems are a statement that elaborates its decimal literal as `Float` (`0.5564 < 17 / 30` is unprovable as a `Float` comparison) and one that did not finish in 4,096 tokens | |
| | 5 SFT data | `build_sft_data.py --max-seq-len 9216` | 46 accepted, 1 duplicate dropped, **45 rows, 59,132 tokens** (5,980 prompt + 53,152 completion), 45 `first`, **0 `correction`** | |
| | 6 train | LoRA r=64, 4 ranks, `configs/p2_sft.toml` + `--train.seq_len=4096 --train.epochs=9 --train.save_every_micro_steps=20` | 18 optimizer steps = 36 micro-steps. Periodic save at micro 20. SIGTERM to rank 2 (exact pid) after micro 25: coordinated stop at **micro 26**, save, exit 143. Relaunch: "resumed from micro_00000026 at micro_step 26 (optimizer_step 13)", finished at micro 36, final save. Loss 0.254 -> 0.197 | |
| | 7 export | `qwen3_export_check.py run ... --keep` | merge 36.8 s; **0/399 tensors differ** between align's merge and the trainer's checkpoint file; 252 adapted tensors changed (relative weight change mean 4.3e-4); vLLM loaded the export unmodified (14 s) | |
| | 8 reload + generate | `lean_gen.py --model <export> --model-rev sft-<hash>`, 8 miniF2F x 2, cap 4,096 | 16 samples, 41,800 tokens | |
| | 9 report | `eval_report.py` base vs SFT on the same 8 problems | pass@1 50.0 % -> 68.8 %, solved@2 4/8 -> 6/8, McNemar p = 0.5. Meaningless. The report correctly says the pre-registered primary (cap 16,384, k=8) "could not be computed from these runs", labels everything secondary and names cap 4,096 in every row; pre-registration hash verified | |
|
|
| ### 9.1 Seam assertions (all on the real files above; `scripts/p2/check_seams.py`, tests in `tests/test_p2_integration.py`) |
| |
| | Seam | Assertion | Result | |
| |---|---|---| |
| | generation -> verification | key set `(problem_id, sample_idx, round, cap_tokens)` equal, `code_sha256` matches the code on disk, no truncated sample accepted | round 0: 64 = 64 keys; round 1: 16 = 16; passed | |
| | verification -> trainer | every stored row is an **accepted** sample; context == its `prompt_ids`; the tokens with loss (re-derived through the trainer's `ShardDataset` + `collate_sft`, independent of `build_sft_data`'s own read-back) == its `completion_ids`, no loss in the prompt | 45 rows, all pass; 1 accepted sample unused (duplicate) | |
| | trainer data order | per micro-step the 4 ranks hold disjoint rows; no micro-step repeated or missing across the SIGTERM/resume boundary (1..36 once each, all four ranks); no row seen more than the 9 epochs | passed (visits per row 6-9; rows 45) | |
| | trainer -> exporter -> vLLM | the exported model's logprobs from vLLM equal align's own forward on the same weights | first-token top-1 same on both fixed prompts; first-token \|d logprob\| 5.0e-6 and 7.4e-6; teacher-forced argmax agreement 64/64 on both; max \|d logprob\| of the sampled token 0.045 and 0.051 (bf16 ulp at logit magnitude 32-64 is 0.25) | |
| | exporter -> generator | `lean_gen.py` refuses a model directory it cannot derive a revision for | **found by the loop**: the documented post-SFT evaluation (`run_round.sh post_eval`) passed no `--model-rev`, so it would have died on its first command; both scripts now pass `sft-<sha256 of the weight shards>` | |
|
|
| Seam mutants (`scripts/p2/mutation_check_integration.py`, on a private copy of the tree): **18/18 killed** (unverified samples allowed, stale verdict, truncated-but-accepted, training on a rejected sample, completion not compared, prompt not compared, empty shard set passes, exit code trusted over completeness, retry without progress, finished phases rerun, orphans not reaped, torn tail counted, children not inheriting the lock, partial verification accepted, parent pid / holder label / held-flock checks removed from `inherit_heavy_job_lock`, vLLM process group not signalled). The first run of this check had 4 survivors: a vacuous "empty shard set" test (it passed on a missing file), and three guard mutants each hidden behind a second, redundant check; each got a test that isolates it. |
|
|
| ### 9.2 Defects the loop found |
|
|
| 1. `qwen3_export_check.py` hung 12+ minutes after the result was already written: vLLM's EngineCore outlived its parent re-parented to init, still holding the parent's stdout/stderr pipes, so `subprocess.run(capture_output=True)` never returned; GPU 0 stayed at 19 GB and the lock stayed held. Killed by exact pid (the orphan). Fixed with `run_vllm_child` (log to a file, own session, signal the exact process group after the result appears). Tested with a real orphan; the old pattern is shown to hang (`test_the_blocking_pattern_really_hangs_on_an_orphan`). |
| 2. `run_round.sh post_eval` had no `--model-rev` (above). |
| 3. `torchrun ... scripts/sft.py` needs `PYTHONPATH=<repo>` (the `align` package is not installed in the venv); `smoke_loop.sh` sets it. The P2-A docs launch line does not. |
| 4. Correction rounds never produced a training row on real data (0/18 accepted), so the SFT `kind=correction` path ran only on synthetic data (`tests/test_p2_sft_data.py`), and real correction prompts were checked by eye and by `build_sft_data`'s completeness test only. |
| 5. About 1.4 % of the pool (28/2,000 by a regex: a decimal literal and no `ℝ`/`ℚ`/`ℂ` in the statement) elaborate numerals as `Float` and are unprovable; they pass the elaboration filter because the statement elaborates. They only cost samples. |
| 6. vLLM with per-sample seeds is not bit-reproducible: the same 16 (problem, sample, seed) triples run twice (`base` vs `launch_baseline` test) gave 2/16 identical completions. |
|
|
| ### 9.3 Cross-owner edits made by the integrator (every one) |
|
|
| | File | Owner | Change | |
| |---|---|---| |
| | `scripts/qwen3_export_check.py` | P2-A | `run_vllm_child` replaces `subprocess.run(capture_output=True)` for the vLLM child | |
| | `scripts/p2/run_round.sh` | P2-C | `export_rev` + `--model-rev` for non-base models in `eval_one` | |
| | `align/utils/guard.py` | repo | new function `inherit_heavy_job_lock(parent_pid)` (no existing function changed) | |
| | `extras/vllm_rollout/lean_gen.py` | P2-B | `--inherit-lock PARENT_PID` (3 lines) | |
| | `scripts/p2/verify_generations.py` | P2-C | `--inherit-lock PARENT_PID` (3 lines) | |
| | new | integrator | `scripts/p2/{smoke_loop.sh,check_seams.py,launch_baseline.py,eta.py,mutation_check_integration.py}`, `tests/test_p2_integration.py` | |
|
|
| ## 10. Launching the real baseline (not launched) |
|
|
| One supervised, resumable job: `scripts/p2/launch_baseline.py` takes the repo heavy-job lock once (waits if held), keeps it for |
| `gen cap 16384 -> verify -> gen cap 40960 -> verify`, and runs each phase as a child that inherits the lock (`--inherit-lock`, verified by |
| `inherit_heavy_job_lock`: direct child of the holder, holder named in the lock file, flock genuinely held). Re-running the same command resumes. |
|
|
| ```bash |
| cd /apps/development/rlhf/align |
| RUN=.tmp/p2/r1/baseline |
| mkdir -p $RUN/scratch |
| # rebuild the eval problem files only if missing (CPU; the Lean elaboration check takes the lock for 8 workers): |
| # .venv/bin/python scripts/p2/build_problems.py --phase eval --out-dir .tmp/p2/problems |
| nohup .venv/bin/python scripts/p2/launch_baseline.py --run-dir $PWD/$RUN \ |
| --problems $PWD/.tmp/p2/problems/minif2f.jsonl --n 8 --caps 16384 40960 \ |
| > $RUN/supervisor.out 2>&1 & |
| echo $! > $RUN/supervisor.pid |
| ``` |
|
|
| Watch: `tail -f $RUN/supervisor.jsonl` (one event per phase attempt), `$RUN/logs/<phase>.log`, `cat $RUN/*.done`. |
| Stop (resumable): `kill -TERM $(cat $RUN/supervisor.pid)` (exact pid; it stops the child's process group and exits 143). Resume: run the `nohup` line again. |
| Expected: about 3.5 h for the cap-16,384 half and about 4 h for the 40,960 half (section 6; the second is bracketed 3-6 h). Result lines: the final `complete` event |
| prints `solved@8` per cap; the report against the post-SFT run is `scripts/p2/eval_report.py` as in section 5. |
|
|
| Printed commands (`--print`) are exactly what the supervisor runs. Exit codes: 0 complete, 3 stalled (a phase made no progress between two attempts), 143 stopped by signal. |
|
|
| ## 11. The remaining commands of the real round, with the integrator's measurements |
|
|
| ```bash |
| cd /apps/development/rlhf/align && export RUN=r1 && D=$PWD/.tmp/p2/$RUN |
| # train: P2_TRAIN_CMD for run_round.sh (PYTHONPATH is required; the package is not installed). MAX_SEQ_LEN=18432 for build_sft_data |
| export P2_TRAIN_CMD="env PYTHONPATH=$PWD $PWD/.venv/bin/python -m torch.distributed.run --standalone --nproc_per_node=4 scripts/sft.py configs/p2_sft.toml --data.shard_dir=$D/sft_data/shards --data.manifest_path=$D/sft_data/manifest.json --paths.checkpoint_dir=$D/sft" |
| # export: P2_EXPORT_CMD (merge + HF export + vLLM reload + first-token logprob check; keeps the 16 GB export, delete it when evaluation is done) |
| export P2_EXPORT_CMD="$PWD/.venv/bin/python scripts/qwen3_export_check.py run --ckpt \$(ls -d $D/sft/*/checkpoints/micro_???????? | sort -V | tail -1) --out-dir $D/export --work $D/export_check --r 64 --alpha 128 --keep" |
| MAX_SEQ_LEN=18432 scripts/p2/run_round.sh sft_data train export post_eval report # after the pool steps |
| ``` |
|
|
| Kill/resume of training is the same command again (checkpoints every 40 micro-steps; two kept; partial ones deleted at start). |
|
|
