| # 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). |
|
|
