metadata

license: apache-2.0
language:
  - en
base_model:
  - BAAI/bge-m3
pipeline_tag: sentence-similarity
library_name: transformers
tags:
  - lean4
  - dependency-retrieval
  - formal-mathematics

[ICLR'25 Spotlight] Rethinking and Improving Autoformalization: Towards a Faithful Metric and a Dependency Retrieval-based Approach

Qi Liu, Xinhao Zheng, Xudong Lu, Qinxiang Cao, Junchi Yan* (* indicates Correspondence author)

Sch. of Computer Science & Sch. of Artificial Intelligence, Shanghai Jiao Tong University

Please refer to the 📺GitHub repo and 📃Paper 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/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]