⏶39
CriticLean: 评论家引导的强化学习，用于数学形式化
发表
由 
zhongyuan peng 提交
zhongyuan peng 提交作者: 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
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摘要
将自然语言数学语句转化为形式化、可执行的代码是自动化定理证明中的一个基本挑战。虽然现有工作主要关注生成和编译的成功，但很少关注批评阶段——即评估所生成的形式化是否真正捕捉了原始问题的语义意图。在本文中，我们引入了CriticLean，这是一个新颖的批评家指导强化学习框架，它将批评家的角色从被动验证者提升为主动学习组件。具体而言，首先，我们提出了CriticLeanGPT，它通过监督微调和强化学习进行训练，以严格评估Lean 4形式化的语义保真度。然后，我们引入了CriticLeanBench，这是一个旨在衡量模型区分语义正确和不正确形式化能力的基准，并证明我们训练的CriticLeanGPT模型可以显著优于强大的开源和闭源基线。在CriticLean框架的基础上，我们构建了FineLeanCorpus，这是一个包含超过28.5万个问题的数据集，该数据集展现了丰富的领域多样性、广泛的难度覆盖和基于人工评估的高正确性。总的来说，我们的发现强调，优化批评阶段对于生成可靠的形式化至关重要，我们希望CriticLean能为形式数学推理的未来发展提供宝贵的见解。
将自然语言数学语句转化为形式化、可执行的代码是自动化定理证明中的一个基本挑战。尽管先前的工作主要集中于生成和编译的成功，但很少关注批评阶段——即评估生成的规范化是否真正捕捉到原始问题的语义意图。在本文中，我们引入了CriticLean，这是一种新颖的批评引导强化学习框架，它将批评者的角色从被动验证器提升为主动学习组件。具体来说，我们首先提出了CriticLeanGPT，通过监督微调和强化学习进行训练，以严格评估Lean 4形式化的语义忠实度。然后，我们引入了CriticLeanBench，这是一个旨在衡量模型区分语义正确和不正确形式化能力的基准，并证明我们训练的CriticLeanGPT模型能够显著优于强大的开源和闭源基线。基于CriticLean框架，我们构建了FineLeanCorpus，一个包含超过28.5万个问题的数据集，该数据集展现了丰富的领域多样性、广泛的难度覆盖范围以及基于人工评估的高正确性。总的来说，我们的研究结果强调，优化批评阶段对于生成可靠的形式化至关重要，我们希望CriticLean能为形式数学推理的未来进展提供宝贵见解。