ICML 2026 | 理论级自动形式化：从孤立命题到统一形式化知识库

导读

自动形式化正在成为大模型推理、数学证明和可信工程系统之间的一座桥。它要解决的问题看似直接：把自然语言中的命题、证明或规范，翻译成 Lean、Coq、Isabelle、TLA+、Cedar 等机器可检查的形式语言。过去几年，研究社区已经在“单个语句”的自动形式化上取得了明显进展，例如把一道数学题、一个定理陈述或一段证明片段翻译成形式化声明。 但这篇 ICML 2026 position paper 指出：真正困难的部分并不是翻译孤立语句，而是构建完整理论。一个定理之所以能被写出来，背后依赖的是公理、定义、记号、例子、引理、证明策略和库之间的依赖网络。没有这些底层结构，目标定理往往甚至无法被正确表述。作者因此提出“理论级自动形式化”这一研究方向：让系统自动构建一个范围内完整、连贯、可复用的形式化知识库，而不只是翻译几个单点命题。 这篇文章的价值在于，它把自动形式化从“翻译任务”重新定位为“知识库工程与理论发现任务”。论文并不只是综述已有方法，而是明确给出研究立场：如果希望 AI 真正参与数学、科学、软件和硬件验证，仅靠 statement-level autoformalization 不够；未来需要能处理完整理论、低资源领域语言、多模态输入以及语义等价检查的通用自动形式化系统。

论文信息

论文题目：Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases 论文链接：https://arxiv.org/abs/2607.13292 会议信息：ICML 2026，43rd International Conference on Machine Learning 作者团队：Marcus J. Min、Mike He、Zhaoyu Li、Zixuan Yi、Sharad Malik、Aarti Gupta、Xujie Si、Osbert Bastani 论文类型：Position Paper 核心问题：自动形式化是否应继续围绕孤立语句展开，还是必须走向完整理论库的自动构建？

1. 从语句到理论：自动形式化的对象正在改变

作者给出的定义非常清晰：理论级自动形式化是指，在给定范围内，自动形式化整个理论上下文，包括公理、定义、记号、例子、引理、定理、证明、策略以及它们之间的依赖关系，并将其组织成一个连贯的形式化库。 这一定义把问题从“翻译一句话”推进到“构建一个可运行的理论系统”。以毕达哥拉斯定理为例，如果只看最终陈述，它似乎是一个简单的几何命题。但在形式系统中，要陈述并证明这个定理，首先需要点、线、角、三角形、同侧关系、垂直、长度、相等等底层概念；还需要一系列引理、记号和自动化策略来支撑证明过程。目标定理只是最上层，真正的工作在下面几层。 论文用“理论级自动形式化塔”刻画这一结构。第 0 层是公理化定义，例如原始对象和原始关系；第 1 层是派生定义，例如角、三角形和复合关系；第 2 层是工具基础设施，包括记号、引理和证明策略；第 3 层才是目标定理及其证明。当前很多 statement-level 方法默认下面几层已经由人类完成，因此只在最上层做翻译。作者认为，这种假设限制了自动形式化走向新领域。

这也是论文最关键的观点：如果一个领域已经有成熟的形式化库，单个语句的翻译会显得可行；但一旦进入 Mathlib 覆盖不足的数学分支、科学建模、硬件协议、软件系统或政策规范，真正缺失的就是底层理论库。自动形式化不能只做“最后一公里”的翻译，它必须参与“前九公里”的理论建构。

2. 为什么需要自动形式化

