GLM-5.3 is live. Run Z.ai's latest model on Friendli Model APIs. Try it today ➜
hmzprover
Available on FriendliAI
Run this model inference on single tenant GPU with unmatched speed and reliability at scale.
Model Details
Model Provider
hmzprover
Model Tree
Qwen/Qwen3-Reranker-4B
Input Modalities
Output Modalities
Supported Functionality
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:
text
Given a Lean 4 proof state, retrieve Mathlib lemmas that help prove its goalhmzprover/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.