| --- |
| 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. |
|
|
