AI 助力数学形式化：自然语言一键生成 Lean4 代码，门槛大幅降低！

始智AI wisemodel 2025年02月06日 18:00 北京

人工智能深度赋能了数学形式化领域，尤其是在自然语言自动转化为形式化定理这一关键环节取得重大突破。

这个突破来自多个维度。在技术应用层面，实现了自然语言到Lean4代码的自动转换，极大降低了数学形式化的技术门槛，让更多缺乏专业形式化语言背景的研究者也能参与其中，扩大了数学形式化研究的人才队伍。

在研究效率提升上，显著加速数学定理的机器验证过程，既有助于验证已知定理，又能助力探索新的数学猜想与证明，推动数学研究向更深层次发展。

从数据资源角度，为自动化定理证明领域提供了生成高质量、多样化训练数据的新思路，像上海交通大学AI4MATH团队开源的全合成Lean4形式化数据集，打破大模型训练数据瓶颈，进一步提升模型在数学推理和定理证明方面的能力 。

同时基于 Qwen2.5-7b 架构的数学形式化模型在两大基准测试上创造新纪录：

MiniF2F: pass@1 语法编译成功率达到 95.3%（465/488）

ProofNet: pass@1 语法编译成功率达到 76.0%（284/374）

这一突破性成果不仅超越了现有(2024)最佳水平，更展现了 AI 在数学形式化验证领域的巨大潜力，以及合成数据在形式化任务中的关键作用。Lean4系列成果已上线始智AI-wisemodel开源社区，欢迎下载和使用。

模型和数据集地址

https://wisemodel.cn/organization/SJTULean

01.

Lean4:新一代交互式定理证明助手

Lean4 作为微软研究院开发的新一代交互式定理证明助手，为数学形式化和大模型数理能力提升提供了强大支持：

强大的类型系统：支持依值类型（dependent type），能够精确表达复杂的数学概念，使得 Lean4 成为描述大模型推理过程的理想工具。 

灵活的元编程能力：通过 tactic 系统，用户可以实现证明过程的自动化，这为大模型学习复杂的推理策略提供了可能。

丰富的数学库支持：mathlib 提供了庞大的数学定理库，为用户提供了便利，也为大模型提供了丰富的数理知识库。

可靠的形式化保证：Lean4 能够生成机器可验证的数学证明，确保数学推理的严谨性，这为构建可靠的大模型推理系统提供了基础。

02.

全球最大规模数据集与高性能模型

研究团队通过构建 LeanStatement 数据集体系和开发 LeanFormalizer 模型系列，在自然语言到 Lean4 形式化定理的转换任务中取得了显著进展。

数据集的多样性和高质量为模型训练提供了坚实基础，而模型的持续优化则进一步提升了任务的准确性和可解释性。这一成果为形式化验证和自动化推理领域的发展提供了重要支持。

1、LeanStatement 数据集体系

为了构建一个完整的训练体系，团队开发了三个互补的数据集，这些数据集共同支持从自然语言到 Lean4 形式化定理的转换任务。以下是每个数据集的详细描述：

LeanStatement_SFT 数据集：

• 规模领先：196 万条自然语言到 Lean4 形式化定理的配对数据

• 全合成数据：采用全合成方式生成训练数据

• 质量保证：严格的语法编译筛选和多重语义验证

• 数据结构：包含自然语言描述和对应的 Lean4 形式化陈述

• 应用价值：支持自然语言到 Lean4 形式化的精确转换

LeanStatement_CoT 数据集：

• 规模与内容：14.2 万条带有详细推理过程的转换数据

• 推理链路：完整记录从自然语言到 Lean4 代码的推理链路

• 模型提升：通过提供详细的推理链路，显著提升了模型的可解释性和推理能力

LeanStatement_RL 数据集：

• 规模与用途：576 万条奖励建模数据

• 应用价值：用于训练质量评估模型

• 数据标注：包含编译成功/失败标注，支持模型优化

2、LeanFormalizer 模型系列

基于上述数据集，团队开发了 LeanFormalizer 模型系列，旨在实现从自然语言到 Lean4 形式化定理的高效转换。以下是各模型的具体表现和优化路径：

LeanFormalizer_SFT：

• 架构与训练：基于 Qwen2.5-7b 架构，在 LeanStatement_SFT 上监督微调

• 性能表现：

  MiniF2F 测试集：94.1% pass@1 (459/488)

  ProofNet 测试集：75.4% pass@1 (282/374)

LeanFormalizer_PPO：

• 优化方法：采用强化学习进一步优化

• 性能提升：

  MiniF2F 提升至 95.3% (465/488)

  ProofNet 提升至 76.0% (284/374)

LeanFormalizer_Reward：

• 专注领域：专注于翻译质量评估

• 训练数据：基于 LeanStatement_RL 训练

• 应用价值：支持模型优化和质量评估

这一系列工作不仅推动了自然语言到形式化定理转换技术的发展，还为形式化验证和自动化推理领域提供了强有力的工具和方法支持。未来，团队将继续优化模型性能，并探索更广泛的应用场景。

SJTU AI4MATH Lab - Lean4 Research Group 开源项目由上海交通大学（SJTU）罗涛教授 的 AI4MATH 实验室与受奇绩创坛投资的企业交影科技共同贡献，聚焦于 Lean4 形式化方向的研究工作。实验室主要探究如何将自然语言的数学表达自动转化为 Lean4 形式化证明的过程，以进一步推动人工智能在数学定理形式化证明领域的发展。

编辑丨赵雅鑫

-----    END   -----