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 | 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 fulldocs/TODO.md: task list to 3 Jan 2027docs/acl-2027-bar.md: how the paper reaches the venue's bardocs/infrastructure/runner-lean435.md: CI runner, Lean/Mathlib environment, images