claude-bot
2b255a333a
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
62 lines
4.5 KiB
Markdown
62 lines
4.5 KiB
Markdown
# 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
|