CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization
作者: 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.CL
发布日期: 2025-07-08
💡 一句话要点
提出CriticLean：一种评论家引导的强化学习框架，用于数学形式化。
🎯 匹配领域: 支柱二：RL算法与架构 (RL & Architecture)
关键词: 数学形式化 强化学习 评论家模型 自动化定理证明 语义保真度
📋 核心要点
- 现有数学形式化方法侧重于生成和编译，忽略了对形式化代码语义正确性的有效评估。
- CriticLean框架通过训练评论家模型CriticLeanGPT，主动评估形式化代码的语义保真度，引导强化学习过程。
- 实验表明，CriticLeanGPT在区分语义正确和错误的形式化方面显著优于现有基线，并构建了高质量的FineLeanCorpus数据集。
📝 摘要（中文）
本文提出了一种新颖的评论家引导的强化学习框架CriticLean，旨在提升数学形式化中评论阶段的作用。与以往工作侧重于生成和编译成功率不同，CriticLean强调对生成的形式化代码是否真正捕捉到原始问题的语义意图进行评估。具体而言，首先提出了CriticLeanGPT，通过监督微调和强化学习进行训练，以严格评估Lean 4形式化的语义保真度。其次，引入了CriticLeanBench，用于衡量模型区分语义正确和错误形式化的能力，并证明了CriticLeanGPT模型显著优于现有的强基线模型。此外，构建了FineLeanCorpus数据集，包含超过28.5万个问题，具有丰富的领域多样性、广泛的难度覆盖和基于人工评估的高正确性。研究结果表明，优化评论阶段对于产生可靠的形式化至关重要，并希望CriticLean能为未来形式数学推理的进展提供有价值的见解。
🔬 方法详解
问题定义：论文旨在解决将自然语言数学陈述翻译成形式化、可执行代码的问题。现有方法主要关注生成和编译的成功率，而忽略了对生成的形式化代码是否真正捕捉到原始问题的语义意图的评估，导致形式化结果的可靠性不足。
核心思路：论文的核心思路是将评论阶段从被动验证转变为主动学习组件。通过训练一个能够准确评估形式化代码语义保真度的评论家模型，并利用该评论家模型的反馈来指导强化学习过程，从而提高生成形式化代码的质量和可靠性。这样设计的目的是为了确保生成的形式化代码不仅在语法上正确，而且在语义上与原始数学陈述保持一致。
技术框架：CriticLean框架主要包含以下几个模块：1) CriticLeanGPT：一个用于评估Lean 4形式化代码语义保真度的评论家模型，通过监督微调和强化学习进行训练。2) CriticLeanBench：一个用于衡量模型区分语义正确和错误形式化代码能力的基准测试。3) FineLeanCorpus：一个包含超过28.5万个问题的、高质量的数学形式化数据集。整体流程是，首先使用FineLeanCorpus训练CriticLeanGPT，然后使用CriticLeanGPT作为评论家来指导强化学习过程，最终生成高质量的数学形式化代码。
关键创新：论文最重要的技术创新点在于将评论家模型从被动验证的角色提升到主动学习的角色。传统的强化学习方法通常使用奖励函数来评估生成结果的质量，而CriticLean则使用训练好的评论家模型CriticLeanGPT来更准确地评估形式化代码的语义保真度，从而更有效地指导强化学习过程。与现有方法的本质区别在于，CriticLean更加关注形式化代码的语义正确性，而不仅仅是语法正确性。
关键设计：CriticLeanGPT的训练采用了监督微调和强化学习相结合的方法。监督微调使用FineLeanCorpus数据集，强化学习则使用评论家模型的反馈作为奖励信号。损失函数的设计旨在最大化评论家模型区分语义正确和错误形式化代码的能力。网络结构方面，具体细节未知，但推测使用了Transformer等常用的序列模型。
🖼️ 关键图片
📊 实验亮点
CriticLeanGPT在CriticLeanBench上显著优于现有的强基线模型，证明了其在评估形式化代码语义保真度方面的有效性。此外，FineLeanCorpus数据集的构建为数学形式化领域提供了高质量的训练数据。具体性能数据和提升幅度在摘要中未明确给出，需查阅论文全文。
🎯 应用场景
CriticLean框架可应用于自动化定理证明、数学教育、软件验证等领域。通过将自然语言数学描述转化为形式化代码，可以帮助研究人员和学生更方便地进行数学推理和验证。此外，该框架还可以用于验证软件代码的正确性，提高软件的可靠性。未来，该研究有望推动形式化方法的普及和应用。
📄 摘要（原文）
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.