CriticLean 团队 投稿
量子位 | 公众号 QbitAI

当人工智能已经能下围棋、写代码，如何让机器理解并证明数学定理，仍是横亘在科研界的重大难题。

字节跳动Seed团队与南京大学联合发布CriticLean框架，一举将数学自然语言到Lean 4代码的形式化准确率从38%提升至84%。

该框架创新性地将评估模型置于核心位置。通过强化学习训练的CriticLeanGPT模型，能像数学专家一样精准判断形式化代码是否贴合原始语义，配合迭代优化机制，让生成的定理证明既符合语法规范，又忠实于数学逻辑。

⽬前论⽂和数据代码仓库均已对外公开，欢迎开源使用。

数学形式化领域的核心挑战

将自然语言描述的数学命题转化为机器可验证的形式化代码（如Lean 4定理），是自动化定理证明领域的基础性难题，其核心挑战不仅在于语法层面的准确转换，更在于对数学语义的深度理解与忠实还原。

尽管现有研究在生成模型与编译有效性上取得一定进展，但在复杂问题的语义对齐上仍存在显著瓶颈，具体体现在以下三方面：

• 语义鸿沟：
  自然语言数学命题的隐含条件等难精准映射为形式逻辑，易出现前提翻译偏差等问题，过往方法因缺语义一致性校验，导致大量逻辑错误的形式化结果。
• 评价缺位：
  对形式化结果的评价依赖编译检查或 LLM 简单判断，存在错误类型覆盖不全、评价可靠性不足的问题，难以识别逻辑矛盾等。
• 数据瓶颈：
  现有数学形式化数据集规模和多样性不足、难度分布单一、语义校验缺失，制约了模型应对复杂数学命题的能力。

引入Critic角色以实现可靠形式化

上述挑战的核心在于：形式化流程中“评价”与“生成”的割裂。

CriticLean框架将引入强化学习的 Critic 模型，通过训练专门的语义评价模型（CriticLeanGPT）、结合 Lean 4 编译器反馈进行迭代生成。系统性解决语义对齐、评价可靠性与数据质量问题，为数学自动化形式化提供了全新范式。

图1：CriticLean框架通过编译器与评估器的双重反馈，实现数学形式化的迭代优化

CriticLeanGPT：会“挑错”的数学评估专家

团队基于Qwen2.5和Qwen3系列模型，通过两步训练打造专业评估器：

• 有监督微调（SFT）
  ：在4.8万条包含：数学、代码以及数学语句-形式化代码对一致性相关的Critic数据CriticLeanInstruct数据集上训练，增强其针对语义判断的评估能力。
• 强化学习优化（RL）
  ：采用GRPO算法，以“判断是否准确”和“输出格式是否规范”作为奖励信号，让模型学会在评估中迭代提升。

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

△图2：不同类型错误的分布

CriticLeanBench：首个聚焦形式化任务语义评估的基准测试

CriticLeanBench是用于评估模型在数学形式化任务中关键推理能力的基准测试，旨在全面衡量模型将自然语言数学陈述转化为经形式验证的定理声明等方面的表现.

其构建和实现过程如下：

CriticLeanBench 在数据收集阶段，从多个数据来源选取数学陈述及对应的Lean 4 陈述，提交Lean 4陈述到编译器。1）对于编译失败的语句，随机采样保留编译器反馈信息。2）对于编译成功的部分，通过使用 DeepSeek R1 结合专家校验的方式保留正确和错误的样本（错误的样本保留错误信息）。

• 数据来源多样：
  数学陈述选取了Omni-MATH、AIME、U-MATH等多个数据源，这些数据源涵盖了不同难度层次和数学领域的问题。有助于更全面准确地评估模型在不同数学内容上的表现。
• 覆盖多种错误类型：
  CriticLeanBench 覆盖语法错误、语义错误、逻辑错误等多种问题，全面考察模型能力。
• 确保评估可靠有效：
  通过专家审查和大模型验证相结合的方式来保证评估基准的可靠性和有效性。在不同类别中选取具有代表性的样本，确保涵盖各种错误类型，从而使评估结果更可靠。

△图3: CriticLeanBench 构建的概览

△表1：CriticLeanBench 数据集统计信息与各类代码基准数据集的对比

在包含500组测试样本的CriticLeanBench基准中，CriticLeanGPT的准确率达到87%，远超GPT-4o（67.8%）和Claude 3.5（74.2%），甚至超过DeepSeek-R1（84%）的表现。

• 核心指标：
  Qwen3-32B-RL版本准确率达87%，true negative rate（正确识别错误样本）达85.6%，远超GPT-4o的40.0%。
• 对比优势：
  在相同模型规模下，经CriticLean训练的Qwen2.5-32B模型准确率（78.6%）较基础版（73.0%）提升5.6%，且对错误样本的识别能力提升明显。

△表2：在 CriticLeanBench 上的性能表现

模型大小的Scaling分析表明，模型性能随规模提升稳步增强。

△图4: 大语言模型在 CriticLeanBench 上的扩展性分析(ˆ 表示闭源的大语言模型)

FineLeanCorpus：28.5万条高质量形式化数据

依托CriticLean框架，团队构建了目前规模最大、质量最高的数学形式化数据集之一：

• 规模与多样性：
  包含285,957条样本，覆盖从高中奥数到大学数学的16个领域，其中高难度子集（Diamond）含36,033条问题。
• 质量保障：
  每条样本均通过编译器语法检查与CriticLeanGPT语义验证，人工抽检准确率达84%以上。
• 结构优势：
  相比LeanWorkbook，其难度分布更均衡（多峰分布），领域覆盖更全面（如解析几何样本量提升300%）。

△表3：FineLeanCorpus 的不同来源及数据集统计信息

与高度偏斜的 Lean-Workbook 相比，FineLeanCorpus 提供了更透明的批判过程、更高比例的顶级问题，以及更加平衡和多样化的主题分布

△表4：数据集统计信息的对比

与高度偏斜的 Lean-Workbook 相比，FineLeanCorpus 提供了更透明的批判过程、更高比例的顶级问题，以及更加平衡和多样化的主题分布

△图5：数据集统计信息的对比()

实验结果：大幅提高数学形式化准确率

将该框架应用于自动形式化流程，配合Kimina-Autoformalizer-7B生成器，准确率从38%（单轮生成）提升至84%（多轮迭代优化），其中语义评估环节贡献了30个百分点的提升。

△表5：自动化形式化性能的人类评估准确率结果

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