hpsearch-embed-xs-agent

The CPU embedder of hpsearch's balanced mode: hmzprover/hpsearch-embed-xs (snowflake-arctic-embed-xs, 22M parameters) fine-tuned further on agents' search queries.

• model.onnx: inputs input_ids, attention_mask (int64); output embedding, unit vectors (batch x 384). fp32 weights (int8 quantization lost 0.01 NDCG@10 on the hmzprover dev half).
• tokenizer.json: the base model's tokenizer. No instruction prefix; hpsearch replaces Lean notation with words and puts a proof state's goal first.

Fine-tuning data:

• agent search queries from hmzprover/query-chains (keyword bags and guessed Lean names an agent typed into a theorem search tool), each paired with the declaration its chain finally found (in hmzprover/proofs); hard negatives are the lexical search hits that are not that declaration;
• replayed public pairs of the base model's own training set.

Decontamination: every chain of the hmzprover search benchmark (positive and negative chains) is excluded, and every pair whose normalised query text, or whose target's name or statement, occurs in any evaluation set used by hpsearch (MathlibQR / MathlibMPR, Lean Finder, LeanStateSearch, TheoremSearch, TBPS, hmzprover) is dropped.