---
license: apache-2.0
language:
- en
base_model:
- BAAI/bge-m3
pipeline_tag: sentence-similarity
library_name: transformers
tags:
- lean4
- dependency-retrieval
- 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
| **Bench**     | **Fmt** | **Method** | **Recall@5** | **Precision@5** |
|---------------|---------|------------|--------------|-----------------|
| **ProofNet** | F    | BM25       | 0.16%        | 0.11%           |
|               | F    | DR         | 35.52%       | 22.89%          |
|               | F+IF  | BM25       | 0.00%        | 0.00%           |
|               | F+IF  | DR         | 32.47%       | 20.32%          |
|   **Con-NF**  | F    | BM25       | 4.41%        | 2.37%           |
|               | F    | DR         | 24.32%       | 14.05%          |
|               | F+IF  | BM25       | 9.86%        | 6.95%           |
|               | F+IF  | DR         | 27.91%       | 17.57%          |

## ⚙️ Usage
- [🤗`purewhite42/dependency_retriever_f`](https://huggingface.co/purewhite42/dependency_retriever_f): Dense dependency retriever whose inputs are formatted using only formal declarations, SFTed from [🤗`BAAI/bge-m3`](https://huggingface.co/BAAI/bge-m3)
- [🤗`purewhite42/dependency_retriever_f_if`](https://huggingface.co/purewhite42/dependency_retriever_f_if): Dense dependency retriever whose inputs are formatted using both formal declarations and informal descriptions, SFTed from [🤗`BAAI/bge-m3`](https://huggingface.co/BAAI/bge-m3)
## 📚 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