docs(pilot): link the recovery audit to the follow-up PR

Raw pilot data stays ignored (copyrighted text); blind key and numeric results are tracked.
Runner notes move into docs/infrastructure.

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01FYqwNMyPUHeTbFWg83GQq6

.gitignore

@@ -38,8 +38,11 @@ htmlcov/
 .idea/
 .vscode/
 
-# Local experiment data: passages from copyrighted books and per-run outputs
+# Local experiment data: passages from copyrighted books and per-run outputs.
+# Each experiment keeps raw data in experiments/<ID>/data/ (ignored) and small,
+# text-free artifacts (keys, verdict-only labels, summaries) in labels/ and results/ (tracked).
 runs/
-**/private/
-*.labels.json
 .leanbench-cache/
+# (data/ above already covers experiments/*/data/; results/ above is ignored for the
+# pipeline's own output, but experiment summaries are numbers only and are tracked.)
+!experiments/*/results/

README.md

@@ -272,6 +272,10 @@ The paper plan for this project (ACL 2027 target, ARR deadline 4 Jan 2027) lives
 [`docs/TODO.md`](docs/TODO.md) and the acceptance-bar analysis in
 [`docs/acl-2027-bar.md`](docs/acl-2027-bar.md).
 
+Experiments have IDs (`P0`, `E0`-`E11`); the registry, phases, gates and conventions are in
+[`docs/experiments/README.md`](docs/experiments/README.md). CI runner and environment notes:
+[`docs/infrastructure/runner-lean435.md`](docs/infrastructure/runner-lean435.md).
+
 ## What this does not claim
 
 Lean says whether the code is *legal*, and — when there is a proof — whether it is

docs/experiments/P0-execution-2026-10-28.md

@@ -0,0 +1,82 @@
+# P0 execution report: 2026-10-28
+
+**Status: blocked by provider billing. No GO, PARTIAL or NO-GO decision.**
+The owner requested delivery of the fixes and this report now, with the remaining paid calls deferred.
+
+## What ran
+
+The owner explicitly authorized sending the 65 textbook passages and corresponding Lean code
+through the existing DashScope endpoint to `qwen-max`, at temperature 0 and a cumulative ceiling
+of 400 HTTP requests. The run issued **131 HTTP requests**. Provider responses accounted for
+**37,699 input tokens and 7,790 output tokens**, 45,489 total. These are recorded token counts,
+not an invoice or a monetary cost estimate. The client counted 89 received model responses;
+a received response is not necessarily a usable detector result.
+
+| Coverage | Count |
+|---|---:|
+| Original cohort | 65 |
+| Items with both detectors complete | 42 |
+| Items with one or both detectors missing | 23 |
+| Successful role-extraction/alignment components | 45 |
+| Successful judge components | 43 |
+| Missing role components | 20 |
+| Missing judge components | 22 |
+| Remaining request reservations | 269 |
+
+DashScope returned HTTP 400 with error code `Arrearage` and its overdue-payment reference.
+The first runner implementation recorded the failures and continued through the cohort, so
+65 saved rows did not mean 65 successful items. The scorer rejected these incomplete outputs.
+No partial-sample gate decision or performance comparison has been produced.
+
+## Inputs and labels
+
+The default `items.jsonl` export omitted `source_text`. All 65 original passages were recovered
+from the matching detection spans and checked byte-for-byte against the archived private
+`review.json`. Item IDs and Lean code were unchanged. The recovery tool also verifies every
+exported field against the archive, normalizing the archive's JSON-encoded imports field.
+Source-inclusive inputs and the regenerated labeling HTML remain in the ignored data directory.
+
+The owner replaced the planned Kimi/human labeling with Codex annotation. All 65 labels were
+frozen before the first detector request. They contain 30 faithful, 25 wrong, 7 minor drift and
+3 not-formalizable verdicts. This is one AI annotator, **not human gold**. The annotator saw the
+detector implementation and aggregate compilation counts, but not per-item compiler outcomes
+or detector outputs. Syntax/proof defects were ignored when the intended semantics were recoverable;
+no compiler or API-name audit was performed. Independent human auditing remains necessary before
+using these labels as evidence for paper-level claims.
+
+## Execution repairs
+
+- Empty passages and mismatched frozen inputs/labels are rejected before paid calls.
+- Each HTTP attempt reserves cumulative budget before sending, including transport and JSON retries.
+  Model, endpoint, temperature, input/label/prompt hashes and cumulative token usage are persisted.
+- Billing/authentication errors now stop immediately, preserving partial results.
+- Resume keeps every successful detector component and retries only missing components. Existing
+  rows are replaced atomically rather than duplicated. A budget stop also preserves completed work
+  within the current item. A lock prevents concurrent writers.
+- `--audit-only` reconciles saved metadata without API calls. It confirmed 42 complete items,
+  23 incomplete items, 42 missing components and 131 already-consumed request reservations.
+- Scoring requires complete results and unchanged frozen-label/result hashes. It restores the
+  preregistered complementary-signal PARTIAL rule and uses wrong versus faithful for primary metrics;
+  minor drift is included as positive only in the secondary comparison.
+- Detector prompts, matching thresholds, the concept table and frozen annotations were not tuned
+  against these outputs. Recovery changes concern transport, persistence and accounting only.
+
+The private first-attempt output and metadata were backed up before reconciliation. The results
+hash and the frozen-label hash did not change during the offline audit.
+
+## Validation and next action
+
+149 offline unit tests passed, including billing-stop and partial-resume regressions; repository-wide
+Ruff and diff checks passed. These checks did not compile Lean or build Docker locally.
+The initial PR revision passed Python tests and real Lean validation on
+`ubuntu24.04-x64-lean4.35`, runner 7, in [CI #427](https://gitea.entroia.com/Zayden-Jung/lean-bench/actions/runs/427).
+The image job was skipped by the PR workflow. The recovery revision's remote result is reported separately in the PR checks.
+
+After the owner confirms billing recovery, resume the existing run with the same inputs, frozen
+labels and cumulative budget. There are 42 missing components; retries may consume more requests.
+Do not change model or prompts to work around the provider block. Only after all 65 items have
+successful outputs should the scorer produce the registered decision and disagreement report.
+Phase 1 has not started.
+
+Tracked audit data: `experiments/P0-pilot/results/execution.json` (counts and hashes only).
+Private raw files: `experiments/P0-pilot/data/` (gitignored).

docs/experiments/P0-pilot.md

@@ -1,11 +1,28 @@
-# Experiment protocol v1 (for approval)
+# P0: pilot protocol (v1)
 
-Status: **awaiting approval. No experiment has been run and no API spend has occurred.**
+Experiment ID **P0**, Phase 0. Registry and conventions: [README.md](README.md).
+
+Status: **approved 2026-10-22; 65 AI labels frozen 2026-10-28; detector run blocked by DashScope Arrearage after 131 requests. 42 items are complete, 23 need missing detector components. No gate decision has been issued.**
+
+The owner explicitly authorized sending the 65 passages and Lean code to DashScope/qwen-max,
+then requested fixes and an execution report now, with paid recovery calls deferred.
+Execution report: [P0 execution, 2026-10-28](P0-execution-2026-10-28.md).
+
+Owner amendment (2026-10-28, in the execution chat): Codex now handles preparation,
+annotation, detector execution and reporting; Kimi's participation is no longer required.
+The frozen labels are from one AI annotator, **not human ground truth**. The annotator saw
+the detector implementation and aggregate compile counts before labeling, but did not see
+per-item compiler outcomes or detector outputs. This departs from the original labeling plan;
+any resulting decision is provisional and cannot substitute for an independent human audit.
+Decision thresholds, detector prompts and the concept table remain fixed. Implementation
+repairs before the first paid call restore the complementary-signal PARTIAL rule, exclude
+minor drift from the primary wrong-versus-faithful comparison, enforce the cumulative HTTP
+request budget, and persist run identity and usage. See `experiments/P0-pilot/README.md`.
 Written 2026-10-22. Companion to `docs/research-plan.md` (what and why), `docs/TODO.md` (task list), `docs/acl-2027-bar.md` (bar). Target: ACL 2027 via ARR, deadline 4 Jan 2027 AoE.
 
-## 1. Decision requested
+## 1. Decision (approved by the owner on 2026-10-22)
 
-Approve **Phase 0 (pilot)** now. It costs a few yuan of API calls, about 4 hours of one person's labeling time, and about 2 days elapsed. Its only job is to tell us whether the paper's central idea (role alignment) has signal before we spend six weeks and a large token budget on it. Phases 1-3 are described so you can see where this leads, but each needs its own go from you after the previous gate.
+**Phase 0 (pilot)** was approved. It costs a few yuan of API calls, about 4 hours of one person's labeling time, and about 2 days elapsed. Its only job is to tell us whether the paper's central idea (role alignment) has signal before we spend six weeks and a large token budget on it. Phases 1-3 are described so you can see where this leads, but each needs its own go from you after the previous gate.
 
 | Phase | What | Cost (API / people) | Elapsed | Gate to continue |
 |---|---|---|---|---|
@@ -20,11 +37,11 @@ Token and CPU figures are the plan's rough estimates (`research-plan.md` 7.9); t
 
 - **H1 (gap).** Compiling overstates fidelity: a large share of formalizations, compiled or not, do not say what the passage says.
 - **H3 (role alignment).** The deterministic alignment of the passage's roles against the Lean signature's roles flags unfaithful items better than the alternatives.
-- Phase 0 does *not* test H2, H4, H5 (guided formalization, retrieval, proving). They need Lean runs and more data.
+- P0 does *not* test H2 (repair), H4 (slot-constrained formalization) or H5 (schema-guided retrieval). They need Lean runs and more data (E8, E7, E9).
 
 ## 3. Phase 0 design
 
-**Items.** The 65 items in `runs/p85-110/items.jsonl` (pages 85-110 of one algebra text; 37 statements, 28 problems). Only 10 of them compiled in Lean. So the pilot judges *fidelity detection over all items*; it cannot yet say anything solid about "compiles but wrong" (n <= 10). That subset is reported with its interval but does not decide anything.
+**Items.** The 65 items in `experiments/P0-pilot/data/items.jsonl` (pages 85-110 of one algebra text; 37 statements, 28 problems). Only 10 of them compiled in Lean. So the pilot judges *fidelity detection over all items*; it cannot yet say anything solid about "compiles but wrong" (n <= 10). That subset is reported with its interval but does not decide anything.
 
 **Labels (ground truth).** One Lean-literate labeler (you, or someone you name) uses `labelsheet.html`: passage and Lean code side by side, shuffled, no compile status, no scores, no model output. Verdicts: faithful / minor drift / wrong / not formalizable, plus error types (missing or extra hypothesis, wrong type, quantifier, wrong conclusion, degenerate, hallucinated API). Labels are finished and saved before any detector output is opened. One labeler means no kappa in Phase 0; that is a stated limitation, fixed in Phase 1.
 
@@ -60,8 +77,8 @@ With about 65 items every interval is wide (a recall of 0.5 on 20 wrong items ha
 ## 5. Infrastructure (ready)
 
 - Runner `ubuntu24.04-x64-lean4.35`, Lean 4.35.0, Mathlib v4.35.0 cache, image `lean-bench:latest` kept on host; CI green on both repos.
-- Code on branch `exp/pilot-prep`: schema, projection, source-side extraction, alignment, lint, stats; labeling sheet, run and score scripts; 140 tests, ruff clean. Offline smoke of run -> score passes with a stub model.
-- Pilot data and labels stay local (`runs/`, `**/private/` are gitignored). The copyrighted book and text derived from it are never committed or released; the public release will use open-licensed books and hashes/spans only.
+- Code on `main`: schema, projection, source-side extraction, alignment, lint, stats; labeling sheet, run and score scripts; 140 tests, ruff clean. Offline smoke of run -> score passes with a stub model.
+- Raw pilot data stays local (`experiments/P0-pilot/data/` is gitignored); the blind key, the verdict-only labels and the numeric summary are tracked. The copyrighted book and text derived from it are never committed or released; the public release will use open-licensed books and hashes/spans only.
 
 ## 6. Risks specific to the near term
 

docs/experiments/README.md

@@ -0,0 +1,61 @@
+# Experiments
+
+Every experiment has one ID. The IDs `E0`-`E11` are the ones used in `docs/research-plan.md` section 6 and `docs/TODO.md`; `P0` is the pilot that gates them. Use the ID in commit messages, result files, and the paper's tables.
+
+Updated 2026-10-22.
+
+## Registry
+
+| ID | Name | Phase | Tests | Spec | Code | Status |
+|---|---|---|---|---|---|---|
+| **P0** | Pilot: do detectors find unfaithful items on the 65 existing ones? | 0 | early look at H1, H3 | [P0-pilot.md](P0-pilot.md) | `experiments/P0-pilot/` | Ready. Waiting on approval record and the 65 human labels. No run yet. |
+| E0 | Simplex projection validated against manual parse (>= 95% on >= 100 signatures) | 1 | method check for C1 | research-plan 6, E0 | `leanbench/project.py`, `tests/test_project.py` | Code done and unit-tested; manual-parse check not done |
+| E1 | Corpus and benchmark construction (6-8 books, >= 1,500 items) | 1 | enables all | research-plan 6, E1 | not written | Not started |
+| E2 | Detection quality (P/R/F1, boundary IoU, run-to-run Jaccard) | 2 | none (measurement) | research-plan 6, E2 | not written | Not started |
+| E3 | Extraction / OCR comparison | 2 | none (measurement) | research-plan 6, E3 | not written | Not started |
+| E4 | Compile vs. faithful gap across >= 4 models | 2 | H1 | research-plan 6, E4 | not written | Not started |
+| E5 | Human annotation: 600-item core, kappa on 200 overlap | 2 | enables E4, E6 | research-plan 6, E5 | `experiments/P0-pilot/make_sheet.py` is the prototype | Not started |
+| E6 | Role-alignment fidelity filter vs. baselines (main method) | 2 | H3 | research-plan 6, E6 | `leanbench/align.py`, `lint.py`, `evalstats.py` | Method code done; P0 is its first check |
+| E7 | Slot-constrained vs. free-form formalization | 2 | H4 | research-plan 6, E7 | not written | Not started |
+| E8 | Repair ablation (0/1/3/5 attempts, whole vs. slot-level) | 2 | H2 | research-plan 6, E8 | not written | Not started |
+| E9 | Schema-guided retrieval and proof guidance | 3 | H5 | research-plan 6, E9 | not written | Not started |
+| E10 | Contamination check | 3 | none (control) | research-plan 6, E10 | not written | Not started |
+| E11 | Cost, time, reliability | 3 | none (report) | research-plan 6, E11 | not written | Not started |
+
+Hypotheses (H1-H5) are stated in `docs/research-plan.md` section 2: H1 compile rate overstates fidelity; H2 repair raises compile more than fidelity; H3 role alignment catches wrong-but-compiles items; H4 slot-constrained formalization raises fidelity; H5 schema-guided retrieval helps provers.
+
+## Phases and gates
+
+| Phase | Experiments | Cost | Elapsed | Gate to continue |
+|---|---|---|---|---|
+| 0 | P0 | ~200 API calls, ~4 h of one labeler | ~2 days | decision rule in P0-pilot.md |
+| 1 | E0, E1, annotation guideline and 50-item kappa pilot | ~10-20M tokens, 2 annotators ~15 h each | ~2 weeks | kappa >= 0.6; E0 >= 95% |
+| 2 | E2-E8 | ~135M tokens plus judges, 2 annotators ~60 h total | 3-4 weeks | go/no-go on 8 Dec |
+| 3 | E9-E11 | bounded by time left | to 24 Dec | tables frozen 24 Dec |
+
+Each phase needs its own go from the project owner. Token and CPU figures are the plan's rough estimates (research-plan 7.9) and are recomputed from P0 before Phase 1.
+
+## Conventions
+
+**Layout.** One directory per experiment: `experiments/<ID>-<slug>/` with
+
+- `README.md`: the commands, in order
+- scripts
+- `data/`: raw inputs and outputs. **Gitignored.** Anything with passages from a copyrighted book, or paraphrases of them, lives here only.
+- `labels/`: human labels and blind keys. Tracked, text-free (verdicts and error types, no passage text).
+- `results/`: summaries (numbers only). Tracked.
+
+**Spec.** `docs/experiments/<ID>-<slug>.md` states hypotheses, design, metrics, decision rule, cost, risks. The decision rule is written before any label or result exists and is not changed afterwards; a change is a new version of the spec.
+
+**Provenance.** Each run records the model id, prompt versions and hashes, call and token counts, and the image/commit it ran on, next to its results.
+
+**Copyright.** The book `uiowa-algebra.pdf` and any text derived from it are never committed or released. The public benchmark uses open-licensed books, with hashes and spans only.
+
+**Blindness.** Labels are finished before detector output is opened. Detectors never see labels.
+
+## Related docs
+
+- `docs/research-plan.md`: idea, venue, related work, experiments in full
+- `docs/TODO.md`: task list to 3 Jan 2027
+- `docs/acl-2027-bar.md`: how the paper reaches the venue's bar
+- `docs/infrastructure/runner-lean435.md`: CI runner, Lean/Mathlib environment, images

docs/infrastructure/runner-lean435.md

@@ -0,0 +1,22 @@
+# Runner `ubuntu24.04-x64-lean4.35` (set up 2026-10-21)
+
+Gitea runner `iZ6we8b3jgd6nc2qehu06lZ` (act_runner v5.2.0, runner id 7), label `ubuntu24.04-x64-lean4.35`. Both `lean-bench` and `lean-agent` CI run here; the old `gitea-cicd-server-for-CODEX` label is no longer used.
+
+## The host
+- Jobs run **on the host, not in a container**, as root. Ubuntu 24.04.5, kernel 6.8, 4 CPU, 15 GiB RAM, no swap, 99 GB disk (88 GB free at setup).
+- Lean 4.35.0 via elan 4.2.4 in `/root/.elan`. Python 3.12.3, git 2.43, gcc 13.3, curl, jq.
+- **No Node**, so `actions/checkout` and other JavaScript actions cannot run. Workflows clone with `git fetch --depth 1 origin $SHA` using `${{ github.token }}`.
+- Docker was not installed; the lean-bench `image` job installs `docker.io` + `docker-buildx` (Docker 29.1.3) if missing.
+- Runner capacity appears to be 1: jobs from both repos queue behind each other.
+
+## What CI does
+- **lean-agent** (`.gitea/workflows/ci.yml`): unit tests with the real Lean verifier, a CLI end-to-end run with a scripted provider, and a Mathlib task against lean-bench's host cache (skips if the cache is not ready).
+- **lean-bench** (`.gitea/workflows/ci.yml`): `python` (ruff + pytest) -> `lean` (host Mathlib cache + `docker/smoke.py` with real Lean) -> `image` (build, smoke inside the image, keep). Triggers: push to `main` and `ci/**`, pull requests, manual. `image` is skipped for pull requests.
+- **Image kept on the host**: `lean-bench:latest`, `:main`, `:lean4.35`, `:sha-<short>` (about 15 GB). `latest`/`main` are tagged only from `main`. Nothing prunes old `sha-*` tags.
+- Mathlib host cache: `/opt/lean-cache/leanbench-<hash of lean-toolchain+lakefile>` with a `.ready` marker, created by `.gitea/scripts/prepare-mathlib.sh` under a flock. `import Mathlib` elaborates in about 4 s there.
+
+## Lessons
+- `lake exe cache get` regularly drops a few of about 9,031 files ("Broken pipe" / "Connection reset"), and the same files can fail twice in a row. Retries fix it.
+- Mathlib's post-update hook runs the cache fetch **inside `lake update`**, so retries placed after it never run. Set `MATHLIB_NO_CACHE_ON_UPDATE=1` for `lake update` and fetch in a retry loop. In the image the archives live in a BuildKit cache mount (`/root/.cache/mathlib`), so a retried build resumes.
+- Cold image build about 19 min; with layers cached about 2 min.
+- Gitea 1.26.1 has no cancel-run API; a person cancels in the web UI, then the API can `DELETE` the finished run. The Actions logs endpoint needs a token; the runs/jobs status endpoints work anonymously on this public repo.

experiments/P0-pilot/README.md

@@ -0,0 +1,65 @@
+# P0: pilot
+
+Experiment ID **P0**. Spec, hypotheses, decision rule and costs: `docs/experiments/P0-pilot.md`.
+Registry of all experiments: `docs/experiments/README.md`.
+
+Question: on the 65 existing items, does role alignment (passage simplex vs. Lean simplex) find
+unfaithful formalizations better than a single LLM judge, compile-only, or static lint?
+
+## Layout
+
+    data/      ignored by git: items.jsonl (copy of the 65 items), labelsheet.html, results.jsonl
+               (all contain or paraphrase passages from a copyrighted book)
+    labels/    tracked: key.json (blind id -> item id, no text), labels.json (verdicts and error
+               types only; do not paste passage text into the notes field)
+    results/   tracked: summary.json written by score.py (numbers only)
+
+## Steps
+
+    # Default exports omit source_text. Restore it from the matching private review.
+    python experiments/P0-pilot/prepare_items.py --items runs/p85-110/items.jsonl \
+        --review runs/p85-110/review.json --out experiments/P0-pilot/data/items.jsonl
+    python experiments/P0-pilot/make_sheet.py --items experiments/P0-pilot/data/items.jsonl \
+        --out experiments/P0-pilot/data --key-dir experiments/P0-pilot/labels --seed 7
+    # a person opens data/labelsheet.html, labels all 65 items, downloads labels.json into labels/
+    python experiments/P0-pilot/run_pilot.py --items experiments/P0-pilot/data/items.jsonl \
+        --out experiments/P0-pilot/data/results.jsonl --dry-run
+    python experiments/P0-pilot/run_pilot.py --items experiments/P0-pilot/data/items.jsonl \
+        --out experiments/P0-pilot/data/results.jsonl --labels experiments/P0-pilot/labels/labels.json
+    python experiments/P0-pilot/score.py --results experiments/P0-pilot/data/results.jsonl \
+        --labels experiments/P0-pilot/labels/labels.json --key experiments/P0-pilot/labels/key.json \
+        --summary experiments/P0-pilot/results/summary.json
+
+Labeling must be finished before anyone opens `results.jsonl`.
+
+## Execution safeguards
+
+- Every item must have a nonempty source passage. `prepare_items.py` restores passages only
+  when all exported fields match the archived review; the exported cohort and Lean code stay intact.
+- Freeze all labels before the paid run. The owner changed the labeler to the Codex assistant
+  on 2026-10-28. These are **AI labels, not human gold**; see the metadata in `labels/labels.json`.
+- `--max-calls` counts actual HTTP attempts, including transport and JSON retries, cumulatively
+  across resumes. The hard ceiling is 400. A reservation is saved before each request; an interrupted
+  request may consume a reservation without a known response or token count.
+- Metadata is stored beside the output as `results.meta.json`. Model, endpoint, temperature,
+  input hash, frozen-label hash and prompt hashes must match on resume. Usage is cumulative.
+  A file lock prevents concurrent writers. A budget stop returns exit status 2.
+- Billing/authentication failures stop immediately. Resume retries only missing detector components,
+  keeping both complete items and the successful side of partial items. Rows are replaced atomically.
+  `--audit-only` reconciles saved completion counts and status without any API request.
+- The nominal successful path uses 130 calls (one source extraction and one judge per item);
+  malformed replies and network retries may increase the actual count.
+- Scoring requires complete labels and results and no unresolved detector errors. The primary
+  comparison is wrong versus faithful; minor drift is included as positive in the secondary analysis.
+  The complementary-signal PARTIAL rule counts wrong items flagged by role alignment but missed
+  by the judge. No threshold, concept table or detector prompt was tuned for these labels.
+- Raw passages, labeling HTML and model responses remain in the ignored `data/` directory.
+  Only verdicts, abstract annotation notes, hashes and text-free summaries belong in Git.
+
+## Current execution
+
+The 2026-10-28 run was blocked by DashScope `Arrearage`: 42 items are complete, 23 need
+42 detector components, and 131 of the 400 request reservations have been consumed.
+The owner requested fixes and a report now, with paid resumption deferred.
+See `docs/experiments/P0-execution-2026-10-28.md` and `results/execution.json`.
+No gate decision has been issued. Restore provider billing before resuming the same run.

experiments/P0-pilot/labels/key.json

@@ -0,0 +1,71 @@
+{
+  "seed": 7,
+  "items_file": "items.jsonl",
+  "key": {
+    "P01": "548ab1a767a685aefa146455",
+    "P02": "6ea85a17cb5decb0670c4afe",
+    "P03": "389a27cbae1957943fae2960",
+    "P04": "b63f0ed4d1ea1e11e34e6f8a",
+    "P05": "db4553333550bccbd3f0e21d",
+    "P06": "c3e75089fbfe8f386b4a22ec",
+    "P07": "91a6a0c1c21014bf08ffa3b6",
+    "P08": "675ac9dbf3ec8a0553149a96",
+    "P09": "8b39fc5b656bac00bc1e863f",
+    "P10": "3549ad65eee67f7b432a8b70",
+    "P11": "0b7db1a8100c33a50a08981f",
+    "P12": "e3d40d93cda13ec59c35d9a5",
+    "P13": "aaf1250a5104a4f7c1ca0d29",
+    "P14": "57966f39253aba58777a4ffd",
+    "P15": "6ef921c49672c73f8f3e0edf",
+    "P16": "371fe1b32fe04da354ad4478",
+    "P17": "a7396b1a5d5ebcd5b48ea7ba",
+    "P18": "59bb865c9bdfb8521e414743",
+    "P19": "283d407566264b02fbee6560",
+    "P20": "7de228e675b949cd64850c04",
+    "P21": "dc1c450987f3e3a5285260f7",
+    "P22": "c42dc687ecc042f5b7a00a9d",
+    "P23": "8491370b02906b6efdb3da5e",
+    "P24": "437d02fe69d580bde075648c",
+    "P25": "5fe4f3fbbead7e6988f015a9",
+    "P26": "8a55f59982e50e4af47b3d55",
+    "P27": "8d4d64143a8b214e38d7ba1b",
+    "P28": "6017927fdafd91ca22ed6ade",
+    "P29": "089c452ec2f9b850733a44f6",
+    "P30": "75009c3d616f02be4d7a5824",
+    "P31": "9091f6a277215174e821d373",
+    "P32": "0cd2f0368a0d8234c2593845",
+    "P33": "8e55e625fa9b10b7b65f59f4",
+    "P34": "534c6ffcf56931559e70657b",
+    "P35": "aa16561dceee591e35e42c4d",
+    "P36": "73ec95bfac2896218d2b1dab",
+    "P37": "6b5a55ec3bb3c85239919649",
+    "P38": "d6ddc1df3ce6b764f3fb8d73",
+    "P39": "ed87589326312890bea42d7c",
+    "P40": "d609c5bb746fc0e05625134a",
+    "P41": "4405f31187373d5e1de622d2",
+    "P42": "05a6defa23576b7da41f8fbf",
+    "P43": "47c39e88c29e3974e8864e90",
+    "P44": "fa61f8cb0e88b11e158c4eec",
+    "P45": "3c00c37b39285cbd7d0be732",
+    "P46": "186d922a4121917ac8643316",
+    "P47": "e845a95d7b5054a0dbdf34eb",
+    "P48": "e7a3cec23c2ecdc655dd12cf",
+    "P49": "e966f3b17e32318acd5f2762",
+    "P50": "2c420bf6ec32069ecd0043dc",
+    "P51": "25af34567cb2040bf41869e5",
+    "P52": "578ae89f353ecbdc0ffb76a2",
+    "P53": "1a8d6a5c9aa3cc5000dee474",
+    "P54": "450c7df89ecd284b0e08504a",
+    "P55": "f908ac15b1bf8228281bcf68",
+    "P56": "bcdfa01447e7060e1fd3d935",
+    "P57": "f86421f93f1381d2ce728bc1",
+    "P58": "89fe687db9136379cd276fff",
+    "P59": "da65aa56505f6c13e6553d0d",
+    "P60": "ab2990e9786d5bda5a04e067",
+    "P61": "a892779bfcaca35b91e7d611",
+    "P62": "7593062cab7c74cdecec08d0",
+    "P63": "c8204e9d19a6dd5d730dccc7",
+    "P64": "b40279b634fffd0841ff0f5a",
+    "P65": "f8d2e206681972927560be2c"
+  }
+}

experiments/P0-pilot/labels/labels.json

@@ -0,0 +1,427 @@
+{
+  "labeler": "Codex AI assistant (this chat; exact deployed model identifier unavailable)",
+  "labeler_type": "AI; not human gold",
+  "frozen_at": "2026-10-28T10:42:10.032234+00:00",
+  "items_sha256": "487ecd22919a5e3b0174a2846ab8fe7c0daf4d3feccccf8ea6571aec04c41bed",
+  "key_sha256": "f827cac92ee4e907554fadcc7c0e006ef2b829350f74e7f8b54ca11945e62836",
+  "method": "Single-pass semantic annotation in shuffled blind-ID order; per-item compiler outcomes and detector outputs hidden. Pure syntax/proof defects are ignored when meaning is recoverable. No compiler/API-name audit. Full extracted-span coverage is assessed; unspecified design tasks or unresolved contextual references are not formalizable.",
+  "limitations": [
+    "Single AI annotator; no human adjudication or inter-annotator agreement.",
+    "The annotator reviewed detector implementation and aggregate compilation counts before labeling; only per-item outputs were hidden.",
+    "AI labels replace the originally planned human/Kimi labels by explicit owner instruction in this chat; the original human-ground-truth protocol is therefore not fully satisfied."
+  ],
+  "labels": {
+    "P01": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The field axioms and nontriviality match the stated definition."
+    },
+    "P02": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The whole carrier and identity singleton are the two specified subgroups; API spelling is not assessed."
+    },
+    "P03": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Every integer unit is constrained to the two specified values."
+    },
+    "P04": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Generated subgroup is equated with all integer powers; escaped notation is treated as a syntax defect."
+    },
+    "P05": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Existence of a bijective multiplication-preserving map matches the definition."
+    },
+    "P06": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The theorem statement gives exactly the inverse-of-product identity; proof validity is not assessed."
+    },
+    "P07": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_conclusion",
+        "degenerate"
+      ],
+      "notes": "Only already-assumed prime factors are asserted to exist; no recovery from the totient is specified."
+    },
+    "P08": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Both identity preservation and inverse preservation are stated under a multiplicative equivalence."
+    },
+    "P09": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type",
+        "wrong_conclusion"
+      ],
+      "notes": "The multiplicative ring carrier does not encode the additive cyclic group, and the second extracted exercise is omitted."
+    },
+    "P10": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Both left and right equations have unique solutions."
+    },
+    "P11": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The group cardinality is the exponent, with the correct identity and quantification."
+    },
+    "P12": {
+      "verdict": "not_formalizable",
+      "errors": [
+        "other"
+      ],
+      "notes": "The extracted design question provides no formal security or authentication specification for a fidelity comparison."
+    },
+    "P13": {
+      "verdict": "minor_drift",
+      "errors": [
+        "wrong_type"
+      ],
+      "notes": "The intended modular identity is retained, but the integer variable is supplied to a natural-number coprimality predicate."
+    },
+    "P14": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_conclusion"
+      ],
+      "notes": "Only existence of a ring structure is stated; the identity and unit characterization are omitted."
+    },
+    "P15": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Unique solvability in both factors expresses the row and column permutation property."
+    },
+    "P16": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Passing to the product representation preserves the order-divisibility claim; capitalization and namespace errors are not semantic changes."
+    },
+    "P17": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_conclusion"
+      ],
+      "notes": "An independent non-field example in the extracted passage is omitted."
+    },
+    "P18": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The norm-one complex carrier and multiplication describe the specified subgroup; bundling/API validity is not assessed."
+    },
+    "P19": {
+      "verdict": "minor_drift",
+      "errors": [
+        "wrong_type"
+      ],
+      "notes": "The natural-valued order convention needs an infinite-order convention absent from the cardinality definition."
+    },
+    "P20": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "A single left-identity action on one group element forces equality to the identity."
+    },
+    "P21": {
+      "verdict": "minor_drift",
+      "errors": [
+        "wrong_type"
+      ],
+      "notes": "The intended commutativity equivalence is visible, but the left operation lacks the carrier annotation needed to identify G."
+    },
+    "P22": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The two quantified unique-solvability claims express the specified table property."
+    },
+    "P23": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Prime factors, modulus, lcm exponent and coprimality reproduce the extracted claim; no unstated distinctness assumption is introduced."
+    },
+    "P24": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_conclusion",
+        "degenerate"
+      ],
+      "notes": "An arbitrary group satisfying an order condition is not identified with the geometric symmetry group."
+    },
+    "P25": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The two declarations cover both cancellation directions."
+    },
+    "P26": {
+      "verdict": "wrong",
+      "errors": [
+        "extra_hypothesis",
+        "missing_hypothesis"
+      ],
+      "notes": "The inserted divisibility assumption does not express the RSA relationship required by the argument."
+    },
+    "P27": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_conclusion"
+      ],
+      "notes": "The isomorphism is asserted for a quotient of the ambient group instead of the stabilizer subgroup."
+    },
+    "P28": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type",
+        "wrong_conclusion"
+      ],
+      "notes": "Natural exponent division fails to express a square root, and the homomorphism target does not encode the specified automorphism."
+    },
+    "P29": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "A bijective homomorphism supplies the isomorphism assumption and both power assertions are retained."
+    },
+    "P30": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type"
+      ],
+      "notes": "An unordered finite product is used for an arbitrary semigroup, losing the ordered nonempty product required by the exercise."
+    },
+    "P31": {
+      "verdict": "not_formalizable",
+      "errors": [
+        "other"
+      ],
+      "notes": "The isolated instruction refers to an earlier map whose definition is absent; the actual proposition cannot be recovered from this span."
+    },
+    "P32": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_conclusion",
+        "degenerate"
+      ],
+      "notes": "The result merely supplies an unspecified ring homomorphism and does not constrain it to evaluation at the matrix parameter."
+    },
+    "P33": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The cardinality assumption and the nonidentity involution conclusion match; the missing instance binder is a compilation defect."
+    },
+    "P34": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The contrasting abelian properties encode the reason these specified groups are not isomorphic."
+    },
+    "P35": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type",
+        "quantifier"
+      ],
+      "notes": "One fixed-arity function is applied at incompatible arities instead of specifying a coherent family of products."
+    },
+    "P36": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type",
+        "wrong_conclusion"
+      ],
+      "notes": "The ring carrier replaces the concrete root-of-unity group, and neither its order nor the specified generator is stated."
+    },
+    "P37": {
+      "verdict": "wrong",
+      "errors": [
+        "degenerate",
+        "wrong_conclusion"
+      ],
+      "notes": "The declaration has no defining expression for the requested subgroup."
+    },
+    "P38": {
+      "verdict": "wrong",
+      "errors": [
+        "missing_hypothesis"
+      ],
+      "notes": "Nonemptiness is missing, so the empty subset satisfies both closure assumptions."
+    },
+    "P39": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type",
+        "wrong_conclusion"
+      ],
+      "notes": "Laurent series replace finite Laurent polynomials, and the requested units are not characterized."
+    },
+    "P40": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The supplied structure body fixes the function to the canonical integer residue map."
+    },
+    "P41": {
+      "verdict": "wrong",
+      "errors": [
+        "extra_hypothesis"
+      ],
+      "notes": "The cardinality assertion is restricted to the range where noncommutativity holds, dropping the smaller symmetric groups."
+    },
+    "P42": {
+      "verdict": "wrong",
+      "errors": [
+        "missing_hypothesis",
+        "wrong_conclusion"
+      ],
+      "notes": "A necessary closure condition is promoted to sufficiency without inverse closure."
+    },
+    "P43": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Any two groups of the specified size are related by a multiplicative equivalence."
+    },
+    "P44": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The defining field is exactly commutativity of the group operation."
+    },
+    "P45": {
+      "verdict": "wrong",
+      "errors": [
+        "quantifier",
+        "wrong_conclusion"
+      ],
+      "notes": "Literal uniqueness of a carrier/structure replaces uniqueness up to group isomorphism."
+    },
+    "P46": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type",
+        "wrong_conclusion"
+      ],
+      "notes": "Univariate polynomials over a product ring replace three-variable real polynomials; the units question is omitted."
+    },
+    "P47": {
+      "verdict": "minor_drift",
+      "errors": [
+        "wrong_conclusion"
+      ],
+      "notes": "The integer-span equality captures the generated set, but the equality for opposite generators is not explicitly stated."
+    },
+    "P48": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The one-sided inverse hypothesis gives the specified inverse element."
+    },
+    "P49": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The theorem statement is exactly involutivity of group inversion."
+    },
+    "P50": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The custom structure supplies additive commutative group, associative multiplication and both distributive laws without imposing a unit."
+    },
+    "P51": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The carrier, multiplication and identity encode the specified finite group; existence of the chosen API is not audited."
+    },
+    "P52": {
+      "verdict": "minor_drift",
+      "errors": [
+        "wrong_conclusion",
+        "degenerate"
+      ],
+      "notes": "Ring structure and unit-to-constant direction are present, but identity characterization is replaced by reflexivity."
+    },
+    "P53": {
+      "verdict": "minor_drift",
+      "errors": [
+        "extra_hypothesis"
+      ],
+      "notes": "Cardinality is represented only for finite groups although the definition is not restricted to them."
+    },
+    "P54": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type"
+      ],
+      "notes": "Multiplicative subgroup closure of a residue is used in place of the additive cyclic subgroup generated by it."
+    },
+    "P55": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The abelian-property equivalence is stated under an isomorphism."
+    },
+    "P56": {
+      "verdict": "not_formalizable",
+      "errors": [
+        "other"
+      ],
+      "notes": "The design question does not specify an authenticity predicate or formal adversarial model."
+    },
+    "P57": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_conclusion"
+      ],
+      "notes": "The homomorphism criterion is retained but the separate isomorphism definition is absent."
+    },
+    "P58": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type"
+      ],
+      "notes": "A multiplicative equivalence on the full residue ring does not represent the additive cyclic group in the comparison."
+    },
+    "P59": {
+      "verdict": "minor_drift",
+      "errors": [
+        "wrong_type"
+      ],
+      "notes": "The inherited-group criterion is recognizable, but operations on the subset are not specified as restricted operations."
+    },
+    "P60": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type",
+        "missing_hypothesis"
+      ],
+      "notes": "Global bijections with local differentiability conditions do not specify self-diffeomorphisms of the open subset."
+    },
+    "P61": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The homeomorphism type supplies the intended carrier and group structure under composition; notation validity is not assessed."
+    },
+    "P62": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Both least-positive exponent and the bounded-power description are retained, ignoring set-minimum API syntax."
+    },
+    "P63": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Both two-sided identity hypotheses and their equality are stated."
+    },
+    "P64": {
+      "verdict": "wrong",
+      "errors": [
+        "missing_hypothesis",
+        "extra_hypothesis"
+      ],
+      "notes": "The exponent relation uses the ciphertext modulus where the RSA exponent modulus is required."
+    },
+    "P65": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_conclusion",
+        "degenerate"
+      ],
+      "notes": "The arbitrary finite group is unrelated to the requested geometric symmetries, with the classification left in a comment."
+    }
+  }
+}

experiments/P0-pilot/make_sheet.py

@@ -1,13 +1,14 @@
 """Build the blind labeling sheet for the pilot.
 
-    python experiments/pilot/make_sheet.py --items runs/p85-110/items.jsonl \
-        --out runs/pilot/private --seed 7
+    python experiments/P0-pilot/make_sheet.py --items experiments/P0-pilot/data/items.jsonl \
+        --out experiments/P0-pilot/data --key-dir experiments/P0-pilot/labels --seed 7
 
-Writes, into a directory that must stay local (it contains passages from a
-copyrighted book; ``runs/`` and ``**/private/`` are gitignored):
+Writes:
 
