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

Three checkpoints are shipped — same recipe, same data, different seed. best_checkpoint.pt is a copy of the one with the highest test score and is what infer.py loads by default.

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.

checkpoint	seed	test	validation
ckpt_8964.pt = best_checkpoint.pt	8964	40.6% (99/244)	42.6% (104/244)
ckpt_1827.pt	1827	39.8% (97/244)	43.0% (105/244)
ckpt_227.pt	227	39.3% (96/244)	42.2% (103/244)

The two columns do not agree on an ordering: validation ranks 1827 > 8964 > 227, test ranks 8964 > 1827 > 227. Only the top pair swaps, and the whole spread is 2 problems on validation and 3 on test — validation does not resolve these three checkpoints. It is also the training-time model-selection signal, so it is not a held-out estimate; the test column is. That is why the default is 8964, and why seed-level differences of a few problems here should not be read as a ranking.

Ablation — ckpt_8964.pt (default)

configuration (test)	solved
satp	40.6% (99/244)
w/ default search budget	40.6% (99/244)
w/o additional tactic	38.1% (93/244)
w/o additional lemma	34.4% (84/244)
distilled static configuration (tactic only)	34.4% (84/244)

Ablation — ckpt_1827.pt

configuration (test)	solved
satp	39.8% (97/244)
w/ default search budget	39.8% (97/244)
w/o additional tactic	35.2% (86/244)
w/o additional lemma	33.6% (82/244)
distilled static configuration (tactic only)	33.6% (82/244)

Ablation — ckpt_227.pt

configuration (test)	solved
satp	39.3% (96/244)
w/ default search budget	39.3% (96/244)
w/o additional tactic	36.1% (88/244)
w/o additional lemma	32.0% (78/244)
distilled static configuration (tactic only)	33.2% (81/244)

Each table is a fresh set of greedy decodes from that checkpoint, verified on Kimina. The first four rows run the policy; the static row does not — it is distilled from that same checkpoint's 244 validation decodes and then measured on test. All three checkpoints rank the two rule kinds the same way: dropping lemma rules costs more than dropping tactic rules (−15 vs −6 for 8964, −15 vs −11 for 1827, −18 vs −8 for 227), and the search budget heads are worth nothing on their own — removing them changes no problem in any of the three runs.

The static row is where per-problem conditioning shows up without moving the count. For 8964 and 1827 it ties w/o additional lemma exactly (84/84 and 82/82), but the two rows are not the same 84 or 82 problems — each pair disagrees on 2. For 227 they differ in count as well (78 vs 81, disagreeing on 5). Conditioning changes which problems get solved even where it does not change how many.

Every Kimina count in all three tables was re-checked under lake env lean and matched, all 18 measurements, row by row (8964 on 2026-08-04, 1827 on 2026-08-06, 227 on 2026-08-07).

Policy-free baselines

Shared by all three tables; no checkpoint involved, lake env lean only.

configuration (test)	solved
aesop	12.7% (31/244)
Expert-tuned aesop (from DSP+, w/o BFS)	34.0% (83/244)

Checkpoints

	ckpt_8964.pt	ckpt_1827.pt	ckpt_227.pt
seed	8964	1827	227
validation-best snapshot	104/244, epoch 9	105/244, epoch 8	103/244, epoch 6
training	10 epochs	10 epochs	10 epochs

Everything else is identical between the three:

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.

Each checkpoint records its own random_seed and wandb_run_id, so a file's identity does not depend on its name.

Distilled static configuration

One constant configuration for every problem, lemma rules off. Each value is the per-head mode over the 244 validation decodes of ckpt_8964.pt; -- % is how often that mode was chosen (joint 10-way: off | type×priority). The other two checkpoints' static rows are distilled the same way from their own decodes; the resulting blocks are not reproduced here.

  aesop (config := {
    maxRuleApplications := 1100              -- 35%
    maxNormIterations := 320                 -- 38%
    enableUnfold := false                    -- 63%
  })
    (add norm 0 (by ring))                   -- 59%
    (add norm 0 (by linarith))               -- 95%
    (add norm 0 (by nlinarith))              -- 86%
    (add norm 0 (by omega))                  -- 96%
    (add norm 0 (by zify))                   -- 74%
    (add norm 0 (by gcongr))                 -- 73%
    (add norm 0 (by bound))                  -- 99%
    (add norm 0 (by ring_nf))                -- 64%
    (add norm 100 (by ext))                  -- 78%
    (add norm 0 (by simp))                   -- 68%
    (add norm 1 (by simp_all))               -- 59%
    (add norm 1 (by field_simp [*] at *))    -- 72%
    (add safe 0 (by norm_num))               -- 91%
    (add safe 1 (by positivity))             -- 89%
    (add safe 0 (by interval_cases))         -- 77%
    (add safe 1 (by split))                  -- 72%
    (add safe 1 (by ring_nf at *))           -- 80%
    (add safe 0 (by rfl))                    -- 77%
    (add safe 1 (by assumption_mod_cast))    -- 53%
    (add unsafe 50% (by field_simp))         -- 52%
    (add unsafe 50% (by norm_cast))          -- 83%
    (add unsafe 50% (by abel))               -- 91%
    (add unsafe 90% (by exfalso))            -- 64%
    (add unsafe 50% (by norm_num [*] at *))  -- 63%
    (add unsafe 90% (by norm_cast at *))     -- 49%
    (add unsafe 90% (by decide))             -- 47%
    (add unsafe 50% (by push_cast))          -- 95%

One of the 28 tactic rules came out modally off — push_neg (37%); the other 27 appear. maxRuleApplicationDepth stayed at its default (30, 48%) and maxGoals at its default (unlimited, 19%). Binary options: enableSimp T 75%, useSimpAll T 75%, enableUnfold F 63%, useDefaultSimpSet T 82%, enableBuiltin T 84% — only enableUnfold departs from the aesop default, so it is the only one that appears in the block above. 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 (ckpt_8964.pt)	40.6% (99/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.12 GB — byte-identical copy of ckpt_8964.pt; infer.py's default
ckpt_8964.pt                  # 1.12 GB — seed 8964, test-best
ckpt_1827.pt                  # 1.12 GB — seed 1827, validation-best
ckpt_227.pt                   # 1.12 GB — seed 227
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

infer.py reads model_state_dict only; the four 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 = ckpt_8964
SATP_CKPT=./ckpt_1827.pt KIMINA_URL=http://localhost:8000 python infer.py
SATP_CKPT=./ckpt_227.pt  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 — ./ckpt_1827.pt or ./ckpt_227.pt for the other seeds
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 the model-card number, 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 99/244
SATP_SPLIT=validation python reproduce.py kimina                       # target 104/244
SATP_LAKE_DIR=/path/to/lean-v4.27-project python reproduce.py lake     # no server

The other two seeds ship as artifacts, not as reproduction targets; measure them against their own table above by pointing infer.py at them with SATP_CKPT.

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.