Reassess all 65 P0 items in a separate GPT-assisted diagnostic #7
No Assignees
Notifications
Due Date
No due date set.
Dependencies
No dependencies set.
Reference: Zayden-Jung/lean-bench#7
Reference in New Issue
Block a user
Delete Branch "codex/gpt-diagnostic"
Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?
The owner requested a full 65-item reassessment by the current GPT assistant after the Qwen pilot was interrupted. This delivers a separate, complete same-assistant diagnostic; it neither patches the Qwen run nor changes the frozen reference labels. It does not depend on the billing-recovery PR #6.
All 65 source schemas and 65 semantic judgments were newly authored in this chat and frozen before deterministic alignment statistics were computed. These are not GPT API responses. The exact deployed model ID and chat token usage are unavailable. The assistant had prior exposure to labels, Lean and detector code, so this is not blind extraction, independent accuracy measurement or the preregistered Qwen gate. No GO/PARTIAL/NO-GO is issued.
Results: 25 faithful, 13 minor drift, 24 wrong, 3 not formalizable. The unchanged matcher flags 55 items, including 16 of the 25 newly judged faithful items. Fresh judgments agree with the earlier AI labels on 59/65 items; this agreement is not an accuracy estimate. The full report includes all limitations and six changed verdicts.
Changes: add an offline validation/replay script, six synthetic regression tests, an English diagnostic report, a README entry, and two text-free result files containing all 65 categorical records plus aggregate provenance/statistics. Source schemas, reasons, passages, Lean and a self-contained per-item review remain in the ignored private directory. No source text or model-derived explanations are published.
Validation: 152 offline unit tests, repository-wide Ruff and git diff --check passed. A second replay is byte-identical. Original reference/Qwen hashes and the frozen new-assessment hash remain unchanged. No external model API call, local Lean compilation or local Docker build was performed. Remote CI #437 passed Python checks and real Lean verification for commit
2f0a217on the owner-confirmed ubuntu24.04-x64-lean4.35 runner (runner 7); the image job was skipped for this PR. Checks: https://gitea.entroia.com/Zayden-Jung/lean-bench/actions/runs/437Related issue: #3 (not closed by this diagnostic). Please review and merge manually; no automatic merge is enabled.