@inproceedings{peng-etal-2026-criticlean,
    title = "{C}ritic{L}ean: Critic-Guided Reinforcement Learning for Mathematical Formalization",
    author = "Peng, Zhongyuan  and
      Yao, Yifan  and
      Ma, Kaijing  and
      Guo, Shuyue  and
      Li, Yizhe  and
      Zhang, Yichi  and
      Zhang, Chenchen  and
      Zhang, Yifan  and
      Yu, Zhouliang  and
      Li, Luming  and
      Liu, Minghao  and
      Xia, Yihang  and
      Shen, Jiawei  and
      Wu, Yuchen  and
      Cao, Yixin  and
      Zhang, Zhaoxiang  and
      Huang, Wenhao  and
      Liu, Jiaheng  and
      Zhang, Ge",
    editor = "Liakata, Maria  and
      Moreira, Viviane P.  and
      Zhang, Jiajun  and
      Jurgens, David",
    booktitle = "Proceedings of the 64th Annual Meeting of the {A}ssociation for {C}omputational {L}inguistics (Volume 1: Long Papers)",
    month = jul,
    year = "2026",
    address = "San Diego, California, United States",
    publisher = "Association for Computational Linguistics",
    url = "https://preview.aclanthology.org/ingest-acl/2026.acl-long.139/",
    pages = "3049--3088",
    ISBN = "979-8-89176-390-6",
    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 509K 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."
}