diff --git a/docs/experiments/P0-pilot.md b/docs/experiments/P0-pilot.md index d65a5b0..efc2b90 100644 --- a/docs/experiments/P0-pilot.md +++ b/docs/experiments/P0-pilot.md @@ -2,7 +2,18 @@ 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.** +Status: **approved 2026-10-22; 65 AI labels frozen 2026-10-28; detector execution pending explicit data-transfer approval. No pilot API request has been sent.** + +Owner amendment (2026-10-28, in the execution chat): Codex now handles preparation, +annotation, detector execution and reporting; Kimi's participation is no longer required. +The frozen labels are from one AI annotator, **not human ground truth**. The annotator saw +the detector implementation and aggregate compile counts before labeling, but did not see +per-item compiler outcomes or detector outputs. This departs from the original labeling plan; +any resulting decision is provisional and cannot substitute for an independent human audit. +Decision thresholds, detector prompts and the concept table remain fixed. Implementation +repairs before the first paid call restore the complementary-signal PARTIAL rule, exclude +minor drift from the primary wrong-versus-faithful comparison, enforce the cumulative HTTP +request budget, and persist run identity and usage. See `experiments/P0-pilot/README.md`. 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 (approved by the owner on 2026-10-22) diff --git a/experiments/P0-pilot/README.md b/experiments/P0-pilot/README.md index d752f7b..b302b47 100644 --- a/experiments/P0-pilot/README.md +++ b/experiments/P0-pilot/README.md @@ -16,16 +16,39 @@ unfaithful formalizations better than a single LLM judge, compile-only, or stati ## Steps - cp runs/p85-110/items.jsonl experiments/P0-pilot/data/items.jsonl + # Default exports omit source_text. Restore it from the matching private review. + python experiments/P0-pilot/prepare_items.py --items runs/p85-110/items.jsonl \ + --review runs/p85-110/review.json --out 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 + --out experiments/P0-pilot/data/results.jsonl --labels experiments/P0-pilot/labels/labels.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 Labeling must be finished before anyone opens `results.jsonl`. + +## Execution safeguards + +- Every item must have a nonempty source passage. `prepare_items.py` restores passages only + when all exported fields match the archived review; the exported cohort and Lean code stay intact. +- Freeze all labels before the paid run. The owner changed the labeler to the Codex assistant + on 2026-10-28. These are **AI labels, not human gold**; see the metadata in `labels/labels.json`. +- `--max-calls` counts actual HTTP attempts, including transport and JSON retries, cumulatively + across resumes. The hard ceiling is 400. A reservation is saved before each request; an interrupted + request may consume a reservation without a known response or token count. +- Metadata is stored beside the output as `results.meta.json`. Model, endpoint, temperature, + input hash, frozen-label hash and prompt hashes must match on resume. Usage is cumulative. + A file lock prevents concurrent writers. A budget stop returns exit status 2. +- The nominal successful path uses 130 calls (one source extraction and one judge per item); + malformed replies and network retries may increase the actual count. +- Scoring requires complete labels and results and no unresolved detector errors. The primary + comparison is wrong versus faithful; minor drift is included as positive in the secondary analysis. + The complementary-signal PARTIAL rule counts wrong items flagged by role alignment but missed + by the judge. No threshold, concept table or detector prompt was tuned for these labels. +- Raw passages, labeling HTML and model responses remain in the ignored `data/` directory. + Only verdicts, abstract annotation notes, hashes and text-free summaries belong in Git. diff --git a/experiments/P0-pilot/labels/labels.json b/experiments/P0-pilot/labels/labels.json new file mode 100644 index 0000000..5b687da --- /dev/null +++ b/experiments/P0-pilot/labels/labels.json @@ -0,0 +1,427 @@ +{ + "labeler": "Codex AI assistant (this chat; exact deployed model identifier unavailable)", + "labeler_type": "AI; not human gold", + "frozen_at": "2026-10-28T10:42:10.032234+00:00", + "items_sha256": "487ecd22919a5e3b0174a2846ab8fe7c0daf4d3feccccf8ea6571aec04c41bed", + "key_sha256": "f827cac92ee4e907554fadcc7c0e006ef2b829350f74e7f8b54ca11945e62836", + "method": "Single-pass semantic annotation in shuffled blind-ID order; per-item compiler outcomes and detector outputs hidden. Pure syntax/proof defects are ignored when meaning is recoverable. No compiler/API-name audit. Full extracted-span coverage is assessed; unspecified design tasks or unresolved contextual references are not formalizable.", + "limitations": [ + "Single AI annotator; no human adjudication or inter-annotator agreement.", + "The annotator reviewed detector implementation and aggregate compilation counts before labeling; only per-item outputs were hidden.", + "AI labels replace the originally planned human/Kimi labels by explicit owner instruction in this chat; the original human-ground-truth protocol is therefore not fully satisfied." + ], + "labels": { + "P01": { + "verdict": "faithful", + "errors": [], + "notes": "The field axioms and nontriviality match the stated definition." + }, + "P02": { + "verdict": "faithful", + "errors": [], + "notes": "The whole carrier and identity singleton are the two specified subgroups; API spelling is not assessed." + }, + "P03": { + "verdict": "faithful", + "errors": [], + "notes": "Every integer unit is constrained to the two specified values." + }, + "P04": { + "verdict": "faithful", + "errors": [], + "notes": "Generated subgroup is equated with all integer powers; escaped notation is treated as a syntax defect." + }, + "P05": { + "verdict": "faithful", + "errors": [], + "notes": "Existence of a bijective multiplication-preserving map matches the definition." + }, + "P06": { + "verdict": "faithful", + "errors": [], + "notes": "The theorem statement gives exactly the inverse-of-product identity; proof validity is not assessed." + }, + "P07": { + "verdict": "wrong", + "errors": [ + "wrong_conclusion", + "degenerate" + ], + "notes": "Only already-assumed prime factors are asserted to exist; no recovery from the totient is specified." + }, + "P08": { + "verdict": "faithful", + "errors": [], + "notes": "Both identity preservation and inverse preservation are stated under a multiplicative equivalence." + }, + "P09": { + "verdict": "wrong", + "errors": [ + "wrong_type", + "wrong_conclusion" + ], + "notes": "The multiplicative ring carrier does not encode the additive cyclic group, and the second extracted exercise is omitted." + }, + "P10": { + "verdict": "faithful", + "errors": [], + "notes": "Both left and right equations have unique solutions." + }, + "P11": { + "verdict": "faithful", + "errors": [], + "notes": "The group cardinality is the exponent, with the correct identity and quantification." + }, + "P12": { + "verdict": "not_formalizable", + "errors": [ + "other" + ], + "notes": "The extracted design question provides no formal security or authentication specification for a fidelity comparison." + }, + "P13": { + "verdict": "minor_drift", + "errors": [ + "wrong_type" + ], + "notes": "The intended modular identity is retained, but the integer variable is supplied to a natural-number coprimality predicate." + }, + "P14": { + "verdict": "wrong", + "errors": [ + "wrong_conclusion" + ], + "notes": "Only existence of a ring structure is stated; the identity and unit characterization are omitted." + }, + "P15": { + "verdict": "faithful", + "errors": [], + "notes": "Unique solvability in both factors expresses the row and column permutation property." + }, + "P16": { + "verdict": "faithful", + "errors": [], + "notes": "Passing to the product representation preserves the order-divisibility claim; capitalization and namespace errors are not semantic changes." + }, + "P17": { + "verdict": "wrong", + "errors": [ + "wrong_conclusion" + ], + "notes": "An independent non-field example in the extracted passage is omitted." + }, + "P18": { + "verdict": "faithful", + "errors": [], + "notes": "The norm-one complex carrier and multiplication describe the specified subgroup; bundling/API validity is not assessed." + }, + "P19": { + "verdict": "minor_drift", + "errors": [ + "wrong_type" + ], + "notes": "The natural-valued order convention needs an infinite-order convention absent from the cardinality definition." + }, + "P20": { + "verdict": "faithful", + "errors": [], + "notes": "A single left-identity action on one group element forces equality to the identity." + }, + "P21": { + "verdict": "minor_drift", + "errors": [ + "wrong_type" + ], + "notes": "The intended commutativity equivalence is visible, but the left operation lacks the carrier annotation needed to identify G." + }, + "P22": { + "verdict": "faithful", + "errors": [], + "notes": "The two quantified unique-solvability claims express the specified table property." + }, + "P23": { + "verdict": "faithful", + "errors": [], + "notes": "Prime factors, modulus, lcm exponent and coprimality reproduce the extracted claim; no unstated distinctness assumption is introduced." + }, + "P24": { + "verdict": "wrong", + "errors": [ + "wrong_conclusion", + "degenerate" + ], + "notes": "An arbitrary group satisfying an order condition is not identified with the geometric symmetry group." + }, + "P25": { + "verdict": "faithful", + "errors": [], + "notes": "The two declarations cover both cancellation directions." + }, + "P26": { + "verdict": "wrong", + "errors": [ + "extra_hypothesis", + "missing_hypothesis" + ], + "notes": "The inserted divisibility assumption does not express the RSA relationship required by the argument." + }, + "P27": { + "verdict": "wrong", + "errors": [ + "wrong_conclusion" + ], + "notes": "The isomorphism is asserted for a quotient of the ambient group instead of the stabilizer subgroup." + }, + "P28": { + "verdict": "wrong", + "errors": [ + "wrong_type", + "wrong_conclusion" + ], + "notes": "Natural exponent division fails to express a square root, and the homomorphism target does not encode the specified automorphism." + }, + "P29": { + "verdict": "faithful", + "errors": [], + "notes": "A bijective homomorphism supplies the isomorphism assumption and both power assertions are retained." + }, + "P30": { + "verdict": "wrong", + "errors": [ + "wrong_type" + ], + "notes": "An unordered finite product is used for an arbitrary semigroup, losing the ordered nonempty product required by the exercise." + }, + "P31": { + "verdict": "not_formalizable", + "errors": [ + "other" + ], + "notes": "The isolated instruction refers to an earlier map whose definition is absent; the actual proposition cannot be recovered from this span." + }, + "P32": { + "verdict": "wrong", + "errors": [ + "wrong_conclusion", + "degenerate" + ], + "notes": "The result merely supplies an unspecified ring homomorphism and does not constrain it to evaluation at the matrix parameter." + }, + "P33": { + "verdict": "faithful", + "errors": [], + "notes": "The cardinality assumption and the nonidentity involution conclusion match; the missing instance binder is a compilation defect." + }, + "P34": { + "verdict": "faithful", + "errors": [], + "notes": "The contrasting abelian properties encode the reason these specified groups are not isomorphic." + }, + "P35": { + "verdict": "wrong", + "errors": [ + "wrong_type", + "quantifier" + ], + "notes": "One fixed-arity function is applied at incompatible arities instead of specifying a coherent family of products." + }, + "P36": { + "verdict": "wrong", + "errors": [ + "wrong_type", + "wrong_conclusion" + ], + "notes": "The ring carrier replaces the concrete root-of-unity group, and neither its order nor the specified generator is stated." + }, + "P37": { + "verdict": "wrong", + "errors": [ + "degenerate", + "wrong_conclusion" + ], + "notes": "The declaration has no defining expression for the requested subgroup." + }, + "P38": { + "verdict": "wrong", + "errors": [ + "missing_hypothesis" + ], + "notes": "Nonemptiness is missing, so the empty subset satisfies both closure assumptions." + }, + "P39": { + "verdict": "wrong", + "errors": [ + "wrong_type", + "wrong_conclusion" + ], + "notes": "Laurent series replace finite Laurent polynomials, and the requested units are not characterized." + }, + "P40": { + "verdict": "faithful", + "errors": [], + "notes": "The supplied structure body fixes the function to the canonical integer residue map." + }, + "P41": { + "verdict": "wrong", + "errors": [ + "extra_hypothesis" + ], + "notes": "The cardinality assertion is restricted to the range where noncommutativity holds, dropping the smaller symmetric groups." + }, + "P42": { + "verdict": "wrong", + "errors": [ + "missing_hypothesis", + "wrong_conclusion" + ], + "notes": "A necessary closure condition is promoted to sufficiency without inverse closure." + }, + "P43": { + "verdict": "faithful", + "errors": [], + "notes": "Any two groups of the specified size are related by a multiplicative equivalence." + }, + "P44": { + "verdict": "faithful", + "errors": [], + "notes": "The defining field is exactly commutativity of the group operation." + }, + "P45": { + "verdict": "wrong", + "errors": [ + "quantifier", + "wrong_conclusion" + ], + "notes": "Literal uniqueness of a carrier/structure replaces uniqueness up to group isomorphism." + }, + "P46": { + "verdict": "wrong", + "errors": [ + "wrong_type", + "wrong_conclusion" + ], + "notes": "Univariate polynomials over a product ring replace three-variable real polynomials; the units question is omitted." + }, + "P47": { + "verdict": "minor_drift", + "errors": [ + "wrong_conclusion" + ], + "notes": "The integer-span equality captures the generated set, but the equality for opposite generators is not explicitly stated." + }, + "P48": { + "verdict": "faithful", + "errors": [], + "notes": "The one-sided inverse hypothesis gives the specified inverse element." + }, + "P49": { + "verdict": "faithful", + "errors": [], + "notes": "The theorem statement is exactly involutivity of group inversion." + }, + "P50": { + "verdict": "faithful", + "errors": [], + "notes": "The custom structure supplies additive commutative group, associative multiplication and both distributive laws without imposing a unit." + }, + "P51": { + "verdict": "faithful", + "errors": [], + "notes": "The carrier, multiplication and identity encode the specified finite group; existence of the chosen API is not audited." + }, + "P52": { + "verdict": "minor_drift", + "errors": [ + "wrong_conclusion", + "degenerate" + ], + "notes": "Ring structure and unit-to-constant direction are present, but identity characterization is replaced by reflexivity." + }, + "P53": { + "verdict": "minor_drift", + "errors": [ + "extra_hypothesis" + ], + "notes": "Cardinality is represented only for finite groups although the definition is not restricted to them." + }, + "P54": { + "verdict": "wrong", + "errors": [ + "wrong_type" + ], + "notes": "Multiplicative subgroup closure of a residue is used in place of the additive cyclic subgroup generated by it." + }, + "P55": { + "verdict": "faithful", + "errors": [], + "notes": "The abelian-property equivalence is stated under an isomorphism." + }, + "P56": { + "verdict": "not_formalizable", + "errors": [ + "other" + ], + "notes": "The design question does not specify an authenticity predicate or formal adversarial model." + }, + "P57": { + "verdict": "wrong", + "errors": [ + "wrong_conclusion" + ], + "notes": "The homomorphism criterion is retained but the separate isomorphism definition is absent." + }, + "P58": { + "verdict": "wrong", + "errors": [ + "wrong_type" + ], + "notes": "A multiplicative equivalence on the full residue ring does not represent the additive cyclic group in the comparison." + }, + "P59": { + "verdict": "minor_drift", + "errors": [ + "wrong_type" + ], + "notes": "The inherited-group criterion is recognizable, but operations on the subset are not specified as restricted operations." + }, + "P60": { + "verdict": "wrong", + "errors": [ + "wrong_type", + "missing_hypothesis" + ], + "notes": "Global bijections with local differentiability conditions do not specify self-diffeomorphisms of the open subset." + }, + "P61": { + "verdict": "faithful", + "errors": [], + "notes": "The homeomorphism type supplies the intended carrier and group structure under composition; notation validity is not assessed." + }, + "P62": { + "verdict": "faithful", + "errors": [], + "notes": "Both least-positive exponent and the bounded-power description are retained, ignoring set-minimum API syntax." + }, + "P63": { + "verdict": "faithful", + "errors": [], + "notes": "Both two-sided identity hypotheses and their equality are stated." + }, + "P64": { + "verdict": "wrong", + "errors": [ + "missing_hypothesis", + "extra_hypothesis" + ], + "notes": "The exponent relation uses the ciphertext modulus where the RSA exponent modulus is required." + }, + "P65": { + "verdict": "wrong", + "errors": [ + "wrong_conclusion", + "degenerate" + ], + "notes": "The arbitrary finite group is unrelated to the requested geometric symmetries, with the classification left in a comment." + } + } +} diff --git a/experiments/P0-pilot/make_sheet.py b/experiments/P0-pilot/make_sheet.py index 78e61cf..8cd6959 100644 --- a/experiments/P0-pilot/make_sheet.py +++ b/experiments/P0-pilot/make_sheet.py @@ -154,6 +154,10 @@ def main() -> int: items = [json.loads(line) for line in args.items.read_text(encoding="utf-8").splitlines() if line.strip()] + if not items or any(not item.get("source_text", "").strip() for item in items): + parser.error("Every item needs nonempty source_text; use a private source-inclusive export.") + if len({item["id"] for item in items}) != len(items): + parser.error("Item IDs must be unique.") 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)] diff --git a/experiments/P0-pilot/prepare_items.py b/experiments/P0-pilot/prepare_items.py new file mode 100644 index 0000000..b028ec7 --- /dev/null +++ b/experiments/P0-pilot/prepare_items.py @@ -0,0 +1,45 @@ +"""Restore source passages from a private archived review without changing the cohort.""" +from __future__ import annotations + +import argparse +import json +from pathlib import Path + + +def restore(items: list[dict], review: dict) -> list[dict]: + archived = review["items"] + by_id = {row["id"]: row for row in archived} + if len(by_id) != len(archived) or len({row["id"] for row in items}) != len(items): + raise ValueError("Duplicate item IDs") + restored = [] + for item in items: + original = by_id[item["id"]] + comparable = dict(original) + if isinstance(comparable.get("imports"), str): + comparable["imports"] = json.loads(comparable["imports"]) + if any(comparable.get(k) != v for k, v in item.items()): + raise ValueError(f"Archived review does not match item {item['id']}") + passage = original.get("source_text", "") + if not passage.strip(): + raise ValueError(f"Missing archived passage for {item['id']}") + restored.append({**item, "source_text": passage}) + return restored + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--items", required=True, type=Path) + parser.add_argument("--review", required=True, type=Path) + parser.add_argument("--out", required=True, type=Path) + args = parser.parse_args() + if args.out.parent.name != "data": + parser.error("Source-inclusive output must go in a gitignored data/ directory") + items = [json.loads(line) for line in args.items.read_text().splitlines() if line.strip()] + rows = restore(items, json.loads(args.review.read_text())) + args.out.parent.mkdir(parents=True, exist_ok=True) + args.out.write_text("".join(json.dumps(row, ensure_ascii=False) + "\n" for row in rows)) + print(f"Restored {len(rows)} passages; all exported fields are unchanged") + + +if __name__ == "__main__": + main() diff --git a/experiments/P0-pilot/run_pilot.py b/experiments/P0-pilot/run_pilot.py index b55947e..e226470 100644 --- a/experiments/P0-pilot/run_pilot.py +++ b/experiments/P0-pilot/run_pilot.py @@ -15,8 +15,11 @@ Hard stops: --max-calls bounds API calls; a rerun skips items already in --out. from __future__ import annotations import argparse +import fcntl import hashlib +import inspect import json +import os import sys from pathlib import Path @@ -24,7 +27,7 @@ from leanbench import srcsimplex from leanbench.align import align from leanbench.config import Settings from leanbench.lint import lint -from leanbench.llm import OpenAICompatibleClient +from leanbench.llm import OpenAICompatibleClient, Usage from leanbench.project import project JUDGE_PROMPT_VERSION = "judge-v1" @@ -41,13 +44,15 @@ def judge(client, passage: str, lean: str) -> dict: {"role": "system", "content": JUDGE_SYSTEM}, {"role": "user", "content": f"Passage:\n{passage}\n\nLean:\n{lean}"}, ]) - if not isinstance(reply, dict) or "faithful" not in reply: + if not isinstance(reply, dict) or type(reply.get("faithful")) is not bool: raise ValueError(f"unusable judge reply: {str(reply)[:200]}") - return {"faithful": bool(reply["faithful"]), "confidence": reply.get("confidence"), + return {"faithful": reply["faithful"], "confidence": reply.get("confidence"), "reason": str(reply.get("reason", ""))[:300]} def run_item(client, item: dict) -> dict: + if not item.get("source_text", "").strip(): + raise ValueError("Missing source_text; use a private source-inclusive export") code = item.get("lean_code") or "" row: dict = {"id": item["id"], "compiled": bool(item.get("verified")), "errors": {}} proj = project(code) @@ -59,51 +64,154 @@ def run_item(client, item: dict) -> dict: al = align(src, proj) row["source"] = [r.__dict__ for r in src.roles] row["role"] = al.as_dict() + except CallBudgetExceeded: + raise except Exception as error: # a failed extraction is data, not a crash row["errors"]["role"] = str(error)[:300] try: row["judge"] = judge(client, item.get("source_text", ""), code) + except CallBudgetExceeded: + raise except Exception as error: row["errors"]["judge"] = str(error)[:300] return row +class CallBudgetExceeded(RuntimeError): + """Stop before issuing a request that would exceed the cumulative budget.""" + + +def digest(path: Path) -> str: + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def atomic_json(path: Path, value: dict) -> None: + temporary = path.with_suffix(path.suffix + ".tmp") + temporary.write_text(json.dumps(value, indent=2, allow_nan=False) + "\n", encoding="utf-8") + os.replace(temporary, path) + + +class AuditedClient(OpenAICompatibleClient): + """Persist reservations before HTTP requests, including transport and JSON retries.""" + + def complete(self, *args, **kwargs): + try: + return super().complete(*args, **kwargs) + finally: + self.checkpoint() + + +def execute(args, items, settings) -> int: + rows = [] + if args.out.exists(): + rows = [json.loads(x) for x in args.out.read_text(encoding="utf-8").splitlines() if x.strip()] + ids = {item["id"] for item in items} + done = {row["id"] for row in rows} + if len(done) != len(rows) or not done <= ids: + raise ValueError("Results have duplicate or unknown item IDs") + hashes = { + "source": hashlib.sha256((srcsimplex.SYSTEM_PROMPT + inspect.getsource(srcsimplex.passage_prompt)).encode()).hexdigest(), + "judge": hashlib.sha256(JUDGE_SYSTEM.encode()).hexdigest(), + } + identity = {"model": settings.llm.model, "base_url": settings.llm.base_url, + "temperature": settings.llm.temperature, "items_sha256": digest(args.items), + "prompt_hashes": hashes, + "prompts": [srcsimplex.PROMPT_VERSION, JUDGE_PROMPT_VERSION]} + labels = getattr(args, "labels", None) + if labels is not None: + identity["labels_sha256"] = digest(labels) + meta_path = args.out.with_suffix(".meta.json") + meta = {**identity, "request_attempts": 0, "usage": Usage().as_dict(), "status": "ready"} + if meta_path.exists(): + meta = json.loads(meta_path.read_text(encoding="utf-8")) + if any(meta.get(k) != v for k, v in identity.items()): + raise ValueError("Run identity changed; use a new output path instead of mixing runs") + elif rows: + raise ValueError("Cannot resume results without their audit metadata") + todo = [item for item in items if item["id"] not in done] + print(f"items={len(items)} done={len(done)} todo={len(todo)} model={settings.llm.model} " + f"nominal_calls={len(todo) * 2} request_attempts={meta['request_attempts']} cap={args.max_calls}") + print("prompt_hashes:", json.dumps(hashes)) + if args.dry_run: + return 0 + if settings.llm.model != "qwen-max" or settings.llm.temperature != 0: + raise ValueError("P0 is preregistered for qwen-max at temperature 0") + client = AuditedClient.from_settings(settings.llm) + client.usage = Usage(**meta["usage"]) + + def checkpoint(): + meta["usage"] = client.usage.as_dict() + meta["completed_items"] = len(done) + atomic_json(meta_path, meta) + + def reserve(): + if meta["request_attempts"] >= args.max_calls: + raise CallBudgetExceeded("Cumulative request cap reached; no further HTTP request was sent") + meta["request_attempts"] += 1 + checkpoint() + + client.checkpoint = checkpoint + client.request_guard = reserve + meta["max_calls"] = args.max_calls + meta["status"] = "running" + checkpoint() + try: + with args.out.open("a", encoding="utf-8") as stream: + for item in todo: + row = run_item(client, item) + stream.write(json.dumps(row, ensure_ascii=False) + "\n") + stream.flush() + os.fsync(stream.fileno()) + done.add(item["id"]) + checkpoint() + print(f"completed={len(done)}/{len(items)} requests={meta['request_attempts']}", flush=True) + meta["status"] = "complete" + except CallBudgetExceeded as error: + meta["status"] = "budget_exhausted" + print(str(error), file=sys.stderr) + except BaseException: + meta["status"] = "interrupted" + raise + finally: + if args.out.exists(): + meta["results_sha256"] = digest(args.out) + checkpoint() + print(json.dumps(meta)) + return 0 if meta["status"] == "complete" else 2 + + def main() -> int: ap = argparse.ArgumentParser(description=__doc__.splitlines()[0]) ap.add_argument("--items", required=True, type=Path) ap.add_argument("--out", required=True, type=Path) ap.add_argument("--max-calls", type=int, default=400) ap.add_argument("--dry-run", action="store_true") + ap.add_argument("--labels", type=Path, help="Frozen labels; their hash is bound to the run") args = ap.parse_args() - + if not 1 <= args.max_calls <= 400: + ap.error("P0 requires a request cap between 1 and 400") items = [json.loads(x) for x in args.items.read_text(encoding="utf-8").splitlines() if x.strip()] - done = set() - if args.out.exists(): - done = {json.loads(x)["id"] for x in args.out.read_text(encoding="utf-8").splitlines() if x.strip()} - todo = [i for i in items if i["id"] not in done] - settings = Settings.from_env() - est = len(todo) * 3 # extract (<=2 tries) + judge - print(f"items={len(items)} done={len(done)} todo={len(todo)} model={settings.llm.model} " - f"est_calls<={est} (extract x2 + judge) cap={args.max_calls}") - print("prompts:", srcsimplex.PROMPT_VERSION, JUDGE_PROMPT_VERSION, - hashlib.sha256((srcsimplex.SYSTEM_PROMPT + JUDGE_SYSTEM).encode()).hexdigest()[:12]) - if args.dry_run: - return 0 - - client = OpenAICompatibleClient.from_settings(settings.llm) + if not items or len({item["id"] for item in items}) != len(items): + ap.error("Input must contain unique item IDs") + if any(not item.get("source_text", "").strip() for item in items): + ap.error("Every item needs nonempty source_text; use a private source-inclusive export") + if not args.dry_run and args.labels is None: + ap.error("Freeze all blind labels first, then pass --labels") + if args.labels is not None: + annotation = json.loads(args.labels.read_text(encoding="utf-8")) + key_path = args.labels.with_name("key.json") + key = json.loads(key_path.read_text(encoding="utf-8"))["key"] + verdicts = {"faithful", "minor_drift", "wrong", "not_formalizable"} + if (set(key.values()) != {item["id"] for item in items} + or set(annotation["labels"]) != set(key) + or any(row.get("verdict") not in verdicts for row in annotation["labels"].values()) + or annotation.get("items_sha256") != digest(args.items) + or annotation.get("key_sha256") != digest(key_path)): + ap.error("Frozen labels, key and source-inclusive items must be complete and match") args.out.parent.mkdir(parents=True, exist_ok=True) - with args.out.open("a", encoding="utf-8") as fh: - for item in todo: - if client.usage.calls >= args.max_calls: - print("call cap reached; rerun to resume", file=sys.stderr) - break - fh.write(json.dumps(run_item(client, item), ensure_ascii=False) + "\n") - fh.flush() - meta = {"model": settings.llm.model, "usage": client.usage.as_dict(), - "prompts": [srcsimplex.PROMPT_VERSION, JUDGE_PROMPT_VERSION]} - (args.out.parent / "run_meta.json").write_text(json.dumps(meta, indent=2), encoding="utf-8") - print(json.dumps(meta)) - return 0 + with args.out.with_suffix(args.out.suffix + ".lock").open("w") as lock: + fcntl.flock(lock, fcntl.LOCK_EX | fcntl.LOCK_NB) + return execute(args, items, Settings.from_env()) if __name__ == "__main__": diff --git a/experiments/P0-pilot/score.py b/experiments/P0-pilot/score.py index 2f04eb6..12107bf 100644 --- a/experiments/P0-pilot/score.py +++ b/experiments/P0-pilot/score.py @@ -1,9 +1,9 @@ -"""Score the pilot: detectors vs. the blind human labels, with the pre-registered decision. +"""Score the pilot against frozen blind labels using the pre-registered decision. 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 +Positive class = unfaithful. Primary: wrong versus faithful, excluding minor drift (role alignment and the judge do not need Lean to accept the code; only 10 of the 65 pilot items compiled, too few to decide on). Secondary: wrong or minor_drift; and the compiled-only subset (the paper's claim, reported with its interval, not used to decide). "not_formalizable" items are excluded. Decision (fixed before @@ -19,22 +19,35 @@ With ~65 items every number carries a wide Wilson interval; the pilot checks for from __future__ import annotations import argparse +import hashlib import json +import math from pathlib import Path -from leanbench.evalstats import auc, confusion +from leanbench.evalstats import auc, confusion, wilson def load(args): - results = {json.loads(x)["id"]: json.loads(x) for x in args.results.read_text(encoding="utf-8").splitlines() if x.strip()} + result_rows = [json.loads(x) for x in args.results.read_text(encoding="utf-8").splitlines() if x.strip()] + results = {row["id"]: row for row in result_rows} labels = json.loads(args.labels.read_text(encoding="utf-8"))["labels"] key = json.loads(args.key.read_text(encoding="utf-8"))["key"] + if not key or len(set(key.values())) != len(key): + raise ValueError("The blind key must contain unique item IDs") + if len(results) != len(result_rows) or set(results) != set(key.values()): + raise ValueError("Results must cover every keyed item exactly once") + if set(labels) != set(key): + raise ValueError("Labels must cover every blind ID exactly once") rows = [] for blind, item_id in key.items(): lab = labels.get(blind) or {} - if item_id in results and lab.get("verdict"): - rows.append({**results[item_id], "blind": blind, "verdict": lab["verdict"], - "human_errors": lab.get("errors", [])}) + if lab.get("verdict") not in {"faithful", "minor_drift", "wrong", "not_formalizable"}: + raise ValueError(f"Missing or invalid verdict for {blind}") + row = results[item_id] + if row.get("errors") or "judge" not in row or "role" not in row: + raise ValueError(f"Unresolved detector failure for {blind}; no decision can be issued") + rows.append({**row, "blind": blind, "verdict": lab["verdict"], + "human_errors": lab.get("errors", [])}) return rows @@ -51,19 +64,24 @@ def report(rows, positive): out = {} for name in ("compile_only", "lint", "role", "judge"): out[name] = confusion([flags(r)[name] for r in rows], [positive(r) for r in rows]).as_dict() + out[name]["precision_ci"] = wilson(out[name]["tp"], out[name]["tp"] + out[name]["fp"]) out["role"]["auc_score"] = auc([-(r.get("role", {}).get("score", 1.0)) for r in rows], [positive(r) for r in rows]) + out["role"]["complementary_wrong"] = sum( + positive(r) and flags(r)["role"] and not flags(r)["judge"] for r in rows + ) return out def decide(sub): role, judge = sub["role"], sub["judge"] - if role["tp"] + role["fn"] == 0: - return "INSUFFICIENT: no wrong items in the labels" + if role["tp"] + role["fn"] == 0 or role["fp"] + role["tn"] == 0: + return "INSUFFICIENT: both wrong and faithful items are required" go = (role["recall"] >= 0.5 and role["false_flag_rate"] <= 0.2 and role["recall"] >= judge["recall"] + 0.10 and role["false_flag_rate"] <= judge["false_flag_rate"]) - partial = (role["recall"] >= 0.4 and role["false_flag_rate"] <= 0.3) + partial = ((role["recall"] >= 0.4 and role["false_flag_rate"] <= 0.3) + or role.get("complementary_wrong", 0) >= 3) return "GO" if go else "PARTIAL" if partial else "NO-GO" @@ -75,19 +93,51 @@ def main() -> int: 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"]] + meta = json.loads(args.results.with_suffix(".meta.json").read_text(encoding="utf-8")) + if (meta.get("status") != "complete" + or meta.get("labels_sha256") != hashlib.sha256(args.labels.read_bytes()).hexdigest() + or meta.get("results_sha256") != hashlib.sha256(args.results.read_bytes()).hexdigest()): + ap.error("Scoring requires a complete run with unchanged frozen labels and results") + all_rows = load(args) + rows = [r for r in all_rows if r["verdict"] != "not_formalizable"] + primary = [r for r in rows if r["verdict"] != "minor_drift"] + compiled = [r for r in primary if r["compiled"]] summary = { - "n_labeled": len(rows), "n_compiled": len(compiled), + "run_metadata": meta, + "n_labeled": len(all_rows), "n_evaluable": len(rows), "n_primary": len(primary), + "n_compiled": len(compiled), "verdicts": {v: sum(r["verdict"] == v for r in rows) for v in - ("faithful", "minor_drift", "wrong")}, + ("faithful", "minor_drift", "wrong", "not_formalizable")}, "compiled_but_wrong": sum(r["verdict"] == "wrong" for r in compiled), - "primary_all": report(rows, lambda r: r["verdict"] == "wrong"), + "primary_all": report(primary, lambda r: r["verdict"] == "wrong"), "secondary_all": report(rows, lambda r: r["verdict"] in ("wrong", "minor_drift")), "compiled_only": report(compiled, lambda r: r["verdict"] == "wrong"), } + summary["verdicts"]["not_formalizable"] = len(all_rows) - len(rows) + summary["role_recall_by_error"] = { + error: {"flagged": sum(flags(r)["role"] for r in rows + if r["verdict"] == "wrong" and error in r["human_errors"]), + "total": sum(r["verdict"] == "wrong" and error in r["human_errors"] for r in rows)} + for error in sorted({e for r in rows for e in r["human_errors"]}) + } + summary["degenerate_projection"] = { + "total": sum(bool(r.get("projection", {}).get("degenerate")) for r in all_rows), + "wrong": sum(r["verdict"] == "wrong" and bool(r.get("projection", {}).get("degenerate")) + for r in all_rows), + } + summary["disagreements"] = [ + {"blind": r["blind"], "verdict": r["verdict"], "flags": flags(r)} + for r in primary if any(f != (r["verdict"] == "wrong") for f in flags(r).values()) + ] summary["decision"] = decide(summary["primary_all"]) - text = json.dumps(summary, indent=2, default=str) + def finite_json(value): + if isinstance(value, dict): + return {k: finite_json(v) for k, v in value.items()} + if isinstance(value, (list, tuple)): + return [finite_json(v) for v in value] + return None if isinstance(value, float) and not math.isfinite(value) else value + + text = json.dumps(finite_json(summary), indent=2, allow_nan=False) if args.summary: args.summary.parent.mkdir(parents=True, exist_ok=True) args.summary.write_text(text + "\n", encoding="utf-8") diff --git a/leanbench/llm.py b/leanbench/llm.py index b6e5c16..4598b39 100644 --- a/leanbench/llm.py +++ b/leanbench/llm.py @@ -14,7 +14,7 @@ import re import time import urllib.error import urllib.request -from collections.abc import Iterable +from collections.abc import Callable, Iterable from dataclasses import dataclass, field from typing import Any, Protocol @@ -66,6 +66,7 @@ class OpenAICompatibleClient: max_retries: int = 4 temperature: float = 0.0 usage: Usage = field(default_factory=Usage) + request_guard: Callable[[], None] | None = field(default=None, repr=False) @classmethod def from_settings(cls, settings: LLMSettings) -> OpenAICompatibleClient: @@ -97,6 +98,8 @@ class OpenAICompatibleClient: } last: Exception | None = None for attempt in range(self.max_retries + 1): + if self.request_guard is not None: + self.request_guard() request = urllib.request.Request(url, data=body, headers=headers, method="POST") try: with urllib.request.urlopen(request, timeout=self.timeout) as response: diff --git a/tests/test_pilot_scripts.py b/tests/test_pilot_scripts.py index dc55d59..ee75b08 100644 --- a/tests/test_pilot_scripts.py +++ b/tests/test_pilot_scripts.py @@ -36,3 +36,108 @@ def test_run_item_and_score(tmp_path): out = sc.report(rows, lambda r: r["verdict"] == "wrong") assert out["judge"]["n"] == 4 assert sc.decide(out) in {"GO", "PARTIAL", "NO-GO"} + + +def test_complementary_signal_is_partial(): + sc = load("score") + rows = [ + {"compiled": True, "lint": [], "role": {"flagged": i < 3, "score": 0.1}, + "judge": {"faithful": False if 3 <= i < 8 else True}, "verdict": "wrong"} + for i in range(10) + ] + [ + {"compiled": True, "lint": [], "role": {"flagged": False, "score": 1}, + "judge": {"faithful": True}, "verdict": "faithful"} + ] + summary = sc.report(rows, lambda row: row["verdict"] == "wrong") + assert summary["role"]["recall"] == 0.3 + assert summary["role"]["complementary_wrong"] == 3 + assert sc.decide(summary) == "PARTIAL" + + +def test_score_rejects_missing_labels_and_detector_failures(tmp_path): + import argparse + import json + + import pytest + + sc = load("score") + args = argparse.Namespace(results=tmp_path / "results.jsonl", labels=tmp_path / "labels.json", + key=tmp_path / "key.json") + args.key.write_text(json.dumps({"key": {"P01": "x1"}})) + args.labels.write_text(json.dumps({"labels": {"P01": {"verdict": None}}})) + args.results.write_text(json.dumps({"id": "x1"}) + "\n") + with pytest.raises(ValueError, match="verdict"): + sc.load(args) + args.labels.write_text(json.dumps({"labels": {"P01": {"verdict": "wrong"}}})) + with pytest.raises(ValueError, match="detector failure"): + sc.load(args) + args.results.write_text("") + with pytest.raises(ValueError, match="every keyed item"): + sc.load(args) + + +def test_request_budget_survives_resume_and_transport_retries(tmp_path, monkeypatch): + import argparse + import json + import urllib.error + + import pytest + + from leanbench.config import Settings + + rp = load("run_pilot") + args = argparse.Namespace(items=tmp_path / "items.jsonl", out=tmp_path / "results.jsonl", + max_calls=2, dry_run=False) + args.items.write_text(json.dumps(ITEM) + "\n") + monkeypatch.setenv("DASHSCOPE_API_KEY", "test-only") + settings = Settings() + settings.llm.max_retries = 5 + requests = [] + + def fail(*args, **kwargs): + requests.append(1) + raise urllib.error.URLError("offline test") + + monkeypatch.setattr("urllib.request.urlopen", fail) + monkeypatch.setattr("leanbench.llm.time.sleep", lambda *_: None) + assert rp.execute(args, [ITEM], settings) == 2 + assert len(requests) == 2 + assert rp.execute(args, [ITEM], settings) == 2 + assert len(requests) == 2 + meta = json.loads(args.out.with_suffix(".meta.json").read_text()) + assert meta["request_attempts"] == 2 + assert len(meta["prompt_hashes"]["judge"]) == 64 + assert meta["status"] == "budget_exhausted" + settings.llm.model = "other-model" + with pytest.raises(ValueError, match="identity changed"): + rp.execute(args, [ITEM], settings) + + +def test_run_rejects_missing_source_passage(): + import pytest + + rp = load("run_pilot") + with pytest.raises(ValueError, match="Missing source_text"): + rp.run_item(Stub(), {**ITEM, "source_text": ""}) + + +def test_restore_passages_checks_cohort_and_normalizes_archived_imports(): + import pytest + + prepare = load("prepare_items") + item = {"id": "x", "lean_code": "example : True := trivial", "imports": ["Mathlib"]} + original = {**item, "imports": '["Mathlib"]', "source_text": "A private passage."} + restored = prepare.restore([item], {"items": [original]}) + assert restored == [{**item, "source_text": "A private passage."}] + with pytest.raises(ValueError, match="does not match"): + prepare.restore([{**item, "lean_code": "changed"}], {"items": [original]}) + + +def test_judge_rejects_string_boolean(): + import pytest + + from leanbench.llm import ScriptedClient + + rp = load("run_pilot") + with pytest.raises(ValueError, match="unusable judge"): + rp.judge(ScriptedClient(['{"faithful": "false"}']), "passage", "code")