diff --git a/docs/experiments/P0-gpt-diagnostic.md b/docs/experiments/P0-gpt-diagnostic.md new file mode 100644 index 0000000..b29b2d2 --- /dev/null +++ b/docs/experiments/P0-gpt-diagnostic.md @@ -0,0 +1,127 @@ +# P0: full-cohort GPT-assisted diagnostic (2026-10-28) + +**All 65 items have a fresh source-role description, a fresh semantic judgment and a +completed deterministic alignment. This is a same-assistant diagnostic, not an independent +benchmark or a completion of the preregistered Qwen gate. No gate decision is issued.** + +## Scope and provenance + +The owner requested that the current GPT assistant reassess the entire cohort after the +Qwen run was interrupted by provider billing failures. Every item was reviewed again; +no Qwen detector output was reused, and the incomplete Qwen run was not patched with GPT +outputs. The earlier labels and Qwen files remain unchanged in the original worktree. +This branch starts at main `5d531c9` and does not depend on the separate billing-recovery PR. + +The source-role structures and four-way judgments were authored directly by the assistant +in this chat, frozen before computing the new alignment statistics, and replayed by an +offline script. They were not responses obtained through a GPT API endpoint. The exact +deployed model identifier, temperature and chat token usage are unavailable; they are not +invented. There were **zero new external model API calls** for this diagnostic, and no +DashScope credential was loaded. + +The assistant had already seen the earlier labels, Lean code, detector implementation and +aggregate compilation statistics. It also viewed passages and Lean together during this +review. Thus the source descriptions are **not a blinded source-only extraction** and the +new judgments are **not independent of the reference labels**. Reading only a passage when +writing a role does not remove prior context exposure. Syntax and proof defects are +separated from recoverable semantic meaning; no new Lean compilation or library API audit +was performed. An independent human review remains necessary for research claims. + +## Results for all 65 items + +| Fresh semantic judgment | Items | +|---|---:| +| Faithful | 25 | +| Minor drift | 13 | +| Wrong | 24 | +| Not formalizable from the extracted specification | 3 | +| Total | 65 | + +The strict binary assistant judge flags every verdict except faithful. The full four-way +judgment, error categories and an individual explanation are retained for every item. +Explanations and role descriptions are private because they paraphrase the source passages. + +The unchanged deterministic role matcher flagged **55/65** items. It flagged all **24** +items newly judged wrong, but also **16/25** newly judged faithful. These are comparisons +between dependent components of the same diagnostic, not an independently measured recall +or false-positive rate. They identify an over-sensitive diagnostic behavior worth auditing. + +Common conflict categories across all items include missing objects (41 items), degenerate +projections (15), goal mismatch (15), missing hypotheses (14), extra hypotheses (13), +quantifier conflicts (7) and type conflicts (5). Categories overlap. In particular, a named +source quantity can be computed inline in Lean, a product representation can replace an +abstract isomorphic group, and a bundled type can encode conditions without separate +binders. The current lexical matcher does not establish equivalence of those representations. +These are hypotheses for a later matcher audit, not measured causal explanations for every flag. +No matching threshold, concept table or authored assessment was changed after the scores +were inspected. + +## Relation to the frozen earlier AI labels + +The fresh four-way judgments agree with **59/65** earlier labels. Six changed: + +| Blind ID | Earlier AI label | Fresh judgment | +|---|---|---| +| P02 | Faithful | Minor drift | +| P18 | Faithful | Minor drift | +| P23 | Faithful | Minor drift | +| P34 | Faithful | Minor drift | +| P51 | Faithful | Minor drift | +| P57 | Wrong | Minor drift | + +The six changes concern representation, type/scope and coverage judgments. They demonstrate +annotation instability and should be independently adjudicated, not silently overwritten. +The 59/65 agreement is **not an accuracy estimate**. + +For debugging continuity, the summary contains confusion counts and Wilson intervals against +the frozen earlier AI labels. The primary comparison excludes earlier minor-drift and +not-formalizable labels (55 items); the secondary comparison includes minor drift as positive +(62 items). These tables are explicitly named `reference_agreement`. They cannot establish +that GPT or role alignment outperforms Qwen. The Qwen coverage is incomplete and this pass +has different provenance and no independent ground truth. `decision` is null; no GO, +PARTIAL or NO-GO is computed. + +## Artifacts and replay + +Tracked, text-free artifacts: + +- `experiments/P0-pilot/results/gpt-diagnostic-summary.json`: provenance, input/assessment/code + hashes, distributions, fixed matching thresholds and non-independent agreement statistics. +- `experiments/P0-pilot/results/gpt-diagnostic-items.json`: all 65 blind IDs, verdicts, error + categories, compile flags, role scores and conflict categories; no passages or explanations. +- `experiments/P0-pilot/assistant_diagnostic.py`: validates authored inputs and replays the + existing projection, lint, alignment and statistics code offline. +- `tests/test_assistant_diagnostic.py`: completeness, identity, schema, offline replay and + public-output privacy regressions using synthetic text. + +Private artifacts under the gitignored `experiments/P0-pilot/data/gpt-diagnostic/`: + +- `items.jsonl`: source-inclusive copy of the unchanged cohort. +- `assistant-assessments.json`: all newly authored source structures and judgments, frozen + before alignment statistics were inspected. +- `results.jsonl`: complete replay outputs for the 65 items. +- `review.html`: local, self-contained per-item source/Lean/reason/role/alignment review. +- `original-hashes.json`: snapshot of the earlier Qwen files and reference labels for + verifying that this work did not change them. + +Run from the repository root with the private files present: + +```sh +PYTHONPATH=. python3 experiments/P0-pilot/assistant_diagnostic.py \ + --items experiments/P0-pilot/data/gpt-diagnostic/items.jsonl \ + --key experiments/P0-pilot/labels/key.json \ + --assessments experiments/P0-pilot/data/gpt-diagnostic/assistant-assessments.json \ + --labels experiments/P0-pilot/labels/labels.json \ + --private-out experiments/P0-pilot/data/gpt-diagnostic \ + --summary experiments/P0-pilot/results/gpt-diagnostic-summary.json \ + --public-items experiments/P0-pilot/results/gpt-diagnostic-items.json +``` + +The replay is deterministic; it does not regenerate GPT judgments, call a model, or compile +Lean. Without the private assessment file, public readers can inspect the categorical +results but cannot reconstruct the authored descriptions and explanations from hashes. + +152 offline unit tests, repository-wide Ruff and diff checks passed locally without a Lean +or Docker build. Remote Python and real Lean verification use the owner-confirmed +`ubuntu24.04-x64-lean4.35` tag; the delivered PR records their current status. The existing +PR workflow skips the Docker image job. No Phase 1 work has started. diff --git a/experiments/P0-pilot/README.md b/experiments/P0-pilot/README.md index b302b47..58ab084 100644 --- a/experiments/P0-pilot/README.md +++ b/experiments/P0-pilot/README.md @@ -52,3 +52,16 @@ 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. + +## Separate GPT-assisted diagnostic + +The owner requested a complete 65-item reassessment by the current GPT assistant on +2026-10-28. This is separate from the incomplete Qwen run: no outputs are mixed and +neither the earlier labels nor Qwen files are overwritten. The assistant had prior +exposure to the reference labels and Lean; this is not blind or independent validation. +No GO/PARTIAL/NO-GO decision is issued. + +See `docs/experiments/P0-gpt-diagnostic.md` for all counts, limitations, artifact locations +and the offline replay command. The tracked `results/gpt-diagnostic-*.json` files contain +only categorical/numeric outputs and audit metadata. The authored source structures, +reasons and full review page stay in the ignored `data/gpt-diagnostic/` directory. diff --git a/experiments/P0-pilot/assistant_diagnostic.py b/experiments/P0-pilot/assistant_diagnostic.py new file mode 100644 index 0000000..7fa578a --- /dev/null +++ b/experiments/P0-pilot/assistant_diagnostic.py @@ -0,0 +1,200 @@ +"""Validate and replay a current-chat assistant review without calling any model. + +Private source schemas and reasons stay in data/. Public summaries contain only +categories, counts, numeric scores, hashes and an explicit non-independent provenance. +""" +from __future__ import annotations + +import argparse +import hashlib +import html +import json +import math +from collections import Counter +from pathlib import Path + +from leanbench.align import DEFAULT_THRESHOLD, GOAL_THRESHOLD, align +from leanbench.evalstats import auc, confusion, wilson +from leanbench.lint import lint +from leanbench.project import project +from leanbench.srcsimplex import parse_source_simplex + +VERDICTS = {"faithful", "minor_drift", "wrong", "not_formalizable"} +ERRORS = {"missing_hypothesis", "extra_hypothesis", "wrong_type", "quantifier", + "wrong_conclusion", "degenerate", "hallucinated_api", "other"} + + +def digest(path: Path) -> str: + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def finite(value): + if isinstance(value, dict): + return {k: finite(v) for k, v in value.items()} + if isinstance(value, (list, tuple)): + return [finite(v) for v in value] + if isinstance(value, float) and not math.isfinite(value): + return None + return value + + +def unique(rows, field): + indexed = {row[field]: row for row in rows} + if len(indexed) != len(rows): + raise ValueError(f"Duplicate {field}") + return indexed + + +def evaluate(items, key, assessment): + """Keep model-authored assessments separate from deterministic detector outputs.""" + by_id = unique(items, "id") + records = unique(assessment["records"], "blind_id") + if (not key or len(set(key.values())) != len(key) or set(records) != set(key) + or set(by_id) != set(key.values())): + raise ValueError("Items, key and assessments must cover the same cohort exactly once") + output = [] + for blind, item_id in key.items(): + item, record = by_id[item_id], records[blind] + if record["id"] != item_id or not item.get("source_text", "").strip(): + raise ValueError(f"Missing source text or mismatched item for {blind}") + judge = record["judge"] + if (judge.get("verdict") not in VERDICTS or type(judge.get("faithful")) is not bool + or judge["faithful"] != (judge["verdict"] == "faithful") + or not isinstance(judge.get("reason"), str) or not judge["reason"].strip() + or not isinstance(judge.get("errors"), list) + or not set(judge["errors"]) <= ERRORS): + raise ValueError(f"Invalid authored judgment for {blind}") + source = parse_source_simplex(record["source"]) + projection = project(item["lean_code"]) + alignment = align(source, projection) + output.append({"id": item_id, "blind_id": blind, + "source": source.as_dict(), "judge": judge, + "projection": projection.as_dict(), "role": alignment.as_dict(), + "lint": lint(projection), "compiled": bool(item.get("verified")), + "errors": {}}) + return output + + +def public_items(rows, labels): + if set(labels) != {row["blind_id"] for row in rows}: + raise ValueError("Reference labels must cover the entire cohort") + out = [] + for row in rows: + reference = labels[row["blind_id"]]["verdict"] + if reference not in VERDICTS: + raise ValueError("Invalid reference verdict") + out.append({"blind_id": row["blind_id"], "reference_verdict": reference, + "assistant_verdict": row["judge"]["verdict"], + "assistant_error_types": row["judge"]["errors"], + "verdict_agrees": reference == row["judge"]["verdict"], + "compiled": row["compiled"], "lint_flagged": bool(row["lint"]), + "role_flagged": row["role"]["flagged"], + "role_score": row["role"]["score"], + "role_conflict_types": row["role"]["errors"], + "source_role_count": len(row["source"]["roles"]), + "lean_role_count": len(row["projection"]["roles"]), + "degenerate_projection": row["projection"]["degenerate"]}) + return out + + +def agreement(rows, labels, secondary=False): + cohort = [r for r in rows if labels[r["blind_id"]]["verdict"] != "not_formalizable" + and (secondary or labels[r["blind_id"]]["verdict"] != "minor_drift")] + positives = {"wrong", "minor_drift"} if secondary else {"wrong"} + target = [labels[r["blind_id"]]["verdict"] in positives for r in cohort] + out = {} + for name, flags in { + "role": [r["role"]["flagged"] for r in cohort], + "assistant_judge": [not r["judge"]["faithful"] for r in cohort], + "lint": [bool(r["lint"]) for r in cohort], + "compile_only": [not r["compiled"] for r in cohort], + }.items(): + counts = confusion(flags, target) + out[name] = {**counts.as_dict(), "precision_ci": wilson(counts.tp, counts.tp + counts.fp)} + out["role"]["auc"] = auc([-r["role"]["score"] for r in cohort], target) + return {"n": len(cohort), "metrics_are_non_independent_reference_agreement": True, + "detectors": out} + + +def write_review(path, rows, items): + by_id = {r["id"]: r for r in items} + sections = [] + for row in rows: + item = by_id[row["id"]] + sections.append( + f'

