hpsearch-embed-xs

A small sentence embedder for searching Lean 4 / Mathlib declarations, used by the dense channel of hpsearch. Fine-tuned from Snowflake/snowflake-arctic-embed-xs.

• model.onnx: inputs input_ids, attention_mask (int64, batch x tokens); output embedding, unit-length vectors (batch x 384). Weights quantized to int8 for CPU inference with onnxruntime.
• tokenizer.json: the base model's tokenizer.

Queries and documents use no instruction prefix. Before tokenizing, hpsearch replaces common Lean notation with words (e.g. ℝ -> real, ∀ -> forall) and puts a proof state's goal first.

Training pairs (in-batch negatives), from public datasets:

• FrenzyMath/mathlib_informal_v4.19.0: informal names, descriptions and docstrings -> declarations
• FrenzyMath/Herald_statements: informal -> formal statements
• ruc-ai4math/mathlib_handler_benchmark_410 (random split, train): proof states -> premises used
• uw-math-ai/theorem-search-dataset: theorem statements -> slogans

Pairs whose query or target declaration appears in the evaluation sets of LeanFinder, LeanSearch v2 (MathlibQR), LeanStateSearch, TheoremSearch, TBPS or hmzprover/query-chains were removed.