hpsearch-rerank-4b-state

Qwen3-Reranker-4B fine-tuned (LoRA r=16, merged) to judge whether a premise helps a Lean proof state, for hpsearch's modes best and deep. Same prompt format as Qwen3-Reranker (instruction: Given a Lean 4 proof state, retrieve Mathlib lemmas that help prove its goal). Listwise loss over a gold premise and 7 hard negatives mined with hmzprover/hpsearch-embed-4b-state (accessible premises only), 40,000 training states.

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.