CriticLean 团队 投稿 量子位 | 公众号 QbitAI 当人工智能已经能下围棋、写代码，如何让机器理解并证明数学定理，仍是横亘在科研界的重大难题。 字节跳动Seed团队与南京大学 联合发布 CriticLean 框架，一举将 数学自然语言到Lean 4代码的形式化准确率从38%提升至84%。 该框架创新性地将评估模型置于核心位置。通过强化学习训练的CriticLeanGPT模型，能像数学专家一样精准判断形式化代码是否贴合原始语 义，配合迭代优化机制，让生成的定理证明既符合语法规范，又忠实于数学逻辑。 ⽬前论⽂和数据代码仓库均已对外公开，欢迎开源使用。 数学形式化领域的核心挑战 将自然语言描述的数学命题转化为机器可验证的形式化代码（如Lean 4定理），是自动化定理证明领域的基础性难题，其核心挑战不仅在于 语法层面的准确转换，更在于对数学语义的深度理解与忠实还原。 尽管现有研究在生成模型与编译有效性上取得一定进展，但在复杂问题的语义对齐上仍存在显著瓶颈，具体体现在以下三方面： 语义鸿沟： 引入Critic角色以实现可靠形式化 上述挑战的核心在于：形式化流程中"评价"与"生成"的割裂。 CriticL ...