CriticLean : Apprentissage par Renforcement Guidé par Critique pour la Formalisation Mathématique

CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization

July 8, 2025

papers.authors: 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

papers.abstract

La traduction d'énoncés mathématiques en langage naturel en code formel et exécutable constitue un défi fondamental dans la démonstration automatique de théorèmes. Alors que les travaux antérieurs se sont concentrés sur la génération et la compilation, peu d'attention a été accordée à la phase de critique - l'évaluation de la capacité des formalisations générées à capturer fidèlement l'intention sémantique du problème original. Dans cet article, nous présentons CriticLean, un cadre novateur d'apprentissage par renforcement guidé par un critique, qui élève le rôle du critique d'un validateur passif à un composant actif d'apprentissage. Plus précisément, nous proposons d'abord CriticLeanGPT, entraîné via un ajustement supervisé et un apprentissage par renforcement, pour évaluer rigoureusement la fidélité sémantique des formalisations en Lean 4. Ensuite, nous introduisons CriticLeanBench, un benchmark conçu pour mesurer la capacité des modèles à distinguer les formalisations sémantiquement correctes des incorrectes, et démontrons que nos modèles CriticLeanGPT entraînés surpassent significativement des bases de référence solides, tant ouvertes que propriétaires. En nous appuyant sur le cadre CriticLean, nous construisons FineLeanCorpus, un ensemble de données comprenant plus de 285 000 problèmes, qui présente une riche diversité de domaines, une large couverture des niveaux de difficulté et une grande exactitude selon l'évaluation humaine. Globalement, nos résultats soulignent que l'optimisation de la phase de critique est essentielle pour produire des formalisations fiables, et nous espérons que CriticLean fournira des insights précieux pour les avancées futures dans le raisonnement mathématique formel.

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.