Elamur Research⌕
☰
home / papers / 2025 / StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion

StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion

Paper · 2025 · Yutong Wu, Di Huang, Ruosi Wan et al.

Summary

Autoformalization means converting natural-language math problems into formal statements, here in Lean 4. Current LLM approaches are still inaccurate. General-purpose models often misuse Lean details, such as calling functions that do not exist. Specialized translators trained on narrow annotated data tend to misread the problem or misalign it with the formal statement. The authors argue that a good autoformalizer needs both formal-language knowledge and informal-to-formal reasoning, and they propose ThinkingF, a pipeline designed to build both.

ThinkingF uses two synthetic datasets:

  • Knowledge data: Kimina-Autoformalizer translates NuminaMath-1.5 problems, and the outputs are filtered by majority voting and an LLM judge.
  • Reasoning data: Claude 3.7 Sonnet writes reasoning traces for existing human-annotated pairs, following an expert template built on problem decomposition and mapping of mathematical objects.

A DeepSeek-R1-Distill-Qwen base model is fine-tuned on both datasets. It is then trained with RLVR, using BEq equivalence checking as the reward. The resulting StepFun-Formalizer-7B and StepFun-Formalizer-32B models set new SOTA results on FormalMATH-Lite and ProverBench. This yields more reliable statements for theorem-prover data and verification.

Key points

  • StepFun-Formalizer-32B reaches BEq@1 of 40.5% on FormalMATH-Lite and 26.7% on ProverBench. This beats both general-purpose and specialized models, and the system was also tested on CombiBench.
  • In the 7B ablation, removing the reasoning data lowers ProverBench BEq@16 from 37.9 to 25.3. Removing the knowledge data gives only a small drop, to 37.4.
  • Replacing template-guided traces with traces distilled directly from Claude4-thinking reduces ProverBench BEq@1 from 25.1 to 21.8. The authors note that the general model tends to solve the problem rather than formalize it.
  • Over 450 RL steps, the 7B model's reward rises from 0.232 to 0.347, and its average BEq@1 rises from 0.258 to 0.303.
  • In an end-to-end test on 10K NuminaMath-1.5 problems, Kimina-Prover-7B proved 4940 statements from StepFun-Formalizer-7B versus 4549 from Kimina-Autoformalizer-7B. Code and models are released on GitHub and Hugging Face (stepfun-ai).

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

 Fields, topics and concepts

📚 Shelves 5The field of science this work belongs to (OpenAlex fields).Computer Science · 16,667 worksArtificial Intelligence · 16,194 worksArts and Humanities · 16,039 worksLanguage and Linguistics · 15,891 worksComputational Theory and Mathematics · 252 works

🧭 Topics 2Research subjects and languages the work is about.Language models & pretraining · 3,320 worksReasoning · 1,426 works

Cite

Cite as Yutong Wu, Di Huang, Ruosi Wan, Yue Peng, Shijie Shang, Chenrui Cao, Lei Qi, Rui Zhang, Zidong Du, Jie Yan and Xing Hu. 2025. StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion. arXiv:2508.04440.

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

@misc{wu2025stepfun,
  title = {{StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion}},
  author = {Yutong Wu, Di Huang, Ruosi Wan, Yue Peng, Shijie Shang, Chenrui Cao, Lei Qi, Rui Zhang, Zidong Du, Jie Yan and Xing Hu},
  year = {2025},
  doi = {10.48550/arxiv.2508.04440},
  eprint = {2508.04440},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2508.04440}
}

