Elamur Research⌕
☰
home / papers / 2025 / Autoformalizer with Tool Feedback

Autoformalizer with Tool Feedback

Paper · 2025 · Qi Guo; Jianing Wang; Jianfei Zhang; Deyang Kong; Xiangzhou Huang; Xiangyu Xi; Wei Wang; Jingang Wang; Xunliang Cai; Shikun Zhang; and Wei Ye

Summary

Automated theorem provers need large amounts of formally stated problems, but such data is scarce. Autoformalization addresses this by translating natural-language math into Lean statements. However, current formalizer models often produce code that does not compile or that subtly changes the problem's meaning. The authors propose ATF (Autoformalizer with Tool Feedback), a model that calls two external tools while it generates. One tool is a Lean 4 compiler wrapper that returns error messages. The other is a consistency checker that uses several LLMs as judges to flag mismatches between the informal problem and the formal statement. The model revises its output until both checks pass.

Training has three stages:

  • a cold start on synthetic tool-calling traces,
  • expert iteration to strengthen formalization and revision skills,
  • DPO to discourage revisions that do not help.

On three standard benchmarks, ATF clearly beats strong baseline formalizers, and human evaluation confirms the gains. It also improves as more inference compute is allowed. The work matters because it supplies more reliable formal data for training provers, and the team releases a large synthetic dataset.

Key points

  • The two tools are syntax_check, which returns Lean 4 compiler feedback using a pre-check and grouped execution, and consistency_check, which returns a multi-LLM judgment with brief explanations. The multi-judge setup was benchmarked on detecting subtle informal–formal mismatches.
  • The training pipeline is cold start, then expert iteration, then Direct Preference Optimization. The target is Lean 4 v4.15 with Mathlib.
  • For context, Kimina-Autoformalizer fails syntax checks on roughly 40% of outputs. The prior leading model, Goedel-Formalizer-v2, reaches only 62.31% syntax pass@1 on CombiBench.
  • ATF improves semantic consistency on CombiBench by 29.13% compared with Goedel-V2-Formalizer-32B.
  • The released resource, Numina-ATF, contains 750K formal statements generated by ATF-32B from Numina-v1.5 problems.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓Peking UniversityBeijing · China335 works · 43,758 citations🏢MeituanBeijing · China28 works · 3,965 citations

 Fields, topics and concepts

📚 Shelves 5The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksArts and Humanities · 17,959 worksLanguage and Linguistics · 17,789 worksComputational Theory and Mathematics · 496 works

Cite

Cite as Qi Guo; Jianing Wang; Jianfei Zhang; Deyang Kong; Xiangzhou Huang; Xiangyu Xi; Wei Wang; Jingang Wang; Xunliang Cai; Shikun Zhang; and Wei Ye. 2025. Autoformalizer with Tool Feedback. arXiv:2510.06857.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.2510.06857 · arXiv 2510.06857

@misc{zhang2025autoformalizer,
  title = {{Autoformalizer with Tool Feedback}},
  author = {Qi Guo; Jianing Wang; Jianfei Zhang; Deyang Kong; Xiangzhou Huang; Xiangyu Xi; Wei Wang; Jingang Wang; Xunliang Cai; Shikun Zhang; and Wei Ye},
  year = {2025},
  doi = {10.48550/arxiv.2510.06857},
  eprint = {2510.06857},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2510.06857}
}

References

