CriticLean: Critic-Guided Reinforcement Learning for Mathematical
  Formalization
Authors: name: Zhongyuan Peng; name: Yifan Yao; name: Kaijing Ma; name: Shuyue Guo; name: Yizhe Li; name: Yichi Zhang; name: Chenchen Zhang; name: Yifan Zhang; name: Zhouliang Yu; name: Luming Li; name: Minghao Liu; name: Yihang Xia; name: Jiawei Shen; name: Yuchen Wu; name: Yixin Cao; name: Zhaoxiang Zhang; name: Wenhao Huang; name: Jiaheng Liu; name: Ge Zhang
Published: 2025-07-08 17:03:39

Abstract: Translating natural language mathematical statements into formal, executable
code is a fundamental challenge in automated theorem proving. While prior work
has focused on generation and compilation success, little attention has been
paid to the critic phase-the evaluation of whether generated formalizations
truly capture the semantic intent of the original problem. In this paper, we
introduce CriticLean, a novel critic-guided reinforcement learning framework
that elevates the role of the critic from a passive validator to an active
learning component. Specifically, first, we propose the CriticLeanGPT, trained
via supervised fine-tuning and reinforcement learning, to rigorously assess the
semantic fidelity of Lean 4 formalizations. Then, we introduce CriticLeanBench,
a benchmark designed to measure models' ability to distinguish semantically
correct from incorrect formalizations, and demonstrate that our trained
CriticLeanGPT models can significantly outperform strong open- and
closed-source baselines. Building on the CriticLean framework, we construct
FineLeanCorpus, a dataset comprising over 285K problems that exhibits rich
domain diversity, broad difficulty coverage, and high correctness based on
human evaluation. Overall, our findings highlight that optimizing the critic
phase is essential for producing reliable formalizations, and we hope our
CriticLean will provide valuable insights for future advances in formal
mathematical reasoning.