-    labelsheet.html     open in a browser; label every item; press "Download labels.json"
-    key.json            blind id -> item id (keep it; the scorer needs it)
+    <out>/labelsheet.html    open in a browser; label every item; press "Download labels.json".
+                             Contains passages from a copyrighted book, so ``data/`` is gitignored.
+    <key-dir>/key.json       blind id -> item id. Text-free, so it is tracked in git; save the
+                             downloaded labels.json next to it.
 
 The sheet shows the passage and the Lean code. It deliberately hides whether Lean
 accepted the code, any model output, and any score, so the labels are independent of
@@ -146,12 +147,17 @@ def card(blind: str, item: dict) -> str:
 def main() -> int:
     parser = argparse.ArgumentParser(description=__doc__.splitlines()[0])
     parser.add_argument("--items", required=True, type=Path)
-    parser.add_argument("--out", required=True, type=Path)
+    parser.add_argument("--out", required=True, type=Path, help="where labelsheet.html goes (ignored by git)")
+    parser.add_argument("--key-dir", type=Path, default=None, help="where key.json goes (default: ../labels)")
     parser.add_argument("--seed", type=int, default=7)
     args = parser.parse_args()
 
     items = [json.loads(line) for line in args.items.read_text(encoding="utf-8").splitlines()
              if line.strip()]
