摘要
将自然语言数学陈述转换为形式化的可执行代码是自动定理证明中的一个基本挑战。尽管先前的研究主要集中在生成和编译的成功率上，但对批评阶段的关注却较少——即评估生成的形式化是否真正捕捉到了原始问题的语义意图。在本文中，我们介绍了CriticLean，这是一种新颖的由批评者引导的强化学习框架，它将批评者的角色从被动验证者提升为主动学习组件。具体而言，首先，我们提出了CriticLeanGPT，该模型通过监督微调和强化学习训练，用于严格评估Lean 4形式化的语义保真度。然后，我们引入了CriticLeanBench，这是一个旨在衡量模型区分语义正确和错误形式化能力的基准测试，并展示了我们的训练后的CriticLeanGPT模型可以显著优于强大的开源和闭源基线模型。基于CriticLean框架，我们构建了FineLeanCorpus数据集，该数据集包含超过28.5万个问题，展现出丰富的领域多样性、广泛的难度覆盖范围以及根据人工评估的高度正确性。总体而言，我们的研究结果强调了优化批评阶段对于生成可靠形式化的重要性，并希望我们的CriticLean能够为未来形式化数学推理的发展提供有价值的见解。