satp-policy-v2-alphaproof

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.

The checkpoint is the overall best of a completed 20-epoch run, selected by validation (wandb-logged step 2336; the checkpoint file records internal step 2300). The test split was evaluated once against it at run end.

Results

miniF2F (ChristianZ97/minif2f-satp-alphaproof pinned at revision 81a8abfa — infer.py resolves the dataset at this immutable commit; override with SATP_DATASET_REVISION), greedy decode, statements submitted raw (Lean default maxHeartbeats 200000), Lean 4 v4.26.0. The validation split is evaluated and independently reproduced below; the test split was evaluated once at this final best checkpoint when the run completed:

split	solved
validation	40.6% (99/244)
test	37.7% (92/244)

ablation (validation)	solved
satp	40.6% (99/244)
w/ default search budget	40.6% (99/244)
w/o additional lemma	34.8% (85/244)
w/o additional tactic	31.6% (77/244)
aesop	11.5% (28/244)

The validation number has been independently re-run through this bundle's infer.py and matches the training-time value exactly. Every number above — the split and all ablation rows — is verified per problem by two independent backends (the Kimina server, and one lake env lean per proof) with identical solved sets, and gated by #print axioms as the arbiter: a counted proof compiles, contains no sorry, and depends on no axioms beyond propext, Classical.choice, Quot.sound (388 row×problem checks, all clean). The input path is verified end to end: live goal states collected by the satp tactic (Meta.ppGoal) are byte-identical to the dataset goal_state on all 244 problems, the service decode is byte-identical to this bundle's decode (244/244), and a full satp? sweep through the Lean tactic solves the identical 99-problem set. The test number is the training-run FINAL evaluation (Kimina backend, all 244 problems evaluated); it has not been put through the two-backend axiom audit above. A distilled static row is not published for this checkpoint.

Checkpoint

run	2rorv25g (wandb satp-v2), epoch 14, seed 1827 — final best of the completed 20-epoch run; best-val event at wandb step 2336, checkpoint file records step 2300
verifier	Kimina-Lean Server, Lean 4 v4.26.0
architecture	ByT5(kaiyuy/leandojo-lean4-retriever-byt5-small)+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

172-way lemma decision = off + 19 hosts × 3 type × 3 priority; the positivity tactic rule is included, with no positivity lemma host.

Files

best_checkpoint.pt            # 1.12 GB — infer.py reads model_state_dict only
infer.py                      # load → retrieve → greedy-decode → Kimina verify
reproduce.py                  # validation-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-v2-alphaproof --local-dir satp-policy-v2-alphaproof
cd satp-policy-v2-alphaproof
KIMINA_URL=http://localhost:8000 python infer.py

var	default	meaning
KIMINA_URL	http://localhost:8000	Kimina /verify endpoint
SATP_SPLIT	validation	or test
SATP_DATASET_REVISION	81a8abfa…	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 → remove the heartbeat cap (diagnostic; 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 validation split end-to-end over the same greedy decode and compares against 99/244, with either verifier:

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

lake runs one lake env lean per problem (300 s timeout) inside any Lean v4.26 project with Mathlib built; writes reproduce_<backend>.jsonl ({name, success, tactic, code} per problem). Greedy decode is deterministic; the test split runs too (SATP_SPLIT=test; reference 92/244).