31 references, 21 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate-level mathematics. arXiv preprint arXiv:2302.12433, 2023a.
  2. Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate-level mathematics. arXiv preprint arXiv:2302.12433, 2023b.
  3. Leonardo De Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In International Conference on Automated Deduction, pp. 378–388. Springer, 2015. find
  4. Abhimanyu Dubey, Abhinav Jauhri, Abhinav Pandey, Abhishek Kadian, Ahmad Al-Dahle, Aiesha Letman, Akhil Mathur, Alan Schelten, Amy Yang, Angela Fan, et al. The llama 3 herd of models. arXiv e-prints, pp. arXiv–2407, 2024.
  5. Yunfan Gao, Yun Xiong, Xinyu Gao, Kangxiang Jia, Jinliu Pan, Yuxi Bi, Yixin Dai, Jiawei Sun, Haofen Wang, and Haofen Wang. Retrieval-augmented generation for large language models: A survey. arXiv preprint arXiv:2312.10997, 2, 2023.
  6. Daya Guo, Dejian Yang, Haowei Zhang, Junxiao Song, Ruoyu Zhang, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang, Xiao Bi, et al. Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning. arXiv preprint arXiv:2501.12948, 2025.
  7. Yanxing Huang, Xinling Jin, Sijie Liang, Peng Li, and Yang Liu. Formarl: Enhancing autoformalization with no labeled data. arXiv preprint arXiv:2508.18914, 2025. find
  8. Xingguang Ji, Yahui Liu, Qi Wang, Jingyuan Zhang, Yang Yue, Rui Shi, Chenxi Sun, Fuzheng Zhang, Guorui Zhou, and Kun Gai. Leanabell-prover-v2: Verifier-integrated reasoning for formal theorem proving via reinforcement learning. arXiv preprint arXiv:2507.08649, 2025. — [arXiv:2507.08649](https://arxiv.org/abs/2507.08649) find
  9. Jia LI, Edward Beeching, Lewis Tunstall, Ben Lipkin, Roman Soletskyi, Shengyi Costa Huang, Kashif Rasul, Longhui Yu, Albert Jiang, Ziju Shen, Zihan Qin, Bin Dong, Li Zhou, Yann Fleureau, Guillaume Lample, and Stanislas Polu. Numinamath. [https://huggingface. co/AI-MO/NuminaMath-1.5](https://github.c… find
  10. Yang Li, Dong Du, Linfeng Song, Chen Li, Weikang Wang, Tao Yang, and Haitao Mi. Hunyuanprover: A scalable data synthesis framework and guided tree search for automated theorem proving. arXiv preprint arXiv:2412.20735, 2024a.
  11. Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, and Xujie Si. A survey on deep learning for theorem proving. arXiv preprint arXiv:2404.09939, 2024b.
  12. Heng Lin and Zhongwen Xu. arXiv:2508.19201, 2025. — [arXiv:2508.19201](https://arxiv.org/abs/2508.19201) find
  13. Understanding tool-integrated reasoning. arXiv preprint Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, et al. Goedel-prover-v2: Scaling formal theorem proving with scaffolded data synthesis and self-correction. arXiv preprint a…
  14. Junqi Liu, Xiaohan Lin, Jonas Bayer, Yael Dillies, Weijie Jiang, Xiaodan Liang, Roman Soletskyi, Haiming Wang, Yunzhou Xie, Beibei Xiong, et al. Combibench: Benchmarking llm capability for combinatorial mathematics. arXiv preprint arXiv:2505.03171, 2025a.
  15. Qi Liu, Xinhao Zheng, Xudong Lu, Qinxiang Cao, and Junchi Yan. Rethinking and improving autoformalization: towards a faithful metric and a dependency retrieval-based approach. In The Thirteenth International Conference on Learning Representations, 2025b. find
  16. Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In International Conference on Automated Deduction, pp. 625–635. Springer, 2021. — The Lean 4 Theorem Prover and Programming Language (System Description)
  17. Lawrence C Paulson. Isabelle: A generic theorem prover. Springer, 1994. find
  18. Rafael Rafailov, Archit Sharma, Eric Mitchell, Christopher D Manning, Stefano Ermon, and Chelsea Finn. Direct preference optimization: Your language model is secretly a reward model. Advances in neural information processing systems, 36:53728–53741, 2023.
  19. ZZ Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, et al. Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. arXiv preprint arXiv:2504.21801, 2025.
  20. Philip Sedgwick. Pearson’s correlation coefficient. Bmj, 345, 2012. find
  21. Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Xiao Bi, Haowei Zhang, Mingchuan Zhang, YK Li, Yang Wu, et al. Deepseekmath: Pushing the limits of mathematical reasoning in open language models. arXiv preprint arXiv:2402.03300, 2024.
  22. George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Amitayush Thakur, and Swarat Chaudhuri. Putnambench: Evaluating neural theorem-provers on the putnam mathematical competition. Advances in Neural Information Processing Systems, 37: 11545–11569, 2024.
  23. Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, et al. Kimina-prover preview: Towards large formal reasoning models with reinforcement learning. arXiv preprint arXiv:2504.11354, 2025.
  24. Yuanfu Wang, Chao Yang, Ying Wen, Yu Liu, and Yu Qiao. Critic-guided decision transformer for offline reinforcement learning. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 38, pp. 15706–15714, 2024. find
  25. Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. Advances in neural information processing systems, 35:32353–32368, 2022.
  26. Yutong Wu, Di Huang, Ruosi Wan, Yue Peng, Shijie Shang, Chenrui Cao, Lei Qi, Rui Zhang, Zidong Du, Jie Yan, et al. Stepfun-formalizer: Unlocking the autoformalization potential of llms through knowledge-reasoning fusion. arXiv preprint arXiv:2508.04440, 2025.
  27. An Yang, Anfeng Li, Baosong Yang, Beichen Zhang, Binyuan Hui, Bo Zheng, Bowen Yu, Chang Gao, Chengen Huang, Chenxu Lv, et al. Qwen3 technical report. arXiv preprint arXiv:2505.09388, 2025.
  28. Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, and Dawn Song. Formal mathematical reasoning: A new frontier in ai. arXiv preprint arXiv:2412.16075, 2024.
  29. Zhouliang Yu, Ruotian Peng, Keyi Ding, Yizhe Li, Zhongyuan Peng, Minghao Liu, Yifan Zhang, Zheng Yuan, Huajian Xin, Wenhao Huang, et al. Formalmath: Benchmarking formal mathematical reasoning of large language models. arXiv preprint arXiv:2505.02735, 2025.
  30. Shengnan Zhang, Yan Hu, and Guangrong Bian. Research on string similarity algorithm based on levenshtein distance. In 2017 IEEE 2nd Advanced Information Technology, Electronic and Automation Control Conference (IAEAC), pp. 2247–2251. find
  31. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. Minif2f: a cross-system benchmark for formal olympiad-level mathematics. arXiv preprint arXiv:2109.00110, 2021.

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/guo-2025-autoformalizer-tool-feedback/