Update README.md

README.md

@@ -1,57 +1,30 @@
----
-library_name: sentence-transformers
-pipeline_tag: sentence-similarity
-tags:
-- sentence-transformers
-- feature-extraction
-- sentence-similarity
+# Model Card: Assisting Mathematical Formalization with A Learning-based Premise Retriever
 
----
+## Model Description
 
-# {MODEL_NAME}
+This model is the first version designed for **premise retrieval** in **Lean**, based on the **state representation** of Lean. The model follows the architecture described in the paper:
 
-This is a [sentence-transformers](https://www.SBERT.net) model: It maps sentences & paragraphs to a 768 dimensional dense vector space and can be used for tasks like clustering or semantic search.
+[Assisting Mathematical Formalization with A Learning-based Premise Retriever](https://arxiv.org/abs/2501.13959)
 
-<!--- Describe your model here -->
+The model implementation and code are available at:
 
-## Usage (Sentence-Transformers)
+[GitHub Repository](https://github.com/ruc-ai4math/Premise-Retrieval)
 
-Using this model becomes easy when you have [sentence-transformers](https://www.SBERT.net) installed:
-
-```
-pip install -U sentence-transformers
-```
-
-Then you can use the model like this:
-
-```python
-from sentence_transformers import SentenceTransformer
-sentences = ["This is an example sentence", "Each sentence is converted"]
-
-model = SentenceTransformer('{MODEL_NAME}')
-embeddings = model.encode(sentences)
-print(embeddings)
-```
+[Try our model](https://premise-search.com)
 
 
 
-## Evaluation Results
+## Citation
+If you use this model, please cite the following paper:
 
-<!--- Describe how your model was evaluated -->
-
-For an automated evaluation of this model, see the *Sentence Embeddings Benchmark*: [https://seb.sbert.net](https://seb.sbert.net?model_name={MODEL_NAME})
-
-
-
-## Full Model Architecture
 ```
-SentenceTransformer(
-  (0): Transformer({'max_seq_length': 512, 'do_lower_case': False}) with Transformer model: BertModel 
-  (1): Pooling({'word_embedding_dimension': 768, 'pooling_mode_cls_token': False, 'pooling_mode_mean_tokens': True, 'pooling_mode_max_tokens': False, 'pooling_mode_mean_sqrt_len_tokens': False, 'pooling_mode_weightedmean_tokens': False, 'pooling_mode_lasttoken': False, 'include_prompt': True})
-  (2): Normalize()
-)
-```
-
-## Citing & Authors
-
-<!--- Describe where people can find more information -->
+@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}, 
+}
+```