Autoformalizer with Tool Feedback
Qi Guo, Jianing Wang, Jianfei Zhang, Deyang Kong, Xiangzhou Huang, Xiangyu Xi, Wei Wang, Jingang Wang, Xunliang Cai, Shikun Zhang, Wei Ye
cs.AI
Oct 8, 2025 · v1
TL;DR
Trains an autoformalizer using Lean 4 compiler syntax feedback and releases Numina-ATF, 750K synthetic Lean formal statements.
Abstract
Autoformalization addresses the scarcity of data for Automated Theorem Proving (ATP) by translating mathematical problems from natural language into formal statements. Efforts in recent work shift from directly prompting large language models to training an end-to-end formalizer model from scratch, achieving remarkable advancements. However, existing formalizer still struggles to consistently generate valid statements that meet syntactic validity and semantic consistency. To address this issue, we propose the Autoformalizer with Tool Feedback (ATF), a novel approach that incorporates syntactic and consistency information as tools into the formalization process. By integrating Lean 4 compilers for syntax corrections and employing a multi-LLMs-as-judge approach for consistency validation, the model is able to adaptively refine generated statements according to the tool feedback, enhancing both syntactic validity and semantic consistency. The training of ATF involves a cold-start phase on synthetic tool-calling data, an expert iteration phase to improve formalization capabilities, and Direct Preference Optimization to alleviate ineffective revisions. Experimental results show that ATF markedly outperforms a range of baseline formalizer models, with its superior performance further validated by human evaluations. Subsequent analysis reveals that ATF demonstrates excellent inference scaling properties. Moreover, we open-source Numina-ATF, a dataset containing 750K synthetic formal statements to facilitate advancements in autoformalization and ATP research.
Problem
Autoformalization (translating mathematical problems from natural language to formal statements) struggles to consistently generate syntactically valid and semantically consistent output, with about 40% of statements failing syntax validation in existing systems.
Approach
The Autoformalizer with Tool Feedback (ATF) incorporates Lean 4 compilers for syntax corrections and a multi-LLMs-as-judge approach for semantic consistency validation as tools within the formalization process. Training involves three phases: a cold-start phase on synthetic tool-calling data, an expert iteration phase to improve formalization capabilities, and Direct Preference Optimization to reduce ineffective revisions.
Results
ATF outperforms baseline formalizer models across benchmarks, with performance validated by human evaluations. The system demonstrates inference scaling properties where more revision attempts improve accuracy. The authors release Numina-ATF, a dataset of 750K synthetic formal statements.