CriticLean: Critic-Gestuurde Reinforcement Learning voor Wiskundige Formalering

CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization

July 8, 2025

Auteurs: 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

cs.AI

Samenvatting

Het vertalen van wiskundige uitspraken in natuurlijke taal naar formele, uitvoerbare code is een fundamentele uitdaging in geautomatiseerd bewijzen. Hoewel eerder werk zich heeft gericht op het succes van generatie en compilatie, is er weinig aandacht besteed aan de criticusfase: de evaluatie of gegenereerde formalisaties daadwerkelijk de semantische intentie van het oorspronkelijke probleem weergeven. In dit artikel introduceren we CriticLean, een nieuw criticus-gestuurd reinforcement learning-framework dat de rol van de criticus verheft van een passieve validator naar een actief leercomponent. Specifiek stellen we eerst de CriticLeanGPT voor, getraind via supervised fine-tuning en reinforcement learning, om de semantische trouw van Lean 4-formalisaties rigoureus te beoordelen. Vervolgens introduceren we CriticLeanBench, een benchmark ontworpen om het vermogen van modellen te meten om semantisch correcte van incorrecte formalisaties te onderscheiden, en tonen we aan dat onze getrainde CriticLeanGPT-modellen aanzienlijk beter presteren dan sterke open- en closed-source baselines. Op basis van het CriticLean-framework construeren we FineLeanCorpus, een dataset met meer dan 285K problemen die een rijke domeindiversiteit, brede moeilijkheidsgraad en hoge correctheid vertoont op basis van menselijke evaluatie. Over het geheel genomen benadrukken onze bevindingen dat het optimaliseren van de criticusfase essentieel is voor het produceren van betrouwbare formalisaties, en we hopen dat onze CriticLean waardevolle inzichten zal bieden voor toekomstige vooruitgang in formeel wiskundig redeneren.

English

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.