satp-policy-v2

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.

Results

miniF2F (ChristianZ97/minif2f-satp), greedy decode, statements submitted raw (Lean default maxHeartbeats 200000), Lean 4 v4.26.0:

Every number above — both splits and all ablation rows — is verified per problem by two independent backends (the Kimina server, and one lake env lean per proof), with #print axioms as the arbiter: a counted proof compiles, contains no sorry, and depends on no axioms beyond propext, Classical.choice, Quot.sound. Policy rows are additionally checked through both input paths (dataset goal_state, and live goal states via the satp tactic) with identical solved sets.

The 92 solved test proofs are published in two forms — the policy-emitted configuration verbatim, and a distilled minimal tactic script — at LeanSATP proofs/minif2f_test_v2 (branch v2, pinned at b9ed73e); every file compiles on stock Mathlib v4.26 with import Mathlib alone. The folder ships distill_v2_trythis.py, the exact script that generates and re-verifies the minimal view from the configs (aesop? trace + lake env lean + #print axioms per file).

Checkpoint

Distilled static configuration

One constant config for every problem (lemma off); per-head mode over the 244 val decodes, -- % = mode agreement (joint 10-way: off | type×priority).

  aesop (config := {
    -- maxRuleApplications 200 = default     -- 50%
    maxRuleApplicationDepth := 10            -- 50%
    maxNormIterations := 520                 -- 36%
    maxGoals := 1024                         -- 24%
  }) (rule_sets := [-builtin])               -- enableBuiltin=F 59%
    (add norm 100 (by ring))                 -- 86%
    (add norm 100 (by field_simp))           -- 82%
    (add norm 100 (by norm_num))             -- 93%
    (add norm 100 (by norm_cast))            -- 82%
    (add norm 0 (by linarith))               -- 64%
    (add norm 0 (by nlinarith))              -- 89%
    (add norm 0 (by omega))                  -- 82%
    (add norm 100 (by abel))                 -- 85%
    (add norm 100 (by zify))                 -- 64%
    (add norm 0 (by bound))                  -- 55%
    (add norm 100 (by interval_cases))       -- 65%
    (add norm 100 (by ext))                  -- 55%
    (add norm 100 (by split))                -- 60%
    (add norm 100 (by exfalso))              -- 84%
    (add norm 100 (by ring_nf at *))         -- 58%
    (add norm 100 (by field_simp [*] at *))  -- 45%
    (add norm 100 (by norm_num [*] at *))    -- 72%
    (add norm 100 (by norm_cast at *))       -- 82%
    (add norm 100 (by rfl))                  -- 86%
    (add norm 100 (by push_cast))            -- 93%
    (add norm 100 (by assumption_mod_cast))  -- 72%
    (add safe 0 (by ring_nf))                -- 32%
    (add safe 0 (by simp_all))               -- 43%

off: positivity 87%, push_neg 85%, gcongr 65%, simp 58%, decide 36%. binary modes: enableSimp T 94%, useSimpAll T 71%, enableUnfold T 63%, useDefaultSimpSet T 86%, enableBuiltin F 59%. Priorities are integers, smaller = higher (0 first, 100 last); unsafe = success %.

Files

best_checkpoint.pt            # 1.12 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-v2 --local-dir satp-policy-v2
cd satp-policy-v2
KIMINA_URL=http://localhost:8000 python infer.py

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 compares against 92/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). Reference: kimina 92/244 exact (twice, bit-identical — greedy decode is deterministic); all 92 replay 92/92 under lake env lean.

Lean-only path

LeanSATP (branch v2, pinned at b9ed73e; its README carries the DSP-pipeline integration numbers and environment pins) runs the same policy as a Lean tactic: take a dataset row's formal_statement, add import LeanSATP, and close the proof with satp (satp? also prints the emitted configuration). Lean handles the rest — elaboration, live goal state → policy, aesop execution. Same 92/244 solved set.