Zayden-Jung/lean-bench
2
1
Fork 0
Code Issues 2 Pull Requests Actions Packages Projects Releases Wiki Activity

Make the P0 pilot reproducible and freeze 65 blind AI labels #5

Merged
Zayden-Jung merged 1 commits from codex/pilot-execution into main 2026-10-28 10:58:11 +00:00
Conversation 0 Commits 1 Files Changed 9
+826 -50
codex-bot commented 2026-10-28 10:54:34 +00:00
Collaborator
Copy Link
Copy Source

The P0 export omitted source_text, producing empty passage panels and invalid detector inputs. Restore passages from the matching private archive, reject empty inputs, and freeze 65 blind AI labels (not human gold) under the owner-amended annotation plan.

Enforce the cumulative 400-request ceiling, preserve run identity and usage, restore the complementary-signal PARTIAL rule, and reject incomplete results before scoring. Validation at the merged revision: 146 offline tests, Ruff and diff checks passed; CI #427 passed Python and real Lean validation on ubuntu24.04-x64-lean4.35 (image skipped for PR).

The owner manually merged this preparation PR. Subsequent billing-stop, partial-resume fixes and the execution report are tracked separately in PR #6. Raw passages and model outputs remain gitignored. Related issue: #3.

The P0 export omitted source_text, producing empty passage panels and invalid detector inputs. Restore passages from the matching private archive, reject empty inputs, and freeze 65 blind AI labels (not human gold) under the owner-amended annotation plan. Enforce the cumulative 400-request ceiling, preserve run identity and usage, restore the complementary-signal PARTIAL rule, and reject incomplete results before scoring. Validation at the merged revision: 146 offline tests, Ruff and diff checks passed; CI #427 passed Python and real Lean validation on ubuntu24.04-x64-lean4.35 (image skipped for PR). The owner manually merged this preparation PR. Subsequent billing-stop, partial-resume fixes and the execution report are tracked separately in PR #6. Raw passages and model outputs remain gitignored. Related issue: #3.
codex-bot added 1 commit 2026-10-28 10:54:34 +00:00
fix(pilot): freeze AI labels and enforce auditable execution
ci / python (pull_request) Successful in 22s
Details
ci / lean (pull_request) Successful in 1m16s
Details
ci / image (pull_request) Has been skipped
Details
6875c79c40
Zayden-Jung merged commit 5d531c9c5f into main 2026-10-28 10:58:11 +00:00
codex-bot changed title from Make the P0 pilot reproducible and freeze 65 blind AI labels to WIP: Make the P0 pilot reproducible and preserve partial results 2026-10-28 11:05:31 +00:00
codex-bot changed title from WIP: Make the P0 pilot reproducible and preserve partial results to Make the P0 pilot reproducible and freeze 65 blind AI labels 2026-10-28 11:08:02 +00:00
Sign in to join this conversation.
Reviewers
No Reviewers
Labels
No items
No Label
Milestone
No items
No Milestone
Projects
Clear projects
No project
Assignees
Clear assignees
claude-bot codex-bot yilin-codex-bot Zayden-Jung
No Assignees
1 Participants
Notifications
Due Date
No due date set.
Dependencies

No dependencies set.

Reference: Zayden-Jung/lean-bench#5
Delete Branch "codex/pilot-execution"

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?