Create README.md

README.md

@@ -0,0 +1,119 @@
+---
+license: apache-2.0
+datasets:
+- hoskinson-center/proofnet
+language:
+- en
+base_model:
+- internlm/internlm2-math-7b
+- deepseek-ai/deepseek-math-7b-base
+pipeline_tag: text-generation
+library_name: transformers
+tags:
+- lean4
+- statement-autoformalization
+- formal-mathematics
+---
+
+<div align="center">
+  <h1 style="font-size: 1.5em;">[ICLR'25 Spotlight] Rethinking and Improving Autoformalization: Towards a Faithful Metric and a Dependency Retrieval-based Approach</h1>
+  <div style="display: flex; justify-content: center; gap: 8px; flex-wrap: wrap;">
+    <a href="https://choosealicense.com/licenses/apache-2.0/"><img src="https://img.shields.io/badge/License-Apache%202.0-blue.svg" alt="License: Apache 2.0"></a>
+    <a href="https://github.com/leanprover-community/mathlib4"><img src="https://img.shields.io/badge/Lean-4-orange" alt="Lean 4"></a>
+    <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>
+  </div>
+  <h2>Qi Liu, Xinhao Zheng, Xudong Lu, Qinxiang Cao, Junchi Yan* (* indicates Correspondence author)</h2>
+  <h2>Sch. of Computer Science & Sch. of Artificial Intelligence, Shanghai Jiao Tong University</h2>
+</div>
+
+Please refer to the [📺GitHub repo](https://github.com/Purewhite2019/rethinking_autoformalization) and 
+[📃Paper](https://openreview.net/pdf?id=hUb2At2DsQ) for more details.
+
+
+## 📈 Performance
+|                       |     **Benchmark**    | **ProofNet** | **Con-NF** |
+|:---------------------:|:--------------------:|--------------|------------|
+| **InternLM2-Math 7B** | Rautoformalizer (-R) | 16.58%       | 4.58%      |
+|                       | RAutoformalizer      | 18.18%       | 16.86%     |
+|                       | Rautoformalizer (+R) | 31.28%       | 55.36%     |
+| **DeepseekMath 7B**   | Rautoformalizer (-R) | 15.24%       | 4.27%      |
+|                       | RAutoformalizer      | 17.91%       | 15.30%     |
+|                       | Rautoformalizer (+R) | 32.62%       | 59.00%     |
+
+## ⚙️ Usage
+### w/o Dependency Retrieval
+- [🤗`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)
+- [🤗`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)
+
+```shell
+python -m autoformalizer.autoformalize_vllm_passk \
+    --port ... \    # Can be arbitrarily set (should avoid conflict)
+    --trust-remote-code \
+    --enable-prefix-caching \
+    --model /path/to/model \
+    --mathlib_root ... \ # Path to Mathlib 4 or path to Con(NF)
+    --eval_set ... \    # {proofnet, connf}
+    --working_root /path/to/output/results \
+    --dataset_root ./data/ \
+    --repl_root /path/to/repl \
+    --try_num 8 \
+    --num_concurrency 8 \
+    --temperature 0.0;
+```
+### RAutofromalizer (w/ Dependency Retrieval)
+- [🤗`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)
+- [🤗`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)
+```shell
+python -m autoformalizer.autoformalize_vllm_w_ra_passk \
+    --port ... \    # Can be arbitrarily set (should avoid conflict)
+    --trust-remote-code \
+    --enable-prefix-caching \
+    --model /path/to/model \
+    --retrieval_result_path /path/to/retrieval/result \
+    --mathlib_root ... \ # Path to Mathlib 4 or path to Con(NF)
+    --eval_set ... \    # {proofnet, connf}
+    --working_root /path/to/output/results \
+    --dataset_root ./data/ \
+    --repl_root /path/to/repl \
+    --try_num 8 \
+    --num_concurrency 8 \
+    --temperature 0.0;
+```
+### Oracle RAutoformalizer (w/ Ground-truth Dependencies)
+- [🤗`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)
+- [🤗`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)
+```shell
+python -m autoformalizer.autoformalize_vllm_w_gt_passk \
+    --port ... \    # Can be arbitrarily set (should avoid conflict)
+    --trust-remote-code \
+    --enable-prefix-caching \
+    --model /path/to/model \
+    --mathlib_root ... \ # Path to Mathlib 4 or path to Con(NF)
+    --eval_set ... \    # {proofnet, connf}
+    --working_root /path/to/output/results \
+    --dataset_root ./data/ \
+    --repl_root /path/to/repl \
+    --try_num 8 \
+    --num_concurrency 8 \
+    --temperature 0.0;
+```
+
+## 📚 Citation
+If you find our work useful in your research, please cite
+```bibtex
+@inproceedings{
+liu2025rethinking,
+title={Rethinking and improving autoformalization: towards a faithful metric and a Dependency Retrieval-based approach},
+author={Qi Liu and Xinhao Zheng and Xudong Lu and Qinxiang Cao and Junchi Yan},
+booktitle={The Thirteenth International Conference on Learning Representations},
+year={2025},
+url={https://openreview.net/forum?id=hUb2At2DsQ}
+}
+```
+
+# License
+This project is released under the Apache 2.0 license. Please see the [LICENSE](https://github.com/Purewhite2019/rethinking_autoformalization/blob/main/LICENSE) file for more information.
+
+# Contact
+Feel free to discuss the paper/data/code with us through issues/emails!
+- Qi Liu: purewhite@sjtu.edu.cn