理论级别的自动形式化：从孤立陈述到统一形式知识库

# 从孤立语句到统一形式化知识库  
来源：https://arxiv.org/html/2607.13292  

## 理论级自动形式化：从孤立语句到统一形式化知识库  

Mike He，Zhaoyu Li，Zixuan Yi，Sharad Malik，Aarti Gupta，Xujie Si，Osbert Bastani  

###### 摘要  

自动形式化（Autoformalization）将非正式的自然语言翻译成形式化的、机器可验证的语言。虽然大多数工作聚焦于孤立语句，但实际的形式化工作本质上是理论层面的：在目标定理可被陈述之前，就需要构建一整套公理、定义和引理网络。在这篇立场论文中，我们主张理论级自动形式化：将完整的理论（包括其所有相互依赖关系）形式化为结构化的库。我们探讨了这一转变的重要性，回应了替代观点，指出了开放挑战，并提出了三条有前景的前进路径。我们的自动形式化调查可在 https://github.com/marcusm117/Awesome-Autoformalization 获取。  

机器学习、自动形式化、ICML  

## 1 引言  

图1：本篇立场论文概览。我们通过探讨其重要性（第2节）、回应替代观点（第3节）、识别开放挑战（第4节）和提出前进路径（第5节），来论证理论级自动形式化。  

我们定义**理论级自动形式化**为：在给定范围内自动形式化整个理论上下文的任务，包括公理、定义、记法、示例、引理、定理、证明、策略以及它们之间的所有相互依赖关系，形成一个连贯的形式化库。如图2（第2节图2）中的“理论级自动形式化塔”所示，即使形式化像勾股定理这样的单一目标定理，也需要首先构建多层公理原语、衍生定义和证明基础设施。这与语句级自动形式化形成对比，后者孤立地翻译单个定理，并隐式依赖像Lean Mathlib（Mathlib社区，2020）这样的形式化理论上下文。对于这些库尚未支持的领域，主要工作正是构建那些缺失的理论上下文。这种转变的必要性从现实世界的形式化工作中可见一斑（表1）。开普勒猜想是一个单一陈述，但其形式化耗费了11年时间，用于构建整个定义和支持引理网络（Hales等，2015）。AI辅助方法可以大大加速这类工作：素数定理的人工形式化花了1.5年（Avigad等，2006），而其定量改进的AI辅助形式化仅用了3周（Math Inc.，2025b）。理论级自动形式化是必要的，因为语句隐式要求周围理论已经被形式化。最重要的是，变革性的新结果依赖于新的抽象，这些抽象重组并压缩了我们整个知识库，使得之前无法表述的证明成为可能。如图1所示，我们探讨了理论级自动形式化的重要性（第2节），并回应了替代观点（第3节）。然后我们识别了评估、分解、低资源领域特定语言和多模态输入等方面的开放挑战（第4节），并提出了前进路径（第5节）。  

## 2 重要性：为什么需要理论级自动形式化？  

### 2.1 为什么需要自动形式化？  

a. 合成神经定理证明器的训练数据。  
神经定理证明的进展高度依赖于大规模、高质量形式化语料库的可用性（Xin等，2024；Lin等，2025a）。自动形式化是从大量非正式语句和证明中合成高质量的非正式-形式化并行数据的最可扩展方式。它解决了两个互补的瓶颈：（i）**语句自动形式化**将自然语言定理和猜想转化为形式化声明，扩大了尚未形式化的有趣或具有挑战性的陈述的覆盖范围；（ii）**证明自动形式化**将非正式证明转化为机器可检查的证明脚本，直接为定理证明产生高质量数据。  

表1：各领域代表性的形式化项目，需要人类专家大量时间和精力。  

| 领域 | 形式化项目 | 验证工具 | 开始 | 持续时间 |
|------|------------|----------|------|----------|
| 数学 | 四色定理（Gonthier，2007） | Coq¹（Barras等，1997） | 2000 | 5年 |
|      | 开普勒猜想（Hales等，2015） | HOL Light²（Harrison，2025） | 2003 | 11年 |
|      | 奇阶定理（Gonthier等，2013） | Coq | 2006 | 6年 |
|      | 液体张量实验（Commelin等，2022） | Lean | 2020 | 1.5年 |
| 科学 | 化学物理（Bobbin等，2023） | Lean | 2022 | 1年 |
|      | 应用偏微分方程（Deniz，2024） | HOL Light | 2022 | 进行中 |
| 软件 | CompCert（Leroy，2009） | Coq | 2005 | 进行中 |
|      | CertiKOS（Shao和Ford，2010） | Coq | 2010 | 进行中 |
|      | Vellvm（Zhao等，2012） | Coq | 2012 | 进行中 |
| 硬件 | ISA-Formal（Reid等，2016） | Verilog模型检查器 | 2011 | 5年 |
|      | CORE-V-Verif（OpenHW Group，2019） | UVM（IEEE，2020） | 2019 | 进行中 |

¹Coq自2025年起更名为Rocq，参见 https://rocq-prover.org/。  
²HOL Light是主要证明助手；Isabelle（Nipkow等，2002）也用于驯服图分类。  

b. 加速理论验证与发现。  
重要定理和关键工程系统的形式化不仅有助于识别潜在错误，还能促进经过认证的扩展和未来的理论发现。表1调查了四个领域（数学、科学、软件、硬件）中有代表性的形式化工作。共同瓶颈是这些项目需要多年来甚至几十年（Leroy，2009）的团队协作努力，由领域专家参与。因此，自动形式化成为加速此类过程的有前景方式。  

