超越图书馆：一种用于自动形式化研究数学的智能体框架

# 超越库：一种用于自动形式化研究数学的智能体框架 来源: https://arxiv.org/html/2606.31134 Arshia Soltani Moakhar asoltan3@umd\.edu & Iman Gholami igholami@umd\.edu & Max Springer maxspringer@princeton\.edu Mahdi JafariRaviz mahdij@umd\.edu & MohammadTaghi Hajiaghayi hajiagha@cs\.umd\.edu ###### 摘要 尽管大语言模型（LLMs）在数学推理方面展现了卓越的能力，但它们经常会产生人类难以察觉的细微错误。像 Lean 4 这样的形式化数学语言提供了机械化的证明检查，这强烈激发了自动形式化的需求：将自然语言数学自动翻译成可验证的代码。最近的趋势表明，针对标准编程进行了高度优化的通用 LLMs，现在已超越了专门针对 Lean 进行微调的较小模型。利用这一转变，我们介绍了一个由通用编码 LLMs 驱动的智能体自动形式化框架。我们系统的核心是一个编排器，它管理着一个专为研究级数学量身定制的多智能体流水线。由于前沿研究经常依赖现有库（如 Mathlib）范围之外的概念，我们的系统会动态扩展必要的类型定义，并通过一种新颖的辅助引理技术对其进行验证，然后再形式化主要定理。我们将我们的方法应用于 PutnamBench，为随机抽样的 32 个问题生成了机器验证的 Lean 证明。此外，我们评估了系统在处理 ACM 计算理论研讨会（STOC）的五篇论文时的表现，这些论文涵盖组合数学、通信复杂性、机制设计和学习理论，成功形式化了它们的主要定理，并与人类专家一起验证了生成的形式化结果；对于所有五篇论文，我们也形式化了陈述及其证明，值得注意的是，其中两篇论文的证明除了 Lean 的内核外没有使用任何公理。我们所有的形式化结果均可在 https://beyondthelibrary.github.io/formal_arxiv/ 获取。

## 1 引言

