CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , , , , , , , , , , , , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866911045659918336 |
|---|---|
| author | Peng, Zhongyuan Yao, Yifan Ma, Kaijing Guo, Shuyue Li, Yizhe Zhang, Yichi Zhang, Chenchen Zhang, Yifan Yu, Zhouliang Li, Luming Liu, Minghao Xia, Yihang Shen, Jiawei Wu, Yuchen Cao, Yixin Zhang, Zhaoxiang Huang, Wenhao Liu, Jiaheng Zhang, Ge |
| author_facet | Peng, Zhongyuan Yao, Yifan Ma, Kaijing Guo, Shuyue Li, Yizhe Zhang, Yichi Zhang, Chenchen Zhang, Yifan Yu, Zhouliang Li, Luming Liu, Minghao Xia, Yihang Shen, Jiawei Wu, Yuchen Cao, Yixin Zhang, Zhaoxiang Huang, Wenhao Liu, Jiaheng Zhang, Ge |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2507_06181 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization Peng, Zhongyuan Yao, Yifan Ma, Kaijing Guo, Shuyue Li, Yizhe Zhang, Yichi Zhang, Chenchen Zhang, Yifan Yu, Zhouliang Li, Luming Liu, Minghao Xia, Yihang Shen, Jiawei Wu, Yuchen Cao, Yixin Zhang, Zhaoxiang Huang, Wenhao Liu, Jiaheng Zhang, Ge Computation and Language 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. |
| title | CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization |
| topic | Computation and Language |
| url | https://arxiv.org/abs/2507.06181 |