c. 为自然语言推理提供基础与指导。  
LLM的自然语言推理容易出现幻觉和事实不一致（Ji等，2023）。自动形式化通过将非正式论证转化为形式可检查的表示来提高可靠性（Yang等，2022；Zhou等，2024），这提供了两个互补的益处：（i）**基础化**通过发现矛盾、类型错误的定义或不存在的假设来排除错误步骤；（ii）**指导**提供检查器反馈作为指导信号，实现自我修正循环。自动形式化也有益于人类非正式推理，因为论证中经常省略常规步骤、忽略微妙情况或携带不必要的假设（Autexier和Fiedler，2006）。自动形式化帮助人类研究人员识别模糊步骤和冗余前提，从而产生更严谨和优雅的论证。此外，自动形式化可以降低使用证明助手的门槛，使领域专家更接近其自然数学语言，而自动形式化器处理大部分形式语法和记账工作（Shulman，2024）。  

d. 推进具备通用推理能力的AI。  
Szegedy（2020）设想了一个由自动形式化驱动的通用推理AI系统：自动形式化器生成候选形式化；推理器利用形式验证器只保留正确证明的语句，然后检查与非正式输入的语义对齐。经验上，模型性能在数学、编程和其他推理基准上高度相关（Emberson和Edelman，2026），表明存在共享的基本能力。在训练方面，Pang等（2025）证明，仅使用数学的初始RL阶段，配合可验证奖励，可以激发出跨领域转移的推理行为，无需专门的奖励模型，从而带来一致的多领域收益。  

图2：以形式化系统E（Avigad等，2009）为例的“理论级自动形式化塔”，该系统由Murphy等（2024）在Lean中实现了欧几里得几何。  

### 2.2 为什么需要理论级自动形式化？  

如图2（第2节图2）中的“理论级自动形式化塔”所示，要形式化带证明的目标定理，我们必须从第0层的公理定义开始：原始种类如Points，以及受公理约束的原始关系如sameSide。基于原始定义，我们可以在第1层构建更复杂的衍生定义，涉及归纳类型如Angle，以及组合多个原始概念的复合关系如formTriangle。在定义之上，第2层提供工具基础设施：使形式语句可读的记法；促进后续证明的引理和策略。只有所有这些层就绪，我们才能在第3层陈述并证明目标定理。当前最佳方法在第3层的语句上达到71.4%（Min等，2026），假设第0-2层已由人类形式化。然而，目前没有方法尝试自动形式化这些较低层。因此，理论级自动形式化是一项系统工程任务，旨在构建一个连贯的、相互依赖的形式化组件库。它对于以下三个原因是必要且迫切的：  

a. 实际的形式化项目本质上是理论级的。  
第2.1节中调查的现实世界形式化工作，从四色定理到CertiKOS，并非孤立的语句翻译，而是大规模形式化理论构建。开普勒猜想确实是一个单一陈述，但它花费了11年时间从头构建整个定义和支持引理网络（Hales等，2015）。类似地，液体张量实验需要在目标定理可被陈述之前形式化相当部分的凝聚态数学（Commelin等，2022）。因此，理论级自动形式化对于减少专家劳动的主要成本是必要的。  

b. 语句形式化需要形式化理论。  
许多现有的语句自动形式化任务之所以看似可行，是因为繁重的工作由证明助手和标准库的成熟形式化环境隐式完成。现代证明助手如Lean（Moura和Ullrich，2021）提供了富有表现力的基础和强大的元编程支持，而像Mathlib（Mathlib社区，2020）这样的大型人工形式化标准库已经提供了大量可直接重用的定义、记法和引理。如果我们想形式化Mathlib支持不佳的领域（如数值分析）中的语句，那么主要工作正是构建缺失的形式化理论上下文。即使对于标准本科数学，Lean Mathlib中仍然缺少一些子理论（Lean社区，2026）。因此，将语句自动形式化扩展到新领域需要理论级能力。  

c. 新的理论发现需要新的抽象。  
重要的理论发现（即困难定理的证明）通常需要新的抽象，这些抽象重构并压缩我们对知识的表示，使得之前无法陈述的论证成为可能。抽象代数引入了群、环、域，它们抽象掉了整数或多项式等具体结构，专注于分析对称性。这一转变导致了伽罗瓦关于一般五次方程不可根式求解的证明，该结论依赖于认识到对称群S5不可解。范畴论抽象掉了内部结构，专注于对象之间的态射。格罗滕迪克发明的平展上同调（Milne，2013）——通过用平展映射范畴替换开集范畴，为有限域上的代数簇定义更丰富的上同调理论——最终促成了德利涅对韦伊猜想的证明（Deligne，1980），以几何方式解决了数论问题。这些例子表明，理论进步依赖于创造新的抽象，这些抽象压缩知识并解锁更一般的结果。在来自所有数学、科学和工程的理论级自动形式化之后，我们将拥有一个庞大的形式化知识代码库。重构这个代码库使我们能够识别各个领域的共同结构和模式，将其抽象出来，压缩我们的知识库，并最终利用这些新抽象来证明新结果。  

总之，理论级自动形式化是迈向能够自动化现实世界验证和真正理论发现的AI系统的必然步骤。  

## 3 替代观点：为什么不是其他方式？  

### 3.1 观点1：非正式推理优于形式推理。  

自OpenAI o1（OpenAI，2024）和DeepSeek-R1（Guo等，2025）发布以来，非正式自然语言推理取得了显著进展。IMO 2025的结果（Luong和Lockhart，2025；Wei，2025）进一步表明，单独的非正式推理就可以解决困难的竞赛问题，而无需形式验证。实际上，非正式推理也更灵活：它不需要专门的语法，也不受领域限制，因此相比形式推理能受益于大规模训练数据。  

反驳。首先，如第2.1节所讨论，形式化方法为AI和人类