论文首先解释自动形式化本身为何重要。作者将其价值概括为四个方面。 第一，自动形式化可以合成神经定理证明器所需的训练数据。神经定理证明高度依赖大规模、高质量的形式化语料，而人类形式化成本极高。自动形式化可以从大量自然语言命题和证明中生成 informal-formal 平行数据，既包括把自然语言定理转成形式声明，也包括把非形式证明转成机器可检查的证明脚本。 第二，自动形式化可以加速理论验证与发现。形式化证明能发现隐藏错误，也能让后续扩展在可验证基础上进行。论文列举了多个跨领域项目：四色定理、Kepler 猜想、Odd Order 定理、Liquid Tensor、CompCert、CertiKOS、Vellvm、ISA-Formal 等。它们共同说明一点：重要形式化项目通常需要多年甚至十多年专家协作，瓶颈不是单个命题，而是完整理论与工程系统的建设。

第三，自动形式化可以为自然语言推理提供“落地”和“导向”。大模型的自然语言推理容易出现幻觉、遗漏条件或使用不存在的前提。把推理转成形式表示后，类型检查器、证明助手和模型检查器可以发现矛盾、未定义对象和非法推理步骤。同时，检查器反馈也可以作为自我修正信号，引导模型改进证明或规范。 第四，自动形式化是通用推理 AI 的重要组成部分。作者引用相关观点指出，未来的通用推理系统可能由两个部分协同工作：自动形式化器生成候选形式化表示，形式验证器筛选可证明、可检查的结果，再回到自然语言层面检查语义是否对齐。形式语言提供了一种可验证的中间层，使推理能力不完全依赖文本表面模式。

3. 为什么必须是理论级

论文进一步说明，为什么自动形式化不能停留在语句级。 首先，真实世界的形式化项目本质上就是理论级的。Kepler 猜想本身是一个单一陈述，但其形式化耗时 11 年，因为项目必须从头构建几何、拓扑、组合和计算验证所需的大量定义与引理。Liquid Tensor 实验也不是简单翻译一个定理，而是要先形式化凝聚数学中的大量前置结构。目标命题只是工程的可见端点，真正成本在于其依赖图。 其次，语句级形式化依赖已有形式理论。很多现有 benchmark 看起来进展很快，是因为 Lean Mathlib 等库已经为模型准备了丰富的定义、记号和引理。模型只需要把自然语言命题对齐到库中已有对象。但如果转向数值分析、硬件协议、政策合规或科学建模，成熟库往往不存在。此时 statement-level 方法会失效，因为它没有能力构建缺失的理论上下文。 第三，真正的新理论发现依赖新的抽象。数学史中的重大进展常常来自对知识结构的重组，例如群、环、域抽象了具体代数对象，范畴论从对象内部结构转向对象之间的态射，étale cohomology 为 Weil 猜想提供了新的几何工具。这些不是单个定理翻译，而是知识表示方式的改变。理论级自动形式化的长远目标，是在大规模形式化知识库中发现可复用结构、压缩知识表示，并产生新的抽象。 因此，作者把理论级自动形式化看成走向自动验证和理论发现的必经阶段。它既是形式方法的基础设施问题，也是 AI 推理系统的知识组织问题。

4. 三种替代观点及回应

论文随后讨论三个可能的反对意见。 第一种观点认为，自然语言推理已经足够强，为什么还需要形式化？近年来，大模型在数学竞赛和复杂推理任务上表现突出，非形式推理更灵活，也能利用海量文本数据。作者并不否认这一点，但指出自然语言推理缺乏可验证边界。形式化的价值不是取代自然语言，而是提供“检查点”：它可以捕获错误、约束推理、给出反馈，并帮助人类和 AI 识别含糊、遗漏或过强的假设。 第二种观点认为，真正重要的是 theorem proving，而不是 autoformalization。也就是说，只要定理已经形式化，神经定理证明器负责搜索证明即可。作者回应说，证明搜索确实关键，但它默认形式陈述和库已经存在。现实中，大量科学、工程和数学知识仍停留在自然语言、图表、代码、规范文档和领域专用语言中。没有自动形式化，定理证明器缺少可操作输入。 第三种观点认为，statement-level autoformalization 已经足够，因为它更简单、更容易评测。论文承认语句级任务有明确价值，尤其适合已有库覆盖良好的数学场景。但它无法解决新领域中的底层构建问题，也无法支持完整理论发现。作者认为，语句级方法可以成为理论级系统的一部分，但不能代表整个自动形式化目标。 这些回应共同指向一个判断：理论级自动形式化不是对现有路线的替代，而是把自然语言推理、语句翻译、证明搜索和形式库构建纳入同一系统目标。

