satp-policy-v4.27

satp-policy-v4.27

41.4% on miniF2F test — vs 34.0% expert-tuned aesop (DSP+), 13.1% LeanHammer, and 12.7% bare aesop. All 244 problems, greedy decode, Lean 4 v4.27.0.

A 0.2B ByT5 policy that reads a Lean 4 goal state and emits a per-problem aesop configuration — search budget, rule-set options, and extra tactic and lemma rules. This repository is a self-contained inference bundle: checkpoints plus a standalone infer.py (no training-repo dependencies), forward-equivalent to the training policy. Everything runs in a Lean 4 v4.27.0 environment.

Results on miniF2F

The dataset is ChristianZ97/minif2f-satp-v4.27, pinned by infer.py at revision 94424f13 and overridable with SATP_DATASET_REVISION (maxHeartbeats 200000).

Inference Ablation & Baselines — test split

• Rows 1–5: greedy decodes of best_checkpoint.pt; the static row applies its per-head modes (block below) as one constant configuration.
• Rows 6–9: no policy. Rows 6–7 take the expert configuration verbatim from microsoft/DSP-Plus@eb98320 — the two model-free attempts of bfsaesopLoop plus its 16 add_aesop_rules, the in-search 7B-prover attempt excluded; card protocol = 300 s, maxRecDepth 512. DSP+ reports 35.2% on its own Lean 4 v4.17-rc1 snapshot.
• Row 8 reruns LeanHammer's released hammer tactic out of the box — aesop preprocessing, cloud premise selection, and the Zipperposition→Duper pipeline — at 600 s/problem; v4.27.0 is the release matching this environment's exact Lean/Mathlib commit, and uncapping maxHeartbeats changes nothing (the same 32 problems solve). Its current release (v4.33.0, a different Lean environment) yields 37.3% on the same statements, with 58 of the 91 proofs closed by Lean core's grind and at most 14 citing a retrieved premise — the jump comes from adding grind to the aesop rule set, not from lemma retrieval. SATP instead couples each retrieved lemma to a learned tactic and priority (the w/o-additional-lemma row).
• Verifiers: every row lake env lean; the full-configuration decode matches its Kimina-measured result exactly on both splits.

Model

Distilled static configuration

One constant configuration for every problem, lemma rules off: each value is the per-head mode over best_checkpoint.pt's 244 validation decodes, and -- % is how often that mode was chosen. Priorities are integers, smaller = higher (0 first, 100 last).

<details> <summary>the full configuration block</summary>

  aesop (config := {
    maxRuleApplications := 1600              -- 54%
    maxRuleApplicationDepth := 10            -- 54%
    maxNormIterations := 320                 -- 86%
  })
    (add norm 100 (by norm_cast))            -- 99%
    (add norm 0 (by linarith))               -- 100%
    (add norm 0 (by nlinarith))              -- 100%
    (add norm 0 (by positivity))             -- 36%
    (add norm 0 (by omega))                  -- 49%
    (add norm 0 (by bound))                  -- 100%
    (add norm 1 (by ext))                    -- 61%
    (add norm 1 (by field_simp [*] at *))    -- 97%
    (add safe 100 (by ring))                 -- 73%
    (add safe 100 (by field_simp))           -- 99%
    (add safe 100 (by norm_num))             -- 99%
    (add safe 100 (by interval_cases))       -- 96%
    (add safe 0 (by split))                  -- 93%
    (add safe 100 (by decide))               -- 100%
    (add safe 0 (by push_cast))              -- 86%
    (add safe 100 (by assumption_mod_cast))  -- 98%

</details>

Files

best_checkpoint.pt               # infer.py's default; copy of ckpt_3ep_val103_test101.pt
ckpt_10ep_val104_test99.pt       # ── 10-epoch runs
ckpt_10ep_val105_test97.pt
ckpt_10ep_val103_test96.pt
ckpt_3ep_val90_test88.pt         # ── 3-epoch runs
ckpt_3ep_val100_test94.pt
ckpt_3ep_val103_test101.pt
ckpt_10ep_nodpo_val100_test92.pt # ── 10-epoch runs, w/o DPO
ckpt_10ep_nodpo_val100_test91.pt
ckpt_10ep_nodpo_val101_test98.pt
ckpt_3ep_nodpo_val78_test78.pt   # ── 3-epoch runs, w/o DPO
ckpt_3ep_nodpo_val81_test79.pt
ckpt_3ep_nodpo_val92_test89.pt
ckpt_10ep_bc_val89_test77.pt     # ── 10-epoch runs, DPO → BC
ckpt_10ep_bc_val77_test70.pt
ckpt_10ep_bc_val71_test78.pt
ckpt_3ep_bc_val49_test49.pt      # ── 3-epoch runs, DPO → BC
ckpt_3ep_bc_val36_test33.pt
ckpt_3ep_bc_val31_test46.pt
infer.py                         # load → retrieve → greedy-decode → Kimina verify
reproduce.py                     # test-split repro, kimina | lake verifier (imports infer.py)
cache/premise_embeddings.npy     # 1.07 GB — 180,957 × 1472 premise embeddings
cache/mathlib4_premises.txt      # 38.9 MB — premise names, index-aligned

Checkpoint names carry their own scores: val{V}_test{T} = problems solved out of 244 on each split; each file is its run's best-val checkpoint (~1.12 GB each). infer.py reads model_state_dict only; the checkpoint files are interchangeable at load time. Premise corpus = LeanDojo Benchmark-4 v10; embeddings come from the frozen retriever → verifier-version independent. ByT5 base auto-downloads on first run.

Run

pip install torch transformers numpy requests huggingface_hub datasets
hf download ChristianZ97/satp-policy-v4.27 --local-dir satp-policy-v4.27
cd satp-policy-v4.27
KIMINA_URL=http://localhost:8000 python infer.py    # default = best_checkpoint.pt
SATP_CKPT=./ckpt_3ep_val103_test101.pt KIMINA_URL=http://localhost:8000 python infer.py    # any other checkpoint

The Kimina server must run a Lean 4 v4.27.0 workspace.

<details> <summary>environment variables</summary> </details>

Verification is sequential (one POST per problem, retried with backoff). Header-less statements get the training header prepended.

Reproduce

reproduce.py re-runs the miniF2F test split end-to-end over the same greedy decode and checks the result against its built-in target, with either verifier. It always loads best_checkpoint.pt — it ignores SATP_CKPT — so the target it prints can never drift from the weights it graded:

KIMINA_URL=http://localhost:8000 python reproduce.py kimina            # target 101/244
SATP_SPLIT=validation python reproduce.py kimina                       # target 103/244
SATP_LAKE_DIR=/path/to/lean-v4.27-project python reproduce.py lake     # no server

lake mode runs one lake env lean per problem inside any Lean 4 v4.27 project with Mathlib built — no server. Both modes write reproduce_<backend>.jsonl; greedy decode is deterministic.