code/docs/P2.md

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.

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_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

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.

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):

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.

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

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).