"""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
Writes, into a directory that must stay local (it contains passages from a
copyrighted book; ``runs/`` and ``**/private/`` are gitignored):
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)
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''
for key, name, _ in FIDELITY
)
errors = "".join(
f''
for key, name in ERRORS
)
label = esc(item.get("label") or "")
return (
f''
f'{blind}· page {item.get("start_page")} · '
f'{esc(item.get("kind", ""))} · {label}'
f'
Passage
'
f'
{esc(item.get("source_text", ""))}
'
f'
Lean
{esc(item.get("lean_code", ""))}
'
f'
Verdict{verdicts}
'
f'
Errors(if not faithful){errors}
'
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)
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))
args.out.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(
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")
return 0
if __name__ == "__main__":
raise SystemExit(main())