CriticLean: 수학적 형식화를 위한 비평가 지도 강화 학습

CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization

July 8, 2025

저자: 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

초록

자연어로 표현된 수학적 명제를 형식적이고 실행 가능한 코드로 번역하는 것은 자동화된 정리 증명에서 근본적인 과제입니다. 기존 연구는 생성과 컴파일 성공에 초점을 맞추었지만, 생성된 형식화가 원래 문제의 의미적 의도를 진정으로 반영하는지 평가하는 비평 단계에는 거의 주의를 기울이지 않았습니다. 본 논문에서는 비평의 역할을 수동적인 검증자에서 능동적인 학습 구성 요소로 격상시키는 새로운 비평 주도 강화 학습 프레임워크인 CriticLean을 소개합니다. 구체적으로, 먼저 Lean 4 형식화의 의미적 충실도를 엄격히 평가하기 위해 지도 미세 조정과 강화 학습을 통해 훈련된 CriticLeanGPT를 제안합니다. 그런 다음, 모델이 의미적으로 올바른 형식화와 잘못된 형식화를 구별하는 능력을 측정하기 위해 설계된 벤치마크인 CriticLeanBench를 소개하고, 우리가 훈련한 CriticLeanGPT 모델이 강력한 오픈소스 및 클로즈드소스 베이스라인을 크게 능가할 수 있음을 보여줍니다. CriticLean 프레임워크를 기반으로, 우리는 풍부한 도메인 다양성, 광범위한 난이도 범위, 그리고 인간 평가를 기반으로 한 높은 정확성을 보여주는 285K개 이상의 문제로 구성된 FineLeanCorpus 데이터셋을 구축했습니다. 전반적으로, 우리의 연구 결과는 신뢰할 수 있는 형식화를 생산하기 위해 비평 단계를 최적화하는 것이 필수적임을 강조하며, CriticLean이 형식적 수학적 추론의 미래 발전에 유용한 통찰력을 제공하기를 바랍니다.

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.