LeanFlow：工作流驱动的Lean自动形式化案例研究

# LeanFlow: 一种工作流驱动的精益自动形式化案例研究
来源: https://arxiv.org/html/2607.20503

###### 摘要

我们介绍并评估了 LeanFlow，这是一个专门用于将数学论文转化为可构建的 Lean 项目的 LLM 智能体系统。最近的验证器在环系统表明，可以生成大规模的形式化产物，但仍不清楚哪些运行时机制会影响文档到项目形式化的完成性、可审计性或效率。我们通过对数论和测度论中两篇先前未形式化的数学论文进行案例研究来探究这一问题，使用 Kimi-K2.6 和 GPT-5.5 进行模型、证明工作流和工具集的消融实验；我们报告了任务结果、API 调用次数、输入令牌数和输出令牌数。使用 Kimi-K2.6 时，完整工作流在 2000 次调用预算内完成了两个文档级项目，而无队列变体则达到了预算上限；使用 GPT-5.5 时，所有文档级变体均完成，完整工作流在两个源上具有最低或并列最低的输入令牌成本。作为补充校准，LeanFlow 在 RLM25 的 PFR 子集上达到 75.7% 的 BEq+，并在我们的 GPT-5.5 运行中解决了 ICML 2026 AI for Math TCS 挑战的所有五个项目。

自动形式化, 定理证明, Lean, LLM 智能体, 文档级形式化, 证明修复

## 1 引言

