Update README.md
Browse files
README.md
CHANGED
@@ -5,7 +5,7 @@ datasets:
|
|
5 |
language:
|
6 |
- en
|
7 |
base_model:
|
8 |
-
- internlm/internlm2-math-7b
|
9 |
- deepseek-ai/deepseek-math-7b-base
|
10 |
pipeline_tag: text-generation
|
11 |
library_name: transformers
|
@@ -22,7 +22,7 @@ tags:
|
|
22 |
<a href="https://github.com/leanprover-community/mathlib4"><img src="https://img.shields.io/badge/Lean-4-orange" alt="Lean 4"></a>
|
23 |
<a href="https://github.com/Purewhite2019/rethinking_autoformalization"><img src="https://img.shields.io/badge/GitHub-%23121011.svg?logo=github&logoColor=white" alt="GitHub"></a>
|
24 |
</div>
|
25 |
-
<h2>Qi Liu, Xinhao Zheng, Xudong Lu, Qinxiang Cao
|
26 |
<h2>Sch. of Computer Science & Sch. of Artificial Intelligence, Shanghai Jiao Tong University</h2>
|
27 |
</div>
|
28 |
|
@@ -33,7 +33,7 @@ Please refer to the [📺GitHub repo](https://github.com/Purewhite2019/rethinkin
|
|
33 |
## 📈 Performance
|
34 |
| | **Benchmark** | **ProofNet** | **Con-NF** |
|
35 |
|:---------------------:|:--------------------:|--------------|------------|
|
36 |
-
| **InternLM2-Math 7B** | Rautoformalizer (-R) | 16.58% | 4.58% |
|
37 |
| | RAutoformalizer | 18.18% | 16.86% |
|
38 |
| | Rautoformalizer (+R) | 31.28% | 55.36% |
|
39 |
| **DeepseekMath 7B** | Rautoformalizer (-R) | 15.24% | 4.27% |
|
@@ -43,7 +43,7 @@ Please refer to the [📺GitHub repo](https://github.com/Purewhite2019/rethinkin
|
|
43 |
## ⚙️ Usage
|
44 |
### w/o Dependency Retrieval
|
45 |
- [🤗`purewhite42/rautoformalizer_nora_deepseek`](https://huggingface.co/purewhite42/rautoformalizer_nora_deepseek): w/o dependency retrieval, SFTed from [🤗`deepseek-ai/deepseek-math-7b-base`](https://huggingface.co/deepseek-ai/deepseek-math-7b-base)
|
46 |
-
- [🤗`purewhite42/rautoformalizer_nora_internlm`](https://huggingface.co/purewhite42/rautoformalizer_nora_internlm): w/o dependency retrieval, SFTed from [🤗`internlm/internlm2-math-7b`](https://huggingface.co/internlm/internlm2-math-7b)
|
47 |
|
48 |
```shell
|
49 |
python -m autoformalizer.autoformalize_vllm_passk \
|
@@ -62,7 +62,7 @@ python -m autoformalizer.autoformalize_vllm_passk \
|
|
62 |
```
|
63 |
### RAutofromalizer (w/ Dependency Retrieval)
|
64 |
- [🤗`purewhite42/rautoformalizer_ra_deepseek`](https://huggingface.co/purewhite42/rautoformalizer_ra_deepseek): w/ dependency retrieval (`dependency_retriever_f`), SFTed from [🤗`deepseek-ai/deepseek-math-7b-base`](https://huggingface.co/deepseek-ai/deepseek-math-7b-base)
|
65 |
-
- [🤗`purewhite42/rautoformalizer_ra_internlm`](https://huggingface.co/purewhite42/rautoformalizer_ra_internlm): w/ dependency retrieval (`dependency_retriever_f`), SFTed from [🤗`internlm/internlm2-math-7b`](https://huggingface.co/internlm/internlm2-math-7b)
|
66 |
```shell
|
67 |
python -m autoformalizer.autoformalize_vllm_w_ra_passk \
|
68 |
--port ... \ # Can be arbitrarily set (should avoid conflict)
|
@@ -81,7 +81,7 @@ python -m autoformalizer.autoformalize_vllm_w_ra_passk \
|
|
81 |
```
|
82 |
### Oracle RAutoformalizer (w/ Ground-truth Dependencies)
|
83 |
- [🤗`purewhite42/rautoformalizer_gtra_deepseek`](https://huggingface.co/purewhite42/rautoformalizer_gtra_deepseek): w/ oracle dependency retrieval, SFTed from [🤗`deepseek-ai/deepseek-math-7b-base`](https://huggingface.co/deepseek-ai/deepseek-math-7b-base)
|
84 |
-
- [🤗`purewhite42/rautoformalizer_gtra_internlm`](https://huggingface.co/purewhite42/rautoformalizer_gtra_internlm): w/ oracle dependency retrieval, SFTed from [🤗`internlm/internlm2-math-7b`](https://huggingface.co/internlm/internlm2-math-7b)
|
85 |
```shell
|
86 |
python -m autoformalizer.autoformalize_vllm_w_gt_passk \
|
87 |
--port ... \ # Can be arbitrarily set (should avoid conflict)
|
|
|
5 |
language:
|
6 |
- en
|
7 |
base_model:
|
8 |
+
- internlm/internlm2-math-base-7b
|
9 |
- deepseek-ai/deepseek-math-7b-base
|
10 |
pipeline_tag: text-generation
|
11 |
library_name: transformers
|
|
|
22 |
<a href="https://github.com/leanprover-community/mathlib4"><img src="https://img.shields.io/badge/Lean-4-orange" alt="Lean 4"></a>
|
23 |
<a href="https://github.com/Purewhite2019/rethinking_autoformalization"><img src="https://img.shields.io/badge/GitHub-%23121011.svg?logo=github&logoColor=white" alt="GitHub"></a>
|
24 |
</div>
|
25 |
+
<h2>Qi Liu, Xinhao Zheng, Xudong Lu, Qinxiang Cao*, Junchi Yan* (* indicates Correspondence author)</h2>
|
26 |
<h2>Sch. of Computer Science & Sch. of Artificial Intelligence, Shanghai Jiao Tong University</h2>
|
27 |
</div>
|
28 |
|
|
|
33 |
## 📈 Performance
|
34 |
| | **Benchmark** | **ProofNet** | **Con-NF** |
|
35 |
|:---------------------:|:--------------------:|--------------|------------|
|
36 |
+
| **InternLM2-Math-Base 7B** | Rautoformalizer (-R) | 16.58% | 4.58% |
|
37 |
| | RAutoformalizer | 18.18% | 16.86% |
|
38 |
| | Rautoformalizer (+R) | 31.28% | 55.36% |
|
39 |
| **DeepseekMath 7B** | Rautoformalizer (-R) | 15.24% | 4.27% |
|
|
|
43 |
## ⚙️ Usage
|
44 |
### w/o Dependency Retrieval
|
45 |
- [🤗`purewhite42/rautoformalizer_nora_deepseek`](https://huggingface.co/purewhite42/rautoformalizer_nora_deepseek): w/o dependency retrieval, SFTed from [🤗`deepseek-ai/deepseek-math-7b-base`](https://huggingface.co/deepseek-ai/deepseek-math-7b-base)
|
46 |
+
- [🤗`purewhite42/rautoformalizer_nora_internlm`](https://huggingface.co/purewhite42/rautoformalizer_nora_internlm): w/o dependency retrieval, SFTed from [🤗`internlm/internlm2-math-base-7b`](https://huggingface.co/internlm/internlm2-math-base-7b)
|
47 |
|
48 |
```shell
|
49 |
python -m autoformalizer.autoformalize_vllm_passk \
|
|
|
62 |
```
|
63 |
### RAutofromalizer (w/ Dependency Retrieval)
|
64 |
- [🤗`purewhite42/rautoformalizer_ra_deepseek`](https://huggingface.co/purewhite42/rautoformalizer_ra_deepseek): w/ dependency retrieval (`dependency_retriever_f`), SFTed from [🤗`deepseek-ai/deepseek-math-7b-base`](https://huggingface.co/deepseek-ai/deepseek-math-7b-base)
|
65 |
+
- [🤗`purewhite42/rautoformalizer_ra_internlm`](https://huggingface.co/purewhite42/rautoformalizer_ra_internlm): w/ dependency retrieval (`dependency_retriever_f`), SFTed from [🤗`internlm/internlm2-math-base-7b`](https://huggingface.co/internlm/internlm2-math-base-7b)
|
66 |
```shell
|
67 |
python -m autoformalizer.autoformalize_vllm_w_ra_passk \
|
68 |
--port ... \ # Can be arbitrarily set (should avoid conflict)
|
|
|
81 |
```
|
82 |
### Oracle RAutoformalizer (w/ Ground-truth Dependencies)
|
83 |
- [🤗`purewhite42/rautoformalizer_gtra_deepseek`](https://huggingface.co/purewhite42/rautoformalizer_gtra_deepseek): w/ oracle dependency retrieval, SFTed from [🤗`deepseek-ai/deepseek-math-7b-base`](https://huggingface.co/deepseek-ai/deepseek-math-7b-base)
|
84 |
+
- [🤗`purewhite42/rautoformalizer_gtra_internlm`](https://huggingface.co/purewhite42/rautoformalizer_gtra_internlm): w/ oracle dependency retrieval, SFTed from [🤗`internlm/internlm2-math-base-7b`](https://huggingface.co/internlm/internlm2-math-base-7b)
|
85 |
```shell
|
86 |
python -m autoformalizer.autoformalize_vllm_w_gt_passk \
|
87 |
--port ... \ # Can be arbitrarily set (should avoid conflict)
|