5.2 KiB
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-onlyreconciles 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.
The image job was skipped by the PR workflow. The recovery revision passed CI #433.
The recovery changes from PR #6 are consolidated with the semantic schema and review page
in PR #9; the combined head is checked separately there.
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).