CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization
Zhongyuan Peng, Yifan Yao, Kaijing Ma, Shuyue Guo, Yizhe Li, Yichi Zhang, Chenchen Zhang, Yifan Zhang, Zhouliang Yu, Luming Li, Minghao Liu, Yihang Xia, Jiawei Shen, Yuchen Wu, Yixin Cao, Zhaoxiang Zhang, Wenhao Huang, Jiaheng Liu, Ge Zhang
2025-07-09
Summary
This paper talks about CriticLean, a new approach that improves how AI systems translate regular math statements into formal code used in automated theorem proving by training a special critic model to better judge if the code correctly matches the math idea.
What's the problem?
The problem is that current AI attempts to turn math problems into formal code often fail because the evaluation step, which checks if the formalization makes sense, is too simple and doesn't catch errors well, leading to incorrect proofs.
What's the solution?
The researchers created CriticLean, which trains a critic model using reinforcement learning to actively evaluate and learn from its mistakes in judging the correctness of the formalized math code. This feedback helps the AI gradually improve its formalizations to better capture the true meaning of the original math problems.
Why it matters?
This matters because better evaluation during formalization enables AI to produce more accurate mathematical proofs, helping automate difficult reasoning tasks and advancing fields like math, computer science, and formal verification.
Abstract
CriticLean, a critic-guided reinforcement learning framework, enhances the evaluation of formalizations in automated theorem proving by actively learning and distinguishing semantically correct formalizations.