| --- |
| license: apache-2.0 |
| base_model: Qwen/Qwen3-Embedding-0.6B |
| library_name: sentence-transformers |
| pipeline_tag: sentence-similarity |
| tags: [lean4, mathlib, retrieval, premise-selection] |
| --- |
| |
| # hpsearch-embed-fast |
|
|
| The query side of [hpsearch](https://github.com/humanfia/hpsearch)'s mode `fast` for proof states and Lean |
| expressions: the first 8 layers of Qwen3-Embedding-0.6B and a linear map to 2,560 dimensions, trained so that a |
| query lands next to the [`hmzprover/hpsearch-embed-4b-v2`](https://huggingface.co/hmzprover/hpsearch-embed-4b-v2) |
| vectors of what it asks for (documents keep their hpsearch-embed-4b-v2 vectors; `pairs_with` names it). About |
| 3 ms per query on an A100 with CUDA-graph replay. |
|
|
| Queries: a proof state (prompt `Instruct: Given a Lean 4 proof state, retrieve Mathlib lemmas that help prove its |
| goal\nQuery: `, goal first), its goal alone, or a Lean expression (a statement's conclusion or Pi type; prompt |
| `Instruct: Given Lean 4 code, retrieve the Mathlib declaration it states or names\nQuery: `). Full softmax over the |
| frozen document vectors, plus distillation (KL over the documents) from hpsearch-embed-4b-v2's own query side on |
| expressions. Lean expressions come from the training corpora's own statements (no evaluation gold among them). |
|
|
| ## Training data |
|
|
| Public training splits only: |
| - LeanDojo Benchmark 4 (v10) `random/train`: each traced tactic's state paired with the premises it uses; |
| - LeanStateSearch (`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. |
|
|
