---
pipeline_tag: sentence-similarity
library_name: transformers
license: mit
---

# Model Card: Assisting Mathematical Formalization with A Learning-based Premise Retriever

## Model Description

This model is designed for **premise retrieval** in **Lean**, based on the **state representation** of Lean. The model follows the architecture described in the paper:

[Assisting Mathematical Formalization with A Learning-based Premise Retriever](https://arxiv.org/abs/2501.13959)

The model implementation and code are available at:

[GitHub Repository](https://github.com/ruc-ai4math/Premise-Retrieval)

[Try our model](https://premise-search.com)

---

## Available Models

The repository provides several models for different tasks:

### Pre-trained Models
Located in the `Pretrain_Model` folder:

- **410_stable_random**: Pre-trained model for **retrieval fine-tuning**.
- **410_stable_random_1024**: Pre-trained model for **reranking fine-tuning**.

### Fine-tuned Models

#### Retrieval Fine-tuned Models
Located in the `Finetune_Model` folder:

- Models fine-tuned on specific datasets for **retrieval tasks**.

#### Rerank Fine-tuned Models
Located in the `Rerank` folder:

- Models fine-tuned on specific datasets for **reranking tasks**.



## Citation
If you use this model, please cite the following paper:

```
@misc{tao2025assistingmathematicalformalizationlearningbased,
      title={Assisting Mathematical Formalization with A Learning-based Premise Retriever}, 
      author={Yicheng Tao and Haotian Liu and Shanwen Wang and Hongteng Xu},
      year={2025},
      eprint={2501.13959},
      archivePrefix={arXiv},
      primaryClass={cs.CL},
      url={https://arxiv.org/abs/2501.13959}, 
}
```