CriticLean: Aprendizado por Reforço Guiado por Crítico para Formalização 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

Resumo

Traduzir declarações matemáticas em linguagem natural para código formal e executável é um desafio fundamental na prova de teoremas automatizada. Embora trabalhos anteriores tenham se concentrado no sucesso da geração e compilação, pouca atenção foi dada à fase do crítico — a avaliação de se as formalizações geradas realmente capturam a intenção semântica do problema original. Neste artigo, apresentamos o CriticLean, uma nova estrutura de aprendizado por reforço guiada por crítico que eleva o papel do crítico de um validador passivo para um componente ativo de aprendizado. Especificamente, primeiro propomos o CriticLeanGPT, treinado por meio de ajuste fino supervisionado e aprendizado por reforço, para avaliar rigorosamente a fidelidade semântica das formalizações em Lean 4. Em seguida, introduzimos o CriticLeanBench, um benchmark projetado para medir a capacidade dos modelos de distinguir formalizações semanticamente corretas das incorretas, e demonstramos que nossos modelos CriticLeanGPT treinados podem superar significativamente baselines fortes de código aberto e fechado. Com base na estrutura CriticLean, construímos o FineLeanCorpus, um conjunto de dados que compreende mais de 285K problemas, exibindo diversidade rica de domínios, ampla cobertura de dificuldade e alta correção com base em avaliação humana. No geral, nossos resultados destacam que otimizar a fase do crítico é essencial para produzir formalizações confiáveis, e esperamos que nosso CriticLean forneça insights valiosos para avanços futuros no raciocínio 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.