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, новую структуру обучения с подкреплением, управляемую критиком, которая повышает роль критика с пассивного валидатора до активного компонента обучения. В частности, сначала мы предлагаем CriticLeanGPT, обученный с помощью контролируемой тонкой настройки и обучения с подкреплением, для строгой оценки семантической точности формализаций в Lean 4. Затем мы представляем CriticLeanBench, эталонный тест, предназначенный для измерения способности моделей отличать семантически корректные формализации от некорректных, и показываем, что наши обученные модели CriticLeanGPT значительно превосходят сильные базовые модели с открытым и закрытым исходным кодом. На основе структуры CriticLean мы создаем FineLeanCorpus, набор данных, содержащий более 285 тысяч задач, который демонстрирует богатое разнообразие областей, широкий охват сложности и высокую корректность по оценке экспертов. В целом, наши результаты подчеркивают, что оптимизация этапа критики необходима для создания надежных формализаций, и мы надеемся, что наш 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.