5. 开放挑战一：语义等价检查

理论级自动形式化的第一个难点是等价检查。形式代码能够通过类型检查，并不意味着它忠实表达了原始自然语言含义；证明成功，也不意味着命题本身被正确翻译。一个过弱的形式化可能容易证明却没有覆盖原意；一个过强的形式化可能加入原文没有的假设；一个看似合理的定义可能在边界条件上偏离专家理解。 语义等价检查因此是自动形式化评测的核心问题。它要回答：自然语言陈述和形式化对象是否表达同一件事？在孤立语句中，这已经很难；在理论级系统中更难，因为等价不仅涉及单个声明，还涉及定义选择、依赖关系、抽象层级和后续可复用性。 论文指出，理想评测需要同时结合形式检查与语义对齐。形式检查保证代码可运行、证明可验证；语义对齐则需要专家判断、反例搜索、双向蕴含证明或更强的自动化语义比较机制。对理论级自动形式化而言，benchmark 不能只看“能否编译”，还要看库是否真实表达原始理论。

6. 开放挑战二：层级分解与抽象学习

理论级形式化需要把一段自然语言理论拆解成多层结构：哪些是公理，哪些是定义，哪些是辅助引理，哪些是目标定理，哪些证明策略值得抽象成工具。这个分解不是机械切句，而是要理解理论内部的依赖关系。 更进一步，系统还要学习抽象。人类形式化专家不会把每个事实都孤立编码，而会寻找可复用概念，让后续证明更短、更稳定、更容易维护。好的形式化库往往在抽象层面高度精炼：它不仅能证明当前目标，还能支持未来定理。自动系统如果只逐句翻译，就可能生成冗余、脆弱、难以复用的库。 这对大模型提出了比文本翻译更高的要求。它需要具备理论建模能力、依赖规划能力和库设计能力。作者认为，未来系统应当能够先规划理论骨架，再逐步生成定义、引理和证明，并在检查器反馈下重构库结构。

7. 开放挑战三：走出 Lean，进入低资源领域语言

当前自动形式化研究高度集中在 Lean 等主流数学证明助手上。这很自然，因为 Lean 生态活跃、Mathlib 丰富、数据较多。但真实世界中的形式化不只发生在 Lean 中。硬件验证、协议验证、软件安全、政策合规、访问控制和领域建模往往使用专门语言或工具链。 论文用多个例子展示这一挑战，包括自动定理证明语言中的 informal-to-formal 翻译、leader election 协议的形式化、硬件规范中的时序约束，以及政策语言 Cedar 中的 HIPAA 相关条款。它们的共同特点是：语料少、语义强、工具链分散、领域知识密集。模型不能简单套用 Lean/Mathlib 中学到的模式。

低资源 DSL 的问题尤其现实。许多工程验证语言没有大规模公开语料，也缺少自然语言与形式规范的平行数据。理论级自动形式化系统必须能在少样本、弱数据和强约束环境中工作。这要求模型具备更通用的语言迁移能力，也要求研究社区建立覆盖多种工具链的新 benchmark。

8. 开放挑战四：从文本走向多模态输入

很多真实理论和工程规范并不是纯文本。硬件协议包含时序图，系统设计包含架构图，数学和物理教材包含图形直觉，政策规范包含表格和层级条款。只处理自然语言，会丢失大量语义信息。 论文强调，理论级自动形式化需要多模态能力。以 AMBA AXI 这样的硬件协议为例，时序图中的信号关系、延迟约束和握手条件往往比文字更直接；以 Cedar policy 为例，自然语言法律条款需要被映射为可执行访问控制规则。系统必须同时理解文本、图表、形式语言和领域约束。

