94 lines
6.0 KiB
Markdown
94 lines
6.0 KiB
Markdown
# P0: pilot
|
|
|
|
Experiment ID **P0**. Spec, hypotheses, decision rule and costs: `docs/experiments/P0-pilot.md`.
|
|
Registry of all experiments: `docs/experiments/README.md`.
|
|
|
|
Question: on the 65 existing items, does role alignment (passage simplex vs. Lean simplex) find
|
|
unfaithful formalizations better than a single LLM judge, compile-only, or static lint?
|
|
|
|
## Layout
|
|
|
|
data/ ignored by git: items.jsonl (copy of the 65 items), labelsheet.html, results.jsonl
|
|
(all contain or paraphrase passages from a copyrighted book)
|
|
labels/ tracked: key.json (blind id -> item id, no text), labels.json (verdicts and error
|
|
types only; do not paste passage text into the notes field)
|
|
results/ tracked: summary.json written by score.py (numbers only)
|
|
|
|
## Steps
|
|
|
|
# Default exports omit source_text. Restore it from the matching private review.
|
|
python experiments/P0-pilot/prepare_items.py --items runs/p85-110/items.jsonl \
|
|
--review runs/p85-110/review.json --out experiments/P0-pilot/data/items.jsonl
|
|
python experiments/P0-pilot/make_sheet.py --items experiments/P0-pilot/data/items.jsonl \
|
|
--out experiments/P0-pilot/data --key-dir experiments/P0-pilot/labels --seed 7
|
|
# a person opens data/labelsheet.html, labels all 65 items, downloads labels.json into labels/
|
|
python experiments/P0-pilot/run_pilot.py --items experiments/P0-pilot/data/items.jsonl \
|
|
--out experiments/P0-pilot/data/results.jsonl --dry-run
|
|
python experiments/P0-pilot/run_pilot.py --items experiments/P0-pilot/data/items.jsonl \
|
|
--out experiments/P0-pilot/data/results.jsonl --labels experiments/P0-pilot/labels/labels.json
|
|
python experiments/P0-pilot/score.py --results experiments/P0-pilot/data/results.jsonl \
|
|
--labels experiments/P0-pilot/labels/labels.json --key experiments/P0-pilot/labels/key.json \
|
|
--summary experiments/P0-pilot/results/summary.json
|
|
|
|
Labeling must be finished before anyone opens `results.jsonl`.
|
|
|
|
## Execution safeguards
|
|
|
|
- Every item must have a nonempty source passage. `prepare_items.py` restores passages only
|
|
when all exported fields match the archived review; the exported cohort and Lean code stay intact.
|
|
- Freeze all labels before the paid run. The owner changed the labeler to the Codex assistant
|
|
on 2026-10-28. These are **AI labels, not human gold**; see the metadata in `labels/labels.json`.
|
|
- `--max-calls` counts actual HTTP attempts, including transport and JSON retries, cumulatively
|
|
across resumes. The hard ceiling is 400. A reservation is saved before each request; an interrupted
|
|
request may consume a reservation without a known response or token count.
|
|
- Metadata is stored beside the output as `results.meta.json`. Model, endpoint, temperature,
|
|
input hash, frozen-label hash and prompt hashes must match on resume. Usage is cumulative.
|
|
A file lock prevents concurrent writers. A budget stop returns exit status 2.
|
|
- Billing/authentication failures stop immediately. Resume retries only missing detector components,
|
|
keeping both complete items and the successful side of partial items. Rows are replaced atomically.
|
|
`--audit-only` reconciles saved completion counts and status without any API request.
|
|
- The nominal successful path uses 130 calls (one source extraction and one judge per item);
|
|
malformed replies and network retries may increase the actual count.
|
|
- Scoring requires complete labels and results and no unresolved detector errors. The primary
|
|
comparison is wrong versus faithful; minor drift is included as positive in the secondary analysis.
|
|
The complementary-signal PARTIAL rule counts wrong items flagged by role alignment but missed
|
|
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.
|
|
Verdicts, abstract annotation notes, hashes and text-free summaries belong in Git;
|
|
the owner-approved schema-only HTML review is also tracked separately under docs/reviews/.
|
|
|
|
## Qwen execution snapshot
|
|
|
|
The 2026-10-28 run was blocked by DashScope `Arrearage`: 42 items are complete, 23 need
|
|
42 detector components, and 131 of the 400 request reservations have been consumed.
|
|
The owner requested fixes and a report now, with paid resumption deferred.
|
|
See `docs/experiments/P0-execution-2026-10-28.md` and `results/execution.json`.
|
|
No gate decision has been issued. Restore provider billing before resuming the same run.
|
|
|
|
## 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.
|
|
|
|
## Semantic simplex registry
|
|
|
|
The current 65-item annotation cohort is materialized as multi-role relation schemas:
|
|
65 source seeds, 50 Lean signature seeds and 15 explicitly incomplete Lean projections.
|
|
See `docs/simplex-schema.md` for the data model, scoped identities, explicit role reuse,
|
|
structural candidate queries, bindings and replay command. Private SQLite/JSON/HTML outputs
|
|
stay under `data/simplex-schemas-v1/`; tracked `results/simplex-schema-*.json` files contain
|
|
only counts, opaque keys, provenance hashes and coverage status. This does not change the
|
|
frozen diagnostic or claim complete semantic extraction or proof verification.
|
|
|
|
The owner-approved schema-only HTML review is tracked at
|
|
`docs/reviews/simplex-schemas.html`. Regenerate it with the builder's `--review-page` option;
|
|
the raw inputs, full assessment explanations and SQLite snapshot remain gitignored.
|