Abstract

Translating natural language mathematical statements into formal, executablecode is a fundamental challenge in automated theorem proving. While prior workhas focused on generation and compilation success, little attention has beenpaid to the critic phase-the evaluation of whether generated formalizationstruly capture the semantic intent of the original problem. In this paper, weintroduce CriticLean, a novel critic-guided reinforcement learning frameworkthat elevates the role of the critic from a passive validator to an activelearning component. Specifically, first, we propose the CriticLeanGPT, trainedvia supervised fine-tuning and reinforcement learning, to rigorously assess thesemantic fidelity of Lean 4 formalizations. Then, we introduce CriticLeanBench,a benchmark designed to measure models' ability to distinguish semanticallycorrect from incorrect formalizations, and demonstrate that our trainedCriticLeanGPT models can significantly outperform strong open- andclosed-source baselines. Building on the CriticLean framework, we constructFineLeanCorpus, a dataset comprising over 285K problems that exhibits richdomain diversity, broad difficulty coverage, and high correctness based onhuman evaluation. Overall, our findings highlight that optimizing the criticphase is essential for producing reliable formalizations, and we hope ourCriticLean will provide valuable insights for future advances in formalmathematical reasoning.