Create README.md

README.md

@@ -0,0 +1,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](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}, 
+}
+```