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