satp-policy-v4.27

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: checkpoint 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.

Interim checkpoint (uploaded 2026-07-27). This is the validation-best of a 40-epoch run that is still training, not a final release. It will be replaced if a later checkpoint sets a new validation best.

Results

miniF2F, greedy decode, all 244 problems of each split, Lean 4 v4.27.0. Statements are submitted raw, at Lean's default maxHeartbeats 200000. The dataset is ChristianZ97/minif2f-satp-v4.27, pinned by infer.py at revision 94424f13 and overridable with SATP_DATASET_REVISION.

split	solved
test	41.0% (100/244)
validation	42.2% (103/244)

configuration (test)	solved
satp	41.0% (100/244)
w/ default search budget	41.0% (100/244)
w/o additional tactic	38.1% (93/244)
w/o additional lemma	32.0% (78/244)
distilled static configuration (tactic only)	30.7% (75/244)
aesop	12.7% (31/244)
Expert-tuned aesop (from DSP+, w/o BFS)	34.0% (83/244)

The first four rows are one greedy decode per problem through infer.py, verified on Kimina; validation reproduces the training-time best, 103/244. The rest use no policy: the static configuration is distilled from the validation decodes and measured on test, and aesop and Expert-tuned aesop are baselines. Every Kimina count was re-checked under lake env lean and matched; the expert-tuned row is lake env lean only.

Checkpoint

run	mv53kefx (wandb), seed 1827 — validation-best at ~epoch 5 of a 40-epoch run; the run had reached ~epoch 24 when this was uploaded
verifier	Kimina-Lean Server, Lean 4 v4.27.0
training data	ChristianZ97/NuminaMath-LEAN-satp-v4.27 (75,008 problems; 5,000 subsampled per epoch)
architecture	ReProver's Retrieval Encoder+LoRA(r16,α32,q/k/v/o) mean-pool → shared MLP → 69-head joint action (28 tactic ×10-way + 32 lemma ×172-way + 4 config_level + 5 config_binary) + dense premise retrieval

The 172-way lemma decision is off + 19 hosts × 3 type × 3 priority. positivity appears as a tactic rule and has no lemma host.

Distilled static configuration

One constant configuration for every problem, lemma rules off. Each value is the per-head mode over the 244 validation decodes; -- % is how often that mode was chosen (joint 10-way: off | type×priority).

  aesop (config := {
    maxRuleApplications := 2400            -- 55%
    maxRuleApplicationDepth := 60          -- 64%
    maxNormIterations := 800               -- 45%
    maxGoals := 32                         -- 64%
    enableSimp := false                    -- 70%
  })
    (add norm 100 (by ring))               -- 70%
    (add norm 100 (by field_simp))         -- 50%
    (add norm 100 (by norm_cast))          -- 65%
    (add norm 1 (by linarith))             -- 100%
    (add norm 0 (by nlinarith))            -- 100%
    (add norm 100 (by abel))               -- 54%
    (add norm 0 (by bound))                -- 100%
    (add norm 100 (by exfalso))            -- 100%
    (add norm 0 (by simp_all))             -- 84%
    (add norm 1 (by field_simp [*] at *))  -- 50%
    (add norm 100 (by norm_cast at *))     -- 100%
    (add norm 0 (by decide))               -- 96%
    (add norm 100 (by push_cast))          -- 100%
    (add safe 0 (by positivity))           -- 98%
    (add safe 0 (by push_neg))             -- 97%
    (add safe 100 (by zify))               -- 98%
    (add safe 0 (by interval_cases))       -- 100%
    (add safe 0 (by ext))                  -- 100%
    (add safe 1 (by split))                -- 100%
    (add safe 0 (by simp))                 -- 82%
    (add safe 0 (by norm_num [*] at *))    -- 100%
    (add unsafe 10% (by norm_num))         -- 100%

Modes that came out off: gcongr 100%, rfl 100%, assumption_mod_cast 100%, ring_nf at * 94%, ring_nf 88%, omega 59%. Binary options: enableSimp F 70%, useSimpAll T 79%, enableUnfold T 97%, useDefaultSimpSet T 74%, enableBuiltin T 84%. Priorities are integers, smaller = higher (0 first, 100 last); unsafe = success %.

Expert-tuned aesop (from DSP+, w/o BFS)

DSP+'s hand-tuned aesop configuration, taken verbatim from microsoft/DSP-Plus@eb98320: the two model-free attempts of bfsaesopLoop plus its 16 add_aesop_rules. Its third attempt, bfsaesop, runs a 7B prover inside the search and is excluded.

Same 244 test problems, same Lean 4.27 toolchain, lake env lean (rc 0, no sorryAx).

configuration	solved
aesop	12.7% (31/244)
Expert-tuned aesop, this card's protocol (300 s, maxRecDepth 512)	34.0% (83/244)
Expert-tuned aesop, DSP+ source limits (1200 s, maxRecDepth 1024)	34.8% (85/244)
satp	41.0% (100/244)

Both limits are given; only maxRecDepth separates them. DSP+ reports 35.2% for this configuration on its own Lean 4 v4.17-rc1 snapshot.

Files

best_checkpoint.pt            # 1.07 GB — infer.py reads model_state_dict only
infer.py                      # load → retrieve → greedy-decode → Kimina verify
reproduce.py                  # test-split repro, kimina | lake verifier (imports infer.py)
cache/premise_embeddings.npy  # 1.0 GB — 180,957 × 1472 premise embeddings
cache/mathlib4_premises.txt   # 38 MB — premise names, index-aligned

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

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

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
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 100/244 (SATP_SPLIT=validation targets 103/244), with either verifier:

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

lake runs one lake env lean per problem (300 s timeout) inside any Lean 4 v4.27 project with Mathlib built; writes reproduce_<backend>.jsonl ({name, success, tactic, code} per problem). Greedy decode is deterministic.