随着 AI 系统在为现实世界的数学定理生成证明方面变得越来越有能力[1 (https://arxiv.org/html/2606.31134#bib.bib1)]，证明验证的负担已成为一个主要瓶颈。大语言模型（LLMs）往往会产生与典型人类错误截然不同的细微逻辑错误[2 (https://arxiv.org/html/2606.31134#bib.bib2)]，使得数学家的人工验证既耗时又异常困难。这一挑战强调了自动化验证的关键需求，这将使研究人员能够大规模地严格测试和验证生成的证明。形式化数学语言，如 Lean 4[3 (https://arxiv.org/html/2606.31134#bib.bib3)]，目前为这类机械化检查提供了最强大的环境。因此，将非形式化推理自动翻译成这些严格、可验证的语言，是 AI 辅助数学未来的关键一步。

自动形式化意味着将非形式化的数学概念翻译成机器可验证的代码，例如 Lean 4。这个流水线自然分为两个不同的任务：形式化定理的陈述和形式化定理的证明。一旦陈述在形式语言中安全建立，任何附带证明的正确性都可以被机械化验证[3 (https://arxiv.org/html/2606.31134#bib.bib3)]。然而，与证明形式化不同，证明形式化受益于编译器的直接反馈，而陈述形式化则缺乏机械化的客观事实。由于无法自动验证翻译后的陈述是否与其自然语言源完全一致，陈述自动形式化面临着独特且重大的挑战。¹¹ 这是因为最初的定理陈述是自然语言形式的，因此无法被机械化处理。

我们提出了一种自动形式化设置，其中编排器管理两个流水线的执行：一个形式化论文的陈述，另一个形式化论文的证明（图1 (https://arxiv.org/html/2606.31134#S1.F1)）。我们的设置克服了单智能体[4 (https://arxiv.org/html/2606.31134#bib.bib4),5 (https://arxiv.org/html/2606.31134#bib.bib5),6 (https://arxiv.org/html/2606.31134#bib.bib6)]和传统固定流水线[7 (https://arxiv.org/html/2606.31134#bib.bib7),8 (https://arxiv.org/html/2606.31134#bib.bib8),9 (https://arxiv.org/html/2606.31134#bib.bib9),10 (https://arxiv.org/html/2606.31134#bib.bib10),11 (https://arxiv.org/html/2606.31134#bib.bib11)]的局限性。在单智能体设置中，失败的证明尝试和编译错误会迅速充斥上下文窗口，削弱长期推理能力；我们的系统通过将子任务委派给子智能体来规避这一点，从而为编排器保留用于高级策略的上下文。我们的系统也优于固定流水线模型[7 (https://arxiv.org/html/2606.31134#bib.bib7),8 (https://arxiv.org/html/2606.31134#bib.bib8),9 (https://arxiv.org/html/2606.31134#bib.bib9),10 (https://arxiv.org/html/2606.31134#bib.bib10),11 (https://arxiv.org/html/2606.31134#bib.bib11)]，因为它们以刚性的顺序处理数学陈述，并且无法在早期步骤出错时回溯。相比之下，我们的编排器可以动态地即时回溯到先前的流水线状态，避免了刚性流水线常见的硬性失败。最后，这种灵活的设计无缝支持人在回路交互，允许研究人员在流程中途注入领域专业知识或纠正逻辑，而无需强制重新启动整个流水线。

见图注 图1：我们智能体系统的概览。用户通过 Claude Code 界面（左侧）进行交互，以 LaTeX 和 PDF 形式提供论文以及提示，系统返回 Lean 代码。编排器驱动两个流水线。*形式化* 流水线（顶部，第2.1节 (https://arxiv.org/html/2606.31134#S2.SS1)）提取主定理，然后遍历所需的类型，规划并形式化每个类型及其辅助引理，最后形式化定理陈述。*证明* 流水线（底部，第2.2节 (https://arxiv.org/html/2606.31134#S2.SS2)）起草一个自然语言证明，将其细节化并分解为引理，形式化并证明这些引理，最终形成一个自包含的 Lean 证明。标记有“*”的阶段会扩展为它们自己的子流水线。绿色徽章表示某个阶段可用的 MCP 工具。虚线箭头显示了两个控制循环：形式化器遍历类型，证明器递归处理每个子引理。该流水线不是静态的：编排器可以重新排序阶段并在它们之间打开反馈桥梁。

在研究级数学和计算机科学自动形式化中，一个主要瓶颈是形式化库的有限范围。由于像 Mathlib[12 (https://arxiv.org/html/2606.31134#bib.bib12)] 这样的库在许多已建立领域缺乏覆盖，因此尝试直接在不受支持的领域翻译复杂定理通常会失败。为了弥补这一差距，我们的架构引入了一种“类型优先”的形式化范式。在处理主定理之前，编排器会明确定义任何缺失的领域特定概念，以构建必要的数学词汇。通过系统地克服现有库的限制，这种方法使得成功形式化更广泛的研究论文成为可能。

如果底层定义是错误的，仅定义新的数学词汇是不够的。为了确保这些新形式化类型的忠实性和可用性，我们引入了一种辅助引理技术，该技术首先生成与一个新类型相关的几个定理，然后尝试证明它们。如果证明器失败，则表明形式化的类型要么不正确，要么形式化得不好，使得证明变得不必要的困难。概念上，这种方法类似于软件工程中的单元测试[13 (https://arxiv.org/html/2606.31134#bib.bib13),14 (https://arxiv.org/html/2606.31134#bib.bib14)]。正如单元测试验证程序的基本组件一样，辅助引理验证形式化类型的正确性，这些类型是形式化的构建块。最终，缺失的假设或糟糕的形式化使得辅助引理无法证明，这允许编排器在继续前进之前重试形式化。

我们整合了三种既定技术以进一步增强流水线的鲁棒性。首先，为了验证主定理的陈述，我们采用反向翻译[15 (https://arxiv.org/html/2606.31134#bib.bib15)]：智能体将生成的 Lean 代码翻译回自然语言，以检测与原始文本的结构性差异。其次，为了简化证明生成过程，一个专门的智能体将复杂证明分解为更小的、易于管理的引理[16 (https://arxiv.org/html/2606.31134#bib.bib16)]。最后，受 MerLean[7 (https://arxiv.org/html/2606.31134#bib.bib7)] 启发，我们不对先前工作的证明进行形式化。相反，我们将这些先前的结果声明为公理，将形式化工作严格限制在论文的核心贡献上。

除了形式化陈述，我们的系统还包括一个完整的证明形式化流水线，能够生成机器验证的证明。它递归地将定理分解为引理，并且在每个节点，从其子引理的陈述出发证明该节点，然后再递归进入子引理，仅将明确标记的先前工作结果作为公理接受。在研究论文上端到端运行后，该流水线为 ACM 计算理论研讨会（STOC）的五篇论文生成了机器验证的证明，其中两篇除了 Lean 的内核外没有使用任何公理。由于它根据论文的字面定义检查每一步，它甚至发现了一篇论文已发表证明中的一个漏洞[17 (https://arxiv.org/html/2606.31134#bib.bib17)]。

为了评估我们的证明形式化流水线，我们在 PutnamBench[18 (https://arxiv.org/html/2606.31134#bib.bib18)] 上端到端运行了它，其形式化的 Lean 语句是给定的。对于每个问题，流水线自己的自然语言证明器仅从陈述生成一个非形式化证明，然后流水线将其细化、分解并形式化为一个机器验证的 Lean 证明；我们没有手工准备任何证明，并且禁用了互联网访问，因此没有检索任何内容。我们在 32 个随机抽样的问题上进行了测试，我们的流水线证明了所有这些问题。这使得整个数据集的准确率下界达到 91.3%，置信水平大于 95%。值得注意的是，这种方法仅使用标准的 200 美元软件订阅就超越了最先进的专门模型，平均每个问题的运营成本约为 5 美元。

我们还针对 STOC 2025 的论文进行了研究。作为理论计算机科学的顶级会议，STOC 以其对数学严谨性的极高要求而著称。我们形式化了五篇 STOC 论文[17 (https://arxiv.org/html/2606.31134#bib.bib17),19 (https://arxiv.org/html/2606.31134#bib.bib19),20 (https://arxiv.org/html/2606.31134#bib.bib20),21 (https://arxiv.org/html/2606.31134#bib.bib21),22 (https://arxiv.org/html/2606.31134#bib.bib22)] 的主要定理，并通过专家人工评审确认了这些翻译的准确性。为了评估我们的端到端证明形式化流水线，我们随后在这些形式化结果上运行了我们的证明器。Lean 编译器验证了代码的句法和逻辑正确性，而人类专家则验证了形式化结果忠实地捕捉了原始的证明策略。值得注意的是，其中两篇论文[19 (https://arxiv.org/html/2606.31134#bib.bib19),20 (https://arxiv.org/html/2606.31134#bib.bib20)] 的证明除了 Lean 的标准内核外没有使用任何公理，我们的流水线甚至从头重新证明了引用的先前结果，而其他的则需要承认众所周知的外部定理作为显式公理。

总而言之，本工作做出了以下关键贡献：

- • 我们引入了一种自动形式化的方法论转变，通过直接将软件工程原则（如面向对象的类型分解和单元测试风格的辅助引理验证）应用于数学证明。
- • 我们引入了一个多智能体自动形式化系统，利用现代编码框架的动态、非线性能力。
- • 我们通过为 PutnamBench 问题和研究级数学生成机器验证的证明，成功形式化了 STOC 出版物的主要定理，从而实证验证了我们的方法。
- • 我们将陈述形式化与一个递归的证明形式化流水线相结合，该流水线产生了研究级定理的机器验证证明，其中两个 STOC 结果除了 Lean 的内核外没有使用任何公理，并且该流水线发现了一个计算机验证的漏洞，存在于一个已发表的 STOC 证明中。
- • 我们通过提供一个极具成本效益的形式化工具，显著降低了自动化定理证明的入门门槛，该工具不需要本地 GPU。

## 2 自动形式化设计

在这一节中，我们介绍我们的智能体自动形式化流水线，旨在将复杂的数学文档（从孤立定理到研究论文）翻译成 Lean。我们的流水线有三个主要输出：从输入论文中提取的主定理，形式化它所需的类型和相应引理，以及形式化结果本身。为了实现这一目标，我们拥有由单个 *编排器* 管理的多种智能体，即 Claude Code 会话。这个管理器负责确保步骤正确完成，如果检测到失败，它会回滚到先前状态，并向相应的智能体提供反馈。尽管流水线作为一系列固定的阶段呈现给编排器，但编排器保留根据需要对执行顺序进行调整的全部自由。这在结构化指导和处理研究级形式化中意外挑战所需的灵活性之间取得了平衡（图1 (https://arxiv.org/html/2606.31134#S1.F1)）。

### 2.1 陈述形式化

陈述形式化流水线如图1 (https://arxiv.org/html/2606.31134#S1.F1) 的上半部分所示。系统由用户通过自然语言提示调用，要求编排器形式化提供的论文或问题；我们使用的确切提示在附录 D (https://arxiv.org/html/2606.31134#A4) 中给出。首先，提取器从论文的 PDF 和 LaTeX 源中找到主定理。它捕获理解定理所需的所有定义和假设，而不仅仅是定理陈述本身。然后，我们的类型规划器确定形式化所需但超出 Lean 标准库范围的类型，生成一个表示 Mathlib 中缺失的基本概念的 *类型计划*。编排器随后按照类型在依赖图中的顺序遍历计划中的类型。在每次迭代中，一个引理规划器智能体首先识别与当前类型相关的众所周知的性质和引理，这些引理用于验证其形式化的正确性和通用性。这些引理陈述尽可能保持通用，并不针对当前问题定制。编排器然后为当前类型生成 k 个类型形式化器智能体，每个智能体负责将类型及其引理从自然语言翻译成 Lean，尝试证明相关的辅助引理，并用忠实性评判智能体（第2.1.3节 (https://arxiv.org/html/2606.31134#S2.SS1.SSS3)）进行验证。一旦这些并行尝试针对该类型结束，拍卖师使用最佳选择策略评估候选者。拍卖师对生成的形式化结果进行排序