标题：数学形式化准确率提升至84% | 字节&南大开源

正文：
人工智能在围棋、代码生成等领域已取得显著进展，但在理解并证明数学定理方面仍面临重大挑战。字节跳动Seed团队与南京大学联合发布CriticLean框架，将数学自然语言转化为Lean 4代码的形式化准确率从38%大幅提升至84%。该框架通过强化学习训练的CriticLeanGPT模型，精准判断形式化代码是否符合原始语义，并结合迭代优化机制，确保生成的定理证明既语法正确又逻辑忠实。论文和代码已开源。

数学形式化的挑战

将自然语言描述的数学命题转化为机器可验证的形式化代码是自动化定理证明的核心难题，主要瓶颈包括：
1. 语义鸿沟：隐含条件难以映射为形式逻辑，导致翻译偏差；
2. 评价缺位：现有方法对形式化结果的评估不够全面，难以识别逻辑矛盾；
3. 数据瓶颈：现有数据集规模小、多样性不足，限制了模型应对复杂问题的能力。

CriticLean框架的创新

CriticLean框架通过引入强化学习的Critic模型，结合编译器反馈和语义评估，系统性解决上述问题。其核心是CriticLeanGPT模型，基于Qwen2.5和Qwen3系列模型训练，分为两步：
1. 有监督微调（SFT）：使用4.8万条包含数学语句和形式化代码的数据进行训练，增强语义判断能力；
2. 强化学习优化（RL）：采用GRPO算法，以判断准确性和格式规范为奖励信号，提升评估能力。

该模型能识别12类常见错误，如类型错误（24.9%）、数学表示错误（23.8%），并发现“代码编译通过但逻辑偏离”的隐性问题。

CriticLeanBench基准测试

团队构建了首个聚焦形式化任务语义评估的基准测试CriticLeanBench，涵盖多种错误类型和数学领域。实验表明，CriticLeanGPT在500组测试样本中的准确率达87%，显著优于GPT-4o（67.8%）和Claude 3.5（74.2%）。

FineLeanCorpus高质量数据集

依托CriticLean框架，团队构建了包含28.5万条样本的高质量数学形式化数据集FineLeanCorpus，覆盖16个领域，人工抽检准确率达84%以上。相比现有数据集，其难度分布更均衡，主题覆盖更全面。

实验结果

应用CriticLean框架后，自动形式化流程的准确率从38%提升至84%，其中语义评估贡献了30个百分点的提升。

论文链接：https://arxiv.org/pdf/2507.06181
项目链接：https://github.com/multimodal-art-projection/CriticLean