Experiment IDs and registry (P0, E0-E11); P0 layout; infrastructure notes #4
+6
-3
@@ -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/
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -1,11 +1,13 @@
|
||||
# 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; 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 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 +22,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 +62,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
|
||||
|
||||
@@ -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
|
||||
@@ -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.
|
||||
@@ -0,0 +1,31 @@
|
||||
# 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
|
||||
|
||||
cp runs/p85-110/items.jsonl 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
|
||||
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`.
|
||||
@@ -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"
|
||||
}
|
||||
}
|
||||
@@ -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,7 +147,8 @@ 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()
|
||||
|
||||
@@ -159,16 +161,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
|
||||
|
||||
|
||||
@@ -1,8 +1,8 @@
|
||||
"""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
|
||||
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)
|
||||
@@ -1,7 +1,7 @@
|
||||
"""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
|
||||
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: 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
|
||||
@@ -72,6 +72,8 @@ def main() -> int:
|
||||
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()
|
||||
rows = [r for r in load(args) if r["verdict"] != "not_formalizable"]
|
||||
compiled = [r for r in rows if r["compiled"]]
|
||||
@@ -85,7 +87,11 @@ def main() -> int:
|
||||
"compiled_only": report(compiled, lambda r: r["verdict"] == "wrong"),
|
||||
}
|
||||
summary["decision"] = decide(summary["primary_all"])
|
||||
print(json.dumps(summary, indent=2, default=str))
|
||||
text = json.dumps(summary, indent=2, default=str)
|
||||
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
|
||||
|
||||
|
||||
@@ -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.
|
||||
@@ -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):
|
||||
|
||||
Reference in New Issue
Block a user