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フレームワークを基盤として、豊富なドメイン多様性、広範な難易度カバレッジ、および人間による評価に基づく高い正確性を備えた28万5千以上の問題を含むデータセット「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.