Blame for code/docs/PREREG_SOTA.md

# Pre-registration: SOTA analysis, Lean prover paper (configuration `sota-v1`)

Status: **REGISTERED v1, 2026-10-19** (signed off by the project owner). The hash is `python scripts/p2/prereg_hash.py`
(sha256 over this text AND the analysis code: `align/eval/paired.py`, `align/eval/proof_stats.py`, `scripts/p2/eval_report.py`,
`scripts/p2/p2_common.py`, `scripts/p2/prereg_hash.py`). It is time-stamped with OpenTimestamps (Bitcoin-anchored; only the
hash leaves the machine): `docs/evidence/prereg/` holds the hash file and its `.ots` proof, verifiable with `ots verify`.
Every edit after registration changes the hash, which `eval_report.py --config sota` prints beside the registered one;
changes are made only as numbered, separately time-stamped amendments (section 9). License of everything released:
Apache-2.0 (data rows keep their source licenses; see NOTICE).

Specification: `docs/SOTA_PLAN.md` v3, sections 1, 3 and 5, Phase 0a item 6. This registration is SEPARATE from the P2
registration in `docs/P2.md` (miniF2F solved@8 at cap 16384, exact McNemar), which stays as it is and is not
reinterpreted by anything below.

## 1. Question and estimand

Does the frozen candidate (the winning recipe chain applied once to Goedel-Prover-V2-8B, plus the K5 inference-time
winner) solve more miniF2F-test problems than the Goedel-Prover-V2-8B anchor, under one frozen verifier and the same protocol?

Estimand, per class: the mean over the problems of the benchmark of the unbiased pass@32 estimate

    pass@32_i = 1 - C(n - c_i, 32) / C(n, 32),    n = 64 samples (class A) or 64 trajectories (class B),

where c_i is the number of samples (trajectories) of problem i accepted by the verifier. It is computed in product form
(`align.eval.paired.pass_at_k_product`, checked against `math.comb`). The estimand is the difference of these means,
candidate minus anchor, over the same problems. k > n is refused, never extrapolated.

Classes (every number carries its class):

* **A**: single pass, cap 40,960 tokens, n = 64 samples per problem.
* **B**: one trajectory is an attempt plus at most 2 Lean-feedback repairs; the cumulative completion tokens of the
  trajectory may not exceed 40,960 (a success reached only after the ledger is exceeded does not count). n = 64
  trajectories per problem. A failed sample with ledger left and no repair record is a missing record, and the report
  refuses it; it is never scored as a failure.
* C (agentic) and PutnamBench class A pass@8 are exploratory and not analysed by this configuration beyond what is listed in section 3.

## 2. Primary endpoints (co-primary, Holm over the two)

| Id | Class | Set | Estimand | Test |
|---|---|---|---|---|
| A | A | miniF2F-test (the elaborating subset, fixed in Phase 0a) | mean unbiased pass@32 from n = 64 | paired sign-flip permutation test over problems |
| B | B | miniF2F-test (same problems) | same | same |

* **Test.** Statistic: the mean of the per-problem differences d_i. Null: d_i symmetric about 0 (exchangeability of the two
  systems within a problem). p = P(|mean(s * d)| >= |observed|) over independent uniform sign vectors s; zero differences
  are dropped from the enumeration. Exact enumeration of all 2^m sign vectors when at most 20 problems differ; otherwise
  Monte Carlo with 10^5 flips, seed 0, p = (count + 1) / (10^5 + 1). Two-sided.
* **alpha** = 0.05 two-sided, familywise over {A, B} by Holm step-down (valid under arbitrary dependence). An endpoint that
  cannot be computed enters Holm with p = 1 (the family is the registered two).
* **Decision rule, applied mechanically:** SUCCESS iff the Holm-adjusted p < 0.05 AND the candidate mean is higher;
  significant with the candidate lower is reported as DEGRADATION; anything else is "no detectable improvement"
  (never "no effect"; never "equivalent").
* **Interval:** 95% percentile bootstrap over problems (10^4 resamples) of the mean paired difference.
* **Label.** A result is CONFIRMATORY only if `eval_report.py` lists no blocker: the problem count equals the registered
  count; n per problem equals 64 in both arms; both arms were verified under the frozen verifier (section 7) at the registered
  300 s budget with a single verifier configuration; the two arms' generation settings and prompts match; the
  registration hash matches the time-stamped one; statement fidelity was checked for every accepted sample; no override
  flag was used. Anything else prints NOT CONFIRMATORY with the reasons, and the numbers are exploratory.

## 3. Secondary and exploratory (no multiplicity control, no decision attached)

Secondary:

1. Exact McNemar on the binary solved@32 of the first 32 samples (by `sample_idx`) of class A.
2. Mean pass@1 (class A), same paired test and interval.
3. ProofNet-test class A, pass@32 estimand, same test (its own elaborating subset; reported with its denominator).

