Instructions to use ruc-ai4math/Lean_State_Search_Random with libraries, inference providers, notebooks, and local apps. Follow these links to get started.
- Libraries
- Transformers
How to use ruc-ai4math/Lean_State_Search_Random with Transformers:
# Load model directly from transformers import AutoModel model = AutoModel.from_pretrained("ruc-ai4math/Lean_State_Search_Random", dtype="auto") - Notebooks
- Google Colab
- Kaggle
Update pipeline tag to text-ranking
#2
by nielsr HF Staff - opened
README.md
CHANGED
|
@@ -1,7 +1,7 @@
|
|
| 1 |
---
|
| 2 |
-
pipeline_tag: sentence-similarity
|
| 3 |
library_name: transformers
|
| 4 |
license: mit
|
|
|
|
| 5 |
---
|
| 6 |
|
| 7 |
# Model Card: Assisting Mathematical Formalization with A Learning-based Premise Retriever
|
|
|
|
| 1 |
---
|
|
|
|
| 2 |
library_name: transformers
|
| 3 |
license: mit
|
| 4 |
+
pipeline_tag: text-ranking
|
| 5 |
---
|
| 6 |
|
| 7 |
# Model Card: Assisting Mathematical Formalization with A Learning-based Premise Retriever
|