自动形式化正从孤立的定理翻译转向将整个数学源转化为 Lean 项目。早期的语言模型形式化工作侧重于将单独的自然语言语句翻译成证明助手的语法（Wu 等人，2022 (https://arxiv.org/html/2607.20503#bib.bib13)），许多定理证明基准仍要求模型一次证明一个给定的形式化语句（Zheng 等人，2022 (https://arxiv.org/html/2607.20503#bib.bib10)；Azerbayev 等人，2023 (https://arxiv.org/html/2607.20503#bib.bib14)）。文档级智能体面临一个不同的问题：它必须将数学散文、TeX 结构、参考文献、定义和证明转化为可构建的 Lean 项目，同时保留预期的陈述并管理一系列依赖的证明义务。M2F（Wang 等人，2026 (https://arxiv.org/html/2607.20503#bib.bib1)）以及最近的教科书或项目级系统（Gloeckle 等人，2026 (https://arxiv.org/html/2607.20503#bib.bib30)；Math, Inc.，2025 (https://arxiv.org/html/2607.20503#bib.bib20)；Hariharan 等人，2026 (https://arxiv.org/html/2607.20503#bib.bib32)；Tsoukalas 等人，2026 (https://arxiv.org/html/2607.20503#bib.bib31)）表明，验证器在环形式化可以生成大型 Lean 制品；我们研究运行时的哪些部分有助于智能体保持源声明不变并完成由此产生的证明工作。

受这种文档级场景的启发，我们引入 LeanFlow 作为一个 Lean 特定运行时，它将对数学的编辑与工作流控制分离开来。它首先执行确定性的源预检：运行时解析输入文档，提取或记录源块、标签、引用、PDF、图表和支持文件，并在模型开始前拒绝不明确的 TeX 根目录。然后，形式化器构建一个蓝图，即一个项目本地源映射，将源跨度链接到计划的 Lean 声明、依赖项、证明笔记和记录的范围更改。在证明搜索之前，一个语句/源门控检查生成的声明类型是否仍然匹配原始源声明。在证明过程中，一个程序化的工作流管理器拥有定理队列、失败尝试记忆、重试预算、验证记录、日志和检查点。模型提出编辑和辅助引理，而管理器一次分配一个目标，并且仅在外部 Lean 验证接受编辑后才前进。这种分离在我们的实验中，在两种模型设置下产生了不同的好处。对于 Kimi-K2.6（Moonshot AI，2026 (https://arxiv.org/html/2607.20503#bib.bib3)），工作流控制在我们的两次文档级运行中起决定性作用：完整工作流完成了两个源，而无队列变体用尽了调用预算。对于 GPT-5.5，所有文档级变体都完成了，因此观察到的好处不是二进制成功差异；相同的结构反而提高了令牌效率并为证明工作保留了明确的审计线索。

LeanFlow 还引入了 LeanProbe（https://github.com/epfl-lara/LeanProbe），这是一个基于 LeanInteract（Poiroux 等人，2025b (https://arxiv.org/html/2607.20503#bib.bib2)）构建的缓存同文件验证器，用于重复的证明修复检查。LeanProbe 为证明智能体提供低延迟的诊断和证明状态反馈，同时最终接受仍由标准的 Lean/Lake 检查负责。在表 6 (https://arxiv.org/html/2607.20503#S5.T6) 总结的连续同文件基准测试中，缓存检查大约比重新运行不断增长前缀的 Lake 检查快 9–14 倍。

我们的主要评估在真实的文档级形式化任务上对 LeanFlow 进行了消融实验，系统必须从源文档中恢复语句，然后完成由此产生的证明工作。我们比较了队列管理与自由运行的证明循环、完整 Lean 工具访问与仅终端交互、以及源蓝图检查点与直接源到代码生成。纯证明基准测试仍然是有用的校准，但它们预先提供了形式化语句，仅测试系统是否能够替换证明占位符。因此，我们报告 RLM25-PFR 智能体运行和 ICML 2026 AI for Math TCS 挑战（AI for Math Workshop，2026 (https://arxiv.org/html/2607.20503#bib.bib5)）作为补充测量。

两个文档级案例研究是 Frisch 和 Vaserstein 的 *通过单组多项式参数化勾股三元组*（Frisch 和 Vaserstein，2007 (https://arxiv.org/html/2607.20503#bib.bib6)）以及 Lyons 和 Zumbrun 的 *Cramer–Wold 定理的微积分证明*（Lyons 和 Zumbrun，2017 (https://arxiv.org/html/2607.20503#bib.bib7)）。勾股源结合了整数值多项式定义、在 \(\mathbb{Z}[x_1,\ldots,x_n]\) 上的一个障碍、显式的有理多项式见证以及自定义的纯 TeX 定理宏。Cramer–Wold 源结合了欧几里得空间上的概率测度、闭半空间值、平均距离函数的 Crofton 重构、奇数维拉普拉斯逆变换以及偶到奇嵌入步骤。这些源足够短以便进行受控消融，但它们仍然是完整的数学论文，包含非平凡的定义、表示选择和证明依赖。两者都需要源感知的定义和可重用的 Lean 基础设施，而这些都是散文中未明确说明的。

本文做出了三项主要贡献：

- • 一种用于 Lean 形式化的文档到项目工作流。LeanFlow 从论文或 TeX 项目开始，记录每个生成的声明由哪些源文本支持，在证明搜索前检查语句，并且仅在 Lean 接受当前证明编辑后才进入下一个定理。
- • 一种用于证明修复的快速本地验证器。LeanProbe 缓存当前声明之前的 Lean 环境，并通过 CLI 和 MCP 服务器返回证明状态和诊断；最终接受仍由标准的 Lean/Lake 构建负责。
- • 对完整数学源和仅证明基准的评估。我们使用 Kimi-K2.6 和 GPT-5.5 在两篇论文的形式化任务上消融了队列控制、工具访问和源检查点，并报告 RLM25-PFR 和 ICML 2026 AI for Math TCS 挑战运行作为校准。我们在 GitHub 上发布了 LeanFlow 实现（https://github.com/epfl-lara/LeanFlow）、LeanProbe 验证器（https://github.com/epfl-lara/LeanProbe）以及生成的案例研究项目（https://github.com/epfl-lara/AutoformalizedProjects）。

## 2 相关工作

#### 使用语言模型的形式定理证明。
Lean 4（de Moura 和 Ullrich，2021 (https://arxiv.org/html/2607.20503#bib.bib8)）和 Mathlib（The mathlib Community，2020 (https://arxiv.org/html/2607.20503#bib.bib9)）为许多最近的神经定理证明系统提供了验证基础。诸如 miniF2F（Zheng 等人，2022 (https://arxiv.org/html/2607.20503#bib.bib10)）、ProofNet（Azerbayev 等人，2023 (https://arxiv.org/html/2607.20503#bib.bib14)）、PutnamBench（Tsoukalas 等人，2024 (https://arxiv.org/html/2607.20503#bib.bib28)）、FormalMATH（Yu 等人，2025 (https://arxiv.org/html/2607.20503#bib.bib27)）、SorryDB（Letson 等人，2026 (https://arxiv.org/html/2607.20503#bib.bib24)）和 VeriSoftBench（Xin 等人，2026 (https://arxiv.org/html/2607.20503#bib.bib25)）等基准测量了不同的纯证明或仓库级能力。它们提供了有用的校准，但大多数都是从已有的形式化语句或仓库上下文开始的。我们的工作则研究当源开始于数学散文且输出必须是一个可构建的项目时所需的运行时。

#### 跨规模自动形式化。
早期的 LLM 自动形式化工作研究了定理规模的自然语言到形式化翻译（Wu 等人，2022 (https://arxiv.org/html/2607.20503#bib.bib13)）；后来的工作改进了 Lean 语句的过程监督和评估（Lu 等人，2024 (https://arxiv.org/html/2607.20503#bib.bib15)；Poiroux 等人，2025c (https://arxiv.org/html/2607.20503#bib.bib16), a (https://arxiv.org/html/2607.20503#bib.bib17)）。M2F（Wang 等人，2026 (https://arxiv.org/html/2607.20503#bib.bib1)）和自动教科书形式化（Gloeckle 等人，2026 (https://arxiv.org/html/2607.20503#bib.bib30)）将长数学源形式化为 Lean 项目，审计生成的语句，并在固定的环境下修复证明。Math, Inc. 的 Gauss 系统是一个用于大型 Lean 项目的自动形式化智能体（Math, Inc.，2025 (https://arxiv.org/html/2607.20503#bib.bib20)）。在球体填充项目（Hariharan 等人，2026 (https://arxiv.org/html/2607.20503#bib.bib32)）中，它帮助完成了从现有蓝图和 Lean 开发中得到的 8 维结果的无 sorry 形式化。AlphaProof Nexus（Tsoukalas 等人，2026 (https://arxiv.org/html/2607.20503#bib.bib31)）使用一种智能体进化框架，在大量形式化猜想集合上进行形式化证明搜索。与 M2F 的直接比较目前很难，因为现有的公开制品有限：在 M2F 下复现我们的文档级运行需要相同的源文档、模型、Mathlib 版本、预算、提示、工作流日志、工具界面和最终接受标准。我们的研究在文档量上较小，但侧重点不同：我们隔离了队列控制、工具路由、语句交接以及在我们实验中的两种模型设置下的模型侧预算。

#### 用于智能体的 Lean 工具。
检索和环境访问是实际 Lean 证明的核心。LeanDojo（Yang 等人，2023 (https://arxiv.org/html/2607.20503#bib.bib11)）研究了检索增强的定理证明，而 LeanExplore（Asher，2025 (https://arxiv.org/html/2607.20503#bib.bib12)）提供了对 Lean 声明的搜索。LeanInteract（Poiroux 等人，2025b (https://arxiv.org/html/2607.20503#bib.bib2)）公开了一个 Python 接口用于 Lean 执行。LeanFlow 建立在这个工具生态系统之上，但引入了 LeanProbe 作为其自己的用于智能体循环的缓存同文件验证器；最终接受仍来自标准的 Lean/Lake 验证。

## 3 问题设定

设 \(D\) 为一个数学源制品：一个 LaTeX 文件、一个 PDF，或一个包含 TeX 项目的目录。设 \(E\) 为一个固定的 Lean 环境：一个 Lean 工具链、一个固定的数学库修订版（如一个 Mathlib 提交），以及用于检查的 Lake 项目配置。数学结果不应依赖于这个特定的快照，但对构建、诊断、导入和可用引理的评估总是相对于 \(E\) 进行的。目标是生成一个 Lean 项目 \(P\) 以及声明级别的溯源。对于每个生成的声明 \(d \in \mathrm{Decl}(P)\)，工作流应记录 \(\pi(d) \subseteq \mathrm{Span}(D)\)，其中 \(\pi(d)\) 是证明 \(d\) 合理的有限源跨度、标签、节、页、方程或参考文献集。

我们区分三个检查。语句类型检查询问生成的 Lean 声明在 \(E\) 下是否类型正确，当类似定理的证明体被显式的 sorry 占位符替换时。语句忠实性检查询问那个类型正确的声明是否陈述了源声明，包括语句类型、量词、定义域、假设和结论。证明完成性检查询问一个忠实的声明是否具有完整的证明，没有不可接受的占位符或自定义公理。最终项目门控比定理局部检查更严格：请求的文件或完整的 Lake 项目必须在 \(E\) 下构建成功，并且卫生扫描必须报告没有未经批准的 sorry、admit、unsafe 或隐藏的公理。

图 1 (https://arxiv.org/html/2607.20503#S3.F1) 和算法 1 (https://arxiv.org/html/2607.20503#alg1) 总结了文档到项目的契约。

源制品 .tex, PDF, TeX 树
↓
预检
清单块, PDF, 引用
↓
蓝图
源映射 依赖, 名称, 笔记
↓
Lean 草稿
带有 sorry 的语句
↓
语句/源门控
批准或重写
↓
证明器队列
一次一个声明
↓
LeanProbe
缓存检查 预热环境
↓
最终门控
Lake 构建 sorry/公理
↑
工作流状态记录
↑
形式化语句
重写
↑
形式化器
↑
证明器

图 1: LeanFlow 文档到项目流水线。虚线区域分隔形式化器和证明器阶段；绿色筒仓是两者共享的项目本地工作流状态记录。形式化器发出一个类型正确的语句骨架和一个持久的蓝图，形式化定理语句在证明器队列尝试在验证器和卫生门控下进行证明闭包之前通过语句/源门控。工作流状态记录活动、证明检查点、失败的尝试、路由决策、证明器计划和结果，因此重写和构建失败会持续存在，而不会留在瞬态的对话状态中。

## 4 方法

### 4.1 工作流概览

图 1 (https://arxiv.org/html/2607.20503#S3.F1) 和算法 1 (https://arxiv.org/html/2607.20503#alg1) 总结了文档到项目的契约。LeanFlow 使用两个主要工作流：**formalize**，它将源文档转化为有源支撑的 Lean 声明和证明计划；以及 **prove**，它修复或完成 Lean 证明，直到请求的文件或项目编译成功。这两个工作流被有意分开。形式化可能引入定义、名称、导入和定理语句，但止步于一个带有源支撑的 sorry 主体的证明骨架。然后证明修复将这些声明视为固定目标：它可以编辑证明主体并添加局部辅助引理，但不能修改定理语句、添加公理或使分配的证明部分未解决。

算法 1 LeanFlow 智能体工作流契约

1: 解析源文档 \(D\) 和固定的 Lean 环境 \(E\)。
2: 提取一个预检清单：源块、标签、引用、PDF、图表和支持文件。
3: 创建一个“蓝图”，将源跨度映射到计划中的声明、依赖项、范围更改和证明笔记。
4: 起草 Lean 声明，仅对类似定理的证明使用占位符；验证语句层类型检查通过。
5: 运行语句/源门控；如果忠实性失败，在证明搜索前重写。
6: **while** 请求的文件或项目仍包含分配的证明义务 **do**
7:   从队列中分配一个类似定理的声明。
8:   使用搜索、证明上下文和基于 LeanProbe 的检查来修复分配的证明。
9:   每次尝试后持久化失败、诊断、路由决策和证明检查点。
10:  仅在验证通过、没有相关的 sorry 以及可接受的公理配置文件后接受分配。
11: **end while**

### 4.2 有源支撑的骨架构建

LeanFlow 首先使用文档处理工具确定性地解析源。对于一个 TeX 项目目录，确定性预检使用正则表达式搜索来识别并选择主入口点，跟踪本地包含，记录参考文献文件，并提取所有标签和交叉引用。对于 PDF 源，预检使用语言模型生成源文本块，但坚持对这些块进行有界编辑，使得每个源跨度保持不可变，直到形式化器发出一个类型的 Lean 代码片段。

蓝图将每个源跨度映射到一个对应的 Lean 声明。蓝图是一个项目本地的数据结构，包含：
- 一个从源跨度到声明的映射，例如将定理环境映射到一个命名为 `theorem` 的 Lean 语句。
- 依赖信息：哪些声明需要其他声明作为导入。
- 作用域更改：例如，如果源定义了一个新符号或类型，蓝图记录该符号及其计划名称。
- 证明笔记：如果源定理的证明在散文中给出，蓝图可能包含一个指向该散文的指针。

形式化器将蓝图和源文本作为输入，并生成一个 Lean 草稿，其中每个定理声明都有一个显式的 `sorry` 主体。该草稿必须通过类型检查，否则形式化器会重试。一旦类型检查通过，声明就进入语句/源门控，该门控将生成的类型与原始源文本进行比较。如果门控失败，形式化器可以使用蓝图提供的源跨度来重新生成声明，或者用户可以提供反馈。

### 4.3 证明修复与队列管理

一旦声明通过语句/源门控，它们就进入证明器队列。队列由程序化的工作流管理器拥有，它一次分配一个声明。管理器维护一个队列，其中包含所有待证明的声明的引用，以及每个声明的失败尝试计数和重试预算。当分配一个声明时，管理器提供证明上下文：当前 Lean 环境、相关的源文本和任何已有的证明尝试。模型使用搜索引擎（如 LeanDojo 或自定义搜索）来查找相关引理，并使用 LeanProbe 来验证编辑。每次尝试后，如果验证失败，管理器会记录诊断并将声明放回队列，或者如果重试预算已用尽，则标记为失败。如果验证通过，管理器会将声明的状态更新为“已完成”，然后分配队列中的下一个声明。

当所有声明的状态都为“已完成”时，项目被认为完成。最终门控运行完整的 Lake 构建，并检查没有未经批准的 sorry、admit、unsafe 或隐藏的公理。

### 4.4 LeanProbe：一个缓存的验证器

LeanProbe 是 LeanFlow 的一个组件，用于加速证明修复循环。它缓存当前声明之前的 Lean 环境，因此当模型编辑证明主体时，LeanProbe 可以只重新检查该编辑，而不需要重新构建整个文件。它通过 CLI 和 MCP 服务器提供证明状态和诊断。最终接受仍然由标准的 Lean/Lake 构建负责，因此 LeanProbe 主要用于快速迭代。

在连续同文件基准测试中，我们比较了 LeanProbe 的缓存检查与重新运行不断增长前缀的 Lake 检查。结果（表 6）显示缓存检查大约快 9–14 倍。

## 5 实验

### 5.1 文档级形式化

我们在两个文档上运行了消融实验：Frisch 和 Vaserstein 的勾股三元组参数化论文，以及 Lyons 和 Zumbrun 的 Cramer–Wold 证明论文。我们使用了两种模型：Kimi-K2.6 和 GPT-5.5。消融变量包括：
- **队列管理**：完整工作流与无队列变体（模型可以自由地以任何顺序证明任何声明）。
- **工具访问**：完整 Lean 工具访问（LeanProbe、搜索引擎、Mathlib 查询）与仅终端访问（模型只能通过终端与 Lean 交互，没有专门的工具）。
- **源蓝图**：使用蓝图进行源映射与直接源到代码生成（模型直接从源文本生成 Lean 代码，没有明确的蓝图步骤）。

我们报告了任务结果（是否完成）、API 调用次数、输入令牌数和输出令牌数。

结果（表 1-4）显示：
- 使用 Kimi-K2.6 时，完整工作流在 2000 次调用预算内完成了两个来源，而无队列变体达到了预算限制。
- 使用 GPT-5.5 时，所有变体都完成了，但完整工作流在输入令牌消耗方面要么是最低的，要么是并列最低的。

这表明工作流控制对于较弱或预算有限模型至关重要，而对于较强模型则主要提高效率。

### 5.2 仅证明基准

我们在 RLM25-PFR 子集上测试了 LeanFlow，达到了 75.7% 的 BEq+，并在 GPT-5.5 上解决了所有五个 ICML 2026 AI for Math TCS 挑战项目。这些结果作为校准补充了文档级评估。

### 5.3 LeanProbe 性能

表 6 显示了在连续同文件基准上 LeanProbe 与 Lake 检查的比较。LeanProbe 的缓存检查比重新运行 Lake 检查快约 9-14 倍，这使得证明修复循环更高效。

## 6 讨论

### 6.1 优势与局限性

LeanFlow 的优势包括：
- 清晰的分离关注点：形式化和证明相互独立，允许使用不同的模型或设置。
- 可审计性：蓝图和门控提供了生成代码的溯源，便于调试和验证。
- 效率：LeanProbe 加速了证明修复循环。

局限性包括：
- 对源文档的依赖：预检可能会错过某些结构，特别是对于格式不规范的 TeX 文件。
- 蓝图构建可能很繁琐，特别是对于包含许多相互依赖定义的论文。
- 当前的实现主要针对 Lean 4 和 Mathlib，移植到其他证明助手需要大量工作。

### 6.2 与相关工作的关系

LeanFlow 与 M2F 和 Gauss 等系统相比，更强调工作流控制和门控。我们的消融实验表明，这些控制对于在一定预算下完成项目至关重要，而不仅是在强大模型上运行。

### 6.3 未来工作

未来方向包括：
- 处理更大规模的文档，如教科书或研究专著。
- 改进蓝图构建自动化，减少人工干预。
- 支持多文件项目和更复杂的依赖解析。
- 探索在其他证明助手（如 Isabelle 或 Coq）上的应用。

## 7 结论

我们介绍了 LeanFlow，一个用于将数学文献自动形式化为 Lean 项目的系统。通过工作流控制、源映射门控和快速缓存验证器，LeanFlow 能够在有限的 API 预算下完成文档级形式化任务，同时提供可审计的溯源。我们的实验表明，工作流控制对于预算有限或能力较弱的模型至关重要，而对于更强大的模型则能提高效率。我们已将 LeanFlow、LeanProbe 和案例研究项目发布在 GitHub 上，希望能促进自动形式化领域的进一步研究。

## 参考文献

[1] Wang et al., 2026. M2F: A Modular Framework for Large-Scale Autoformalization. arXiv:...

[2] Poiroux et al., 2025b. LeanInteract: A Python Interface for Lean Execution. ...

[3] Moonshot AI, 2026. Kimi-K2.6: A Large Language Model for Reasoning and Coding. ...

[4] AI for Math Workshop, 2026. ICML 2026 AI for Math TCS Challenge. ...

[5] Frisch and Vaserstein, 2007. Parametrization of Pythagorean Triples by a Single Triple of Polynomials. ...

[6] Lyons and Zumbrun, 2017. A Calculus Proof of the Cramer–Wold Theorem. ...

[7] Wu et al., 2022. Autoformalization with Large Language Models. NeurIPS 2022.

[8] Zheng et al., 2022. miniF2F: A Benchmark for Formal Math. ICLR 2022.

[9] Azerbayev et al., 2023. ProofNet: A Benchmark for Neural Theorem Proving. ...

[10] Gloeckle et al., 2026. Automatic Textbook Formalization. ...

[11] Math, Inc., 2025. Gauss: An Autoformalization Agent for Large Lean Projects. ...

[12] Hariharan et al., 2026. The Sphere-Packing Project: A Blueprint-Driven Formalization. ...

[13] Tsoukalas et al., 2026. AlphaProof Nexus: Evolutionary Proof Search. ...

[14] Yang et al., 2023. LeanDojo: Retrieval-Augmented Theorem Proving. ...

[15] Asher, 2025. LeanExplore: A Search Engine for Lean Declarations. ...

[16] de Moura and Ullrich, 2021. Lean 4. ...

[17] The mathlib Community, 2020. The Mathlib Library. ...

[18] Poiroux et al., 2025c. Process Supervision for Lean Formalization. ...

[19] Lu et al., 2024. Evaluating Autoformalization with Lean. ...

[20] Letson et al., 2026. SorryDB: A Benchmark for Proof Completion. ...

[21] Xin et al., 2026. VeriSoftBench: A Verification Benchmark for Software and Math. ...

[22] Tsoukalas et al., 2024. PutnamBench: A Benchmark for Formalizing Putnam Problems. ...

[23] Yu et al., 2025. FormalMATH: A Benchmark for Formalization of Mathematical Texts. ...

（注意：由于原始文本的参考文献部分被截断，我无法完整翻译剩余的参考文献。实际翻译时应提供完整的参考文献列表。）