References

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

  1. Anthropic. 2025. Claude 4. Accessed: 2025-07-24. find
  2. Azerbayev, Z.; Piotrowski, B.; Schoelkopf, H.; Ayers, E. W.; Radev, D.; and Avigad, J. 2023. ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics. arXiv:2302.12433. Barras, B.; Boutin, S.; Cornes, C.; Courant, J.; Coscoy, Y.; Delahaye, D.; de Rauglaudre, D.; Filliâtre, J.-…
  3. Beg, A.; O’Donoghue, D.; and Monahan, R. 2025. A Short Survey on Formalising Software Requirements using Large Language Models. arXiv:2506.11874. — [arXiv:2506.11874](https://arxiv.org/abs/2506.11874) find
  4. Brown, T. B.; Mann, B.; Ryder, N.; Subbiah, M.; Kaplan, J.; Dhariwal, P.; Neelakantan, A.; Shyam, P.; Sastry, G.; Askell, A.; Agarwal, S.; Herbert-Voss, A.; Krueger, G.; Henighan, T.; Child, R.; Ramesh, A.; Ziegler, D. M.; Wu, J.; Winter, C.; Hesse, C.; Chen, M.; Sigler, E.; Litwin, M.; Gray, S.; Ch… — Language Models are Few-Shot Learners
  5. Chen, J.; Tang, H.; Chu, Z.; Chen, Q.; Wang, Z.; Liu, M.; and Qin, B. 2024. Divide-and-Conquer Meets Consensus: Unleashing the Power of Functions in Code Generation. arXiv:2405.20092. — [arXiv:2405.20092](https://arxiv.org/abs/2405.20092) find
  6. Chen, Y.; Liu, Y.; Zhou, J.; Hao, Y.; Wang, J.; Zhang, Y.; and Fan, C. 2025. R1-Code-Interpreter: Training LLMs to Reason with Code via Supervised and Reinforcement Learning. arXiv:2505.21668. — [arXiv:2505.21668](https://arxiv.org/abs/2505.21668) find
  7. Community, L. 2023. Lean Documentation - lean3changes. https://lean-lang.org/lean4/doc/lean3changes.html. Accessed: 2025-07-23. ↗
  8. DeepSeek-AI. 2025. DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning. arXiv:2501.12948.
  9. Gao, G.; Wang, Y.; Jiang, J.; Gao, Q.; Qin, Z.; Xu, T.; and Dong, B. 2025. Herald: A Natural Language Annotated Lean 4 Dataset. arXiv:2410.10878. find
  10. Google. 2025. Gemini 2.5: Pushing the Frontier with Advanced Reasoning, Multimodality, Long Context, and Next Generation Agentic Capabilities. arXiv:2507.06261.
  11. Ji, X.; Liu, Y.; Wang, Q.; Zhang, J.; Yue, Y.; Shi, R.; Sun, C.; Zhang, F.; Zhou, G.; and Gai, K. 2025. Leanabell-Prover-V2: Verifier-integrated Reasoning for Formal Theorem Proving via Reinforcement Learning. arXiv:2507.08649. — [arXiv:2507.08649](https://arxiv.org/abs/2507.08649) find
  12. Jiang, A. Q.; Li, W.; and Jamnik, M. 2023. Multilingual Mathematical Autoformalization. arXiv:2311.03755. find
  13. Kimi; Du, A.; Gao, B.; Xing, B.; Jiang, C.; Chen, C.; Li, C.; Xiao, C.; Du, C.; Liao, C.; et al. 2025. Kimi k1. 5: Scaling reinforcement learning with llms. arXiv preprint arXiv:2501.12599. — Kimi k1.5: Scaling Reinforcement Learning with LLMs
  14. LI, J.; Beeching, E.; Tunstall, L.; Lipkin, B.; Soletskyi, R.; Huang, S. C.; Rasul, K.; Yu, L.; Jiang, A.; Shen, Z.; Qin, Z.; Dong, B.; Zhou, L.; Fleureau, Y.; Lample, G.; and Polu, S. 2024. NuminaMath. Li, Y.; Choi, D.; Chung, J.; Kushman, N.; Schrittwieser, J.; Leblond, R.; Eccles, T.; Keeling, J.…
  15. Li, Z.; Sun, J.; Murphy, L.; Su, Q.; Li, Z.; Zhang, X.; Yang, K.; and Si, X. 2024. A Survey on Deep Learning for Theorem Proving. arXiv:2404.09939. find
  16. Lin, X.; Cao, Q.; Huang, Y.; Wang, H.; Lu, J.; Liu, Z.; Song, L.; and Liang, X. 2024. FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving. arXiv:2406.14408. — [arXiv:2406.14408](https://arxiv.org/abs/2406.14408) find
  17. Lin, Y.; Tang, S.; Lyu, B.; Wu, J.; Lin, H.; Yang, K.; Li, J.; Xia, M.; Chen, D.; Arora, S.; and Jin, C. 2025a. Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving. arXiv:2502.07640. find
  18. Lin, Y.; Tang, S.; Lyu, B.; Yang, Z.; Chung, J.-H.; Zhao, H.; Jiang, L.; Geng, Y.; Ge, J.; Sun, J.; Wu, J.; Gesi, J.; Lu, X.; Acuna, D.; Yang, K.; Lin, H.; Choi, Y.; Chen, D.; Arora, S.; and Jin, C. 2025b. Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Corre… find
  19. Liu, J.; Lin, X.; Bayer, J.; Dillies, Y.; Jiang, W.; Liang, X.; Soletskyi, R.; Wang, H.; Xie, Y.; Xiong, B.; Yang, Z.; Zhang, J.; Zhi, L.; Li, J.; and Liu, Z. 2025a. CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics. arXiv:2505.03171. find
  20. Liu, J.; Xia, C. S.; Wang, Y.; and Zhang, L. 2023. Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generation. arXiv:2305.01210.
  21. Liu, Q.; Zheng, X.; Lu, X.; Cao, Q.; and Yan, J. 2025b. Rethinking and Improving Autoformalization: Towards a Faithful Metric and a Dependency Retrieval-based Approach. In The Thirteenth International Conference on Learning Representations. find
  22. Liu, Z.; Guo, X.; Lou, F.; Zeng, L.; Niu, J.; Wang, Z.; Xu, J.; Cai, W.; Yang, Z.; Zhao, X.; Li, C.; Xu, S.; Chen, D.; Chen, Y.; Bai, Z.; and Zhang, L. 2025c. Fin-R1: A Large Language Model for Financial Reasoning through Reinforcement Learning. arXiv:2503.16252. — [arXiv:2503.16252](https://arxiv.org/abs/2503.16252) find
  23. Miranda, B.; Zhou, Z.; Nie, A.; Obbad, E.; Aniva, L.; Frons-dal, K.; Kirk, W.; Soylu, D.; Yu, A.; Li, Y.; and Koyejo, S. 2025. VeriBench: End-to-End Formal Verification Benchmark for AI Code Generation in Lean 4. In 2nd AI for Math Workshop @ ICML 2025. Moura, L. d.; and Ullrich, S. 2021. The Lean 4… find
  24. Springer. OpenAI. 2024a. GPT-4o System Card. arXiv:2410.21276.
  25. OpenAI. 2024b. OpenAI o1 System Card. arXiv:2412.16720.
  26. OpenAI. 2025. Introducing O3 and O4 Mini. Accessed: 2025-07-24. find
  27. Isabelle: A Generic Theorem Prover. Springer. Qwen. 2025. Qwen3 Technical Report. arXiv:2505.09388.
  28. Ren, Z. Z.; Shao, Z.; Song, J.; Xin, H.; Wang, H.; Zhao, W.; Zhang, L.; Fu, Z.; Zhu, Q.; Yang, D.; Wu, Z. F.; Gou, Z.; Ma, S.; Tang, H.; Liu, Y.; Gao, W.; Guo, D.; and Ruan, C. 2025. DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition. arX…
  29. Renshaw, D. 2024. Compfiles: Catalog Of Math Problems Formalized In Lean. https://github.com/dwrensha/compfiles. GitHub repository. Santos, M. D.; Wang, H.; de Saxcé, H.; Wang, R.; Baksys, M.; Unsal, M.; Liu, J.; Liu, Z.; and Li, J. 2025. Kimina Lean Server: Technical Report. arXiv:2504.21230. ↗
  30. Shao, Z.; Wang, P.; Zhu, Q.; Xu, R.; Song, J.; Bi, X.; Zhang, H.; Zhang, M.; Li, Y. K.; Wu, Y.; and Guo, D. 2024. DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models. arXiv:2402.03300.
  31. SJTULean. 2024. LeanFormalizer PPO. https://huggingface.co/SJTULean/LeanFormalizer PPO. Accessed: 2025-07-30. ↗
  32. Thakur, A.; Lee, J.; Tsoukalas, G.; Sistla, M.; Zhao, M.; Zetzsche, S.; Durrett, G.; Yue, Y.; and Chaudhuri, S. 2025. CLEVER: A Curated Benchmark for Formally Verified Code Generation. arXiv:2505.13938. — [arXiv:2505.13938](https://arxiv.org/abs/2505.13938) find
  33. Tsoukalas, G.; Lee, J.; Jennings, J.; Xin, J.; Ding, M.; Jennings, M.; Thakur, A.; and Chaudhuri, S. 2024. Putnam-Bench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition. arXiv:2407.11214. Wang, H.; Unsal, M.; Lin, X.; Baksys, M.; Liu, J.; Santos, M. D.; Sung, F.; Vinyes, M.;… find
  34. Wang, X.; Wei, J.; Schuurmans, D.; Le, Q.; Chi, E.; Narang, S.; Chowdhery, A.; and Zhou, D. 2023. Self-Consistency Improves Chain of Thought Reasoning in Language Models. arXiv:2203.11171.
  35. Weng, K.; Du, L.; Li, S.; Lu, W.; Sun, H.; Liu, H.; and Zhang, T. 2025. Autoformalization in the Era of Large Language Models: A Survey. arXiv:2505.23486.
  36. Wu, Y.; Huang, D.; Shi, W.; Wang, W.; Pu, Y.; Gao, L.; Liu, S.; Nan, Z.; Yuan, K.; Zhang, R.; Zhang, X.; Du, Z.; Guo, Q.; Yin, D.; Hu, X.; and Chen, Y. 2025. InverseCoder: self-improving instruction-tuned code LLMs with inverse-instruct. In Proceedings of the Thirty-Ninth AAAI Conference on Artifici… find
  37. Wu, Y.; Jiang, A. Q.; Li, W.; Rabe, M. N.; Staats, C.; Jamnik, M.; and Szegedy, C. 2022. Autoformalization with Large Language Models. arXiv:2205.12615.
  38. Xie, J.; Liu, C.; Yuan, Y.; Li, S.; Xiao, Z.; and Zhang, M. 2025. FMC: Formalization of Natural Language Mathematical Competition Problems. arXiv:2507.11275. — [arXiv:2507.11275](https://arxiv.org/abs/2507.11275) find
  39. Xin, H.; Guo, D.; Shao, Z.; Ren, Z.; Zhu, Q.; Liu, B.; Ruan, C.; Li, W.; and Liang, X. 2024a. DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data.
  40. Xin, H.; Ren, Z. Z.; Song, J.; Shao, Z.; Zhao, W.; Wang, H.; Liu, B.; Zhang, L.; Lu, X.; Du, Q.; Gao, W.; Zhu, Q.; Yang, D.; Gou, Z.; Wu, Z. F.; Luo, F.; and Ruan, C. 2024b. DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search.
  41. Xuejun, Y.; Zhong, J.; Feng, Z.; Zhai, P.; Yousefzadeh, R.; Ng, W. C.; Liu, H.; Shou, Z.; Xiong, J.; Zhou, Y.; Ong, C. B.; Sug-iarto, A. J.; Zhang, Y.; Tai, W. M.; Cao, H.; Lu, D.; Sun, J.; Xu, Q.; Xin, S.; and Li, Z. 2025. Mathesis: Towards Formal Theorem Proving from Natural Languages. arXiv:2506.… find
  42. Yang, Z.; Chen, L.; Cohan, A.; and Zhao, Y. 2025. Table-R1: Inference-Time Scaling for Table Reasoning. arXiv:2505.23621. — [arXiv:2505.23621](https://arxiv.org/abs/2505.23621) find
  43. Ying, H.; Wu, Z.; Geng, Y.; Yuan, Z.; Lin, D.; and Chen, K. 2025. Lean Workbook: A large-scale Lean problem set formalized from natural language math problems. arXiv:2406.03847. find
  44. Ying, H.; Zhang, S.; Li, L.; Zhou, Z.; Shao, Y.; Fei, Z.; Ma, Y.; Hong, J.; Liu, K.; Wang, Z.; Wang, Y.; Wu, Z.; Li, S.; Zhou, F.; Liu, H.; Zhang, S.; Zhang, W.; Yan, H.; Qiu, X.; Wang, J.; Chen, K.; and Lin, D. 2024. InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoning. arXiv:… find
  45. Yu, Q.; Zhang, Z.; Zhu, R.; Yuan, Y.; Zuo, X.; Yue, Y.; Dai, W.; Fan, T.; Liu, G.; Liu, L.; Liu, X.; Lin, H.; Lin, Z.; Ma, B.; Sheng, G.; Tong, Y.; Zhang, C.; Zhang, M.; Zhang, W.; Zhu, H.; Zhu, J.; Chen, J.; Chen, J.; Wang, C.; Yu, H.; Song, Y.; Wei, X.; Zhou, H.; Liu, J.; Ma, W.-Y.; Zhang, Y.-Q.;… — DAPO: An Open-Source LLM Reinforcement Learning System at Scale
  46. Yu, Z.; Peng, R.; Ding, K.; Li, Y.; Peng, Z.; Liu, M.; Zhang, Y.; Yuan, Z.; Xin, H.; Huang, W.; Wen, Y.; Zhang, G.; and Liu, W. 2025b. FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models. arXiv:2505.02735. find
  47. Zhang, J.; Wang, Q.; Ji, X.; Liu, Y.; Yue, Y.; Zhang, F.; Zhang, D.; Zhou, G.; and Gai, K. 2025. Leanabell-Prover: Posttraining Scaling in Formal Reasoning. arXiv:2504.06122. find
  48. Zhang, L.; Valentino, M.; and Freitas, A. 2025. Formalizing Complex Mathematical Statements with LLMs: A Study on Mathematical Definitions. arXiv:2502.12065. find
  49. Zheng, K.; Han, J. M.; and Polu, S. 2022. MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics. arXiv:2109.00110.
  50. Zhou, J. P.; Staats, C.; Li, W.; Szegedy, C.; Weinberger, K. Q.; and Wu, Y. 2024. Don’t Trust: Verify – Grounding LLM Quantitative Reasoning with Autoformalization. arXiv:2403.18120. find
  51. Zhu, Y.; Huang, D.; Lyu, H.; Zhang, X.; Li, C.; Shi, W.; Wu, Y.; Mu, J.; Wang, J.; Zhao, Y.; et al. 2025. CodeV-R1: Reasoning-Enhanced Verilog Generation. arXiv preprint arXiv:2505.24183. — [arXiv:2505.24183](https://arxiv.org/abs/2505.24183) find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/wu-2025-stepfun-formalizer-unlocking-autoformalization/