DAPS-Math/DAPS-text-encoder

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.