这也解释了为什么作者主张通用模型而不是只训练小型专用翻译器。多模态、跨领域、低资源和长依赖是同一问题的不同侧面。理论级自动形式化系统需要在自然语言、图像、代码、DSL 和证明助手之间建立稳定映射，而不是只在单一语料分布内拟合。

9. 三条推进路径

论文最后给出三条建议。 第一，构建带有可靠等价检查的理论级 benchmark。现有 benchmark 多数评测单个语句翻译，难以反映完整理论库构建能力。未来数据集应覆盖从公理、定义到引理、定理和证明的完整依赖链，并设计更强的语义等价验证机制。否则模型可能学会生成可编译但语义错误的形式化代码。 第二，优先发展通用模型，而不是过度依赖 fine-tuned specialist。专用模型在特定语言和库上可能表现很好，但容易过拟合语法与局部生态。理论级自动形式化需要跨语言、跨领域、多模态迁移能力，因此作者更看好具备广泛代码、数学、语言和视觉能力的通用模型，再配合工具反馈与检索机制完成形式化。 第三，探索用于理论发现的公共中间表示。作者设想一种 common intermediate representation，用来连接自然语言、形式语言、图表和图像，并能翻译到不同领域的形式系统。这个中间表示需要足够表达复杂理论，又能被验证器检查，还要便于嵌入到下游工具链。论文提到 Lean 具备成为候选表示的潜力，但更核心的问题是如何设计可迁移、可验证、可扩展的理论表示层。

这三条路径分别对应评测、模型和表示三个层面。没有理论级 benchmark，就无法衡量真实进展；没有通用模型，就难以跨越领域和模态；没有公共中间表示，就难以把分散知识组织成可复用的统一库。

10. 对 AI 推理研究的启示

这篇论文最值得关注的地方，是它把自动形式化放到了更大的 AI 推理版图中。大模型推理的一个核心问题是：系统如何知道自己真的推对了？自然语言链式思考可以提高可解释性，但不能保证正确性；外部工具可以提供反馈，但工具输入本身需要被正确建模。自动形式化正好位于二者之间：它把非形式知识转成可检查对象，让推理进入可验证空间。 如果这一方向成熟，未来的 AI 系统可能不只是回答数学题，而是能把一篇论文、一份规范、一套协议或一个科学模型逐步转成形式化库，然后利用证明助手、模型检查器或 SMT 求解器进行验证和发现。这样的系统将同时具备阅读、建模、抽象、证明和重构能力。 当然，这也意味着研究难度会显著上升。理论级自动形式化不是一个单一 NLP 任务，而是长上下文理解、程序合成、形式验证、库设计、多模态理解和人机协同的交叉问题。它需要更强的数据集、更可靠的评测协议，也需要形式方法社区与机器学习社区更深的协作。

总结

《Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases》提出了一个清晰而重要的研究判断：自动形式化的下一步，不应只围绕孤立命题翻译，而应走向完整理论库的自动构建。 论文将这一转变拆解为四个层面：为什么自动形式化重要，为什么必须进入理论级，现有替代路线为何不足，以及未来还缺哪些关键能力。它强调，真实形式化工程的成本主要来自公理、定义、引理、证明基础设施和依赖关系，而不是最终命题本身。要让 AI 真正参与数学、科学、软件和硬件验证，就必须让系统具备构建理论上下文的能力。 对研究社区而言，这篇论文更像是一份路线图：从 statement-level 走向 theory-level，从 Lean 中的成熟库走向低资源 DSL，从纯文本走向多模态规范，从可编译代码走向语义等价，从局部翻译走向统一形式化知识库。自动形式化如果要成为可信 AI 推理的基础设施，这一步几乎不可避免。