diff --git a/docs/experiments/P0-execution-2026-10-28.md b/docs/experiments/P0-execution-2026-10-28.md new file mode 100644 index 0000000..30704f8 --- /dev/null +++ b/docs/experiments/P0-execution-2026-10-28.md @@ -0,0 +1,82 @@ +# P0 execution report: 2026-10-28 + +**Status: blocked by provider billing. No GO, PARTIAL or NO-GO decision.** +The owner requested delivery of the fixes and this report now, with the remaining paid calls deferred. + +## What ran + +The owner explicitly authorized sending the 65 textbook passages and corresponding Lean code +through the existing DashScope endpoint to `qwen-max`, at temperature 0 and a cumulative ceiling +of 400 HTTP requests. The run issued **131 HTTP requests**. Provider responses accounted for +**37,699 input tokens and 7,790 output tokens**, 45,489 total. These are recorded token counts, +not an invoice or a monetary cost estimate. The client counted 89 received model responses; +a received response is not necessarily a usable detector result. + +| Coverage | Count | +|---|---:| +| Original cohort | 65 | +| Items with both detectors complete | 42 | +| Items with one or both detectors missing | 23 | +| Successful role-extraction/alignment components | 45 | +| Successful judge components | 43 | +| Missing role components | 20 | +| Missing judge components | 22 | +| Remaining request reservations | 269 | + +DashScope returned HTTP 400 with error code `Arrearage` and its overdue-payment reference. +The first runner implementation recorded the failures and continued through the cohort, so +65 saved rows did not mean 65 successful items. The scorer rejected these incomplete outputs. +No partial-sample gate decision or performance comparison has been produced. + +## Inputs and labels + +The default `items.jsonl` export omitted `source_text`. All 65 original passages were recovered +from the matching detection spans and checked byte-for-byte against the archived private +`review.json`. Item IDs and Lean code were unchanged. The recovery tool also verifies every +exported field against the archive, normalizing the archive's JSON-encoded imports field. +Source-inclusive inputs and the regenerated labeling HTML remain in the ignored data directory. + +The owner replaced the planned Kimi/human labeling with Codex annotation. All 65 labels were +frozen before the first detector request. They contain 30 faithful, 25 wrong, 7 minor drift and +3 not-formalizable verdicts. This is one AI annotator, **not human gold**. The annotator saw the +detector implementation and aggregate compilation counts, but not per-item compiler outcomes +or detector outputs. Syntax/proof defects were ignored when the intended semantics were recoverable; +no compiler or API-name audit was performed. Independent human auditing remains necessary before +using these labels as evidence for paper-level claims. + +## Execution repairs + +- Empty passages and mismatched frozen inputs/labels are rejected before paid calls. +- Each HTTP attempt reserves cumulative budget before sending, including transport and JSON retries. + Model, endpoint, temperature, input/label/prompt hashes and cumulative token usage are persisted. +- Billing/authentication errors now stop immediately, preserving partial results. +- Resume keeps every successful detector component and retries only missing components. Existing + rows are replaced atomically rather than duplicated. A budget stop also preserves completed work + within the current item. A lock prevents concurrent writers. +- `--audit-only` reconciles saved metadata without API calls. It confirmed 42 complete items, + 23 incomplete items, 42 missing components and 131 already-consumed request reservations. +- Scoring requires complete results and unchanged frozen-label/result hashes. It restores the + preregistered complementary-signal PARTIAL rule and uses wrong versus faithful for primary metrics; + minor drift is included as positive only in the secondary comparison. +- Detector prompts, matching thresholds, the concept table and frozen annotations were not tuned + against these outputs. Recovery changes concern transport, persistence and accounting only. + +The private first-attempt output and metadata were backed up before reconciliation. The results +hash and the frozen-label hash did not change during the offline audit. + +## Validation and next action + +149 offline unit tests passed, including billing-stop and partial-resume regressions; repository-wide +Ruff and diff checks passed. These checks did not compile Lean or build Docker locally. +The initial PR revision passed Python tests and real Lean validation on +`ubuntu24.04-x64-lean4.35`, runner 7, in [CI #427](https://gitea.entroia.com/Zayden-Jung/lean-bench/actions/runs/427). +The image job was skipped by the PR workflow. The recovery revision's remote result is reported separately in the PR checks. + +After the owner confirms billing recovery, resume the existing run with the same inputs, frozen +labels and cumulative budget. There are 42 missing components; retries may consume more requests. +Do not change model or prompts to work around the provider block. Only after all 65 items have +successful outputs should the scorer produce the registered decision and disagreement report. +Phase 1 has not started. + +Tracked audit data: `experiments/P0-pilot/results/execution.json` (counts and hashes only). +Private raw files: `experiments/P0-pilot/data/` (gitignored). diff --git a/docs/experiments/P0-pilot.md b/docs/experiments/P0-pilot.md index efc2b90..6414444 100644 --- a/docs/experiments/P0-pilot.md +++ b/docs/experiments/P0-pilot.md @@ -2,7 +2,11 @@ Experiment ID **P0**, Phase 0. Registry and conventions: [README.md](README.md). -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.** +Status: **approved 2026-10-22; 65 AI labels frozen 2026-10-28; detector run blocked by DashScope Arrearage after 131 requests. 42 items are complete, 23 need missing detector components. No gate decision has been issued.** + +The owner explicitly authorized sending the 65 passages and Lean code to DashScope/qwen-max, +then requested fixes and an execution report now, with paid recovery calls deferred. +Execution report: [P0 execution, 2026-10-28](P0-execution-2026-10-28.md). 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. diff --git a/experiments/P0-pilot/README.md b/experiments/P0-pilot/README.md index b302b47..986436e 100644 --- a/experiments/P0-pilot/README.md +++ b/experiments/P0-pilot/README.md @@ -44,6 +44,9 @@ Labeling must be finished before anyone opens `results.jsonl`. - 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. +- Billing/authentication failures stop immediately. Resume retries only missing detector components, + keeping both complete items and the successful side of partial items. Rows are replaced atomically. + `--audit-only` reconciles saved completion counts and status without any API request. - 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 @@ -52,3 +55,11 @@ Labeling must be finished before anyone opens `results.jsonl`. 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. + +## Current execution + +The 2026-10-28 run was blocked by DashScope `Arrearage`: 42 items are complete, 23 need +42 detector components, and 131 of the 400 request reservations have been consumed. +The owner requested fixes and a report now, with paid resumption deferred. +See `docs/experiments/P0-execution-2026-10-28.md` and `results/execution.json`. +No gate decision has been issued. Restore provider billing before resuming the same run. diff --git a/experiments/P0-pilot/results/execution.json b/experiments/P0-pilot/results/execution.json new file mode 100644 index 0000000..c82e3a7 --- /dev/null +++ b/experiments/P0-pilot/results/execution.json @@ -0,0 +1,71 @@ +{ + "experiment": "P0", + "status": "provider_blocked", + "decision": null, + "decision_withheld_reason": "Incomplete detector outputs after DashScope Arrearage; no GO/PARTIAL/NO-GO is valid.", + "cohort_size": 65, + "completed_items": 42, + "items_with_failures": 23, + "missing_components": { + "judge": 22, + "role": 20 + }, + "request_attempts": 131, + "max_calls": 400, + "remaining_request_budget": 269, + "usage": { + "calls": 89, + "prompt_tokens": 37699, + "completion_tokens": 7790 + }, + "model": "qwen-max", + "temperature": 0.0, + "items_sha256": "487ecd22919a5e3b0174a2846ab8fe7c0daf4d3feccccf8ea6571aec04c41bed", + "labels_sha256": "1552dba85e75426799151384e7e28c9a0b1072ed4c862df0876df89920d2a638", + "results_sha256": "fce402e6eab460a48bb9a8e94140bb23f305843ab46d227bbffa5100d7de69e5", + "prompt_hashes": { + "source": "382f9a7b5a0cfb2d50d525f884dc806f45adaa59bcc45e388920c4759db1546f", + "judge": "7ab92682bd71d78a212471289f0f01db39d6b68f49d44df65d7b1c9e34ebb5e2" + }, + "labels": { + "type": "single AI annotator; not human gold", + "frozen": true, + "count": 65 + }, + "affected_blind_ids": [ + "P02", + "P04", + "P09", + "P18", + "P19", + "P20", + "P21", + "P22", + "P24", + "P27", + "P29", + "P30", + "P33", + "P36", + "P37", + "P38", + "P42", + "P43", + "P45", + "P47", + "P54", + "P59", + "P62" + ], + "successful_components_preserved": 88, + "resume_policy": "After owner confirms billing recovery, retry missing components only using the same run files, frozen labels, model, prompts and cumulative 400-request ceiling.", + "owner_instruction": "2026-10-28: complete fixes and the execution report now; resume paid calls later.", + "validation": { + "offline_unit_tests": 149, + "ruff": "passed", + "remote_runner_tag": "ubuntu24.04-x64-lean4.35", + "initial_remote_ci": "https://gitea.entroia.com/Zayden-Jung/lean-bench/actions/runs/427", + "initial_remote_ci_status": "success; image job skipped for PR", + "recovery_remote_ci": "See PR #5 checks for the delivered head revision" + } +} diff --git a/experiments/P0-pilot/run_pilot.py b/experiments/P0-pilot/run_pilot.py index e226470..d4a41cf 100644 --- a/experiments/P0-pilot/run_pilot.py +++ b/experiments/P0-pilot/run_pilot.py @@ -50,37 +50,64 @@ def judge(client, passage: str, lean: str) -> dict: "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) - row["projection"] = proj.as_dict() - row["lint"] = lint(proj) - try: - src = srcsimplex.extract_source_simplex(client, item.get("source_text", ""), - item.get("label", "")) - 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 +def provider_blocked(error: Exception) -> bool: + text = str(error).lower() + return any(code in text for code in ("arrearage", "overdue-payment", "invalid_api_key", "http 401", "http 403")) + + +def complete_row(row: dict) -> bool: + return not row.get("errors") and "role" in row and "judge" in row + + +class ProviderBlocked(RuntimeError): + """A billing or authentication failure requires external recovery before resuming.""" + + def __init__(self, row): + super().__init__("Provider billing/authentication blocked; partial results were preserved") + self.row = row class CallBudgetExceeded(RuntimeError): """Stop before issuing a request that would exceed the cumulative budget.""" +def run_item(client, item: dict, previous: dict | None = None) -> 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 = {**(previous or {}), "id": item["id"], "compiled": bool(item.get("verified"))} + row["errors"] = dict(row.get("errors", {})) + proj = project(code) + row["projection"] = proj.as_dict() + row["lint"] = lint(proj) + if "role" not in row: + try: + src = srcsimplex.extract_source_simplex(client, item["source_text"], item.get("label", "")) + al = align(src, proj) + row["source"] = [r.__dict__ for r in src.roles] + row["role"] = al.as_dict() + row["errors"].pop("role", None) + except CallBudgetExceeded as error: + error.row = row + raise + except Exception as error: + row["errors"]["role"] = str(error)[:300] + if provider_blocked(error): + raise ProviderBlocked(row) from error + if "judge" not in row: + try: + row["judge"] = judge(client, item["source_text"], code) + row["errors"].pop("judge", None) + except CallBudgetExceeded as error: + error.row = row + raise + except Exception as error: + row["errors"]["judge"] = str(error)[:300] + if provider_blocked(error): + raise ProviderBlocked(row) from error + return row + + def digest(path: Path) -> str: return hashlib.sha256(path.read_bytes()).hexdigest() @@ -106,8 +133,9 @@ def execute(args, items, settings) -> int: 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: + by_id = {row["id"]: row for row in rows} + done = {row["id"] for row in rows if complete_row(row)} + if len(by_id) != len(rows) or not set(by_id) <= ids: raise ValueError("Results have duplicate or unknown item IDs") hashes = { "source": hashlib.sha256((srcsimplex.SYSTEM_PROMPT + inspect.getsource(srcsimplex.passage_prompt)).encode()).hexdigest(), @@ -129,11 +157,24 @@ def execute(args, items, settings) -> int: elif rows: raise ValueError("Cannot resume results without their audit metadata") todo = [item for item in items if item["id"] not in done] + missing = sum(2 - int("role" in by_id.get(i["id"], {})) + - int("judge" in by_id.get(i["id"], {})) for i in todo) 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}") + f"missing_components={missing} request_attempts={meta['request_attempts']} cap={args.max_calls}") print("prompt_hashes:", json.dumps(hashes)) if args.dry_run: return 0 + if getattr(args, "audit_only", False): + meta["completed_items"] = len(done) + meta["processed_items"] = len(rows) + meta["status"] = ("provider_blocked" if any(provider_blocked(RuntimeError(message)) + for row in rows for message in row.get("errors", {}).values()) + else "detector_errors" if todo else "complete") + if args.out.exists(): + meta["results_sha256"] = digest(args.out) + atomic_json(meta_path, meta) + print(json.dumps(meta)) + return 0 if meta["status"] == "complete" else 2 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) @@ -142,6 +183,7 @@ def execute(args, items, settings) -> int: def checkpoint(): meta["usage"] = client.usage.as_dict() meta["completed_items"] = len(done) + meta["processed_items"] = len(by_id) atomic_json(meta_path, meta) def reserve(): @@ -155,19 +197,30 @@ def execute(args, items, settings) -> int: meta["max_calls"] = args.max_calls meta["status"] = "running" checkpoint() + def save_row(row): + by_id[row["id"]] = row + if complete_row(row): + done.add(row["id"]) + temporary = args.out.with_suffix(args.out.suffix + ".tmp") + with temporary.open("w", encoding="utf-8") as stream: + for item in items: + if item["id"] in by_id: + stream.write(json.dumps(by_id[item["id"]], ensure_ascii=False) + "\n") + stream.flush() + os.fsync(stream.fileno()) + os.replace(temporary, args.out) + 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" + for item in todo: + row = run_item(client, item, by_id.get(item["id"])) + save_row(row) + print(f"completed={len(done)}/{len(items)} requests={meta['request_attempts']}", flush=True) + meta["status"] = "complete" if len(done) == len(items) else "detector_errors" + except (CallBudgetExceeded, ProviderBlocked) as error: + if getattr(error, "row", None) is not None: + save_row(error.row) + meta["status"] = "provider_blocked" if isinstance(error, ProviderBlocked) else "budget_exhausted" print(str(error), file=sys.stderr) except BaseException: meta["status"] = "interrupted" @@ -186,6 +239,7 @@ def main() -> int: 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("--audit-only", action="store_true", help="Reconcile saved state without making API calls") 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: diff --git a/tests/test_pilot_scripts.py b/tests/test_pilot_scripts.py index ee75b08..7cbcc17 100644 --- a/tests/test_pilot_scripts.py +++ b/tests/test_pilot_scripts.py @@ -141,3 +141,82 @@ def test_judge_rejects_string_boolean(): rp = load("run_pilot") with pytest.raises(ValueError, match="unusable judge"): rp.judge(ScriptedClient(['{"faithful": "false"}']), "passage", "code") + + +def test_partial_resume_keeps_successful_detector_output(): + rp = load("run_pilot") + row = rp.run_item(Stub(), ITEM) + expected_role = row["role"] + row.pop("judge") + row["errors"]["judge"] = "temporary failure" + + class JudgeOnly: + calls = 0 + + def complete_json(self, messages): + self.calls += 1 + assert "faithful" in messages[0]["content"] + return {"faithful": True} + + client = JudgeOnly() + resumed = rp.run_item(client, ITEM, row) + assert client.calls == 1 + assert resumed["role"] == expected_role + assert rp.complete_row(resumed) + assert row["errors"] == {"judge": "temporary failure"} + + +def test_billing_failure_stops_before_next_detector(): + import pytest + + from leanbench.llm import LLMError + + rp = load("run_pilot") + + class Blocked: + calls = 0 + + def complete_json(self, messages): + self.calls += 1 + raise LLMError("HTTP 400: Arrearage overdue-payment") + + client = Blocked() + with pytest.raises(rp.ProviderBlocked) as caught: + rp.run_item(client, ITEM) + assert client.calls == 1 + assert "role" in caught.value.row["errors"] + assert "judge" not in caught.value.row["errors"] + + +def test_blocked_run_preserves_and_replaces_partial_row(tmp_path, monkeypatch): + import argparse + import json + + from leanbench.config import Settings + + rp = load("run_pilot") + args = argparse.Namespace(items=tmp_path / "items.jsonl", out=tmp_path / "results.jsonl", + max_calls=400, dry_run=False) + args.items.write_text(json.dumps(ITEM) + "\n") + partial = {"id": "x1", "compiled": True, "role": {"flagged": False}, + "errors": {"judge": "Arrearage"}} + + def blocked(client, item, previous): + raise rp.ProviderBlocked(partial) + + monkeypatch.setattr(rp, "run_item", blocked) + assert rp.execute(args, [ITEM], Settings()) == 2 + meta = json.loads(args.out.with_suffix(".meta.json").read_text()) + assert meta["status"] == "provider_blocked" + assert meta["completed_items"] == 0 + + def recover(client, item, previous): + assert previous["role"] == partial["role"] + return {**previous, "judge": {"faithful": True}, "errors": {}} + + monkeypatch.setattr(rp, "run_item", recover) + assert rp.execute(args, [ITEM], Settings()) == 0 + rows = [json.loads(line) for line in args.out.read_text().splitlines()] + assert len(rows) == 1 and rp.complete_row(rows[0]) + meta = json.loads(args.out.with_suffix(".meta.json").read_text()) + assert meta["completed_items"] == 1 and meta["status"] == "complete"