CriticLean: Apprendimento per Rinforzo Guidato dal Critico per la Formalizzazione Matematica

CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization

July 8, 2025

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

Abstract

La traduzione di enunciati matematici in linguaggio naturale in codice formale ed eseguibile rappresenta una sfida fondamentale nel campo della dimostrazione automatica di teoremi. Mentre il lavoro precedente si è concentrato sul successo della generazione e della compilazione, poca attenzione è stata dedicata alla fase del critico, ovvero alla valutazione se le formalizzazioni generate catturino veramente l'intento semantico del problema originale. In questo articolo, introduciamo CriticLean, un nuovo framework di apprendimento per rinforzo guidato dal critico che eleva il ruolo del critico da validatore passivo a componente attivo dell'apprendimento. Nello specifico, proponiamo prima CriticLeanGPT, addestrato tramite fine-tuning supervisionato e apprendimento per rinforzo, per valutare rigorosamente la fedeltà semantica delle formalizzazioni in Lean 4. Successivamente, introduciamo CriticLeanBench, un benchmark progettato per misurare la capacità dei modelli di distinguere formalizzazioni semanticamente corrette da quelle errate, e dimostriamo che i nostri modelli CriticLeanGPT addestrati superano significativamente i forti baseline open-source e closed-source. Basandoci sul framework CriticLean, costruiamo FineLeanCorpus, un dataset che comprende oltre 285K problemi e che mostra una ricca diversità di dominio, un'ampia copertura delle difficoltà e un'elevata correttezza basata sulla valutazione umana. Nel complesso, i nostri risultati evidenziano che ottimizzare la fase del critico è essenziale per produrre formalizzazioni affidabili, e speriamo che il nostro CriticLean fornisca spunti preziosi per i futuri progressi nel ragionamento matematico formale.

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.