README.md

metadata

license: apache-2.0
datasets:
  - hoskinson-center/proofnet
language:
  - en
base_model:
  - internlm/internlm2-math-7b
  - deepseek-ai/deepseek-math-7b-base
pipeline_tag: text-generation
library_name: transformers
tags:
  - lean4
  - statement-autoformalization
  - 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

	Benchmark	ProofNet	Con-NF
InternLM2-Math 7B	Rautoformalizer (-R)	16.58%	4.58%
	RAutoformalizer	18.18%	16.86%
	Rautoformalizer (+R)	31.28%	55.36%
DeepseekMath 7B	Rautoformalizer (-R)	15.24%	4.27%
	RAutoformalizer	17.91%	15.30%
	Rautoformalizer (+R)	32.62%	59.00%

⚙️ Usage

w/o Dependency Retrieval

• 🤗purewhite42/rautoformalizer_nora_deepseek: w/o dependency retrieval, SFTed from 🤗deepseek-ai/deepseek-math-7b-base
• 🤗purewhite42/rautoformalizer_nora_internlm: w/o dependency retrieval, SFTed from 🤗internlm/internlm2-math-7b

python -m autoformalizer.autoformalize_vllm_passk \
    --port ... \    # Can be arbitrarily set (should avoid conflict)
    --trust-remote-code \
    --enable-prefix-caching \
    --model /path/to/model \
    --mathlib_root ... \ # Path to Mathlib 4 or path to Con(NF)
    --eval_set ... \    # {proofnet, connf}
    --working_root /path/to/output/results \
    --dataset_root ./data/ \
    --repl_root /path/to/repl \
    --try_num 8 \
    --num_concurrency 8 \
    --temperature 0.0;

RAutofromalizer (w/ Dependency Retrieval)

• 🤗purewhite42/rautoformalizer_ra_deepseek: w/ dependency retrieval (dependency_retriever_f), SFTed from 🤗deepseek-ai/deepseek-math-7b-base
• 🤗purewhite42/rautoformalizer_ra_internlm: w/ dependency retrieval (dependency_retriever_f), SFTed from 🤗internlm/internlm2-math-7b

python -m autoformalizer.autoformalize_vllm_w_ra_passk \
    --port ... \    # Can be arbitrarily set (should avoid conflict)
    --trust-remote-code \
    --enable-prefix-caching \
    --model /path/to/model \
    --retrieval_result_path /path/to/retrieval/result \
    --mathlib_root ... \ # Path to Mathlib 4 or path to Con(NF)
    --eval_set ... \    # {proofnet, connf}
    --working_root /path/to/output/results \
    --dataset_root ./data/ \
    --repl_root /path/to/repl \
    --try_num 8 \
    --num_concurrency 8 \
    --temperature 0.0;

Oracle RAutoformalizer (w/ Ground-truth Dependencies)

• 🤗purewhite42/rautoformalizer_gtra_deepseek: w/ oracle dependency retrieval, SFTed from 🤗deepseek-ai/deepseek-math-7b-base
• 🤗purewhite42/rautoformalizer_gtra_internlm: w/ oracle dependency retrieval, SFTed from 🤗internlm/internlm2-math-7b

python -m autoformalizer.autoformalize_vllm_w_gt_passk \
    --port ... \    # Can be arbitrarily set (should avoid conflict)
    --trust-remote-code \
    --enable-prefix-caching \
    --model /path/to/model \
    --mathlib_root ... \ # Path to Mathlib 4 or path to Con(NF)
    --eval_set ... \    # {proofnet, connf}
    --working_root /path/to/output/results \
    --dataset_root ./data/ \
    --repl_root /path/to/repl \
    --try_num 8 \
    --num_concurrency 8 \
    --temperature 0.0;

📚 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: purewhite@sjtu.edu.cn