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

License: Apache 2.0 Lean 4 GitHub

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

πŸ“š 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!

Downloads last month
5
Safetensors
Model size
568M params
Tensor type
F32
Β·
Inference Providers NEW
This model is not currently available via any of the supported Inference Providers.
The model cannot be deployed to the HF Inference API: The HF Inference API does not support sentence-similarity models for transformers library.

Model tree for purewhite42/dependency_retriever_f_if

Base model

BAAI/bge-m3
Finetuned
(214)
this model

Collection including purewhite42/dependency_retriever_f_if