自动形式化（Autoformalization）旨在将自然语言数学陈述自动转换为机器可验证的形式化语言（如 Lean、Coq），是构建大规模数学知识库的关键技术。然而，平行语料稀缺、形式化语法严格、语义对齐困难等挑战长期制约着该领域发展。ATLAS（Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data）框架通过系统化的数据生成流水线，在 10 轮迭代中构建出 117k 条本科级别定理陈述数据集，其微调后的 Llama3.1-8B-Instruct 模型在多个基准测试中实现了统计显著的性能提升。
三阶段流水线架构
ATLAS 的核心创新在于将数据生成形式化为可迭代的教师 - 学生范式。整个流水线由三个关键阶段构成：
Lifting（提升阶段） 从概念库（Concept Repository）出发，将非结构化的自然数学描述转化为结构化的定理陈述候选。这一阶段不依赖已有的平行语料，而是通过概念组合与模板扩展生成初始的 NL-FL（自然语言 - 形式语言）对，有效突破了数据稀缺的瓶颈。
Augmentation（增强阶段） 针对形式语言的结构性特征设计了两类增强策略：语法层面的变量重命名与表达式等价变换，以及语义层面的条件强化与弱化。这些增强操作不仅扩充了数据规模，更重要的是提升了模型对形式语言结构不变性的理解能力。
Synthesis（合成阶段） 通过专家迭代（Expert Iteration）结合知识蒸馏，持续优化学生模型的翻译质量。每一轮迭代中，教师模型对生成的形式化陈述进行修正与对齐，形成高质量的训练信号反馈给学生模型。
可复现流水线的工程要点
构建可复现的自动形式化流水线需要在数据生成、验证与评估三个环节建立严格的工程规范。
数据生成配置 需关注 configs/config_generation.py 中的关键参数：概念库路径决定生成空间的覆盖范围，建议从数学分析、线性代数、抽象代数等本科核心课程构建分层概念体系；温度参数控制生成多样性，定理陈述生成建议设置在 0.7-0.9 区间以平衡创造性与语法正确性；批量大小需根据 Lean REPL 的并发处理能力调整，默认配置下建议每批次不超过 100 条陈述。
验证层设计 采用多层过滤机制确保输出质量。第一层为 Lean4 编译检查，通过 src/repl/ 中的 REPL 项目验证形式化陈述的语法正确性；第二层为回译验证（Back-translation），将形式化陈述重新翻译为自然语言，通过语义一致性判断原始转换的可靠性；第三层引入 NLI（自然语言推理）模型进行语义对齐检查，过滤逻辑不等价的转换结果。
评估流水线 在 evaluation.py 中实现端到端评估，支持 MiniF2F、ProofNet、Putnam、MathQual 等标准基准。评估指标需同时关注编译通过率与语义保持率，前者衡量语法正确性，后者通过回译 - NLI 联合检查衡量语义等价性。
从教科书到形式化知识库
将 ATLAS 流水线应用于教科书形式化时，建议采用分阶段推进策略。初期聚焦于定义与定理陈述的转换，暂不深究证明细节；中期引入证明草图的自动形式化，利用现有的证明自动化工具（如 Lean 的 aesop 策略）填补简单推理步骤；后期构建完整的证明链，形成可验证的知识图谱。
在工程实践中，需特别注意形式化语言的版本兼容性。ATLAS 基于 Lean4 构建，需确保本地 Lean 工具链与 lakefile.toml 中声明的版本一致。对于大规模部署，建议采用分片索引策略，将概念库按数学领域划分为独立子集，分别生成后合并，以降低单点故障风险。
该框架的模块化设计（src/workers/ 中的合成器、增强器、验证器、回译器、NLI 检查器）支持灵活的组件替换与能力扩展。例如，可将 NLI 检查器替换为领域特定的语义验证模块，或将合成器接入更强的基础模型以提升生成质量。
局限与展望
ATLAS 当前主要聚焦于定理陈述的形式化，对完整证明的形式化支持仍依赖外部证明自动化工具。此外，形式化语言的选择（Lean4）虽然兼顾了表达力与自动化支持，但与 Coq、Isabelle 等生态的互操作性仍需额外适配层。
尽管如此，ATLAS 提供的可复现流水线为自动形式化的工程化部署提供了可行路径。通过标准化的数据生成、多层验证与迭代优化机制，该框架有望支撑从教科书到大规模机器验证数学知识库的系统性转化。
资料来源
- Liu, X., et al. (2025). ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data. arXiv:2502.05567.
- ATLAS GitHub Repository: https://github.com/XiaoyangLiu-sjtu/ATLAS
内容声明：本文无广告投放、无付费植入。
如有事实性问题，欢迎发送勘误至 i@hotdrydog.com。