当人工智能已经能下围棋、写代码线上正规配资，如何让机器理解并证明数学定理，仍是横亘在科研界的重大难题。
字节跳动 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：数据集统计信息的对比
△图 5：数据集统计信息的对比 ( ) 实验结果：大幅提高数学形式化准确率
将该框架应用于自动形式化流程，配合 Kimina-Autoformalizer-7B 生成器，准确率从 38%（单轮生成）提升至 84%（多轮迭代优化），其中语义评估环节贡献了 30 个百分点的提升。
△表 5：自动化形式化性能的人类评估准确率结果
论文链接：https://arxiv.org/pdf/2507.06181
项目链接：https://github.com/multimodal-art-projection/CriticLean
一键三连「点赞」「转发」「小心心」
欢迎在评论区留下你的想法！
— 完 —
� � 点亮星标 � �
科技前沿进展每日见线上正规配资
银河配资提示：文章来自网络，不代表本站观点。
炒股配资查询之家 第三届世界科学智能大赛圆满收官！开放多项真实数据，1.6万人共探产业场景关键科学问题
线上正规配资 超越DeepSeek-R1，数学形式化准确率飙升至84%
