hpsearch-embed-fast-v2

The query side of hpsearch's mode fast for proof states and Lean terms: the first layers of Qwen3-Embedding-0.6B and a linear map to 2,560 dimensions, trained so that a query lands next to the hmzprover/hpsearch-embed-4b-v2 vectors of what it asks for (documents keep their hpsearch-embed-4b-v2 vectors; pairs_with names it). A few ms per query on an A100 with CUDA-graph replay.

Queries: a proof state (prompt Instruct: Given a Lean 4 proof state, retrieve Mathlib lemmas that help prove its goal\nQuery: , goal first), its goal alone, or a Lean expression (a statement's conclusion or Pi type; prompt Instruct: Given Lean 4 code, retrieve the Mathlib declaration it states or names\nQuery: ). Full softmax over the frozen document vectors, plus distillation (KL over the documents) from hpsearch-embed-4b-v2's own query side on expressions. Lean expressions come from the training corpora's own statements (no evaluation gold among them).

Training data

Public training splits only, in full:

• LeanDojo Benchmark 4 (v10) random/train: each traced tactic's state paired with the premises it uses;
• LeanStateSearch (ruc-ai4math/mathlib_handler_benchmark_410) random/train, the same way. For part of the states, a one-to-three-sentence English description of the next step (written by an LLM from the state and the tactic) follows the state, as in Lean Finder's "augmented" proof states.

Decontamination: a training state is dropped when its text equals any evaluation query (MathlibQR/MPR, Lean Finder, LeanStateSearch, TBPS, TheoremSearch, MIRB, LeanDojo, hpsearch's own), or when its goals and hypotheses equal those of a proof-state evaluation query; a (state, premise) pair is dropped when the state's goal equals an evaluation query's goal and the premise is that query's gold. Premises that are golds of evaluation queries stay in training with other states, as the training splits' own authors train. Kept: 243,040 states, 566,274 (state, premise) pairs, 112,529 premises.