update model
Browse files- README.md +3 -25
- config.json +1 -1
- generation_config.json +1 -1
- model.safetensors +1 -1
README.md
CHANGED
@@ -1,25 +1,3 @@
|
|
1 |
-
---
|
2 |
-
license: mit
|
3 |
-
|
4 |
-
parameters:
|
5 |
-
max_length: 1024
|
6 |
-
widget:
|
7 |
-
- text: "a b : ℕ\n⊢ a + b = b + a"
|
8 |
-
example_title: "Example"
|
9 |
-
---
|
10 |
-
|
11 |
-
[LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://arxiv.org/abs/xxxx.xxxxx)
|
12 |
-
NeurIPS (Datasets and Benchmarks Track), 2023
|
13 |
-
[Kaiyu Yang](https://yangky11.github.io/), [Aidan Swope](https://aidanswope.com/about), [Alex Gu](https://minimario.github.io/), [Rahul Chalamala](https://www.linkedin.com/in/rchalamala),
|
14 |
-
[Peiyang Song](https://www.linkedin.com/in/peiyang-song-3279b3251/), [Shixing Yu](https://billysx.github.io/), [Saad Godil](https://www.linkedin.com/in/saad-godil-9728353/), [Ryan Prenger](https://www.linkedin.com/in/ryan-prenger-18797ba1/), [Anima Anandkumar](http://tensorlab.cms.caltech.edu/users/anima/)
|
15 |
-
|
16 |
-
```bibtex
|
17 |
-
@inproceedings{yang2023leandojo,
|
18 |
-
title={{LeanDojo}: Theorem Proving with Retrieval-Augmented Language Models},
|
19 |
-
author={Yang, Kaiyu and Swope, Aidan and Gu, Alex and Chalamala, Rahul and Song, Peiyang and Yu, Shixing and Godil, Saad and Prenger, Ryan and Anandkumar, Anima},
|
20 |
-
booktitle={Neural Information Processing Systems (NeurIPS)},
|
21 |
-
year={2023}
|
22 |
-
}
|
23 |
-
```
|
24 |
-
|
25 |
-
Please visit [LeanDojo Website](https://leandojo.org/) for details.
|
|
|
1 |
+
---
|
2 |
+
license: mit
|
3 |
+
---
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
config.json
CHANGED
@@ -27,7 +27,7 @@
|
|
27 |
"tie_word_embeddings": false,
|
28 |
"tokenizer_class": "ByT5Tokenizer",
|
29 |
"torch_dtype": "float32",
|
30 |
-
"transformers_version": "4.
|
31 |
"use_cache": true,
|
32 |
"vocab_size": 384
|
33 |
}
|
|
|
27 |
"tie_word_embeddings": false,
|
28 |
"tokenizer_class": "ByT5Tokenizer",
|
29 |
"torch_dtype": "float32",
|
30 |
+
"transformers_version": "4.42.3",
|
31 |
"use_cache": true,
|
32 |
"vocab_size": 384
|
33 |
}
|
generation_config.json
CHANGED
@@ -3,5 +3,5 @@
|
|
3 |
"decoder_start_token_id": 0,
|
4 |
"eos_token_id": 1,
|
5 |
"pad_token_id": 0,
|
6 |
-
"transformers_version": "4.
|
7 |
}
|
|
|
3 |
"decoder_start_token_id": 0,
|
4 |
"eos_token_id": 1,
|
5 |
"pad_token_id": 0,
|
6 |
+
"transformers_version": "4.42.3"
|
7 |
}
|
model.safetensors
CHANGED
@@ -1,3 +1,3 @@
|
|
1 |
version https://git-lfs.github.com/spec/v1
|
2 |
-
oid sha256:
|
3 |
size 1198571496
|
|
|
1 |
version https://git-lfs.github.com/spec/v1
|
2 |
+
oid sha256:769fc3b498785e2492b35da4ee3e92a9a48a386807f2885258d6a4340aa2473c
|
3 |
size 1198571496
|