Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases

背景

自动形式化（Autoformalization）旨在将非形式化的自然语言转换为机器可验证的形式语言。长期以来，该领域的研究主要聚焦于孤立的数学或逻辑语句——例如单个定理、单个定义——并尝试将其翻译成形式化证明系统（如 Lean、Coq、Isabelle）中的代码。然而，真正的数学知识体系并非由孤立语句构成：一个定理的陈述往往依赖于一整套公理、定义、引理以及它们之间复杂的相互依赖关系。现实中的形式化工程，如数学基础库或大型定理证明项目，本质上是“理论级”的：在目标定理能够被表述之前，必须已经存在一个完整的理论网络。现有自动形式化方法在处理这种全局结构时存在明显短板，因此 arXiv 上的这篇立场文章（提交于 2026 年 7 月 14 日，分类 cs.AI）正式提出了“理论级自动形式化”的概念，呼吁将研究重心从单语句转向完整理论的结构化形式化。

核心内容

本文是一篇立场论文（position paper），核心论点是：自动形式化应当从单语句级别提升到理论级别（theory-level），即形式化过程应产出包含所有公理、定义、引理及其相互依赖关系的结构化形式化库，而不仅仅是孤立定理的翻译。作者通过以下逻辑展开论述：

1. 界定“理论级自动形式化”：与传统自动形式化聚焦于单个陈述不同，理论级自动形式化要求系统能够处理整个理论——包括理论之间的继承、依赖、模块化组织等。这类似于软件工程中将代码重构为可复用的库，而非仅关注单个函数。

2. 论证这一转变的重要性：现实中的数学和科学推理总是在某个理论框架内进行。如果在形式化目标定理之前没有先形式化其依赖的底层理论，那么即使单个语句翻译正确，也无法在形式化系统中实现真正的可验证性。理论级自动形式化有望弥合非形式化数学与形式化知识库之间的鸿沟，使得大规模、自动化的形式化成为可能。

3. 回应替代观点：作者承认可能存在反对意见，例如“逐语句翻译已足够，依赖关系可后续手工添加”或“完全理论级形式化过于困难”。文章逐一反驳这些观点，指出手工添加依赖关系在实践中不可扩展，而放弃理论级结构会导致形式化知识库碎片化、不可复用。

4. 指出开放性挑战：包括如何自动识别非形式化文本中的理论边界、如何建模隐式依赖（如换元法、约定俗成的记号）、如何保证形式化库的内部一致性、以及如何与现有形式化系统（如 Mathlib、UniMath）对接等。

5. 提出三条有前景的路径（论文未在摘要中详述，但提及“three promising paths forward”），包括：

   • 利用大语言模型（LLM）生成理论骨架，再通过交互式证明助手填充细节；
   • 设计一种中间表示（intermediate representation），既能捕获非形式化理论的结构，又能映射到多个形式化系统；
   • 构建渐进式自动形式化流水线，先翻译理论节点，再自动推理其间的依赖网络。

最后，论文提及一份关于自动形式化领域现状的调研报告（提供了链接），供读者参考。

关键要点

• 核心主张：自动形式化必须从单语句级别（statement-level）拓展到理论级别（theory-level），后者要求形式化整个理论网络，包括公理、定义、引理及其依赖关系。
• 本质差异：单语句形式化只做“点翻译”，而理论级形式化产出“结构化形式化库”，可被多次复用和按需扩展。
• 现实驱动力：现有形式化工程项目（如数学定理证明、软件验证）天然需要理论级支持；若缺乏，自动化形式化将始终停留在玩具例子层面。
• 反对观点反驳：作者驳斥“先形式化语句，手工补依赖”的可行性和“理论级太难需放弃”的悲观论，认为前者不具规模化，后者可通过渐进方法克服。
• 开放挑战：
  • 从自然语言文本中自动识别理论边界和结构；
  • 处理隐式约定和上下文依赖（如符号重载、构造主义 vs 经典逻辑选择）；
  • 保证形式化库内部一致性和相容性；
  • 与现有形式化基础设施（如 Lean 的 Mathlib）互操作。
• 三条前行路径（论文内详）：
  1. LLM 辅助生成理论骨架，经交互式验证完善；
  2. 设计独立于具体证明系统的理论表示中间件；
  3. 构建依赖驱动的渐进式形式化流程。
• 附带资源：作者提供了一份当前自动形式化领域调研的 URL，供进一步阅读。

意义与影响

这篇立场文章标志着自动形式化领域的一个重要转向。此前，大多数研究（如 GPT-f、Draft-Sketch-Prove 等）集中在单句定理的翻译，对数学知识体系的“生态性”关注不足。理论级自动形式化的提出，将形式化研究的视野从“翻译”扩展到“知识工程”，直接呼应了数学库维护、验证软件栈等现实需求。

具体意义包括：

• 推动规模化形式化：一旦理论级自动化成熟，非形式化数学论文、教科书甚至软件规范可以批量转换为结构化形式化知识库，极大降低人工形式化的门槛。
• 促进不同形式化系统之间的互操作：通过独立的理论表示中间件，可以将同一非形式化理论同时输出到 Lean、Coq、Isabelle 等系统，打破“形式化孤岛”。
• 影响 AI for Math 方向：自动形式化是大语言模型在数学推理领域的重要应用场景。理论级版本要求模型不仅理解局部语法，还要掌握整体知识结构，这对模型的理解力、规划力和一致性推理提出了更高挑战，可能催生新的评估基准和方法。
• 为未来数学基础设施奠基：若理论级自动形式化得以实现，未来数学研究可能形成“非形式化撰写 → 自动形式化入库 → 机器验证和推理”的工作流，数学知识将成为可被计算机直接操作的结构化资源。

当然，该方向仍面临巨大困难：依赖关系的隐式性、语境的跨文档性、形式化语言本身的表达能力限制等。但本文至少为领域指明了前进方向，并给出了可落地的路线图。学界和工业界（如 OpenAI 的数学推理、Lean 社区）很可能就此展开新一轮探索。