# 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