当东谈主工智能也曾能下围棋、写代码，何如让机器康健并表现数学定理，仍是横亘在科研界的紧要发愤。

字节朝上 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

一键三连「点赞」「转发」「留意心」

迎接在褒贬区留住你的思法！

—  完  —

� � 点亮星标 � �

科技前沿进展逐日见体育游戏app平台