"""Build the blind labeling sheet for the pilot. 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: /labelsheet.html open in a browser; label every item; press "Download labels.json". Contains passages from a copyrighted book, so ``data/`` is gitignored. /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 everything being evaluated. Order is shuffled with --seed. """ from __future__ import annotations import argparse import html import json import random from pathlib import Path FIDELITY = [ ("faithful", "Faithful", "Says what the passage says (notation and encoding choices aside)."), ("minor_drift", "Minor drift", "Right idea, but a small difference a careful reader would object to."), ("wrong", "Wrong", "States a different or false/vacuous claim, or drops/adds a " "hypothesis that changes the meaning."), ("not_formalizable", "Not formalizable / no claim", "The passage is not a precise statement, or the extraction is garbled."), ] ERRORS = [ ("missing_hypothesis", "Missing hypothesis"), ("extra_hypothesis", "Extra hypothesis"), ("wrong_type", "Wrong type / structure (e.g. ℕ for ℤ, Group for CommGroup)"), ("quantifier", "Quantifier error (∀/∃, order)"), ("wrong_conclusion", "Wrong conclusion"), ("degenerate", "Vacuous / trivial / degenerate"), ("hallucinated_api", "Names that do not exist in Mathlib"), ("other", "Other (say in notes)"), ] PAGE = """ lean-bench pilot labeling sheet

lean-bench pilot: label {n} items

For each item: if this Lean code compiled, would it state what the passage states? Judge the meaning of what is written, not whether Lean accepts it (that is hidden on purpose). Notation and harmless encoding choices are fine. Tick the error types that apply when the verdict is not "Faithful". Your answers are saved in this browser as you go; press Download labels.json when finished and put the file next to key.json.

Verdicts

{legend}

{cards}

""" def esc(text: str) -> str: return html.escape(text or "", quote=True) def card(blind: str, item: dict) -> str: verdicts = "".join( f' {esc(name)}' for key, name, _ in FIDELITY ) errors = "".join( f' {esc(name)}' for key, name in ERRORS ) label = esc(item.get("label") or "") return ( f'' ) 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, 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() items = [json.loads(line) for line in args.items.read_text(encoding="utf-8").splitlines() if line.strip()] order = list(range(len(items))) random.Random(args.seed).shuffle(order) blind_ids = [f"P{n:02d}" for n in range(1, len(items) + 1)] key = {blind_ids[pos]: items[idx]["id"] for pos, idx in enumerate(order)} legend = "".join(f"

{esc(n)}: {esc(d)}

" 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", ) (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_dir/'key.json'}") return 0 if __name__ == "__main__": raise SystemExit(main())