hpsearch-embed-4b-state-v3

The proof-state query embedder of hpsearch's GPU modes: the query side (LoRA r=16, merged) of its base, trained so that a proof state, optionally followed by an English description of the next step, lands next to the base's vectors of the premises the next tactic uses (documents keep the base's vectors; pairs_with names it). Full softmax over all premise vectors.

Training data

Public training splits only, in full:

• 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: a training state is dropped when its text equals any evaluation query (MathlibQR/MPR, Lean Finder, LeanStateSearch, TBPS, TheoremSearch, MIRB, LeanDojo, hpsearch's own), or when its goals and hypotheses equal those of a proof-state evaluation query; a (state, premise) pair is dropped when the state's goal equals an evaluation query's goal and the premise is that query's gold. Premises that are golds of evaluation queries stay in training with other states, as the training splits' own authors train. Kept: 243,040 states, 566,274 (state, premise) pairs, 112,529 premises.