lean-bench/docs/experiments/P0-pilot.md

P0: pilot protocol (v1)

Experiment ID P0, Phase 0. Registry and conventions: README.md.

Status: approved 2026-10-22; labels pending. No detector has been run and no API spend has occurred. 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 (approved by the owner on 2026-10-22)

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
0 Pilot	65 existing items: detectors vs. blind human labels	~200 calls (< 1M tokens) / 1 labeler, ~4 h	2 days	Section 3 rule
1 Calibration	6-8 books ingested, 150-page detection gold, labeling guideline, kappa pilot on 50 items	~10-20M tokens / 2 annotators, ~15 h each	2 weeks	kappa >= 0.6
2 Main	E4 (4+ models), E5 (600 labeled), E6 (filter comparison), E7, E8	~135M tokens + judges / 2 annotators, ~60 h total	3-4 weeks	go/no-go on 8 Dec
3 Extras	E9 retrieval/proving, E10-E11, robustness	open, bounded by time left	to 24 Dec	tables frozen 24 Dec

Token and CPU figures are the plan's rough estimates (research-plan.md 7.9); they are recomputed from the Phase 0 numbers before Phase 1.

2. Hypotheses tested in Phase 0

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

Detectors, all run on the same 65 items:

Detector	Sees	Cost
compile-only	Lean verdict stored in the items file	0
static lint	Lean code (projected simplex)	0
single LLM judge	passage + Lean code, one call	65 calls
role alignment	passage -> source simplex (LLM, never sees Lean); Lean -> simplex (deterministic); deterministic alignment	<= 130 calls

Model: qwen-max via DashScope (the only key available). Temperature 0. Prompts are versioned and hashed in the run metadata (srcsimplex-v1, judge-v1). The judge and the source extractor are the same model family, which is a known confound and is listed as a limitation; Phase 2 adds a second family.

Metrics. Positive class = "wrong". For each detector: recall, precision, false-flag rate on faithful items, F1, Wilson 95% intervals; role-alignment score AUC. Secondary: positive = wrong or minor drift. Per-error-type recall for role alignment. Reported alongside: share of items degenerate in the projection (closed statements with no binders project to one role; 15 of 65 here, and several of those are also wrong formalizations, e.g. IsGroup, a name that does not exist).

Decision rule (fixed now, before any label exists).

• GO: role recall on wrong items >= 0.5, false-flag rate on faithful items <= 0.2, role recall >= judge recall + 0.10, and role false-flag rate no higher than the judge's.
• PARTIAL: role recall >= 0.4 with false-flag rate <= 0.3, or role alignment flags at least 3 wrong items the judge misses (complementary signal).
• NO-GO: otherwise. Then the paper is re-scoped to evaluation + taxonomy + resource (Findings-level), and I tell you before spending anything else.

With about 65 items every interval is wide (a recall of 0.5 on 20 wrong items has a 95% interval of roughly 0.30-0.70). The pilot can reject an idea with no signal; it cannot confirm effect size. I will say so in the report and will not present a GO as a result for the paper.

What I will not do. Tune thresholds (0.3, 0.2), the concept table, or the prompts after seeing labels or detector output on these 65 items; if any change is needed it is recorded as a new version and rerun on a fresh sample in Phase 1. No cherry-picking of items. Every run writes its model id, prompt hashes, call counts and token usage next to its results.

4. Phase 1-3 outline (not requested yet)

• Phase 1. Pick and license-check 6-8 books (>= 3 open); ingest to >= 1,500 items; sample 150 pages (detection gold), 600 items (audited core), 150 passages (gold source simplices); annotation guideline v1 with 30 worked examples; two annotators label 50 items; gate kappa >= 0.6. Also E0 (projection vs. manual parse on >= 100 signatures, gate >= 95%).
• Phase 2. E4 gap across >= 4 general models + 1 specialised formalizer (paired McNemar, bootstrap CIs); E5 labels for the 600-item core (kappa on a 200-item overlap, third adjudicator); E6 filter comparison against single judge, two-judge, BEq+, static checkers, CriticLean/FormalAlign, trajectory length, with shuffled-span and same-family-judge controls; E7 slot-constrained vs. free-form; E8 repair ablation. Go/no-go on 8 Dec: role alignment must beat a single judge on at least two error types at equal false-reject rate to stay a headline contribution.
• Phase 3. E9 schema-guided retrieval/proving (only if schedule holds), E10 contamination, E11 cost/time; tables frozen 24 Dec; writing from 1 Dec; submit by 3 Jan.

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

Risk	Effect	Mitigation
Single model family for extractor and judge	Judge and role alignment errors correlate; bias favors neither fairly	Disclosed; second family in Phase 2
One labeler	No agreement estimate; label noise unknown	Phase 1 two-annotator kappa; pilot reported as signal-only
Closed statements project to one role	Role alignment has little to compare	Counted and reported; degenerate flag treated as its own detector output
65 items from one chapter span	Narrow topics, small n	Pilot only gates a decision; Phase 1 widens
Competing 2026 papers (Beyond Compilation, ShadowBench, Lean-GAP, ATLAS)	Novelty narrows	Position as role-level structural fidelity; weekly literature check
11 weeks to deadline	Slippage in annotation	Fixed gates; fallback to evaluation + resource paper

7. What I need from you

1. Approve Phase 0, or tell me what to change.
2. A labeler for the 65 items (about 4 hours; Lean-literate). If it is you, say so and I will hand you labelsheet.html. I will not label them myself, because I produced the code being judged and the detectors share my model's blind spots.
3. For Phase 1 (not yet): a second annotator, a second model key (a different family from Qwen, for the judge control), and your choice of books once I have the license shortlist.

8. After approval

I run, in order: build the sheet; (you label); dry-run to confirm counts; run detectors (<= 400 calls hard cap, resumable); score; report the decision with the numbers, the failures, and the items where detectors disagree with you. Then I stop and wait for your go on Phase 1.