Views
No views yet
| Benchmark | ProofNet | Con-NF | |
|---|---|---|---|
| InternLM2-Math-Base 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% |
purewhite42/rautoformalizer_nora_deepseek: w/o dependency retrieval, SFTed from 🤗deepseek-ai/deepseek-math-7b-basepurewhite42/rautoformalizer_nora_internlm: w/o dependency retrieval, SFTed from 🤗internlm/internlm2-math-base-7b1python -m autoformalizer.autoformalize_vllm_passk \
2 --port ... \ # Can be arbitrarily set (should avoid conflict)
3 --trust-remote-code \
4 --enable-prefix-caching \
5 --model /path/to/model \
6 --mathlib_root ... \ # Path to Mathlib 4 or path to Con(NF)
7 --eval_set ... \ # {proofnet, connf}
8 --working_root /path/to/output/results \
9 --dataset_root ./data/ \
10 --repl_root /path/to/repl \
11 --try_num 8 \
12 --num_concurrency 8 \
13 --temperature 0.0;purewhite42/rautoformalizer_ra_deepseek: w/ dependency retrieval (dependency_retriever_f), SFTed from 🤗deepseek-ai/deepseek-math-7b-basepurewhite42/rautoformalizer_ra_internlm: w/ dependency retrieval (dependency_retriever_f), SFTed from 🤗internlm/internlm2-math-base-7b1python -m autoformalizer.autoformalize_vllm_w_ra_passk \
2 --port ... \ # Can be arbitrarily set (should avoid conflict)
3 --trust-remote-code \
4 --enable-prefix-caching \
5 --model /path/to/model \
6 --retrieval_result_path /path/to/retrieval/result \
7 --mathlib_root ... \ # Path to Mathlib 4 or path to Con(NF)
8 --eval_set ... \ # {proofnet, connf}
9 --working_root /path/to/output/results \
10 --dataset_root ./data/ \
11 --repl_root /path/to/repl \
12 --try_num 8 \
13 --num_concurrency 8 \
14 --temperature 0.0;purewhite42/rautoformalizer_gtra_deepseek: w/ oracle dependency retrieval, SFTed from 🤗deepseek-ai/deepseek-math-7b-basepurewhite42/rautoformalizer_gtra_internlm: w/ oracle dependency retrieval, SFTed from 🤗internlm/internlm2-math-base-7b1python -m autoformalizer.autoformalize_vllm_w_gt_passk \
2 --port ... \ # Can be arbitrarily set (should avoid conflict)
3 --trust-remote-code \
4 --enable-prefix-caching \
5 --model /path/to/model \
6 --mathlib_root ... \ # Path to Mathlib 4 or path to Con(NF)
7 --eval_set ... \ # {proofnet, connf}
8 --working_root /path/to/output/results \
9 --dataset_root ./data/ \
10 --repl_root /path/to/repl \
11 --try_num 8 \
12 --num_concurrency 8 \
13 --temperature 0.0;1@inproceedings{
2liu2025rethinking,
3title={Rethinking and improving autoformalization: towards a faithful metric and a Dependency Retrieval-based approach},
4author={Qi Liu and Xinhao Zheng and Xudong Lu and Qinxiang Cao and Junchi Yan},
5booktitle={The Thirteenth International Conference on Learning Representations},
6year={2025},
7url={https://openreview.net/forum?id=hUb2At2DsQ}
8}