hpsearch-embed-4b-state

The proof-state query embedder of hpsearch's GPU modes. It is the query side only of hmzprover/hpsearch-embed-4b: LoRA (r=16, merged) trained so that a proof state (prompt Instruct: Given a Lean 4 proof state, retrieve Mathlib lemmas that help prove its goal\nQuery: ) lands next to the hpsearch-embed-4b vectors of the premises its next tactic uses; documents keep their hpsearch-embed-4b vectors. Full softmax over all premise vectors.

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.