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.
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.
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).
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.
The Kimina server must run a Lean 4 v4.27.0 workspace.
environment variables
var
default
meaning
KIMINA_URL
http://localhost:8000
Kimina /verify endpoint
SATP_SPLIT
validation
or test
SATP_DATASET_REVISION
94424f13…
dataset commit infer.py resolves (pinned)
SATP_LIMIT
0
>0 → first N problems only
SATP_CKPT
./best_checkpoint.pt
checkpoint path — point it at any other ckpt_*.pt
SATP_CACHE
./cache
premise files dir
SATP_HEARTBEATS0
unset
1 removes the heartbeat cap; reported numbers use the default
SATP_LEAN_TIMEOUT
300
server-side Lean timeout (s); HTTP timeout = +60
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:
bash
1KIMINA_URL=http://localhost:8000 python reproduce.py kimina # target 101/2442SATP_SPLIT=validation python reproduce.py kimina # target 103/2443SATP_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.