{row["blind_id"]}

' + f'

Passage

{html.escape(item["source_text"])}
' + f'

Lean

{html.escape(item["lean_code"])}
' + f'

Fresh assistant judgment: {row["judge"]["verdict"]}

' + f'

{html.escape(row["judge"]["reason"])}

' + f'

Source roles

{html.escape(json.dumps(row["source"], indent=2, ensure_ascii=False))}
' + f'

Deterministic alignment

{html.escape(json.dumps(row["role"], indent=2, ensure_ascii=False))}
' + ) + path.write_text('' + 'P0 GPT-assisted diagnostic' + '

P0: 65-item GPT-assisted diagnostic

' + '

Private review. Same-assistant, non-blind diagnosis; no independent accuracy or gate decision. ' + 'Passages and model-derived descriptions must remain outside Git.

' + + ''.join(sections) + '', encoding="utf-8") + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--items", type=Path, required=True) + parser.add_argument("--key", type=Path, required=True) + parser.add_argument("--assessments", type=Path, required=True) + parser.add_argument("--labels", type=Path, required=True) + parser.add_argument("--private-out", type=Path, required=True) + parser.add_argument("--summary", type=Path, required=True) + parser.add_argument("--public-items", type=Path, required=True) + args = parser.parse_args() + if "data" not in args.private_out.parts: + parser.error("Private output must be under the gitignored data/ directory") + items = [json.loads(x) for x in args.items.read_text().splitlines() if x.strip()] + key = json.loads(args.key.read_text())["key"] + assessment = json.loads(args.assessments.read_text()) + provenance = assessment["provenance"] + if (provenance["items_sha256"] != digest(args.items) + or provenance["key_sha256"] != digest(args.key)): + parser.error("Authored review is bound to different inputs or blind key") + rows = evaluate(items, key, assessment) + labels = json.loads(args.labels.read_text())["labels"] + public = public_items(rows, labels) + summary = { + "experiment": "P0-GPT-diagnostic", "status": "complete", "n": len(rows), + "provenance": provenance, "decision": None, + "decision_withheld_reason": "Same-assistant, non-blind diagnostic; not the preregistered Qwen pilot or independent ground-truth validation.", + "hashes": {"items": digest(args.items), "key": digest(args.key), + "assessments": digest(args.assessments), "reference_labels": digest(args.labels), + "replay_script": digest(Path(__file__)), + **{f"leanbench/{name}.py": digest(Path(__file__).resolve().parents[2] / "leanbench" / f"{name}.py") + for name in ("align", "project", "srcsimplex", "lint")}}, + "fixed_thresholds": {"matching": DEFAULT_THRESHOLD, "goal": GOAL_THRESHOLD}, + "verdict_counts": dict(Counter(r["judge"]["verdict"] for r in rows)), + "role_flagged": sum(r["role"]["flagged"] for r in rows), + "lint_flagged": sum(bool(r["lint"]) for r in rows), + "compiled": sum(r["compiled"] for r in rows), + "degenerate_projection": sum(r["projection"]["degenerate"] for r in rows), + "exact_verdict_agreement": sum(r["verdict_agrees"] for r in public), + "changed_verdicts": [r["blind_id"] for r in public if not r["verdict_agrees"]], + "primary_reference_agreement": agreement(rows, labels), + "secondary_reference_agreement": agreement(rows, labels, secondary=True), + "role_flagged_by_new_verdict": {v: {"n": sum(r["judge"]["verdict"] == v for r in rows), + "flagged": sum(r["judge"]["verdict"] == v and r["role"]["flagged"] for r in rows)} + for v in sorted(VERDICTS)}, + } + args.private_out.mkdir(parents=True, exist_ok=True) + (args.private_out / "results.jsonl").write_text(''.join(json.dumps(r, ensure_ascii=False) + '\n' for r in rows)) + write_review(args.private_out / "review.html", rows, items) + args.summary.parent.mkdir(parents=True, exist_ok=True) + args.public_items.parent.mkdir(parents=True, exist_ok=True) + args.summary.write_text(json.dumps(finite(summary), indent=2, allow_nan=False) + '\n') + args.public_items.write_text(json.dumps(public, indent=2, allow_nan=False) + '\n') + print(json.dumps({k: summary[k] for k in ("n", "status", "verdict_counts", "role_flagged", "exact_verdict_agreement", "decision")})) + + +if __name__ == "__main__": + main() diff --git a/experiments/P0-pilot/results/gpt-diagnostic-items.json b/experiments/P0-pilot/results/gpt-diagnostic-items.json new file mode 100644 index 0000000..feb7dfa --- /dev/null +++ b/experiments/P0-pilot/results/gpt-diagnostic-items.json @@ -0,0 +1,1253 @@ +[ + { + "blind_id": "P01", + "reference_verdict": "faithful", + "assistant_verdict": "faithful", + "assistant_error_types": [], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": false, + "role_flagged": true, + "role_score": 0.0, + "role_conflict_types": [ + "missing_object", + "missing_hypothesis", + "extra_object", + "goal_mismatch" + ], + "source_role_count": 4, + "lean_role_count": 2, + "degenerate_projection": false + }, + { + "blind_id": "P02", + "reference_verdict": "faithful", + "assistant_verdict": "minor_drift", + "assistant_error_types": [ + "wrong_type" + ], + "verdict_agrees": false, + "compiled": false, + "lint_flagged": false, + "role_flagged": true, + "role_score": 0.667, + "role_conflict_types": [ + "missing_object" + ], + "source_role_count": 4, + "lean_role_count": 2, + "degenerate_projection": false + }, + { + "blind_id": "P03", + "reference_verdict": "faithful", + "assistant_verdict": "faithful", + "assistant_error_types": [], + "verdict_agrees": true, + "compiled": true, + "lint_flagged": false, + "role_flagged": true, + "role_score": 0.0, + "role_conflict_types": [ + "missing_object", + "extra_hypothesis", + "goal_mismatch" + ], + "source_role_count": 3, + "lean_role_count": 3, + "degenerate_projection": false + }, + { + "blind_id": "P04", + "reference_verdict": "faithful", + "assistant_verdict": "faithful", + "assistant_error_types": [], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": false, + "role_flagged": false, + "role_score": 1.0, + "role_conflict_types": [], + "source_role_count": 3, + "lean_role_count": 3, + "degenerate_projection": false + }, + { + "blind_id": "P05", + "reference_verdict": "faithful", + "assistant_verdict": "faithful", + "assistant_error_types": [], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": false, + "role_flagged": true, + "role_score": 0.444, + "role_conflict_types": [ + "missing_object", + "missing_hypothesis", + "goal_mismatch", + "quantifier" + ], + "source_role_count": 6, + "lean_role_count": 3, + "degenerate_projection": false + }, + { + "blind_id": "P06", + "reference_verdict": "faithful", + "assistant_verdict": "faithful", + "assistant_error_types": [], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": false, + "role_flagged": false, + "role_score": 1.0, + "role_conflict_types": [], + "source_role_count": 4, + "lean_role_count": 4, + "degenerate_projection": false + }, + { + "blind_id": "P07", + "reference_verdict": "wrong", + "assistant_verdict": "wrong", + "assistant_error_types": [ + "degenerate", + "wrong_conclusion" + ], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": false, + "role_flagged": true, + "role_score": 0.615, + "role_conflict_types": [ + "type_conflict", + "missing_object", + "missing_hypothesis", + "extra_hypothesis" + ], + "source_role_count": 6, + "lean_role_count": 7, + "degenerate_projection": false + }, + { + "blind_id": "P08", + "reference_verdict": "faithful", + "assistant_verdict": "faithful", + "assistant_error_types": [], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": false, + "role_flagged": true, + "role_score": 0.667, + "role_conflict_types": [ + "missing_object", + "goal_mismatch" + ], + "source_role_count": 6, + "lean_role_count": 3, + "degenerate_projection": false + }, + { + "blind_id": "P09", + "reference_verdict": "wrong", + "assistant_verdict": "wrong", + "assistant_error_types": [ + "wrong_type", + "wrong_conclusion" + ], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": true, + "role_flagged": true, + "role_score": 0.222, + "role_conflict_types": [ + "degenerate", + "missing_object" + ], + "source_role_count": 8, + "lean_role_count": 1, + "degenerate_projection": true + }, + { + "blind_id": "P10", + "reference_verdict": "faithful", + "assistant_verdict": "faithful", + "assistant_error_types": [], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": false, + "role_flagged": false, + "role_score": 1.0, + "role_conflict_types": [], + "source_role_count": 4, + "lean_role_count": 4, + "degenerate_projection": false + }, + { + "blind_id": "P11", + "reference_verdict": "faithful", + "assistant_verdict": "faithful", + "assistant_error_types": [], + "verdict_agrees": true, + "compiled": true, + "lint_flagged": false, + "role_flagged": true, + "role_score": 1.0, + "role_conflict_types": [ + "missing_object" + ], + "source_role_count": 5, + "lean_role_count": 3, + "degenerate_projection": false + }, + { + "blind_id": "P12", + "reference_verdict": "not_formalizable", + "assistant_verdict": "not_formalizable", + "assistant_error_types": [ + "other" + ], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": true, + "role_flagged": true, + "role_score": 0.5, + "role_conflict_types": [ + "degenerate", + "missing_object", + "quantifier" + ], + "source_role_count": 3, + "lean_role_count": 1, + "degenerate_projection": true + }, + { + "blind_id": "P13", + "reference_verdict": "minor_drift", + "assistant_verdict": "minor_drift", + "assistant_error_types": [ + "wrong_type" + ], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": false, + "role_flagged": true, + "role_score": 0.889, + "role_conflict_types": [ + "missing_object" + ], + "source_role_count": 5, + "lean_role_count": 4, + "degenerate_projection": false + }, + { + "blind_id": "P14", + "reference_verdict": "wrong", + "assistant_verdict": "wrong", + "assistant_error_types": [ + "wrong_conclusion" + ], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": false, + "role_flagged": true, + "role_score": 0.8, + "role_conflict_types": [ + "missing_object" + ], + "source_role_count": 3, + "lean_role_count": 2, + "degenerate_projection": false + }, + { + "blind_id": "P15", + "reference_verdict": "faithful", + "assistant_verdict": "faithful", + "assistant_error_types": [], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": false, + "role_flagged": false, + "role_score": 0.857, + "role_conflict_types": [ + "extra_object" + ], + "source_role_count": 3, + "lean_role_count": 4, + "degenerate_projection": false + }, + { + "blind_id": "P16", + "reference_verdict": "faithful", + "assistant_verdict": "faithful", + "assistant_error_types": [], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": false, + "role_flagged": true, + "role_score": 0.833, + "role_conflict_types": [ + "missing_object", + "missing_hypothesis", + "extra_object" + ], + "source_role_count": 8, + "lean_role_count": 4, + "degenerate_projection": false + }, + { + "blind_id": "P17", + "reference_verdict": "wrong", + "assistant_verdict": "wrong", + "assistant_error_types": [ + "wrong_conclusion" + ], + "verdict_agrees": true, + "compiled": true, + "lint_flagged": true, + "role_flagged": true, + "role_score": 0.286, + "role_conflict_types": [ + "degenerate", + "missing_object" + ], + "source_role_count": 6, + "lean_role_count": 1, + "degenerate_projection": true + }, + { + "blind_id": "P18", + "reference_verdict": "faithful", + "assistant_verdict": "minor_drift", + "assistant_error_types": [ + "wrong_type" + ], + "verdict_agrees": false, + "compiled": false, + "lint_flagged": true, + "role_flagged": true, + "role_score": 0.4, + "role_conflict_types": [ + "degenerate", + "missing_object" + ], + "source_role_count": 4, + "lean_role_count": 1, + "degenerate_projection": true + }, + { + "blind_id": "P19", + "reference_verdict": "minor_drift", + "assistant_verdict": "minor_drift", + "assistant_error_types": [ + "wrong_type" + ], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": true, + "role_flagged": true, + "role_score": 0.333, + "role_conflict_types": [ + "missing_object", + "extra_object", + "goal_mismatch" + ], + "source_role_count": 3, + "lean_role_count": 3, + "degenerate_projection": false + }, + { + "blind_id": "P20", + "reference_verdict": "faithful", + "assistant_verdict": "faithful", + "assistant_error_types": [], + "verdict_agrees": true, + "compiled": true, + "lint_flagged": false, + "role_flagged": true, + "role_score": 0.727, + "role_conflict_types": [ + "missing_object", + "goal_mismatch" + ], + "source_role_count": 6, + "lean_role_count": 5, + "degenerate_projection": false + }, + { + "blind_id": "P21", + "reference_verdict": "minor_drift", + "assistant_verdict": "minor_drift", + "assistant_error_types": [ + "wrong_type" + ], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": false, + "role_flagged": true, + "role_score": 1.0, + "role_conflict_types": [ + "missing_object" + ], + "source_role_count": 5, + "lean_role_count": 3, + "degenerate_projection": false + }, + { + "blind_id": "P22", + "reference_verdict": "faithful", + "assistant_verdict": "faithful", + "assistant_error_types": [], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": false, + "role_flagged": true, + "role_score": 0.8, + "role_conflict_types": [ + "goal_mismatch" + ], + "source_role_count": 3, + "lean_role_count": 2, + "degenerate_projection": false + }, + { + "blind_id": "P23", + "reference_verdict": "faithful", + "assistant_verdict": "minor_drift", + "assistant_error_types": [ + "wrong_type" + ], + "verdict_agrees": false, + "compiled": false, + "lint_flagged": true, + "role_flagged": true, + "role_score": 0.9, + "role_conflict_types": [ + "type_conflict", + "extra_hypothesis" + ], + "source_role_count": 9, + "lean_role_count": 11, + "degenerate_projection": false + }, + { + "blind_id": "P24", + "reference_verdict": "wrong", + "assistant_verdict": "wrong", + "assistant_error_types": [ + "degenerate", + "wrong_conclusion" + ], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": true, + "role_flagged": true, + "role_score": 0.5, + "role_conflict_types": [ + "degenerate", + "missing_object" + ], + "source_role_count": 3, + "lean_role_count": 1, + "degenerate_projection": true + }, + { + "blind_id": "P25", + "reference_verdict": "faithful", + "assistant_verdict": "faithful", + "assistant_error_types": [], + "verdict_agrees": true, + "compiled": true, + "lint_flagged": false, + "role_flagged": true, + "role_score": 0.909, + "role_conflict_types": [ + "extra_hypothesis" + ], + "source_role_count": 5, + "lean_role_count": 6, + "degenerate_projection": false + }, + { + "blind_id": "P26", + "reference_verdict": "wrong", + "assistant_verdict": "wrong", + "assistant_error_types": [ + "extra_hypothesis", + "missing_hypothesis" + ], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": false, + "role_flagged": true, + "role_score": 0.769, + "role_conflict_types": [ + "extra_hypothesis", + "goal_mismatch" + ], + "source_role_count": 6, + "lean_role_count": 7, + "degenerate_projection": false + }, + { + "blind_id": "P27", + "reference_verdict": "wrong", + "assistant_verdict": "wrong", + "assistant_error_types": [ + "wrong_conclusion" + ], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": true, + "role_flagged": true, + "role_score": 0.333, + "role_conflict_types": [ + "degenerate", + "missing_object", + "missing_hypothesis" + ], + "source_role_count": 5, + "lean_role_count": 1, + "degenerate_projection": true + }, + { + "blind_id": "P28", + "reference_verdict": "wrong", + "assistant_verdict": "wrong", + "assistant_error_types": [ + "wrong_type", + "wrong_conclusion" + ], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": true, + "role_flagged": true, + "role_score": 0.333, + "role_conflict_types": [ + "degenerate", + "missing_object" + ], + "source_role_count": 5, + "lean_role_count": 1, + "degenerate_projection": true + }, + { + "blind_id": "P29", + "reference_verdict": "faithful", + "assistant_verdict": "faithful", + "assistant_error_types": [], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": false, + "role_flagged": true, + "role_score": 0.833, + "role_conflict_types": [ + "missing_object", + "goal_mismatch" + ], + "source_role_count": 7, + "lean_role_count": 5, + "degenerate_projection": false + }, + { + "blind_id": "P30", + "reference_verdict": "wrong", + "assistant_verdict": "wrong", + "assistant_error_types": [ + "wrong_type" + ], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": false, + "role_flagged": true, + "role_score": 0.941, + "role_conflict_types": [ + "type_conflict", + "goal_mismatch" + ], + "source_role_count": 9, + "lean_role_count": 8, + "degenerate_projection": false + }, + { + "blind_id": "P31", + "reference_verdict": "not_formalizable", + "assistant_verdict": "not_formalizable", + "assistant_error_types": [ + "other" + ], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": false, + "role_flagged": false, + "role_score": 0.8, + "role_conflict_types": [ + "extra_object" + ], + "source_role_count": 2, + "lean_role_count": 3, + "degenerate_projection": false + }, + { + "blind_id": "P32", + "reference_verdict": "wrong", + "assistant_verdict": "wrong", + "assistant_error_types": [ + "degenerate", + "wrong_conclusion" + ], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": true, + "role_flagged": true, + "role_score": 1.0, + "role_conflict_types": [ + "quantifier" + ], + "source_role_count": 3, + "lean_role_count": 3, + "degenerate_projection": false + }, + { + "blind_id": "P33", + "reference_verdict": "faithful", + "assistant_verdict": "faithful", + "assistant_error_types": [], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": false, + "role_flagged": false, + "role_score": 1.0, + "role_conflict_types": [], + "source_role_count": 3, + "lean_role_count": 3, + "degenerate_projection": false + }, + { + "blind_id": "P34", + "reference_verdict": "faithful", + "assistant_verdict": "minor_drift", + "assistant_error_types": [ + "wrong_type" + ], + "verdict_agrees": false, + "compiled": false, + "lint_flagged": true, + "role_flagged": true, + "role_score": 0.5, + "role_conflict_types": [ + "degenerate", + "missing_object" + ], + "source_role_count": 3, + "lean_role_count": 1, + "degenerate_projection": true + }, + { + "blind_id": "P35", + "reference_verdict": "wrong", + "assistant_verdict": "wrong", + "assistant_error_types": [ + "wrong_type", + "quantifier" + ], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": false, + "role_flagged": true, + "role_score": 1.0, + "role_conflict_types": [ + "type_conflict", + "extra_hypothesis", + "quantifier" + ], + "source_role_count": 5, + "lean_role_count": 5, + "degenerate_projection": false + }, + { + "blind_id": "P36", + "reference_verdict": "wrong", + "assistant_verdict": "wrong", + "assistant_error_types": [ + "wrong_type", + "wrong_conclusion" + ], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": false, + "role_flagged": true, + "role_score": 0.571, + "role_conflict_types": [ + "missing_object", + "extra_hypothesis" + ], + "source_role_count": 4, + "lean_role_count": 3, + "degenerate_projection": false + }, + { + "blind_id": "P37", + "reference_verdict": "wrong", + "assistant_verdict": "wrong", + "assistant_error_types": [ + "degenerate", + "wrong_conclusion" + ], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": true, + "role_flagged": true, + "role_score": 0.286, + "role_conflict_types": [ + "missing_object", + "type_conflict", + "missing_hypothesis", + "goal_mismatch" + ], + "source_role_count": 5, + "lean_role_count": 2, + "degenerate_projection": false + }, + { + "blind_id": "P38", + "reference_verdict": "wrong", + "assistant_verdict": "wrong", + "assistant_error_types": [ + "missing_hypothesis" + ], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": false, + "role_flagged": true, + "role_score": 0.909, + "role_conflict_types": [ + "missing_hypothesis" + ], + "source_role_count": 6, + "lean_role_count": 5, + "degenerate_projection": false + }, + { + "blind_id": "P39", + "reference_verdict": "wrong", + "assistant_verdict": "wrong", + "assistant_error_types": [ + "wrong_type", + "wrong_conclusion" + ], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": false, + "role_flagged": true, + "role_score": 0.8, + "role_conflict_types": [ + "missing_object" + ], + "source_role_count": 3, + "lean_role_count": 2, + "degenerate_projection": false + }, + { + "blind_id": "P40", + "reference_verdict": "faithful", + "assistant_verdict": "faithful", + "assistant_error_types": [], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": false, + "role_flagged": true, + "role_score": 0.571, + "role_conflict_types": [ + "missing_object" + ], + "source_role_count": 5, + "lean_role_count": 2, + "degenerate_projection": false + }, + { + "blind_id": "P41", + "reference_verdict": "wrong", + "assistant_verdict": "wrong", + "assistant_error_types": [ + "extra_hypothesis" + ], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": false, + "role_flagged": true, + "role_score": 0.667, + "role_conflict_types": [ + "missing_object", + "extra_hypothesis" + ], + "source_role_count": 3, + "lean_role_count": 3, + "degenerate_projection": false + }, + { + "blind_id": "P42", + "reference_verdict": "wrong", + "assistant_verdict": "wrong", + "assistant_error_types": [ + "wrong_conclusion", + "missing_hypothesis" + ], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": true, + "role_flagged": true, + "role_score": 0.8, + "role_conflict_types": [ + "missing_hypothesis", + "extra_object" + ], + "source_role_count": 5, + "lean_role_count": 5, + "degenerate_projection": false + }, + { + "blind_id": "P43", + "reference_verdict": "faithful", + "assistant_verdict": "faithful", + "assistant_error_types": [], + "verdict_agrees": true, + "compiled": true, + "lint_flagged": false, + "role_flagged": true, + "role_score": 0.5, + "role_conflict_types": [ + "missing_hypothesis", + "extra_object", + "extra_hypothesis", + "quantifier" + ], + "source_role_count": 3, + "lean_role_count": 5, + "degenerate_projection": false + }, + { + "blind_id": "P44", + "reference_verdict": "faithful", + "assistant_verdict": "faithful", + "assistant_error_types": [], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": false, + "role_flagged": true, + "role_score": 0.333, + "role_conflict_types": [ + "missing_object", + "goal_mismatch" + ], + "source_role_count": 4, + "lean_role_count": 2, + "degenerate_projection": false + }, + { + "blind_id": "P45", + "reference_verdict": "wrong", + "assistant_verdict": "wrong", + "assistant_error_types": [ + "quantifier", + "wrong_conclusion" + ], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": true, + "role_flagged": true, + "role_score": 0.5, + "role_conflict_types": [ + "degenerate", + "missing_object", + "missing_hypothesis" + ], + "source_role_count": 3, + "lean_role_count": 1, + "degenerate_projection": true + }, + { + "blind_id": "P46", + "reference_verdict": "wrong", + "assistant_verdict": "wrong", + "assistant_error_types": [ + "wrong_type", + "wrong_conclusion" + ], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": true, + "role_flagged": true, + "role_score": 0.667, + "role_conflict_types": [ + "degenerate", + "missing_object" + ], + "source_role_count": 2, + "lean_role_count": 1, + "degenerate_projection": true + }, + { + "blind_id": "P47", + "reference_verdict": "minor_drift", + "assistant_verdict": "minor_drift", + "assistant_error_types": [ + "wrong_conclusion" + ], + "verdict_agrees": true, + "compiled": true, + "lint_flagged": false, + "role_flagged": true, + "role_score": 0.8, + "role_conflict_types": [ + "missing_object" + ], + "source_role_count": 3, + "lean_role_count": 2, + "degenerate_projection": false + }, + { + "blind_id": "P48", + "reference_verdict": "faithful", + "assistant_verdict": "faithful", + "assistant_error_types": [], + "verdict_agrees": true, + "compiled": true, + "lint_flagged": false, + "role_flagged": false, + "role_score": 1.0, + "role_conflict_types": [], + "source_role_count": 5, + "lean_role_count": 5, + "degenerate_projection": false + }, + { + "blind_id": "P49", + "reference_verdict": "faithful", + "assistant_verdict": "faithful", + "assistant_error_types": [], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": false, + "role_flagged": false, + "role_score": 1.0, + "role_conflict_types": [], + "source_role_count": 3, + "lean_role_count": 3, + "degenerate_projection": false + }, + { + "blind_id": "P50", + "reference_verdict": "faithful", + "assistant_verdict": "faithful", + "assistant_error_types": [], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": false, + "role_flagged": true, + "role_score": 0.286, + "role_conflict_types": [ + "missing_object", + "missing_hypothesis", + "goal_mismatch" + ], + "source_role_count": 5, + "lean_role_count": 2, + "degenerate_projection": false + }, + { + "blind_id": "P51", + "reference_verdict": "faithful", + "assistant_verdict": "minor_drift", + "assistant_error_types": [ + "wrong_type" + ], + "verdict_agrees": false, + "compiled": false, + "lint_flagged": true, + "role_flagged": true, + "role_score": 0.5, + "role_conflict_types": [ + "degenerate", + "missing_object" + ], + "source_role_count": 3, + "lean_role_count": 1, + "degenerate_projection": true + }, + { + "blind_id": "P52", + "reference_verdict": "minor_drift", + "assistant_verdict": "minor_drift", + "assistant_error_types": [ + "degenerate", + "wrong_conclusion" + ], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": false, + "role_flagged": true, + "role_score": 0.8, + "role_conflict_types": [ + "missing_object", + "quantifier" + ], + "source_role_count": 3, + "lean_role_count": 2, + "degenerate_projection": false + }, + { + "blind_id": "P53", + "reference_verdict": "minor_drift", + "assistant_verdict": "minor_drift", + "assistant_error_types": [ + "extra_hypothesis" + ], + "verdict_agrees": true, + "compiled": true, + "lint_flagged": false, + "role_flagged": true, + "role_score": 0.5, + "role_conflict_types": [ + "goal_mismatch" + ], + "source_role_count": 2, + "lean_role_count": 2, + "degenerate_projection": false + }, + { + "blind_id": "P54", + "reference_verdict": "wrong", + "assistant_verdict": "wrong", + "assistant_error_types": [ + "wrong_type" + ], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": false, + "role_flagged": true, + "role_score": 0.75, + "role_conflict_types": [ + "missing_object", + "extra_hypothesis" + ], + "source_role_count": 4, + "lean_role_count": 4, + "degenerate_projection": false + }, + { + "blind_id": "P55", + "reference_verdict": "faithful", + "assistant_verdict": "faithful", + "assistant_error_types": [], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": false, + "role_flagged": true, + "role_score": 1.0, + "role_conflict_types": [ + "extra_hypothesis" + ], + "source_role_count": 4, + "lean_role_count": 4, + "degenerate_projection": false + }, + { + "blind_id": "P56", + "reference_verdict": "not_formalizable", + "assistant_verdict": "not_formalizable", + "assistant_error_types": [ + "other" + ], + "verdict_agrees": true, + "compiled": true, + "lint_flagged": true, + "role_flagged": true, + "role_score": 0.5, + "role_conflict_types": [ + "degenerate", + "missing_object" + ], + "source_role_count": 3, + "lean_role_count": 1, + "degenerate_projection": true + }, + { + "blind_id": "P57", + "reference_verdict": "wrong", + "assistant_verdict": "minor_drift", + "assistant_error_types": [ + "wrong_conclusion" + ], + "verdict_agrees": false, + "compiled": false, + "lint_flagged": false, + "role_flagged": true, + "role_score": 0.6, + "role_conflict_types": [ + "missing_object", + "goal_mismatch" + ], + "source_role_count": 6, + "lean_role_count": 4, + "degenerate_projection": false + }, + { + "blind_id": "P58", + "reference_verdict": "wrong", + "assistant_verdict": "wrong", + "assistant_error_types": [ + "wrong_type" + ], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": true, + "role_flagged": true, + "role_score": 0.5, + "role_conflict_types": [ + "degenerate", + "missing_object", + "quantifier" + ], + "source_role_count": 3, + "lean_role_count": 1, + "degenerate_projection": true + }, + { + "blind_id": "P59", + "reference_verdict": "minor_drift", + "assistant_verdict": "minor_drift", + "assistant_error_types": [ + "wrong_type" + ], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": true, + "role_flagged": true, + "role_score": 0.75, + "role_conflict_types": [ + "missing_hypothesis", + "extra_object" + ], + "source_role_count": 4, + "lean_role_count": 4, + "degenerate_projection": false + }, + { + "blind_id": "P60", + "reference_verdict": "wrong", + "assistant_verdict": "wrong", + "assistant_error_types": [ + "wrong_type", + "missing_hypothesis" + ], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": false, + "role_flagged": true, + "role_score": 0.25, + "role_conflict_types": [ + "missing_object", + "missing_hypothesis", + "extra_object", + "extra_hypothesis" + ], + "source_role_count": 5, + "lean_role_count": 3, + "degenerate_projection": false + }, + { + "blind_id": "P61", + "reference_verdict": "faithful", + "assistant_verdict": "faithful", + "assistant_error_types": [], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": true, + "role_flagged": true, + "role_score": 0.286, + "role_conflict_types": [ + "degenerate", + "missing_object", + "missing_hypothesis" + ], + "source_role_count": 6, + "lean_role_count": 1, + "degenerate_projection": true + }, + { + "blind_id": "P62", + "reference_verdict": "faithful", + "assistant_verdict": "faithful", + "assistant_error_types": [], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": false, + "role_flagged": false, + "role_score": 0.857, + "role_conflict_types": [ + "extra_object" + ], + "source_role_count": 3, + "lean_role_count": 4, + "degenerate_projection": false + }, + { + "blind_id": "P63", + "reference_verdict": "faithful", + "assistant_verdict": "faithful", + "assistant_error_types": [], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": false, + "role_flagged": false, + "role_score": 1.0, + "role_conflict_types": [], + "source_role_count": 6, + "lean_role_count": 6, + "degenerate_projection": false + }, + { + "blind_id": "P64", + "reference_verdict": "wrong", + "assistant_verdict": "wrong", + "assistant_error_types": [ + "extra_hypothesis", + "missing_hypothesis" + ], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": false, + "role_flagged": true, + "role_score": 0.875, + "role_conflict_types": [ + "extra_object", + "extra_hypothesis" + ], + "source_role_count": 7, + "lean_role_count": 9, + "degenerate_projection": false + }, + { + "blind_id": "P65", + "reference_verdict": "wrong", + "assistant_verdict": "wrong", + "assistant_error_types": [ + "degenerate", + "wrong_conclusion" + ], + "verdict_agrees": true, + "compiled": false, + "lint_flagged": true, + "role_flagged": true, + "role_score": 0.5, + "role_conflict_types": [ + "degenerate", + "missing_object" + ], + "source_role_count": 3, + "lean_role_count": 1, + "degenerate_projection": true + } +] diff --git a/experiments/P0-pilot/results/gpt-diagnostic-summary.json b/experiments/P0-pilot/results/gpt-diagnostic-summary.json new file mode 100644 index 0000000..49ac8ec --- /dev/null +++ b/experiments/P0-pilot/results/gpt-diagnostic-summary.json @@ -0,0 +1,275 @@ +{ + "experiment": "P0-GPT-diagnostic", + "status": "complete", + "n": 65, + "provenance": { + "run_kind": "current-chat assistant-authored diagnostic; not an API benchmark", + "evaluator": "Codex GPT assistant; exact deployed model identifier unavailable", + "authored_at": "2026-10-28T11:23:06.275167+00:00", + "items_sha256": "487ecd22919a5e3b0174a2846ab8fe7c0daf4d3feccccf8ea6571aec04c41bed", + "key_sha256": "f827cac92ee4e907554fadcc7c0e006ef2b829350f74e7f8b54ca11945e62836", + "reference_labels_seen_in_prior_chat": true, + "lean_seen_while_authoring_source_roles": true, + "new_external_api_calls": 0, + "assistant_token_usage": null, + "limitations": [ + "Same assistant previously authored the reference labels; agreement is not independent accuracy.", + "Prior context contains the earlier review and detector code. This is not a blinded source-only extraction or a fresh-model replicate.", + "All judgments are manually authored in this chat, not responses from a GPT API endpoint.", + "Semantics are assessed conditionally on recoverable notation. No new Lean compilation or library API audit is performed.", + "The strict Boolean judge flags all verdicts except faithful, including not_formalizable; four-way verdicts are also retained." + ] + }, + "decision": null, + "decision_withheld_reason": "Same-assistant, non-blind diagnostic; not the preregistered Qwen pilot or independent ground-truth validation.", + "hashes": { + "items": "487ecd22919a5e3b0174a2846ab8fe7c0daf4d3feccccf8ea6571aec04c41bed", + "key": "f827cac92ee4e907554fadcc7c0e006ef2b829350f74e7f8b54ca11945e62836", + "assessments": "f12735802ba0d4d94b776a91581a13a508eab0ce90ba8973a6c9c4e4d1390272", + "reference_labels": "1552dba85e75426799151384e7e28c9a0b1072ed4c862df0876df89920d2a638", + "replay_script": "5c02e3d26761ce0b4e38d4be9e65b95bfd8db048c9c7c73edaac17e654e10c0f", + "leanbench/align.py": "730e44f1158e6e441e4745dff7324e565b89b6e5148017c3fd93f4c69c22c9ce", + "leanbench/project.py": "8ed76924b463ba418ceb732d0fcb6c572a548d94fe7f23759c67746da24d9430", + "leanbench/srcsimplex.py": "d10b785299ceb17cadc4e97737eef74183ed390d04b4571a702cd4fd42b069d0", + "leanbench/lint.py": "4396e879312f370cd70beeffcbd7ffeab8a41ee1704cc1f235dbbcd6e843fd68" + }, + "fixed_thresholds": { + "matching": 0.3, + "goal": 0.2 + }, + "verdict_counts": { + "faithful": 25, + "minor_drift": 13, + "wrong": 24, + "not_formalizable": 3 + }, + "role_flagged": 55, + "lint_flagged": 21, + "compiled": 10, + "degenerate_projection": 15, + "exact_verdict_agreement": 59, + "changed_verdicts": [ + "P02", + "P18", + "P23", + "P34", + "P51", + "P57" + ], + "primary_reference_agreement": { + "n": 55, + "metrics_are_non_independent_reference_agreement": true, + "detectors": { + "role": { + "tp": 25, + "fp": 21, + "fn": 0, + "tn": 9, + "n": 55, + "recall": 1.0, + "precision": 0.5434782608695652, + "false_flag_rate": 0.7, + "f1": 0.704225352112676, + "recall_ci": [ + 0.8668035060468213, + 1.0 + ], + "false_flag_ci": [ + 0.5212387898833981, + 0.8333543735604105 + ], + "precision_ci": [ + 0.4017993496608042, + 0.67845489578878 + ], + "auc": 0.61 + }, + "assistant_judge": { + "tp": 25, + "fp": 5, + "fn": 0, + "tn": 25, + "n": 55, + "recall": 1.0, + "precision": 0.8333333333333334, + "false_flag_rate": 0.16666666666666666, + "f1": 0.9090909090909091, + "recall_ci": [ + 0.8668035060468213, + 1.0 + ], + "false_flag_ci": [ + 0.07336434240351683, + 0.33564705185680177 + ], + "precision_ci": [ + 0.6643529481431982, + 0.9266356575964831 + ] + }, + "lint": { + "tp": 12, + "fp": 5, + "fn": 13, + "tn": 25, + "n": 55, + "recall": 0.48, + "precision": 0.7058823529411765, + "false_flag_rate": 0.16666666666666666, + "f1": 0.5714285714285713, + "recall_ci": [ + 0.30031003928960015, + 0.6650178204685269 + ], + "false_flag_ci": [ + 0.07336434240351683, + 0.33564705185680177 + ], + "precision_ci": [ + 0.468664666737861, + 0.8672020613444361 + ] + }, + "compile_only": { + "tp": 24, + "fp": 24, + "fn": 1, + "tn": 6, + "n": 55, + "recall": 0.96, + "precision": 0.5, + "false_flag_rate": 0.8, + "f1": 0.6575342465753424, + "recall_ci": [ + 0.8045552759497747, + 0.9929039496133008 + ], + "false_flag_ci": [ + 0.6269395261897256, + 0.9049502189759876 + ], + "precision_ci": [ + 0.36389098932037767, + 0.6361090106796223 + ] + } + } + }, + "secondary_reference_agreement": { + "n": 62, + "metrics_are_non_independent_reference_agreement": true, + "detectors": { + "role": { + "tp": 32, + "fp": 21, + "fn": 0, + "tn": 9, + "n": 62, + "recall": 1.0, + "precision": 0.6037735849056604, + "false_flag_rate": 0.7, + "f1": 0.7529411764705882, + "recall_ci": [ + 0.8928172849426366, + 1.0 + ], + "false_flag_ci": [ + 0.5212387898833981, + 0.8333543735604105 + ], + "precision_ci": [ + 0.4694123578888073, + 0.7241078808096105 + ], + "auc": 0.590625 + }, + "assistant_judge": { + "tp": 32, + "fp": 5, + "fn": 0, + "tn": 25, + "n": 62, + "recall": 1.0, + "precision": 0.8648648648648649, + "false_flag_rate": 0.16666666666666666, + "f1": 0.927536231884058, + "recall_ci": [ + 0.8928172849426366, + 1.0 + ], + "false_flag_ci": [ + 0.07336434240351683, + 0.33564705185680177 + ], + "precision_ci": [ + 0.7202227252929444, + 0.9408679273749238 + ] + }, + "lint": { + "tp": 14, + "fp": 5, + "fn": 18, + "tn": 25, + "n": 62, + "recall": 0.4375, + "precision": 0.7368421052631579, + "false_flag_rate": 0.16666666666666666, + "f1": 0.5490196078431372, + "recall_ci": [ + 0.2816508596944317, + 0.6067469796877387 + ], + "false_flag_ci": [ + 0.07336434240351683, + 0.33564705185680177 + ], + "precision_ci": [ + 0.5120803155892935, + 0.8819376166045982 + ] + }, + "compile_only": { + "tp": 29, + "fp": 24, + "fn": 3, + "tn": 6, + "n": 62, + "recall": 0.90625, + "precision": 0.5471698113207547, + "false_flag_rate": 0.8, + "f1": 0.6823529411764705, + "recall_ci": [ + 0.7578150066422116, + 0.9675990373736805 + ], + "false_flag_ci": [ + 0.6269395261897256, + 0.9049502189759876 + ], + "precision_ci": [ + 0.41453742646439184, + 0.6734263183985253 + ] + } + } + }, + "role_flagged_by_new_verdict": { + "faithful": { + "n": 25, + "flagged": 16 + }, + "minor_drift": { + "n": 13, + "flagged": 13 + }, + "not_formalizable": { + "n": 3, + "flagged": 2 + }, + "wrong": { + "n": 24, + "flagged": 24 + } + } +} diff --git a/tests/test_assistant_diagnostic.py b/tests/test_assistant_diagnostic.py new file mode 100644 index 0000000..5cbe648 --- /dev/null +++ b/tests/test_assistant_diagnostic.py @@ -0,0 +1,74 @@ +"""Current-chat review replay is offline, complete and text-free at its public boundary.""" +import copy +import importlib.util +from pathlib import Path + +import pytest + +PATH = Path(__file__).resolve().parents[1] / "experiments/P0-pilot/assistant_diagnostic.py" +SPEC = importlib.util.spec_from_file_location("assistant_diagnostic", PATH) +DIAG = importlib.util.module_from_spec(SPEC) +SPEC.loader.exec_module(DIAG) + +ITEM = {"id": "synthetic", "source_text": "Synthetic private prose.", + "lean_code": "theorem t (n : Nat) : n = n := rfl", "verified": True} +ASSESSMENT = {"records": [{"id": "synthetic", "blind_id": "P01", "source": { + "roles": [{"kind": "object", "symbols": ["n"], "description": "Private object wording", + "keywords": ["natural"]}, + {"kind": "goal", "description": "Private goal wording", "keywords": ["equal"]}], + "goal_has_exists": False}, + "judge": {"verdict": "faithful", "faithful": True, "errors": [], + "reason": "Private reviewer explanation"}}]} + + +def test_offline_replay_and_text_free_public_output(monkeypatch): + def no_network(*args, **kwargs): + raise AssertionError("Replay must not call an API") + + monkeypatch.setattr("urllib.request.urlopen", no_network) + rows = DIAG.evaluate([ITEM], {"P01": "synthetic"}, ASSESSMENT) + assert len(rows) == 1 and rows[0]["errors"] == {} + public = DIAG.public_items(rows, {"P01": {"verdict": "faithful"}}) + assert public[0]["assistant_verdict"] == "faithful" + assert not any(word in str(public) for word in ["Private", "Synthetic", "explanation"]) + assert all(key not in public[0] for key in ["source", "judge", "reason", "lean_code", "source_text"]) + + +def test_duplicate_or_missing_assessments_are_rejected(): + assessment = copy.deepcopy(ASSESSMENT) + assessment["records"] *= 2 + with pytest.raises(ValueError, match="Duplicate"): + DIAG.evaluate([ITEM], {"P01": "synthetic"}, assessment) + with pytest.raises(ValueError, match="same cohort"): + DIAG.evaluate([ITEM], {"P01": "synthetic"}, {"records": []}) + + +def test_mismatched_item_and_missing_source_are_rejected(): + assessment = copy.deepcopy(ASSESSMENT) + assessment["records"][0]["id"] = "different" + with pytest.raises(ValueError, match="mismatched"): + DIAG.evaluate([ITEM], {"P01": "synthetic"}, assessment) + with pytest.raises(ValueError, match="Missing source"): + DIAG.evaluate([{**ITEM, "source_text": ""}], {"P01": "synthetic"}, ASSESSMENT) + + +def test_judge_cannot_disagree_with_its_boolean_flag(): + assessment = copy.deepcopy(ASSESSMENT) + assessment["records"][0]["judge"]["faithful"] = False + with pytest.raises(ValueError, match="Invalid authored judgment"): + DIAG.evaluate([ITEM], {"P01": "synthetic"}, assessment) + + +def test_invalid_source_schema_is_rejected(): + assessment = copy.deepcopy(ASSESSMENT) + assessment["records"][0]["source"]["roles"] = [] + with pytest.raises(ValueError, match="goal"): + DIAG.evaluate([ITEM], {"P01": "synthetic"}, assessment) + + +def test_agreement_is_explicitly_not_independent_and_has_no_gate(): + rows = DIAG.evaluate([ITEM], {"P01": "synthetic"}, ASSESSMENT) + result = DIAG.agreement(rows, {"P01": {"verdict": "faithful"}}) + assert result["metrics_are_non_independent_reference_agreement"] is True + assert "decision" not in result + assert DIAG.finite(float("nan")) is None