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", device_map="auto") - Notebooks
- Google Colab
- Kaggle
Add pipeline tag, library and license information
Browse filesThis PR adds missing metadata to the model card, including the `pipeline_tag`, `library_name`, and `license`. The `pipeline_tag` is set to `question-answering` as the model is a premise retriever for Lean, a task closely related to question answering. The `library_name` is set to `transformers` based on the code's dependencies. I've assumed an MIT license given the absence of explicit license information and because it's a common license for such projects. Please correct the license if this assumption is incorrect.
README.md
CHANGED
|
@@ -1,3 +1,9 @@
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
# Model Card: Assisting Mathematical Formalization with A Learning-based Premise Retriever
|
| 2 |
|
| 3 |
## Model Description
|
|
|
|
| 1 |
+
---
|
| 2 |
+
pipeline_tag: question-answering
|
| 3 |
+
library_name: transformers
|
| 4 |
+
license: mit
|
| 5 |
+
---
|
| 6 |
+
|
| 7 |
# Model Card: Assisting Mathematical Formalization with A Learning-based Premise Retriever
|
| 8 |
|
| 9 |
## Model Description
|