| # SOTA plan v3: implementation lanes (2026-10-14) |
|
|
| `docs/SOTA_PLAN.md` v3 is the specification. This file says who builds what, in parallel, without collisions. |
|
|
| ## The constraint that shapes everything |
|
|
| * **One GPU lane.** The heavy-job flock serialises every GPU job on this shared box (`/apps/CLAUDE.md` rule 2). |
| Queue: pool round 0 (`chain4`) -> `chain5` (valid n=8 + repair round) -> `chain6` (miniF2F-test anchor n=64 @40k). |
| Later GPU jobs are appended as `chainN.sh` scripts that each wait for the previous chain's bash PID. |
| * **Frozen files.** Files imported by a live chain (`.tmp/audit_2026-10-14/frozen_files.txt`, plus all of |
| `align/verify/`) are edited only on branches and merged after the last chain that imports them has exited. |
| * **Everything else runs in parallel.** Each code lane is one agent in its own git worktree and branch, owning a |
| disjoint set of files. Lanes merge into `master` one at a time, after the full CPU suite passes on the merged tree. |
| * **Disk.** `/home` is a shared 50 GB volume that filled on 2026-10-14. All caches, toolchains and scratch go under |
| `/apps` (set `CARGO_HOME`, `RUSTUP_HOME`, `OPAMROOT`, `ELAN_HOME`, `TMPDIR`, `TORCHINDUCTOR_CACHE_DIR`, |
| `HF_HOME` explicitly). |
|
|
| ## Lanes |
|
|
| | Lane | Branch | Plan items | Owns | Merge gate | |
| |---|---|---|---|---| |
| | V1 verifier freeze | `phase0/verifier` | 0a.1: deferred code-verification findings U08-1/2/3/5/8 (lexer desync, axiom-walk fail-open, sandbox wiring, orphaned REPLs) + red-team fixes; ceiling test | `align/verify/**`, `tests/test_lean*`, `docs/LEAN_VERIFIER.md` | after chain6 exits; frozen hash recorded | |
| | V2 generation harness | `phase0/genharness` | class-B trajectory ledger, U12-2 (lean_gen SIGTERM exit code), U12-3 (orphan reaping), U07-1/2/4 (inference engine), un-merged LoRA adapter serving option (0b.1) | `extras/vllm_rollout/**`, `scripts/p2/pipeline_gen_verify.py`, `align/inference/**` | after chain6 exits | |
| | S statistics + registration | `phase0/stats` | 0a.6: SOTA analysis in eval_report (unbiased pass@k from n=64, paired sign-flip, problem bootstrap, McNemar secondary, Holm, MDE calculator, test-look log), pre-registration document + hash | `scripts/p2/eval_report.py`, new `align/eval/paired.py`, `docs/PREREG_SOTA.md`, tests | any time | |
| | D data supply + decontamination | `phase0/supply` | 0a.4 + 0a.5: candidate-set ingestion (streamed, to `/apps`), problem schema, MinHash + normalised-text decontam, elaborated-type hash tool (Lean, run later in the GPU-free window), membership-check and classifier code (features computed on GPU later) | new `scripts/p2/supply/**`, new `align/data/decontam.py`, tests | any time | |
| | T training | `phase0/training` | U03-2 global token-mean option (config flag, default unchanged), LoRA export fidelity tooling, K-contrast driver (A/A, K1/K2/K4/K6 configs), Kimina-Distill-8B download + config check | `align/train/train_module.py`, `align/train/sft_loss.py`, `configs/p2_*`, new `scripts/p2/contrasts.py`, tests | any time | |
| | B bug-finding benchmark | `paper2/bench` | Phase 5 Part A on CPU: Rust + Charon + Aeneas toolchain under `/apps`, separate Lean 4.31 env, RustSec / fix-commit / mutant ground-truth builder, bounded-checker harness (Kani, proptest, cargo-fuzz) | new top-level `bugfind/` | any time | |
| | R RL wiring [v3.1] | `phase0/rl-lean` | Phase 0b.1: Qwen3 LoRA policy + Lean reward + un-merged adapter publication + resume; positive-only / signed / CISPO / Dr.GRPO loss modes; global token-count normalisation; budget ledger | new `scripts/p2/rl_lean.py`, `configs/p2_rl_lean.toml`, tests | any time (GPU probe after chain6) | |
| | MV math verifier [v3.1] | `phase0/mathverify` | Codex-found false accepts in the math-answer checker (U08-17..24, 29) | `align/verify/{equiv,expr,extract,normalize}.py`, tests | after chain6 (align/verify is frozen) | |
| | N notes | `notes/phase0` | 0307 Aeneas semantics, 0209 variance components + equivalence tests, 0210 data selection + contamination, 0107 Leanstral-variant subsection | `notes/**`, `notebooks/**` | any time | |
| |
| ## Decisions (all taken 2026-10-19 by the project owner) |
| |
| * License: **Apache-2.0** for code, models and data we release (open-source research); data rows keep their source |
| licenses (Nemotron rows CC-BY-SA-4.0, shipped separately). See LICENSE and NOTICE. |
| * Pre-registration `sota-v1` REGISTERED, time-stamped with OpenTimestamps (`docs/evidence/prereg/`); Amendment A1 |
| (MDE recompute from the n = 64 anchor) scheduled before any contrast or candidate result. |
| * Pre-registration choices signed off: dev pass@8 from n = 32; headline = Holm p < 0.05 AND beyond the K0 97.5th |
| percentile; Holm families {K1, K2, K4, K6} and {K5}; priors K2 0-3 pp, K4 0-2 pp, K6 0-1 pp (conditional 0-2 pp). |
| * Host guard rules are permanent (`/apps/development/rlhf/CLAUDE.md`). |
| |
