File size: 1,627 Bytes
1efe71e dbb8c9c 1efe71e |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 |
# 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},
}
``` |