hpsearch-embed-xs-state

The proof-state query embedder of hpsearch's balanced mode (CPU, onnxruntime). It is the query side only: hmzprover/hpsearch-embed-xs-agent (snowflake-arctic-embed-xs, 22M parameters) fine-tuned so that a Lean proof state lands next to the xs-agent vectors of the premises its next tactic uses. Documents keep their xs-agent vectors (pairs_with holds that model's id), so an index needs no extra vectors.

• model.onnx: int8 (dynamic quantization); inputs input_ids, attention_mask; output unit vectors (batch x 384).
• Training: full softmax over all 180,973 premise vectors (frozen), other golds of a state masked, plus distillation (KL) from hmzprover/hpsearch-embed-4b-state's top-64 lists; 3 epochs.

Training data: the public train split of LeanDojo Benchmark 4 v10 (Zenodo 12740403, mathlib4 29dcec07): each traced tactic's state_before paired with every premise its annotation locates in the premise corpus (367,730 (state, premise) pairs from 118,517 theorems).

Decontamination (strict): dropped every pair whose theorem is in the val or test split of either LeanDojo split (random, novel_premises; 20,761 pairs), whose state equals a LeanDojo val/test state (100), whose state equals a query of any other evaluation hpsearch is measured on (4,775), or whose premise's name (161,550) or statement (307) is a gold of any other evaluation (MathlibQR/MPR, Lean Finder, LeanStateSearch, TheoremSearch, TBPS, hmzprover, MIRB premise and Mathlib). Kept: 180,237 pairs, 107,936 states, 51,145 distinct premises.