超越DeepSeek-R1，数学形式化准确率飙升至84% 字节南大开源

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

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

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

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

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

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

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

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

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

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

　　特别声明：以上文章内容仅代表作者本人观点，不代表新浪网观点或立场。如有关于作品内容、版权或其它问题请于作品发表后的30日内与新浪网联系。

　　中共中央政治局召开会议 决定召开二十届四中全会 分析研究当前经济形势和经济工作 中共中央总书记习近平主持会议

　　中共中央政治局召开会议 决定召开二十届四中全会 分析研究当前经济形势和经济工作 中共中央总书记习近平主持会议