+    if not items or any(not item.get("source_text", "").strip() for item in items):
+        parser.error("Every item needs nonempty source_text; use a private source-inclusive export.")
+    if len({item["id"] for item in items}) != len(items):
+        parser.error("Item IDs must be unique.")
     order = list(range(len(items)))
     random.Random(args.seed).shuffle(order)
     blind_ids = [f"P{n:02d}" for n in range(1, len(items) + 1)]
@@ -159,16 +165,18 @@ def main() -> int:
 
     legend = "".join(f"<li><b>{esc(n)}</b>: {esc(d)}</li>" for _, n, d in FIDELITY)
     cards = "\n".join(card(blind_ids[pos], items[idx]) for pos, idx in enumerate(order))
+    key_dir = args.key_dir or args.out.parent / "labels"
     args.out.mkdir(parents=True, exist_ok=True)
+    key_dir.mkdir(parents=True, exist_ok=True)
     (args.out / "labelsheet.html").write_text(
         PAGE.format(n=len(items), legend=legend, cards=cards, ids=json.dumps(blind_ids)),
         encoding="utf-8",
     )
-    (args.out / "key.json").write_text(
+    (key_dir / "key.json").write_text(
         json.dumps({"seed": args.seed, "items_file": args.items.name, "key": key}, indent=2),
         encoding="utf-8",
     )
-    print(f"wrote {args.out/'labelsheet.html'} ({len(items)} items) and key.json")
+    print(f"wrote {args.out/'labelsheet.html'} ({len(items)} items) and {key_dir/'key.json'}")
     return 0
 
 

experiments/P0-pilot/prepare_items.py

@@ -0,0 +1,45 @@
+"""Restore source passages from a private archived review without changing the cohort."""
+from __future__ import annotations
+
+import argparse
+import json
+from pathlib import Path
+
+
+def restore(items: list[dict], review: dict) -> list[dict]:
+    archived = review["items"]
+    by_id = {row["id"]: row for row in archived}
+    if len(by_id) != len(archived) or len({row["id"] for row in items}) != len(items):
+        raise ValueError("Duplicate item IDs")
+    restored = []
+    for item in items:
+        original = by_id[item["id"]]
+        comparable = dict(original)
+        if isinstance(comparable.get("imports"), str):
+            comparable["imports"] = json.loads(comparable["imports"])
+        if any(comparable.get(k) != v for k, v in item.items()):
+            raise ValueError(f"Archived review does not match item {item['id']}")
+        passage = original.get("source_text", "")
+        if not passage.strip():
+            raise ValueError(f"Missing archived passage for {item['id']}")
+        restored.append({**item, "source_text": passage})
+    return restored
+
+
+def main() -> None:
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--items", required=True, type=Path)
+    parser.add_argument("--review", required=True, type=Path)
+    parser.add_argument("--out", required=True, type=Path)
+    args = parser.parse_args()
+    if args.out.parent.name != "data":
+        parser.error("Source-inclusive output must go in a gitignored data/ directory")
+    items = [json.loads(line) for line in args.items.read_text().splitlines() if line.strip()]
+    rows = restore(items, json.loads(args.review.read_text()))
+    args.out.parent.mkdir(parents=True, exist_ok=True)
+    args.out.write_text("".join(json.dumps(row, ensure_ascii=False) + "\n" for row in rows))
+    print(f"Restored {len(rows)} passages; all exported fields are unchanged")
+
+
+if __name__ == "__main__":
+    main()

experiments/P0-pilot/results/execution.json

@@ -0,0 +1,71 @@
+{
+  "experiment": "P0",
+  "status": "provider_blocked",
+  "decision": null,
+  "decision_withheld_reason": "Incomplete detector outputs after DashScope Arrearage; no GO/PARTIAL/NO-GO is valid.",
+  "cohort_size": 65,
+  "completed_items": 42,
+  "items_with_failures": 23,
+  "missing_components": {
+    "judge": 22,
+    "role": 20
+  },
+  "request_attempts": 131,
+  "max_calls": 400,
+  "remaining_request_budget": 269,
+  "usage": {
+    "calls": 89,
+    "prompt_tokens": 37699,
+    "completion_tokens": 7790
+  },
+  "model": "qwen-max",
+  "temperature": 0.0,
+  "items_sha256": "487ecd22919a5e3b0174a2846ab8fe7c0daf4d3feccccf8ea6571aec04c41bed",
+  "labels_sha256": "1552dba85e75426799151384e7e28c9a0b1072ed4c862df0876df89920d2a638",
+  "results_sha256": "fce402e6eab460a48bb9a8e94140bb23f305843ab46d227bbffa5100d7de69e5",
+  "prompt_hashes": {
+    "source": "382f9a7b5a0cfb2d50d525f884dc806f45adaa59bcc45e388920c4759db1546f",
+    "judge": "7ab92682bd71d78a212471289f0f01db39d6b68f49d44df65d7b1c9e34ebb5e2"
+  },
+  "labels": {
+    "type": "single AI annotator; not human gold",
+    "frozen": true,
+    "count": 65
+  },
+  "affected_blind_ids": [
+    "P02",
+    "P04",
+    "P09",
+    "P18",
+    "P19",
+    "P20",
+    "P21",
+    "P22",
+    "P24",
+    "P27",
+    "P29",
+    "P30",
+    "P33",
+    "P36",
+    "P37",
+    "P38",
+    "P42",
+    "P43",
+    "P45",
+    "P47",
+    "P54",
+    "P59",
+    "P62"
+  ],
+  "successful_components_preserved": 88,
+  "resume_policy": "After owner confirms billing recovery, retry missing components only using the same run files, frozen labels, model, prompts and cumulative 400-request ceiling.",
+  "owner_instruction": "2026-10-28: complete fixes and the execution report now; resume paid calls later.",
+  "validation": {
+    "offline_unit_tests": 149,
+    "ruff": "passed",
+    "remote_runner_tag": "ubuntu24.04-x64-lean4.35",
+    "initial_remote_ci": "https://gitea.entroia.com/Zayden-Jung/lean-bench/actions/runs/427",
+    "initial_remote_ci_status": "success; image job skipped for PR",
+    "recovery_remote_ci": "See follow-up PR #6 checks for the delivered head revision"
+  }
+}

experiments/P0-pilot/run_pilot.py

@@ -0,0 +1,272 @@
+"""Run the pilot detectors over the pilot items. Resumable; one JSON line per item.
+
+    python experiments/P0-pilot/run_pilot.py --items experiments/P0-pilot/data/items.jsonl \
+        --out experiments/P0-pilot/data/results.jsonl --dry-run          # no API calls: shows the plan
+    python experiments/P0-pilot/run_pilot.py --items ... --out ... --max-calls 400
+
+Detectors (all see the passage and/or the Lean code, never the human labels):
+  lint    static patterns on the projected simplex          (no LLM)
+  role    source-side simplex (LLM sees only the passage) aligned to the Lean simplex
+  judge   one LLM call that sees passage + Lean and says faithful / not
+  compile the stored Lean verdict (``verified``), read from the items file
+
+Hard stops: --max-calls bounds API calls; a rerun skips items already in --out.
+"""
+from __future__ import annotations
+
+import argparse
+import fcntl
+import hashlib
+import inspect
+import json
+import os
+import sys
+from pathlib import Path
+
+from leanbench import srcsimplex
+from leanbench.align import align
+from leanbench.config import Settings
+from leanbench.lint import lint
+from leanbench.llm import OpenAICompatibleClient, Usage
+from leanbench.project import project
+
+JUDGE_PROMPT_VERSION = "judge-v1"
+JUDGE_SYSTEM = (
+    "You check a Lean 4 (Mathlib) formalization against a textbook passage. Decide whether the "
+    "Lean statement says what the passage says: same objects, same hypotheses, same conclusion, "
+    "same quantifiers. Ignore whether it compiles. Reply with JSON only: "
+    '{"faithful": true|false, "confidence": 0..1, "reason": "one sentence"}'
+)
+
+
+def judge(client, passage: str, lean: str) -> dict:
+    reply = client.complete_json([
+        {"role": "system", "content": JUDGE_SYSTEM},
+        {"role": "user", "content": f"Passage:\n{passage}\n\nLean:\n{lean}"},
+    ])
+    if not isinstance(reply, dict) or type(reply.get("faithful")) is not bool:
+        raise ValueError(f"unusable judge reply: {str(reply)[:200]}")
+    return {"faithful": reply["faithful"], "confidence": reply.get("confidence"),
+            "reason": str(reply.get("reason", ""))[:300]}
+
+
+def provider_blocked(error: Exception) -> bool:
+    text = str(error).lower()
+    return any(code in text for code in ("arrearage", "overdue-payment", "invalid_api_key", "http 401", "http 403"))
+
+
+def complete_row(row: dict) -> bool:
+    return not row.get("errors") and "role" in row and "judge" in row
+
+
+class ProviderBlocked(RuntimeError):
+    """A billing or authentication failure requires external recovery before resuming."""
+
+    def __init__(self, row):
+        super().__init__("Provider billing/authentication blocked; partial results were preserved")
+        self.row = row
+
+
+class CallBudgetExceeded(RuntimeError):
+    """Stop before issuing a request that would exceed the cumulative budget."""
+
+
+def run_item(client, item: dict, previous: dict | None = None) -> dict:
+    if not item.get("source_text", "").strip():
+        raise ValueError("Missing source_text; use a private source-inclusive export")
+    code = item.get("lean_code") or ""
+    row: dict = {**(previous or {}), "id": item["id"], "compiled": bool(item.get("verified"))}
+    row["errors"] = dict(row.get("errors", {}))
+    proj = project(code)
+    row["projection"] = proj.as_dict()
+    row["lint"] = lint(proj)
+    if "role" not in row:
+        try:
+            src = srcsimplex.extract_source_simplex(client, item["source_text"], item.get("label", ""))
+            al = align(src, proj)
+            row["source"] = [r.__dict__ for r in src.roles]
+            row["role"] = al.as_dict()
+            row["errors"].pop("role", None)
+        except CallBudgetExceeded as error:
+            error.row = row
+            raise
+        except Exception as error:
+            row["errors"]["role"] = str(error)[:300]
+            if provider_blocked(error):
+                raise ProviderBlocked(row) from error
+    if "judge" not in row:
+        try:
+            row["judge"] = judge(client, item["source_text"], code)
+            row["errors"].pop("judge", None)
+        except CallBudgetExceeded as error:
+            error.row = row
+            raise
+        except Exception as error:
+            row["errors"]["judge"] = str(error)[:300]
+            if provider_blocked(error):
+                raise ProviderBlocked(row) from error
+    return row
+
+
+def digest(path: Path) -> str:
+    return hashlib.sha256(path.read_bytes()).hexdigest()
+
+
+def atomic_json(path: Path, value: dict) -> None:
+    temporary = path.with_suffix(path.suffix + ".tmp")
+    temporary.write_text(json.dumps(value, indent=2, allow_nan=False) + "\n", encoding="utf-8")
+    os.replace(temporary, path)
+
+
+class AuditedClient(OpenAICompatibleClient):
+    """Persist reservations before HTTP requests, including transport and JSON retries."""
+
+    def complete(self, *args, **kwargs):
+        try:
+            return super().complete(*args, **kwargs)
+        finally:
+            self.checkpoint()
+
+
+def execute(args, items, settings) -> int:
+    rows = []
+    if args.out.exists():
+        rows = [json.loads(x) for x in args.out.read_text(encoding="utf-8").splitlines() if x.strip()]
+    ids = {item["id"] for item in items}
+    by_id = {row["id"]: row for row in rows}
+    done = {row["id"] for row in rows if complete_row(row)}
+    if len(by_id) != len(rows) or not set(by_id) <= ids:
+        raise ValueError("Results have duplicate or unknown item IDs")
+    hashes = {
+        "source": hashlib.sha256((srcsimplex.SYSTEM_PROMPT + inspect.getsource(srcsimplex.passage_prompt)).encode()).hexdigest(),
+        "judge": hashlib.sha256(JUDGE_SYSTEM.encode()).hexdigest(),
+    }
+    identity = {"model": settings.llm.model, "base_url": settings.llm.base_url,
+                "temperature": settings.llm.temperature, "items_sha256": digest(args.items),
+                "prompt_hashes": hashes,
+                "prompts": [srcsimplex.PROMPT_VERSION, JUDGE_PROMPT_VERSION]}
+    labels = getattr(args, "labels", None)
+    if labels is not None:
+        identity["labels_sha256"] = digest(labels)
+    meta_path = args.out.with_suffix(".meta.json")
+    meta = {**identity, "request_attempts": 0, "usage": Usage().as_dict(), "status": "ready"}
+    if meta_path.exists():
+        meta = json.loads(meta_path.read_text(encoding="utf-8"))
+        if any(meta.get(k) != v for k, v in identity.items()):
+            raise ValueError("Run identity changed; use a new output path instead of mixing runs")
+    elif rows:
+        raise ValueError("Cannot resume results without their audit metadata")
+    todo = [item for item in items if item["id"] not in done]
+    missing = sum(2 - int("role" in by_id.get(i["id"], {}))
+                  - int("judge" in by_id.get(i["id"], {})) for i in todo)
+    print(f"items={len(items)} done={len(done)} todo={len(todo)} model={settings.llm.model} "
+          f"missing_components={missing} request_attempts={meta['request_attempts']} cap={args.max_calls}")
+    print("prompt_hashes:", json.dumps(hashes))
+    if args.dry_run:
+        return 0
+    if getattr(args, "audit_only", False):
+        meta["completed_items"] = len(done)
+        meta["processed_items"] = len(rows)
+        meta["status"] = ("provider_blocked" if any(provider_blocked(RuntimeError(message))
+                          for row in rows for message in row.get("errors", {}).values())
+                          else "detector_errors" if todo else "complete")
+        if args.out.exists():
+            meta["results_sha256"] = digest(args.out)
+        atomic_json(meta_path, meta)
+        print(json.dumps(meta))
+        return 0 if meta["status"] == "complete" else 2
+    if settings.llm.model != "qwen-max" or settings.llm.temperature != 0:
+        raise ValueError("P0 is preregistered for qwen-max at temperature 0")
+    client = AuditedClient.from_settings(settings.llm)
+    client.usage = Usage(**meta["usage"])
+
+    def checkpoint():
+        meta["usage"] = client.usage.as_dict()
+        meta["completed_items"] = len(done)
+        meta["processed_items"] = len(by_id)
+        atomic_json(meta_path, meta)
+
+    def reserve():
+        if meta["request_attempts"] >= args.max_calls:
+            raise CallBudgetExceeded("Cumulative request cap reached; no further HTTP request was sent")
+        meta["request_attempts"] += 1
+        checkpoint()
+
+    client.checkpoint = checkpoint
+    client.request_guard = reserve
+    meta["max_calls"] = args.max_calls
+    meta["status"] = "running"
+    checkpoint()
+    def save_row(row):
+        by_id[row["id"]] = row
+        if complete_row(row):
+            done.add(row["id"])
+        temporary = args.out.with_suffix(args.out.suffix + ".tmp")
+        with temporary.open("w", encoding="utf-8") as stream:
+            for item in items:
+                if item["id"] in by_id:
+                    stream.write(json.dumps(by_id[item["id"]], ensure_ascii=False) + "\n")
+            stream.flush()
+            os.fsync(stream.fileno())
+        os.replace(temporary, args.out)
+        checkpoint()
+
+    try:
+        for item in todo:
+            row = run_item(client, item, by_id.get(item["id"]))
+            save_row(row)
+            print(f"completed={len(done)}/{len(items)} requests={meta['request_attempts']}", flush=True)
+        meta["status"] = "complete" if len(done) == len(items) else "detector_errors"
+    except (CallBudgetExceeded, ProviderBlocked) as error:
+        if getattr(error, "row", None) is not None:
+            save_row(error.row)
+        meta["status"] = "provider_blocked" if isinstance(error, ProviderBlocked) else "budget_exhausted"
+        print(str(error), file=sys.stderr)
+    except BaseException:
+        meta["status"] = "interrupted"
+        raise
+    finally:
+        if args.out.exists():
+            meta["results_sha256"] = digest(args.out)
+        checkpoint()
+    print(json.dumps(meta))
+    return 0 if meta["status"] == "complete" else 2
+
+
+def main() -> int:
+    ap = argparse.ArgumentParser(description=__doc__.splitlines()[0])
+    ap.add_argument("--items", required=True, type=Path)
+    ap.add_argument("--out", required=True, type=Path)
+    ap.add_argument("--max-calls", type=int, default=400)
+    ap.add_argument("--dry-run", action="store_true")
+    ap.add_argument("--audit-only", action="store_true", help="Reconcile saved state without making API calls")
+    ap.add_argument("--labels", type=Path, help="Frozen labels; their hash is bound to the run")
+    args = ap.parse_args()
+    if not 1 <= args.max_calls <= 400:
+        ap.error("P0 requires a request cap between 1 and 400")
+    items = [json.loads(x) for x in args.items.read_text(encoding="utf-8").splitlines() if x.strip()]
+    if not items or len({item["id"] for item in items}) != len(items):
+        ap.error("Input must contain unique item IDs")
+    if any(not item.get("source_text", "").strip() for item in items):
+        ap.error("Every item needs nonempty source_text; use a private source-inclusive export")
+    if not args.dry_run and args.labels is None:
+        ap.error("Freeze all blind labels first, then pass --labels")
+    if args.labels is not None:
+        annotation = json.loads(args.labels.read_text(encoding="utf-8"))
+        key_path = args.labels.with_name("key.json")
+        key = json.loads(key_path.read_text(encoding="utf-8"))["key"]
+        verdicts = {"faithful", "minor_drift", "wrong", "not_formalizable"}
+        if (set(key.values()) != {item["id"] for item in items}
+                or set(annotation["labels"]) != set(key)
+                or any(row.get("verdict") not in verdicts for row in annotation["labels"].values())
+                or annotation.get("items_sha256") != digest(args.items)
+                or annotation.get("key_sha256") != digest(key_path)):
+            ap.error("Frozen labels, key and source-inclusive items must be complete and match")
+    args.out.parent.mkdir(parents=True, exist_ok=True)
+    with args.out.with_suffix(args.out.suffix + ".lock").open("w") as lock:
+        fcntl.flock(lock, fcntl.LOCK_EX | fcntl.LOCK_NB)
+        return execute(args, items, Settings.from_env())
+
+
+if __name__ == "__main__":
+    raise SystemExit(main())

experiments/P0-pilot/score.py

@@ -0,0 +1,149 @@
+"""Score the pilot against frozen blind labels using the pre-registered decision.
+
+    python experiments/P0-pilot/score.py --results experiments/P0-pilot/data/results.jsonl \
+        --labels experiments/P0-pilot/labels/labels.json --key experiments/P0-pilot/labels/key.json --summary experiments/P0-pilot/results/summary.json
+
+Positive class = unfaithful. Primary: wrong versus faithful, excluding minor drift (role alignment and
+the judge do not need Lean to accept the code; only 10 of the 65 pilot items compiled, too few to
+decide on). Secondary: wrong or minor_drift; and the compiled-only subset (the paper's claim, reported
+with its interval, not used to decide). "not_formalizable" items are excluded. Decision (fixed before
+looking at labels):
+
+  GO       role recall on wrong items >= 0.5 AND false-flag rate on faithful items <= 0.2
+           AND role recall >= judge recall + 0.10 at a false-flag rate no higher than the judge's
+  PARTIAL  role recall >= 0.4 with false-flag <= 0.3, or role complements the judge
+           (flags >= 3 wrong items the judge misses)
+  NO-GO    otherwise (re-scope to evaluation + taxonomy + resource)
+With ~65 items every number carries a wide Wilson interval; the pilot checks for signal, not effect size.
+"""
+from __future__ import annotations
+
+import argparse
+import hashlib
+import json
+import math
+from pathlib import Path
+
+from leanbench.evalstats import auc, confusion, wilson
+
+
+def load(args):
+    result_rows = [json.loads(x) for x in args.results.read_text(encoding="utf-8").splitlines() if x.strip()]
+    results = {row["id"]: row for row in result_rows}
+    labels = json.loads(args.labels.read_text(encoding="utf-8"))["labels"]
+    key = json.loads(args.key.read_text(encoding="utf-8"))["key"]
+    if not key or len(set(key.values())) != len(key):
+        raise ValueError("The blind key must contain unique item IDs")
+    if len(results) != len(result_rows) or set(results) != set(key.values()):
+        raise ValueError("Results must cover every keyed item exactly once")
+    if set(labels) != set(key):
+        raise ValueError("Labels must cover every blind ID exactly once")
+    rows = []
+    for blind, item_id in key.items():
+        lab = labels.get(blind) or {}
+        if lab.get("verdict") not in {"faithful", "minor_drift", "wrong", "not_formalizable"}:
+            raise ValueError(f"Missing or invalid verdict for {blind}")
+        row = results[item_id]
+        if row.get("errors") or "judge" not in row or "role" not in row:
+            raise ValueError(f"Unresolved detector failure for {blind}; no decision can be issued")
+        rows.append({**row, "blind": blind, "verdict": lab["verdict"],
+                     "human_errors": lab.get("errors", [])})
+    return rows
+
+
+def flags(row):
+    return {
+        "compile_only": not row["compiled"],
+        "lint": bool(row.get("lint")),
+        "role": bool(row.get("role", {}).get("flagged")),
+        "judge": (not row["judge"]["faithful"]) if "judge" in row else False,
+    }
+
+
+def report(rows, positive):
+    out = {}
+    for name in ("compile_only", "lint", "role", "judge"):
+        out[name] = confusion([flags(r)[name] for r in rows], [positive(r) for r in rows]).as_dict()
+        out[name]["precision_ci"] = wilson(out[name]["tp"], out[name]["tp"] + out[name]["fp"])
+    out["role"]["auc_score"] = auc([-(r.get("role", {}).get("score", 1.0)) for r in rows],
+                                   [positive(r) for r in rows])
+    out["role"]["complementary_wrong"] = sum(
+        positive(r) and flags(r)["role"] and not flags(r)["judge"] for r in rows
+    )
+    return out
+
+
+def decide(sub):
+    role, judge = sub["role"], sub["judge"]
+    if role["tp"] + role["fn"] == 0 or role["fp"] + role["tn"] == 0:
+        return "INSUFFICIENT: both wrong and faithful items are required"
+    go = (role["recall"] >= 0.5 and role["false_flag_rate"] <= 0.2
+          and role["recall"] >= judge["recall"] + 0.10
+          and role["false_flag_rate"] <= judge["false_flag_rate"])
+    partial = ((role["recall"] >= 0.4 and role["false_flag_rate"] <= 0.3)
+               or role.get("complementary_wrong", 0) >= 3)
+    return "GO" if go else "PARTIAL" if partial else "NO-GO"
+
+
+def main() -> int:
+    ap = argparse.ArgumentParser(description=__doc__.splitlines()[0])
+    ap.add_argument("--results", required=True, type=Path)
+    ap.add_argument("--labels", required=True, type=Path)
+    ap.add_argument("--key", required=True, type=Path)
+    ap.add_argument("--summary", type=Path, default=None,
+                    help="also write the (text-free) summary here, e.g. results/summary.json")
+    args = ap.parse_args()
+    meta = json.loads(args.results.with_suffix(".meta.json").read_text(encoding="utf-8"))
+    if (meta.get("status") != "complete"
+            or meta.get("labels_sha256") != hashlib.sha256(args.labels.read_bytes()).hexdigest()
+            or meta.get("results_sha256") != hashlib.sha256(args.results.read_bytes()).hexdigest()):
+        ap.error("Scoring requires a complete run with unchanged frozen labels and results")
+    all_rows = load(args)
+    rows = [r for r in all_rows if r["verdict"] != "not_formalizable"]
+    primary = [r for r in rows if r["verdict"] != "minor_drift"]
+    compiled = [r for r in primary if r["compiled"]]
+    summary = {
+        "run_metadata": meta,
+        "n_labeled": len(all_rows), "n_evaluable": len(rows), "n_primary": len(primary),
+        "n_compiled": len(compiled),
+        "verdicts": {v: sum(r["verdict"] == v for r in rows) for v in
+                     ("faithful", "minor_drift", "wrong", "not_formalizable")},
+        "compiled_but_wrong": sum(r["verdict"] == "wrong" for r in compiled),
+        "primary_all": report(primary, lambda r: r["verdict"] == "wrong"),
+        "secondary_all": report(rows, lambda r: r["verdict"] in ("wrong", "minor_drift")),
+        "compiled_only": report(compiled, lambda r: r["verdict"] == "wrong"),
+    }
+    summary["verdicts"]["not_formalizable"] = len(all_rows) - len(rows)
+    summary["role_recall_by_error"] = {
+        error: {"flagged": sum(flags(r)["role"] for r in rows
+                                if r["verdict"] == "wrong" and error in r["human_errors"]),
+                "total": sum(r["verdict"] == "wrong" and error in r["human_errors"] for r in rows)}
+        for error in sorted({e for r in rows for e in r["human_errors"]})
+    }
+    summary["degenerate_projection"] = {
+        "total": sum(bool(r.get("projection", {}).get("degenerate")) for r in all_rows),
+        "wrong": sum(r["verdict"] == "wrong" and bool(r.get("projection", {}).get("degenerate"))
+                     for r in all_rows),
+    }
+    summary["disagreements"] = [
+        {"blind": r["blind"], "verdict": r["verdict"], "flags": flags(r)}
+        for r in primary if any(f != (r["verdict"] == "wrong") for f in flags(r).values())
+    ]
+    summary["decision"] = decide(summary["primary_all"])
+    def finite_json(value):
+        if isinstance(value, dict):
+            return {k: finite_json(v) for k, v in value.items()}
+        if isinstance(value, (list, tuple)):
+            return [finite_json(v) for v in value]
+        return None if isinstance(value, float) and not math.isfinite(value) else value
+
+    text = json.dumps(finite_json(summary), indent=2, allow_nan=False)
+    if args.summary:
+        args.summary.parent.mkdir(parents=True, exist_ok=True)
+        args.summary.write_text(text + "\n", encoding="utf-8")
+    print(text)
+    return 0
+
+
+if __name__ == "__main__":
+    raise SystemExit(main())

experiments/pilot/README.md

@@ -1,15 +0,0 @@
-# Pilot (Phase 0)
-
-Question: on the 65 existing items, does role alignment (passage simplex vs. Lean simplex) find
-unfaithful formalizations better than a single LLM judge, compile-only, or static lint?
-Full protocol and decision rule: `docs/experiments/PROTOCOL.md`.
-
-    python experiments/pilot/make_sheet.py --items runs/p85-110/items.jsonl --out runs/pilot/private
-    # a person opens runs/pilot/private/labelsheet.html, labels all items, saves labels.json
-    python experiments/pilot/run_pilot.py --items runs/p85-110/items.jsonl --out runs/pilot/results.jsonl --dry-run
-    python experiments/pilot/run_pilot.py --items runs/p85-110/items.jsonl --out runs/pilot/results.jsonl
-    python experiments/pilot/score.py --results runs/pilot/results.jsonl \
-        --labels runs/pilot/private/labels.json --key runs/pilot/private/key.json
-
-`runs/` and `**/private/` are gitignored: the passages come from a copyrighted book and must not be
-committed. Labeling must finish BEFORE `score.py` is run; do not look at `results.jsonl` while labeling.

experiments/pilot/run_pilot.py

@@ -1,110 +0,0 @@
-"""Run the pilot detectors over the pilot items. Resumable; one JSON line per item.
-
-    python experiments/pilot/run_pilot.py --items runs/p85-110/items.jsonl \
-        --out runs/pilot/results.jsonl --dry-run          # no API calls: shows the plan
-    python experiments/pilot/run_pilot.py --items ... --out ... --max-calls 400
-
-Detectors (all see the passage and/or the Lean code, never the human labels):
-  lint    static patterns on the projected simplex          (no LLM)
-  role    source-side simplex (LLM sees only the passage) aligned to the Lean simplex
-  judge   one LLM call that sees passage + Lean and says faithful / not
-  compile the stored Lean verdict (``verified``), read from the items file
-
-Hard stops: --max-calls bounds API calls; a rerun skips items already in --out.
-"""
-from __future__ import annotations
-
-import argparse
-import hashlib
-import json
-import sys
-from pathlib import Path
-
-from leanbench import srcsimplex
-from leanbench.align import align
-from leanbench.config import Settings
-from leanbench.lint import lint
-from leanbench.llm import OpenAICompatibleClient
-from leanbench.project import project
-
-JUDGE_PROMPT_VERSION = "judge-v1"
-JUDGE_SYSTEM = (
-    "You check a Lean 4 (Mathlib) formalization against a textbook passage. Decide whether the "
-    "Lean statement says what the passage says: same objects, same hypotheses, same conclusion, "
-    "same quantifiers. Ignore whether it compiles. Reply with JSON only: "
-    '{"faithful": true|false, "confidence": 0..1, "reason": "one sentence"}'
-)
-
-
-def judge(client, passage: str, lean: str) -> dict:
-    reply = client.complete_json([
-        {"role": "system", "content": JUDGE_SYSTEM},
-        {"role": "user", "content": f"Passage:\n{passage}\n\nLean:\n{lean}"},
-    ])
-    if not isinstance(reply, dict) or "faithful" not in reply:
-        raise ValueError(f"unusable judge reply: {str(reply)[:200]}")
-    return {"faithful": bool(reply["faithful"]), "confidence": reply.get("confidence"),
-            "reason": str(reply.get("reason", ""))[:300]}
-
-
-def run_item(client, item: dict) -> dict:
-    code = item.get("lean_code") or ""
-    row: dict = {"id": item["id"], "compiled": bool(item.get("verified")), "errors": {}}
-    proj = project(code)
-    row["projection"] = proj.as_dict()
-    row["lint"] = lint(proj)
-    try:
-        src = srcsimplex.extract_source_simplex(client, item.get("source_text", ""),
-                                                item.get("label", ""))
-        al = align(src, proj)
-        row["source"] = [r.__dict__ for r in src.roles]
-        row["role"] = al.as_dict()
-    except Exception as error:  # a failed extraction is data, not a crash
-        row["errors"]["role"] = str(error)[:300]
-    try:
-        row["judge"] = judge(client, item.get("source_text", ""), code)
-    except Exception as error:
-        row["errors"]["judge"] = str(error)[:300]
-    return row
-
-
-def main() -> int:
-    ap = argparse.ArgumentParser(description=__doc__.splitlines()[0])
-    ap.add_argument("--items", required=True, type=Path)
-    ap.add_argument("--out", required=True, type=Path)
-    ap.add_argument("--max-calls", type=int, default=400)
-    ap.add_argument("--dry-run", action="store_true")
-    args = ap.parse_args()
-
-    items = [json.loads(x) for x in args.items.read_text(encoding="utf-8").splitlines() if x.strip()]
-    done = set()
-    if args.out.exists():
-        done = {json.loads(x)["id"] for x in args.out.read_text(encoding="utf-8").splitlines() if x.strip()}
-    todo = [i for i in items if i["id"] not in done]
-    settings = Settings.from_env()
-    est = len(todo) * 3  # extract (<=2 tries) + judge
-    print(f"items={len(items)} done={len(done)} todo={len(todo)} model={settings.llm.model} "
-          f"est_calls<={est} (extract x2 + judge) cap={args.max_calls}")
-    print("prompts:", srcsimplex.PROMPT_VERSION, JUDGE_PROMPT_VERSION,
-          hashlib.sha256((srcsimplex.SYSTEM_PROMPT + JUDGE_SYSTEM).encode()).hexdigest()[:12])
-    if args.dry_run:
-        return 0
-
-    client = OpenAICompatibleClient.from_settings(settings.llm)
-    args.out.parent.mkdir(parents=True, exist_ok=True)
-    with args.out.open("a", encoding="utf-8") as fh:
-        for item in todo:
-            if client.usage.calls >= args.max_calls:
-                print("call cap reached; rerun to resume", file=sys.stderr)
-                break
-            fh.write(json.dumps(run_item(client, item), ensure_ascii=False) + "\n")
-            fh.flush()
-    meta = {"model": settings.llm.model, "usage": client.usage.as_dict(),
-            "prompts": [srcsimplex.PROMPT_VERSION, JUDGE_PROMPT_VERSION]}
-    (args.out.parent / "run_meta.json").write_text(json.dumps(meta, indent=2), encoding="utf-8")
-    print(json.dumps(meta))
-    return 0
-
-
-if __name__ == "__main__":
-    raise SystemExit(main())

experiments/pilot/score.py

@@ -1,93 +0,0 @@
-"""Score the pilot: detectors vs. the blind human labels, with the pre-registered decision.
-
-    python experiments/pilot/score.py --results runs/pilot/results.jsonl \
-        --labels runs/pilot/private/labels.json --key runs/pilot/private/key.json
-
-Positive class = unfaithful. Primary: verdict == "wrong", over ALL labeled items (role alignment and
-the judge do not need Lean to accept the code; only 10 of the 65 pilot items compiled, too few to
-decide on). Secondary: wrong or minor_drift; and the compiled-only subset (the paper's claim, reported
-with its interval, not used to decide). "not_formalizable" items are excluded. Decision (fixed before
-looking at labels):
-
-  GO       role recall on wrong items >= 0.5 AND false-flag rate on faithful items <= 0.2
-           AND role recall >= judge recall + 0.10 at a false-flag rate no higher than the judge's
-  PARTIAL  role recall >= 0.4 with false-flag <= 0.3, or role complements the judge
-           (flags >= 3 wrong items the judge misses)
-  NO-GO    otherwise (re-scope to evaluation + taxonomy + resource)
-With ~65 items every number carries a wide Wilson interval; the pilot checks for signal, not effect size.
-"""
-from __future__ import annotations
-
-import argparse
-import json
-from pathlib import Path
-
-from leanbench.evalstats import auc, confusion
-
-
-def load(args):
-    results = {json.loads(x)["id"]: json.loads(x) for x in args.results.read_text(encoding="utf-8").splitlines() if x.strip()}
-    labels = json.loads(args.labels.read_text(encoding="utf-8"))["labels"]
-    key = json.loads(args.key.read_text(encoding="utf-8"))["key"]
-    rows = []
-    for blind, item_id in key.items():
-        lab = labels.get(blind) or {}
-        if item_id in results and lab.get("verdict"):
-            rows.append({**results[item_id], "blind": blind, "verdict": lab["verdict"],
-                         "human_errors": lab.get("errors", [])})
-    return rows
-
-
-def flags(row):
-    return {
-        "compile_only": not row["compiled"],
-        "lint": bool(row.get("lint")),
-        "role": bool(row.get("role", {}).get("flagged")),
-        "judge": (not row["judge"]["faithful"]) if "judge" in row else False,
-    }
-
-
-def report(rows, positive):
-    out = {}
-    for name in ("compile_only", "lint", "role", "judge"):
-        out[name] = confusion([flags(r)[name] for r in rows], [positive(r) for r in rows]).as_dict()
-    out["role"]["auc_score"] = auc([-(r.get("role", {}).get("score", 1.0)) for r in rows],
-                                   [positive(r) for r in rows])
-    return out
-
-
-def decide(sub):
-    role, judge = sub["role"], sub["judge"]
-    if role["tp"] + role["fn"] == 0:
-        return "INSUFFICIENT: no wrong items in the labels"
-    go = (role["recall"] >= 0.5 and role["false_flag_rate"] <= 0.2
-          and role["recall"] >= judge["recall"] + 0.10
-          and role["false_flag_rate"] <= judge["false_flag_rate"])
-    partial = (role["recall"] >= 0.4 and role["false_flag_rate"] <= 0.3)
-    return "GO" if go else "PARTIAL" if partial else "NO-GO"
-
-
-def main() -> int:
-    ap = argparse.ArgumentParser(description=__doc__.splitlines()[0])
-    ap.add_argument("--results", required=True, type=Path)
-    ap.add_argument("--labels", required=True, type=Path)
-    ap.add_argument("--key", required=True, type=Path)
-    args = ap.parse_args()
-    rows = [r for r in load(args) if r["verdict"] != "not_formalizable"]
-    compiled = [r for r in rows if r["compiled"]]
-    summary = {
-        "n_labeled": len(rows), "n_compiled": len(compiled),
-        "verdicts": {v: sum(r["verdict"] == v for r in rows) for v in
-                     ("faithful", "minor_drift", "wrong")},
-        "compiled_but_wrong": sum(r["verdict"] == "wrong" for r in compiled),
-        "primary_all": report(rows, lambda r: r["verdict"] == "wrong"),
-        "secondary_all": report(rows, lambda r: r["verdict"] in ("wrong", "minor_drift")),
-        "compiled_only": report(compiled, lambda r: r["verdict"] == "wrong"),
-    }
-    summary["decision"] = decide(summary["primary_all"])
-    print(json.dumps(summary, indent=2, default=str))
-    return 0
-
-
-if __name__ == "__main__":
-    raise SystemExit(main())

leanbench/llm.py

@@ -14,7 +14,7 @@ import re
 import time
 import urllib.error
 import urllib.request
-from collections.abc import Iterable
+from collections.abc import Callable, Iterable
 from dataclasses import dataclass, field
 from typing import Any, Protocol
 
@@ -66,6 +66,7 @@ class OpenAICompatibleClient:
     max_retries: int = 4
     temperature: float = 0.0
     usage: Usage = field(default_factory=Usage)
+    request_guard: Callable[[], None] | None = field(default=None, repr=False)
 
     @classmethod
     def from_settings(cls, settings: LLMSettings) -> OpenAICompatibleClient:
@@ -97,6 +98,8 @@ class OpenAICompatibleClient:
         }
         last: Exception | None = None
         for attempt in range(self.max_retries + 1):
