metadata
license: apache-2.0
base_model: Alibaba-NLP/gte-modernbert-base
base_model_relation: finetune
library_name: sentence-transformers
pipeline_tag: sentence-similarity
tags:
- premise-selection
- lean
- mathlib
DAPS Text Encoder
The text encoder produced by Phase 1 of DAPS, fine-tuned on Mathlib from gte-modernbert-base. It produces 768-dimensional embeddings using CLS pooling and can be used independently as a Mathlib text encoder.
For better premise-selection performance, we recommend pairing it with the graph-aware DAPS Selector produced by Phase 2.
from sentence_transformers import SentenceTransformer
model = SentenceTransformer("DAPS-Math/DAPS-text-encoder")
model.max_seq_length = 1024
embeddings = model.encode(
["∀ n : ℕ, n + 0 = n", "∀ a b : ℕ, a + b = b + a"],
normalize_embeddings=True,
)
print(embeddings.shape)
DAPS uses a 1024-token input limit. See the DAPS project page for the full premise-selection pipeline.