lean-bench/experiments/pilot/make_sheet.py

"""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 = """<!doctype html>
<html lang="en"><head><meta charset="utf-8"><meta name="viewport" content="width=device-width">
<title>lean-bench pilot labeling sheet</title>
<style>
:root {{ --bg:#fff; --fg:#1b1f24; --mute:#59636e; --line:#d0d7de; --card:#f6f8fa; --accent:#0969da; }}
@media (prefers-color-scheme: dark) {{ :root {{ --bg:#0d1117; --fg:#e6edf3; --mute:#9198a1;
  --line:#30363d; --card:#161b22; --accent:#4493f8; }} }}
body {{ margin:0; background:var(--bg); color:var(--fg); font:15px/1.5 system-ui,sans-serif; }}
main {{ max-width:980px; margin:0 auto; padding:16px; }}
h1 {{ font-size:20px; }} .mute {{ color:var(--mute); }}
.card {{ background:var(--card); border:1px solid var(--line); border-radius:8px;
  padding:12px 14px; margin:14px 0; }}
.card.done {{ border-left:4px solid var(--accent); }}
pre {{ white-space:pre-wrap; word-break:break-word; margin:6px 0; padding:8px;
  background:var(--bg); border:1px solid var(--line); border-radius:6px;
  font:13px/1.45 ui-monospace,monospace; }}
label {{ display:block; margin:2px 0; }} .row {{ display:flex; gap:24px; flex-wrap:wrap; }}
.row > div {{ flex:1 1 300px; }} textarea {{ width:100%; box-sizing:border-box; }}
button {{ font:inherit; padding:6px 12px; border:1px solid var(--line); border-radius:6px;
  background:var(--card); color:var(--fg); cursor:pointer; }}
#bar {{ position:sticky; top:0; background:var(--bg); padding:8px 0; border-bottom:1px solid var(--line);
  display:flex; gap:12px; align-items:center; z-index:2; }}
</style></head><body><main>
<h1>lean-bench pilot: label {n} items</h1>
<p class="mute">For each item: <b>if this Lean code compiled, would it state what the passage
states?</b> 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 <b>Download labels.json</b> when finished and put the file next to key.json.</p>
<div class="card"><b>Verdicts</b><ul>{legend}</ul></div>
<div id="bar"><span id="count"></span><button onclick="download()">Download labels.json</button></div>
{cards}
<script>
const IDS = {ids};
const STORE = "leanbench-pilot-labels-v1";
let labels = {{}};
try {{ labels = JSON.parse(localStorage.getItem(STORE) || "{{}}"); }} catch (e) {{ labels = {{}}; }}
function save() {{ try {{ localStorage.setItem(STORE, JSON.stringify(labels)); }} catch (e) {{}} }}
function read(id) {{
  const card = document.getElementById(id);
  const verdict = card.querySelector('input[name="v_' + id + '"]:checked');
  const errors = [...card.querySelectorAll('input[name="e_' + id + '"]:checked')].map(x => x.value);
  const notes = card.querySelector("textarea").value;
  labels[id] = {{ verdict: verdict ? verdict.value : null, errors: errors, notes: notes }};
  card.classList.toggle("done", !!verdict);
  save(); count();
}}
function count() {{
  const done = IDS.filter(i => labels[i] && labels[i].verdict).length;
  document.getElementById("count").textContent = done + " / " + IDS.length + " labeled";
}}
function restore() {{
  for (const id of IDS) {{
    const l = labels[id]; if (!l) continue;
    const card = document.getElementById(id);
    if (l.verdict) {{ const r = card.querySelector('input[name="v_' + id + '"][value="' + l.verdict + '"]');
      if (r) r.checked = true; card.classList.add("done"); }}
    for (const e of l.errors || []) {{ const c = card.querySelector('input[name="e_' + id + '"][value="' + e + '"]');
      if (c) c.checked = true; }}
    card.querySelector("textarea").value = l.notes || "";
  }}
  count();
}}
function download() {{
  IDS.forEach(i => {{ if (!labels[i]) labels[i] = {{ verdict: null, errors: [], notes: "" }}; }});
  const blob = new Blob([JSON.stringify({{ labeler: "", labels: labels }}, null, 2)], {{ type: "application/json" }});
  const a = document.createElement("a"); a.href = URL.createObjectURL(blob);
  a.download = "labels.json"; a.click();
}}
document.querySelectorAll(".card[id]").forEach(c => c.addEventListener("input", () => read(c.id)));
restore();
</script></main></body></html>
"""


def esc(text: str) -> str:
    return html.escape(text or "", quote=True)


def card(blind: str, item: dict) -> str:
    verdicts = "".join(
        f'<label><input type="radio" name="v_{blind}" value="{key}"> {esc(name)}</label>'
        for key, name, _ in FIDELITY
    )
    errors = "".join(
        f'<label><input type="checkbox" name="e_{blind}" value="{key}"> {esc(name)}</label>'
        for key, name in ERRORS
    )
    label = esc(item.get("label") or "")
    return (
        f'<section class="card" id="{blind}">'
        f'<b>{blind}</b> <span class="mute">· page {item.get("start_page")} · '
        f'{esc(item.get("kind", ""))} · {label}</span>'
        f'<div class="row"><div><div class="mute">Passage</div>'
        f'<pre>{esc(item.get("source_text", ""))}</pre></div>'
        f'<div><div class="mute">Lean</div><pre>{esc(item.get("lean_code", ""))}</pre></div></div>'
        f'<div class="row"><div><b>Verdict</b>{verdicts}</div>'
        f'<div><b>Errors</b> <span class="mute">(if not faithful)</span>{errors}</div></div>'
        f'<textarea rows="2" placeholder="notes (optional)"></textarea></section>'
    )


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"<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))
    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())