uw-math-ai/MathLeap-Octen-8B

MathLeap-Octen-8B

An 8B retrieval-tuned embedding model for mathematical text. Fine-tuned from Octen/Octen-Embedding-8B. It's a retrieval-specialized variant of Qwen3-Embedding-8B — on mathlib4 concepts via multi-view contrastive learning. The goal is to embed mathematically equivalent statements close together regardless of the surface language they are written in.

Usage

from huggingface_hub import snapshot_download
from sentence_transformers import SentenceTransformer

# Download model files from anonymous mirror
model_path = snapshot_download(
    repo_id="anonymous-submission/MathLeap-Octen-8B",
    endpoint="https://anonymous-hf.up.railway.app/a/9n9cngyu38hk/", 
)

# Load locally
model = SentenceTransformer(model_path)

query = "For any natural number n, n + 0 = n."
docs = [
    "theorem add_zero (n : ℕ) : n + 0 = n := rfl",
    "theorem mul_zero (n : ℕ) : n * 0 = 0 := rfl",
]
q_emb = model.encode([query])
d_emb = model.encode(docs)
print(q_emb @ d_emb.T)

The model accepts queries and documents interchangeably across three forms: informal natural-language descriptions, Lean 4 type signatures (e.g., α → α → α), and full Lean 4 declarations (e.g., theorem foo (x : ℕ) : ...).

Model details

Training

Data

The training set is derived from FrenzyMath/mathlib_informal_v4.19.0 (Apache 2.0), augmented with LLM-generated natural-language rephrasings. Each mathlib concept has up to four parallel "views":

• —nl_informal: informal natural-language description
• —nl_informal_2: LLM-generated NL rephrasing (~85% of concepts)
• —lean_type: Lean 4 type signature
• —lean_signature: full Lean 4 declaration

Rephrasings were generated by prompting an LLM to first decompose each statement into hypotheses and conclusions, then reassemble them with a different surface form (different variable names, sentence structure, voice, or quantifier ordering) while preserving mathematical content.

The full training set contains 118,334 concepts; held-out evaluation uses 15,287 concepts. Train/dev split is by mathlib module to prevent leakage of structurally related theorems.

Objective

Multi-view contrastive learning with CachedMultipleNegativesRankingLoss (Gao et al., 2021). For each concept, the data loader samples a random view pair as (anchor, positive); other concepts in the same batch serve as in-batch negatives. The cached variant chunks forward passes so that 8B models fit at batch_size 16 on a single 80GB GPU while remaining mathematically equivalent to standard MNRL.

This setup implicitly covers all six retrieval directions across NL and Lean modalities (NL→Lean, Lean→NL, NL↔NL, Lean↔Lean) without explicit direction supervision.

Hyperparameters

Evaluation

In-domain held-out FrenzyMath retrieval (six directions)

R@1 / MRR on the held-out test set (15,287 concepts):

All six directions improve, with the largest gains on Lean → Informal directions. Improvements stack on top of the strong retrieval-specialized starting point that Octen-Embedding-8B already provides.

Lean Blueprints retrieval

MIRB (out-of-distribution; nDCG@10)

MathLeap-Octen-8B improves on Mathlib Retrieval (the task closest to the training distribution) but degrades on MathOverflow Duplicate retrieval (which involves conversational math beyond rigorous theorem statements) and Lean Premise retrieval (whose queries are proof states, not represented in our training data).

Intended use

• —Semantic search over mathlib4 declarations (NL → Lean or Lean → NL)
• —Cross-presentation similarity scoring for mathematical statements written in different mathematical sub-languages
• —Embedding feature extraction for downstream math NLP tasks
• —Retrieval-augmented generation in mathematical contexts

Out-of-scope use

• —Open-ended math QA or proof generation (this is a retrieval model)
• —Non-mathematical English text — heavily specialized, no general-purpose embedding ability guaranteed
• —Safety-critical mathematical verification without independent checking
• —Proof-state retrieval (training data does not include tactic-mode Lean)
• —Languages other than English
• —Cross-lingual mathematical retrieval (not evaluated)

Limitations

1. 1.Same-distribution training: Trained on FrenzyMath-derived data with a particular informalization style. Performance on math text in substantially different registers (conversational math, textbook prose, research-paper exposition) may degrade. We observe this on MathOverflow Duplicate retrieval, where MathLeap-Octen-8B underperforms its base.

1. 1.No proof-state coverage: Training data contains theorem statements (lean_type, lean_signature) but not Lean proof states. On Lean Premise retrieval (MIRB), where queries are tactic-mode terms, MathLeap-Octen-8B underperforms its base.

1. 1.Stacked specialization: Since the base (Octen-Embedding-8B) is already a retrieval-specialized fine-tune of Qwen3-Embedding-8B, gains from MathLeap fine-tuning are smaller in absolute magnitude than for the Qwen-base variant. The trade-off pattern across tasks is similar.

1. 1.Single-seed estimates: All reported numbers are from a single training run with seed 42; training variance is not characterized.

License

Apache 2.0, matching the upstream Octen-Embedding-8B base model and FrenzyMath training data.

Acknowledgments

Built on Octen-Embedding-8B (Octen Team). Training data derived from FrenzyMath's mathlib_informal release. Mathematics from the mathlib4 community.