hpsearch-rerank-4b

The reranker of hpsearch's best mode: Qwen/Qwen3-Reranker-4B (4B parameters) LoRA-fine-tuned twice (listwise softmax over one positive and seven hard negatives per query) and averaged with the base model: weights = 0.5 base + 0.25 each fine-tune. Same prompt and yes/no scoring as Qwen3-Reranker; hpsearch shows each document as its Lean statement then its NL statement, cut at 112 tokens (16 documents per query).

Fine-tuning data (public, generated locally):

• six-style search queries (a Lean fragment, LaTeX, a plain-English description, a slogan, a nickname, a concrete special case) written by Qwen3-30B-A3B-Instruct-2507 for 201k declarations of the LeanSearch v2 Mathlib corpus (FrenzyMath/lsv2-mathlib-v4.28.0-rc1-jsonl: every definition, structure, class, instance and abbrev, and 120k theorems), from each declaration's Lean statement and its public informalization; hard negatives mined with the previous embedder (positive-aware: a negative's cosine is below 0.95 x the positive's);
• replayed public pairs of hmzprover/hpsearch-embed-4b's training set (Lean Finder and LeanSearch v2 informalizations, Mathlib signatures, LeanStateSearch's train split).

Decontamination: no declaration that is a gold of any evaluation set used by hpsearch (MathlibQR / MathlibMPR, Lean Finder, LeanStateSearch, LeanDojo, MIRB, TheoremSearch, TBPS, hmzprover; every split) is used as a positive or prompted for, by name or by statement, and every query equal (normalised) to an evaluation query is dropped.