ATLAS：基于大语言模型的规模化自动形式化教材库

背景

形式化验证（Formal Verification）是数学和计算机科学中确保逻辑严谨性的黄金标准，而 Lean 作为一种强大的交互式定理证明器，近年来在形式化数学领域取得了显著进展。然而，将非形式化的数学教材（如本科和研究生级别的教科书）转化为机器可读的 Lean 代码，一直是一项耗时且极具挑战性的工作。传统的形式化工作主要依赖人类专家手动完成，规模有限且扩展性不足。

随着大语言模型（LLM）在代码生成和逻辑推理能力上的提升，利用 AI 辅助甚至主导形式化过程成为可能。在此背景下，Facebook Research（现 Meta AI）的研究团队推出了 ATLAS（Autoformalized Textbook Library At Scale）。这是一个旨在通过 LLM 大规模自动形式化数学教材的项目，其核心目标是解决形式化数学“规模”与“覆盖率”的瓶颈，为未来的人类驱动和机器驱动的形式化工作提供可复用的基础构件。

核心内容

ATLAS 是一个基于 Lean 4 的大型库，包含了由 LLM 自动形式化的教科书数学内容。该项目将非形式化的数学陈述和证明翻译为 Lean 代码，涵盖了分析、代数、几何、拓扑、组合学、概率、统计、偏微分方程（PDE）、数论以及理论计算机科学等多个本科和研究生级别的数学领域。

生成流程与工具

ATLAS 的内容是通过 AutoformBot 这一自动形式化流水线生成的。该流水线不仅负责将文本转换为代码，还包含了一套完整的评估和筛选机制：

• 目标选择：每个书籍目录下包含一个 targets.yaml 文件，列出了被选中进行形式化的教科书陈述。
• 自动化评估：每个目录还包含一个 report.json 文件，记录了匹配 Lean 声明的自动化评估结果。评估指标包括忠实度（faithfulness）、证明完整性（proof-integrity）和代码质量（code-quality）。

项目规模与数据

ATLAS 目前是一个持续扩展的项目，而非最终成品。其最新数据规模如下：

• 书籍数量：26 本教科书。
• 代码行数：总计 630,999 行代码，其中 Lean 代码（不含注释和空行）为 483,917 行。
• 声明与证明：包含 46,203 个声明，其中 42,837 个已得到证明（证明率 92.7%）。
• 陈述形式化率：在 4,007 个被形式化的陈述中，成功形式化了 2,855 个（形式化率 71.3%）。
• 计算资源：生成过程消耗了 183,157M tokens。

用户交互与可视化

为了方便研究人员和开发者使用，项目提供了一个可视化工具（https://rammalahmad.github.io/atlas/）。该工具允许用户：

1. 浏览 ATLAS 库中的内容。
2. 对比非形式化陈述与其 Lean 形式化版本。
3. 检查结果之间的逻辑依赖图。
4. 提取陈述特定定理所需的 Lean 代码。

构建与贡献

用户可以通过运行 lake build 命令，使用固定的 Lean 和 Mathlib 版本构建完整的库。项目强调这是一个活跃的努力方向，团队正在持续扩展来源、整理生成的材料、提高覆盖率和可维护性，并使库更贴近 Mathlib 的惯例。外部贡献者被欢迎参与进来，共同改进代码的惯用性和复用性。

关键要点

• 规模化突破：ATLAS 是目前规模最大的 LLM 自动形式化数学教材库之一，涵盖了从本科到研究生水平的多个核心数学分支。
• 自动化流水线：依托 AutoformBot 流水线，实现了从非形式化文本到 Lean 4 代码的端到端转换，并内置了质量评估机制（忠实度、完整性、代码质量）。
• 高证明覆盖率：在已形式化的声明中，证明成功率高达 92.7%，显示出 LLM 在生成可验证证明方面的强大能力。
• 基础设施导向：ATLAS 的定位是提供“可复用的形式化构件”，旨在为未来的形式化工作（无论是人工还是机器）打下基础，而非仅仅作为一个静态的知识库。
• 持续迭代：项目明确表示这是一个 ongoing（进行中）的努力，重点在于扩展语料库、整理代码、形式化剩余陈述以及提高与 Mathlib 的兼容性。
• 透明与开放：项目公开了代码库、评估报告、可视化界面以及相关的学术论文，鼓励社区贡献和复用。

意义与影响

ATLAS 的出现标志着形式化数学研究进入了一个新的阶段，即从“小规模、高精度的人工形式化”向“大规模、自动化、人机协作的形式化”转变。

首先，它极大地降低了形式化数学的门槛。通过提供大量现成的、经过初步验证的 Lean 代码片段，研究人员和开发者可以在此基础上进行更复杂的证明，而无需从零开始。这种“积木式”的方法有助于加速数学发现和技术验证的过程。

其次，ATLAS 展示了 LLM 在逻辑推理和代码生成方面的巨大潜力。尽管目前的形式化率（71.3%）仍有提升空间，但 92.7% 的证明成功率表明，AI 已经能够处理相当复杂的数学逻辑结构。这为未来开发更强大的 AI 辅助数学证明工具奠定了基础。

最后，ATLAS 强调了人机协作的重要性。项目不仅依赖 AI 生成代码，还引入了自动化评估和人工策展（curate）环节，旨在提高代码的质量和可维护性。这种混合模式可能是未来形式化数学发展的主流方向：AI 负责大规模生成和初步筛选，人类专家负责审查、优化和整合，从而构建出更加健壮和可信的形式化数学库。

对于 Mathlib 社区而言，ATLAS 提供了丰富的潜在贡献源。通过将这些自动生成的高质量代码整合进 Mathlib，可以丰富库的内容，提高其覆盖范围，并推动形式化数学在更广泛领域的应用。