lean-bench/docs/experiments/P0-gpt-diagnostic.md

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:

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.