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
hmzprover/hpsearch-rerank-4b-state
Input Modalities
Output Modalities
Supported Functionality
Public training splits only:
random/train: each traced tactic's state paired with the premises it uses;ruc-ai4math/mathlib_handler_benchmark_410) random/train, the same way.
For part of the states, a one-to-three-sentence English description of the next step (written by an LLM from
the state and the tactic) follows the state, as in Lean Finder's "augmented" proof states.Decontamination (strict): a state is dropped when its theorem is in a held-out split or is the theorem of any evaluation query, when its text equals any evaluation query, or when its goal equals the goal of any proof-state evaluation query; a premise is dropped when its name or statement is a gold of any evaluation (MathlibQR/MPR, Lean Finder, LeanStateSearch, TBPS, TheoremSearch, MIRB, LeanDojo, hpsearch's own); such premises are also left out of the contrastive softmax. Kept: 147,412 states (89,719 LeanDojo, 57,693 LeanStateSearch), 89,298 premises.