Exploratory: class-A pass@1/8/16 on miniF2F-test; every other (benchmark, split) supplied, class A at k in {1, 8, 16, 32};
the strict-fidelity sensitivity (rewritten or unreadable accepted samples counted as failures); anything on class C.
If the strict-fidelity sensitivity reverses the sign or the significance of a co-primary, the headline is published with that
reversal in the same sentence.

## 4. Minimum detectable effects

Power is by simulation (`align.eval.paired.simulate_power` / `mde_curve`; 400 to 5,000 simulations per point, seed 3). It
is a statement about a **stated difficulty distribution**, not about a real benchmark: per-problem success probabilities
drawn from the mixture of `.tmp/audit_scratch/power_sim3.py` (68% Beta(3, 1.5); 20% Beta(0.45, 5); 12% log-uniform on
10^-6 to 10^-3.2), and the candidate's log-odds shifted by mu plus problem-specific noise of sd 1. MDE = true gain in pass@k (pp)
at which the linearly interpolated simulated power reaches 80%.

Reproduction check (N = 226, n = 32, k = 8, as in power_sim3.py): +1.4 pp gives power 0.28 (reference 0.30), and +3.6 pp
gives 0.95 (reference 0.96), for the estimator test; binary McNemar gives 0.08 and 0.41 (reference 0.07 and 0.42).
The estimator test needs about half the effect of binary McNemar for the same power.

| Contrast (plan section 3) | Set, estimand | Difficulty assumed | MDE, estimator test (80%) | MDE, binary McNemar (80%) | Prior effect to beat (plan section 2) |
|---|---|---|---|---|---|
| Co-primary A and B | miniF2F-test, N = 244, pass@32 from n = 64 | Goedel-like mixture above | **2.8 pp** (about 6.7 problems) | not reached below +3.8 pp | descriptive target: >= 207 of 244 |
| K0 A/A null | dev, N >= 1,000, pass@8 from n = 32 | Goedel-like | not a test: supplies the null spread of paired differences between two identical-recipe seeds | | 0 |
| K5 inference levers | dev, N >= 1,000, pass@8 from n = 32 | Goedel-like | 1.3 pp | 2.5 pp | L1: +2.1 (SR, same model) |
| K1 EI-SFT vs RL (+PKPO arm) | dev, N >= 1,000, pass@8 from n = 32 | headroom (log-odds shifted by -1) | 1.7 pp | 3.1 pp | L3: 0 to +2.5; L5: +1.8 to +2.8 |
| K2 mutation vs temperature-matched | same | headroom | 1.7 pp | 3.1 pp | **0 to +3.0 pp** (Pythagoras ALF +6.97 pp at 4B with ~2M instances; ours ~100x smaller; judgment) |
| K4 averaging / scale | same, per arm at its own validated alpha | headroom | 1.7 pp | 3.1 pp | **0 to +2.0 pp** at the best validated alpha vs alpha = 1.0 (Goedel-V2 averaging: pass@N rises then falls with alpha; judgment); curves reported |
| K6 classifier vs random statements | same, 0.1B tokens | headroom | 1.7 pp | 3.1 pp | **0 to +1.0 pp** (text-feature classifier held-out AUC 0.52: no signal); **conditional:** if the 8B hidden-state classifier reaches held-out in-band AUC >= 0.65 (measured before K6 data are built), the prior is 0 to +2.0 pp |

Rules attached to the table:

* A contrast whose MDE exceeds the upper end of its prior effect is **dropped, not run** (plan section 3). By this rule
  K1 (1.7 < 2.5), K2 (1.7 < 3.0) and K4 (1.7 < 2.0) are run; K6 (1.7 > 1.0) is DROPPED unless its pre-stated condition
  (hidden-state AUC >= 0.65) is met, in which case it runs (1.7 < 2.0). The rule is re-applied with the recomputed MDEs
  of Amendment A1.
* **Amendment A1 (scheduled):** the table is recomputed with the **anchor's own per-problem (n, c) table** at n = 64
  (`align.eval.paired.empirical_difficulty`) and the actual dev N, and the co-primary `n_problems` is set to the final
  elaborating subset. A1 uses baseline data only, is time-stamped like v1, and must exist BEFORE any contrast or candidate
  result is computed. MDEs scale roughly with 1 / sqrt(N).
* These MDEs cover benchmark-sampling noise only. Training-seed noise is added by design in section 5.
* Dev-set size: at least 1,000 problems (plan section 3: held-out in-band pool statements with labelling samples disjoint from the
  selection samples, plus ProofNet-dev, plus miniF2F-valid (226, filtered, disclosed)). Fewer problems means the MDE is re-stated, not ignored.

## 5. Contrasts K0 to K6: analysis (decided on the dev set at matched generated tokens)

* The unit is the problem. Per arm, the per-problem estimate is the mean over training seeds (at least 3) of the unbiased
  pass@k estimate; arms are compared with the same paired sign-flip test and bootstrap interval as section 2.
