bm25_f

<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 and 📃Paper for more details.

📈 Performance

⚙️ Usage

• 🤗purewhite42/bm25_f: BM25 dependency retriever whose inputs are formatted using only formal declarations, based on Rank-BM25
• 🤗purewhite42/bm25_f_if: BM25 dependency retriever whose inputs are formatted using both formal declarations and informal descriptions, based on Rank-BM25

python -m retriever.retrieve_bm25 \
    --model_path /path/to/the/model \
    --save_path /path/to/output/results \
    --eval_set ... # {proofnet, connf}

📚 Citation

If you find our work useful in your research, please cite

@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 file for more information.

Contact

Feel free to discuss the paper/data/code with us through issues/emails!

• Qi Liu: [email protected]