|
--- |
|
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: [email protected] |
|
|