* A K-contrast headline requires BOTH: Holm-adjusted p < 0.05 within its family, AND the observed paired difference exceeds the
  97.5th percentile of the K0 null distribution of paired differences (two seeds of the identical recipe), so training-seed
  noise cannot pass as an effect. Families: {K1, K2, K4, K6} (mechanism contrasts on Kimina-Distill-8B, one Holm family);
  K5's pairwise comparisons (2-repair vs restarts vs agentic) another. K0 is a calibration, not a test.
* Contrasts use the registered code path (`sota_contrast`); nothing is tuned on the dev set after its first read except the
  K4 alpha, which is selected per arm on the dev half disjoint from the confirmation half.
* No contrast may be described as equivalence (we claim only failure to detect a difference at its MDE).

## 6. Anchor

The anchor is Goedel-Prover-V2-8B at the revision `dfd02e6271a58375dfbf3ece0175277cf6b6a89a` (the revision pinned in
`scripts/p2/eval_report.py` for the P2 registration). In Phase 0a it is **re-generated at n = 64** (cap 40,960, the
P2 sampling settings temperature 1.0 / top_p 0.95, no top_k) and **re-verified under the frozen verifier at 300 s**; a
sensitivity run at 1,200 s is reported separately and never pooled. A second seed of the generation is run to measure generation variability.
The published self-reported 202 of 244 (pass@32, 40k, 180 s) is context, not the anchor: the anchor is our own n = 64 regeneration, and every
comparison uses the baseline and the candidate under the same harness, sampler settings and prompts.

Class B's anchor is the same model run through the same repair protocol (2 Lean-feedback repairs, 40,960 cumulative tokens).

## 7. Frozen-verifier rule

Before any candidate result exists, the verifier (everything under `align/verify/`, the Lean and Mathlib pins, the axiom
policy, timeouts) is merged, ceiling-tested (known-good accepted, the adversarial suite rejected) and frozen. Its hash is
`verifier_hash` of `eval_report.py` (sha256 of the canonical JSON of the recorded pins and configuration, workers excluded).
All arms of every confirmatory comparison are verified under that one verifier, passed as `--frozen-verifier-hash`. A verifier
fix after the freeze invalidates every confirmatory number produced before it: the anchor and candidate are both re-verified, never mixed.
Re-verifying the same generations is allowed and does not consume a test look; generating anew does.

## 8. Rewritten statements

The verifier replaces the statement the model wrote with the reference statement, so a sample whose displayed theorem
differs from the reference can be accepted. The Goedel protocol credits these, and so does the primary analysis (comparability).
Every report states, per arm, the **rewritten-statement count**: accepted samples whose displayed theorem (signature
tokens, theorem name ignored) differs from the reference statement or cannot be parsed, with the number of affected problems and how many fall in repair
rounds. The strict-fidelity sensitivity (section 3) is the exploratory counterpart.

## 9. Stopping and exclusion rules

* **One confirmatory look** at the test split per frozen candidate. No interim analysis, no optional stopping, no peeking: n = 64 is fixed in advance.
* Every look at a test split is appended to `docs/evidence/test_split_looks.jsonl` (who, when, which files and sha256 of the report and inputs; hash-chained, verifiable
  with `verify_look_log`). A look not in the log did not happen.
* A generation job that dies is re-run for the missing shard under the same seed settings. A problem or sample is never dropped for having failed.
  An incomplete run (missing round-0 sample, missing verification, ragged n) makes the report refuse, not score the gap as failure.
* **Exclusions are only the pre-declared ones:** problems that do not elaborate under the frozen Lean environment are excluded as a set, fixed
  in Phase 0a before any candidate result and disclosed with the denominator; the registered `n_problems` in `eval_report.SOTA` must equal that
  denominator at hash time. No other exclusion, and no outlier trimming, ever.
* If any registered input changes (denominator, n, cap, verifier, test), the registration is re-hashed and re-stamped and the earlier results lose the label.

## 10. Protocol tuple

Every reported number carries: benchmark and split; denominator; sha256 of the (problem id, statement hash) set;
Lean and Mathlib pins; verifier hash, budget and configuration (axiom policy); the rewritten-statement count per arm;
n, k, cap, ledger and total completion tokens; class. "SOTA" is never claimed without the class beside it. Cost
(box-hours, decode/prefill tokens, verifier CPU-hours) is reported from the run logs alongside.

## 11. What this registration does not claim

That we match Leanstral's numbers; that any gain comes from a specific objective; equivalence where only a difference was not detected; a
cross-paper PutnamBench ranking; that the MDEs describe the real benchmark rather than the stated difficulty distribution.


## 9. Amendments

Each amendment is appended here with its date, its reason, the hash before and after, and its own OpenTimestamps proof.
None yet (A1 is scheduled, see section 4).