Files
lean-bench/tests/test_pilot_scripts.py
claude-bot 2b255a333a
ci / python (pull_request) Successful in 16s
ci / lean (pull_request) Successful in 1m15s
ci / image (pull_request) Has been skipped
Give experiments IDs (P0, E0-E11): registry, per-experiment layout, spec moved to docs/experiments/P0-pilot.md
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
2026-10-22 11:46:59 +00:00

39 lines
1.6 KiB
Python

"""Offline smoke test of the pilot scripts with a stub model (no network)."""
import importlib.util
from pathlib import Path
ROOT = Path(__file__).resolve().parents[1] / "experiments" / "P0-pilot"
def load(name):
spec = importlib.util.spec_from_file_location(name, ROOT / f"{name}.py")
mod = importlib.util.module_from_spec(spec)
spec.loader.exec_module(mod)
return mod
class Stub:
def complete_json(self, messages, **kw):
if "roles" in messages[0]["content"] or "passage" in messages[0]["content"].lower() and "faithful" not in messages[0]["content"]:
return {"roles": [
{"kind": "object", "symbols": ["G"], "description": "finite group", "keywords": ["group", "finite"]},
{"kind": "goal", "symbols": [], "description": "g^n = e", "keywords": ["identity"]},
]}
return {"faithful": True, "confidence": 0.9, "reason": "ok"}
ITEM = {"id": "x1", "source_text": "Let G be a finite group. Then g^n = e.", "label": "t",
"lean_code": "theorem t (G : Type*) [Group G] [Fintype G] (g : G) : g ^ Fintype.card G = 1 := sorry",
"verified": True}
def test_run_item_and_score(tmp_path):
rp, sc = load("run_pilot"), load("score")
row = rp.run_item(Stub(), ITEM)
assert row["id"] == "x1" and row["compiled"] and "judge" in row
assert set(sc.flags(row)) == {"compile_only", "lint", "role", "judge"}
rows = [dict(row, verdict=v) for v in ("wrong", "faithful", "faithful", "wrong")]
out = sc.report(rows, lambda r: r["verdict"] == "wrong")
assert out["judge"]["n"] == 4
assert sc.decide(out) in {"GO", "PARTIAL", "NO-GO"}