README.md

---
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](https://huggingface.co/datasets/DAPS-Math/DAPS-Mathlib-Graph) from [gte-modernbert-base](https://huggingface.co/Alibaba-NLP/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](https://huggingface.co/DAPS-Math/DAPS-selector) produced by Phase 2.

```python
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](https://relational-conjecturing.github.io/Dependency-Aware-Premise-Selection/) for the full premise-selection pipeline.