File size: 6,275 Bytes
d37986b |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 |
---
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: [email protected]
|