CriticLean: Aprendizaje por Refuerzo Guiado por Críticas para la Formalización Matemática

CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization

July 8, 2025

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

Resumen

Traducir enunciados matemáticos en lenguaje natural a código formal y ejecutable es un desafío fundamental en la demostración automática de teoremas. Si bien trabajos previos se han centrado en la generación y compilación exitosa, se ha prestado poca atención a la fase del crítico: la evaluación de si las formalizaciones generadas capturan verdaderamente la intención semántica del problema original. En este artículo, presentamos CriticLean, un novedoso marco de aprendizaje por refuerzo guiado por un crítico que eleva el papel del crítico de un validador pasivo a un componente activo de aprendizaje. Específicamente, primero proponemos CriticLeanGPT, entrenado mediante ajuste fino supervisado y aprendizaje por refuerzo, para evaluar rigurosamente la fidelidad semántica de las formalizaciones en Lean 4. Luego, introducimos CriticLeanBench, un punto de referencia diseñado para medir la capacidad de los modelos para distinguir formalizaciones semánticamente correctas de incorrectas, y demostramos que nuestros modelos CriticLeanGPT entrenados superan significativamente a fuertes líneas base de código abierto y cerrado. Basándonos en el marco de CriticLean, construimos FineLeanCorpus, un conjunto de datos que comprende más de 285K problemas y que exhibe una rica diversidad de dominios, una amplia cobertura de dificultad y una alta corrección según la evaluación humana. En general, nuestros hallazgos destacan que optimizar la fase del crítico es esencial para producir formalizaciones confiables, y esperamos que nuestro CriticLean brinde valiosos insights para futuros avances en el razonamiento matemático formal.

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.