+            if self.request_guard is not None:
+                self.request_guard()
             request = urllib.request.Request(url, data=body, headers=headers, method="POST")
             try:
                 with urllib.request.urlopen(request, timeout=self.timeout) as response:

tests/test_pilot_scripts.py

@@ -2,7 +2,7 @@
 import importlib.util
 from pathlib import Path
 
-ROOT = Path(__file__).resolve().parents[1] / "experiments" / "pilot"
+ROOT = Path(__file__).resolve().parents[1] / "experiments" / "P0-pilot"
 
 
 def load(name):
@@ -36,3 +36,187 @@ def test_run_item_and_score(tmp_path):
     out = sc.report(rows, lambda r: r["verdict"] == "wrong")
     assert out["judge"]["n"] == 4
     assert sc.decide(out) in {"GO", "PARTIAL", "NO-GO"}
+
+
+def test_complementary_signal_is_partial():
+    sc = load("score")
+    rows = [
+        {"compiled": True, "lint": [], "role": {"flagged": i < 3, "score": 0.1},
+         "judge": {"faithful": False if 3 <= i < 8 else True}, "verdict": "wrong"}
+        for i in range(10)
+    ] + [
+        {"compiled": True, "lint": [], "role": {"flagged": False, "score": 1},
+         "judge": {"faithful": True}, "verdict": "faithful"}
+    ]
+    summary = sc.report(rows, lambda row: row["verdict"] == "wrong")
+    assert summary["role"]["recall"] == 0.3
+    assert summary["role"]["complementary_wrong"] == 3
+    assert sc.decide(summary) == "PARTIAL"
+
+
+def test_score_rejects_missing_labels_and_detector_failures(tmp_path):
+    import argparse
+    import json
+
+    import pytest
+
+    sc = load("score")
+    args = argparse.Namespace(results=tmp_path / "results.jsonl", labels=tmp_path / "labels.json",
+                              key=tmp_path / "key.json")
+    args.key.write_text(json.dumps({"key": {"P01": "x1"}}))
+    args.labels.write_text(json.dumps({"labels": {"P01": {"verdict": None}}}))
+    args.results.write_text(json.dumps({"id": "x1"}) + "\n")
+    with pytest.raises(ValueError, match="verdict"):
+        sc.load(args)
+    args.labels.write_text(json.dumps({"labels": {"P01": {"verdict": "wrong"}}}))
+    with pytest.raises(ValueError, match="detector failure"):
+        sc.load(args)
+    args.results.write_text("")
+    with pytest.raises(ValueError, match="every keyed item"):
+        sc.load(args)
+
+
+def test_request_budget_survives_resume_and_transport_retries(tmp_path, monkeypatch):
+    import argparse
+    import json
+    import urllib.error
+
+    import pytest
+
+    from leanbench.config import Settings
+
+    rp = load("run_pilot")
+    args = argparse.Namespace(items=tmp_path / "items.jsonl", out=tmp_path / "results.jsonl",
+                              max_calls=2, dry_run=False)
+    args.items.write_text(json.dumps(ITEM) + "\n")
+    monkeypatch.setenv("DASHSCOPE_API_KEY", "test-only")
+    settings = Settings()
+    settings.llm.max_retries = 5
+    requests = []
+
+    def fail(*args, **kwargs):
+        requests.append(1)
+        raise urllib.error.URLError("offline test")
+
+    monkeypatch.setattr("urllib.request.urlopen", fail)
+    monkeypatch.setattr("leanbench.llm.time.sleep", lambda *_: None)
+    assert rp.execute(args, [ITEM], settings) == 2
+    assert len(requests) == 2
+    assert rp.execute(args, [ITEM], settings) == 2
+    assert len(requests) == 2
+    meta = json.loads(args.out.with_suffix(".meta.json").read_text())
+    assert meta["request_attempts"] == 2
+    assert len(meta["prompt_hashes"]["judge"]) == 64
+    assert meta["status"] == "budget_exhausted"
+    settings.llm.model = "other-model"
+    with pytest.raises(ValueError, match="identity changed"):
+        rp.execute(args, [ITEM], settings)
+
+
+def test_run_rejects_missing_source_passage():
+    import pytest
+
+    rp = load("run_pilot")
+    with pytest.raises(ValueError, match="Missing source_text"):
+        rp.run_item(Stub(), {**ITEM, "source_text": ""})
+
+
+def test_restore_passages_checks_cohort_and_normalizes_archived_imports():
+    import pytest
+
+    prepare = load("prepare_items")
+    item = {"id": "x", "lean_code": "example : True := trivial", "imports": ["Mathlib"]}
+    original = {**item, "imports": '["Mathlib"]', "source_text": "A private passage."}
+    restored = prepare.restore([item], {"items": [original]})
+    assert restored == [{**item, "source_text": "A private passage."}]
+    with pytest.raises(ValueError, match="does not match"):
+        prepare.restore([{**item, "lean_code": "changed"}], {"items": [original]})
+
+
+def test_judge_rejects_string_boolean():
+    import pytest
+
+    from leanbench.llm import ScriptedClient
+
+    rp = load("run_pilot")
+    with pytest.raises(ValueError, match="unusable judge"):
+        rp.judge(ScriptedClient(['{"faithful": "false"}']), "passage", "code")
+
+
+def test_partial_resume_keeps_successful_detector_output():
+    rp = load("run_pilot")
+    row = rp.run_item(Stub(), ITEM)
+    expected_role = row["role"]
+    row.pop("judge")
+    row["errors"]["judge"] = "temporary failure"
+
+    class JudgeOnly:
+        calls = 0
+
+        def complete_json(self, messages):
+            self.calls += 1
+            assert "faithful" in messages[0]["content"]
+            return {"faithful": True}
+
+    client = JudgeOnly()
+    resumed = rp.run_item(client, ITEM, row)
+    assert client.calls == 1
+    assert resumed["role"] == expected_role
+    assert rp.complete_row(resumed)
+    assert row["errors"] == {"judge": "temporary failure"}
+
+
+def test_billing_failure_stops_before_next_detector():
+    import pytest
+
+    from leanbench.llm import LLMError
+
+    rp = load("run_pilot")
+
+    class Blocked:
+        calls = 0
+
+        def complete_json(self, messages):
+            self.calls += 1
+            raise LLMError("HTTP 400: Arrearage overdue-payment")
+
+    client = Blocked()
+    with pytest.raises(rp.ProviderBlocked) as caught:
+        rp.run_item(client, ITEM)
+    assert client.calls == 1
+    assert "role" in caught.value.row["errors"]
+    assert "judge" not in caught.value.row["errors"]
+
+
+def test_blocked_run_preserves_and_replaces_partial_row(tmp_path, monkeypatch):
+    import argparse
+    import json
+
+    from leanbench.config import Settings
+
+    rp = load("run_pilot")
+    args = argparse.Namespace(items=tmp_path / "items.jsonl", out=tmp_path / "results.jsonl",
+                              max_calls=400, dry_run=False)
+    args.items.write_text(json.dumps(ITEM) + "\n")
+    partial = {"id": "x1", "compiled": True, "role": {"flagged": False},
+               "errors": {"judge": "Arrearage"}}
+
+    def blocked(client, item, previous):
+        raise rp.ProviderBlocked(partial)
+
+    monkeypatch.setattr(rp, "run_item", blocked)
+    assert rp.execute(args, [ITEM], Settings()) == 2
+    meta = json.loads(args.out.with_suffix(".meta.json").read_text())
+    assert meta["status"] == "provider_blocked"
+    assert meta["completed_items"] == 0
+
+    def recover(client, item, previous):
+        assert previous["role"] == partial["role"]
+        return {**previous, "judge": {"faithful": True}, "errors": {}}
+
+    monkeypatch.setattr(rp, "run_item", recover)
+    assert rp.execute(args, [ITEM], Settings()) == 0
+    rows = [json.loads(line) for line in args.out.read_text().splitlines()]
+    assert len(rows) == 1 and rp.complete_row(rows[0])
+    meta = json.loads(args.out.with_suffix(".meta.json").read_text())
+    assert meta["completed_items"] == 1 and meta["status"] == "complete"