数值分析形式化：超越内核接受的智能体流水线与质量审计

## 数值分析的自动化形式化：一种Agent流水线与超出内核接受范围的质量审计

来源：https://arxiv.org/html/2606.14000

###### 摘要

近期工作表明，编码Agent能够将整个高等数学教材形式化为Lean 4代码，然而现有工作集中于已在mathlib中充分表示的数学分支，并且仅通过内核接受来衡量成功。我们通过将编码Agent应用于数值分析教材《常微分方程数值方法》来解决这两个局限性，该教材很大程度上未在mathlib中出现，从而考验Agent从零开始开发新理论的能力。我们进一步引入一个系统化、可复现的三维框架，用于评估Agent生成的形式化代码质量，超越编译层面：语义正确性、Mathlib复用以及跨文件复用（采用LLM-as-judge方法）。将该框架应用于我们自己的形式化结果以及RepoProver和M2F发布的结果，我们发现了反复出现的不忠实形式化模式——包括不完整的多部分语句、添加弱化假设以及参数限制——而这些完全被内核接受所掩盖。我们的结果表明，基于编译的指标显著高估了形式化质量，我们提供了一种可复现的审计方法，以支持未来自动形式化系统的更严格评估。

机器学习，ICML

## 1 引言

交互式定理证明器如Lean（de Moura & Ullrich, 2021 (https://arxiv.org/html/2606.14000#bib.bib7)）能够以机器可检验的严谨性验证数学。Lean的数学库mathlib（mathlib社区, 2020 (https://arxiv.org/html/2606.14000#bib.bib21)）现已包含数十万个定义和定理，涵盖本科和研究生课程的大部分内容，使Lean成为验证研究级数学以及大规模构建机器可检验数学知识的日益实用的基础。

规模化形式化的主要障碍在于其成本。将自然语言撰写的数学翻译成形式化代码既缓慢又劳动密集，需要同时具备数学和形式化语言的专业知识。这一障碍推动了大量关于自动形式化的研究，即尝试使用语言模型自动将非形式化数学翻译成形式化语句和证明（Szegedy, 2020 (https://arxiv.org/html/2606.14000#bib.bib27); Wu et al., 2022 (https://arxiv.org/html/2606.14000#bib.bib33); Jiang et al., 2023 (https://arxiv.org/html/2606.14000#bib.bib12)）。目前已出现三类方法。专门为形式化数学训练的专用模型在miniF2F（Zheng et al., 2022 (https://arxiv.org/html/2606.14000#bib.bib35)）、ProofNet（Azerbayev et al., 2023 (https://arxiv.org/html/2606.14000#bib.bib2)）和PutnamBench（Tsoukalas et al., 2024 (https://arxiv.org/html/2606.14000#bib.bib28)）等逐问题基准测试上展示了其性能，最近的系统包括DeepSeek-Prover-V2（Ren et al., 2025 (https://arxiv.org/html/2606.14000#bib.bib26)）、Goedel-Prover-V2（Lin et al., 2025 (https://arxiv.org/html/2606.14000#bib.bib16)）、Kimina-Prover（Wang et al., 2025 (https://arxiv.org/html/2606.14000#bib.bib30)）和Aristotle（Achim et al., 2025 (https://arxiv.org/html/2606.14000#bib.bib1)）。通用前沿模型通过提示工程和多模型协作，在没有任务特定训练的情况下展现出了令人惊讶的形式化能力（Wu et al., 2022 (https://arxiv.org/html/2606.14000#bib.bib33)）。最近，编码Agent（即配备工具、文件访问、编译器反馈以及多步操作能力的前沿模型）已被用于将整个教材规模的数学形式化，在数天内产出数百页的形式化开发（Urban, 2026 (https://arxiv.org/html/2606.14000#bib.bib29); Wang et al., 2026 (https://arxiv.org/html/2606.14000#bib.bib31); Gloeckle et al., 2026 (https://arxiv.org/html/2606.14000#bib.bib11); Liu et al., 2026 (https://arxiv.org/html/2606.14000#bib.bib17); Ren et al., 2026 (https://arxiv.org/html/2606.14000#bib.bib25)）。

随着自动形式化从孤立问题扩展到整本教材，两个问题变得紧迫。第一个是泛化性。大多数现有结果涉及已在mathlib中充分表示的数学，而这些系统在mathlib尚未覆盖的数学上表现如何远不清楚，此时Agent必须从头开发相关理论，而非检索现有结果（Kumarappan et al., 2025 (https://arxiv.org/html/2606.14000#bib.bib13); Gloeckle et al., 2026 (https://arxiv.org/html/2606.14000#bib.bib11)）。第二个是评估。现有的整本教材形式化工作几乎只以代码是否通过类型检查且不含`sorry`来报告“成功”。然而，内核接受仅确定形式化代码是良好形成的且可编译，并不保证其语义正确性（Poiroux et al., 2025 (https://arxiv.org/html/2606.14000#bib.bib24); Li et al., 2024a (https://arxiv.org/html/2606.14000#bib.bib14); Liu et al., 2025 (https://arxiv.org/html/2606.14000#bib.bib18); Lu et al., 2024 (https://arxiv.org/html/2606.14000#bib.bib19); Weng et al., 2025 (https://arxiv.org/html/2606.14000#bib.bib32)）。例如，一个编译通过的语句可能是空真（Li et al., 2024a (https://arxiv.org/html/2606.14000#bib.bib14)），或者可能误解了量词作用域或隐含约束（Zhang et al., 2025 (https://arxiv.org/html/2606.14000#bib.bib34); Chen et al., 2026 (https://arxiv.org/html/2606.14000#bib.bib6)）。然而在整本教材场景下，超出编译的质量评估仅通过有限、主观的抽查进行（Wang et al., 2026 (https://arxiv.org/html/2606.14000#bib.bib31); Gloeckle et al., 2026 (https://arxiv.org/html/2606.14000#bib.bib11)）。

在本工作中，我们解决了这两个问题。首先，我们将编码Agent应用于形式化《常微分方程数值方法》，这是一本关于数值分析分支的教材，该分支几乎完全未在mathlib中出现，从而考验Agent开发新理论而非重新组合现有库内容的能力。其次，我们引入了一种系统化且可复现的方法来评估结果形式化的质量，沿三个维度进行审计：(1) *语义正确性*：每个形式化语句是否忠实反映原文；(2) *mathlib复用*：Agent是否在应当使用时复用了现有的mathlib结果，而非重新形式化；(3) *跨文件复用*：Agent是否复用了项目中其他地方已经形式化的结果，而非重复实现。我们的方法将形式化代码的自动分析与LLM-as-judge（Zheng et al., 2023 (https://arxiv.org/html/2606.14000#bib.bib36); Zhang et al., 2025 (https://arxiv.org/html/2606.14000#bib.bib34)）相结合，并通过对我们自己的形式化结果以及RepoProver和M2F发布的结果进行案例研究来展示这一方法。

我们的贡献在于：

- •我们将编码Agent应用于形式化一本数值分析教材，该数学分支在很大程度上未被mathlib覆盖，从而为在先前工作研究的充分覆盖领域之外的智能体自动形式化提供压力测试。
- •我们引入了一种系统化、可复现的方法，在超出内核接受的范围，沿三个维度——语义正确性、mathlib复用和跨文件复用——评估形式化质量，并使用LLM-as-judge。
- •我们报告了在此方法下对我们形式化结果的详细评估，刻画当前智能体形式化在何处以及如何成功和不足。

## 2 相关工作

### 2.1 智能体自动形式化

早期的自动形式化将翻译视为单次、逐语句的任务（Wu et al., 2022 (https://arxiv.org/html/2606.14000#bib.bib33); Jiang et al., 2023 (https://arxiv.org/html/2606.14000#bib.bib12); Azerbayev et al., 2023 (https://arxiv.org/html/2606.14000#bib.bib2)），专用证明器继续在miniF2F和ProofNet等基准测试上推动语句级和证明级性能（Ren et al., 2025 (https://arxiv.org/html/2606.14000#bib.bib26); Lin et al., 2025 (https://arxiv.org/html/2606.14000#bib.bib16); Wang et al., 2025 (https://arxiv.org/html/2606.14000#bib.bib30)）。最近一条研究路线为前沿模型配备工具、文件访问、编译器反馈和多步控制，产生了*智能体*形式化系统（Liu et al., 2026 (https://arxiv.org/html/2606.14000#bib.bib17); Ren et al., 2026 (https://arxiv.org/html/2606.14000#bib.bib25)）。几项并行工作已将该范式扩展到整本教材和项目：最近一项工作将一般拓扑形式化为Megalodon（Urban, 2026 (https://arxiv.org/html/2606.14000#bib.bib29)）；M2F将数百页分析编译为一个可构建的Lean项目（Wang et al., 2026 (https://arxiv.org/html/2606.14000#bib.bib31)）；RepoProver协调数千个并行Agent将研究生代数组合学教材形式化为Lean（Gloeckle et al., 2026 (https://arxiv.org/html/2606.14000#bib.bib11)）；进一步的多Agent和跨系统工作瞄准其他教材材料（Brown et al., 2026 (https://arxiv.org/html/2606.14000#bib.bib3); Bryant et al., 2026 (https://arxiv.org/html/2606.14000#bib.bib4)）。这些工作表明，教材规模的智能体形式化是可行的，但它们处理的是已充分形式化的数学分支，并且主要以内核接受来报告成功。相比之下，我们研究一个很大程度上未在mathlib中出现分支，并专注于评估Agent生成的形式化质量。

### 2.2 形式化评估

已充分确立的是，在证明助手中编译是忠实形式化的必要但不充分条件（Poiroux et al., 2025 (https://arxiv.org/html/2606.14000#bib.bib24); Li et al., 2024a (https://arxiv.org/html/2606.14000#bib.bib14); Liu et al., 2025 (https://arxiv.org/html/2606.14000#bib.bib18); Weng et al., 2025 (https://arxiv.org/html/2606.14000#bib.bib32)）。表面形式的指标如BLEU与正确性相关性差（Lu et al., 2024 (https://arxiv.org/html/2606.14000#bib.bib19)），激发了专门的方法：符号和双向等价性检查（Li et al., 2024a (https://arxiv.org/html/2606.14000#bib.bib14); Poiroux et al., 2025 (https://arxiv.org/html/2606.14000#bib.bib24)）、反向翻译和学习对齐模型（Lu et al., 2024 (https://arxiv.org/html/2606.14000#bib.bib19); Gao et al., 2025 (https://arxiv.org/html/2606.14000#bib.bib9)）以及LLM-as-judge方法（Peng et al., 2025 (https://arxiv.org/html/2606.14000#bib.bib23); Zhang et al., 2025 (https://arxiv.org/html/2606.14000#bib.bib34); Chen et al., 2026 (https://arxiv.org/html/2606.14000#bib.bib6)）。然而，这些方法评估的是孤立语句相对于单个非形式化对应物的质量。我们的工作有两个方面的不同：我们评估的是Agent生成的项目规模形式化而非逐语句形式化，并且我们引入了结构维度，通过分析mathlib使用情况和跨文件使用情况，来评估形式化如何与库和项目集成。这种集成对于大规模形式化变得至关重要。

## 3 方法

### 3.1 形式化流水线

我们的流水线是一个由Python编排器驱动的自主循环，重复调用四个LLM角色：规划者（Planner）、工作者（Worker）、评估者（Evaluator）以及仅在升级时召回的顾问（Consultant）。与近期项目规模自动形式化框架如RepoProver（Gloeckle et al., 2026 (https://arxiv.org/html/2606.14000#bib.bib11)）和M2F（Wang et al., 2026 (https://arxiv.org/html/2606.14000#bib.bib31)）类似，我们针对整个Lean项目而非孤立定理。我们仅在Lean构建成功时提交编辑。与M2F固定的两阶段（先语句后证明）流水线不同，我们运行一个开放循环，其目标在每个周期从实时仓库状态中选择。规划者和工作者角色使用Claude Opus 4.6实现；评估者使用Claude Sonnet。我们将RepoProver的草图器/证明器/审查器拆分替换为通过GitHub Actions协调的规划者/工作者/评估者/顾问分解。

##### 无状态Agent与共享状态。
Agent本身是无状态的：没有Agent跨周期保留记忆。所有跨周期通信通过提交到仓库的文件以及GitHub本身进行。关键工件包括：`strategy.md`（由规划者编写，工作者读取，每周期间覆盖）；`task_results/cycle_NNN.md`（工作者的每周期间报告）；`issues/<名称>.md`（障碍描述）；`history.jsonl`（每个周期一条记录，包含评估者的结构化判断：分数、摘要、卡住内容、建议）；以及`cycle`、`heartbeat.json`和`run.lock`（保存编排器和看门狗的控制状态）。

##### 每周期间流水线。
每个周期按以下阶段进行：
- •**同步。** 编排器拉取最新提交并查询GitHub Actions的构建状态。如果Lean构建失败，规划者被硬编码为首先修复构建。
- •**规划。** 规划者读取`plan.md`、当前的`sorry`位置、近期任务结果、开放问题以及近期周期历史，并在`strategy.md`中发出一组具体指令。
- •**执行。** 工作者编辑Lean源代码树，遵循sorr-first策略：完整陈述定理，验证骨架可编译，然后逐个关闭每个`sorry`。它使用Lean LSP工具和Mathlib搜索（LeanSearch (Gao et al., 2026 (https://arxiv.org/html/2606.14000#bib.bib10)), Loogle (Mathlib社区, 2024 (https://arxiv.org/html/2606.14000#bib.bib20))）。它提交更改并写入任务结果文件；如果受阻，则打开一个问题文件。
- •**评估。** 一个独立的LLM会话读取该周期的Git差异、工作者的任务结果以及近期尝试，并输出一个进度分数（范围为[-2,2]）、一句摘要、当前障碍、下一个规划者周期的建议以及一个压缩的`attempts.md`行。
- •**机械门控。** 独立于LLM判断，编排器强制执行硬约束。我们采用M2F风格的验证器认证细化（Wang et al., 2026 (https://arxiv.org/html/2606.14000#bib.bib31)）检查整个源代码树上的总`sorry`计数，禁止其严格增加；预算增加需限速并提供理由。通过正则表达式提取`strategy.md`中声明的范围并检查工作者提交是否符合来执行策略合规性。构建门控确保修改后的文件在工作者被允许提交之前可编译。
- •**升级。** 如果近期历史显示连续四次或更多非正分数，则调用顾问角色，其建议写入问题跟踪器供下一个规划者周期使用。
- •**记账。** 评估记录附加到`history.jsonl`，周期计数器前进。

##### Agent技能。
每个Agent由仓库级指令（`CLAUDE.md`或`AGENTS.md`文件）塑造，这些指令在会话启动时自动加载。这些常驻规则吸收了过去迭代中必须通过重复人工提示提供的内容。

### 3.2 分析方法

#### 3.2.1 语义正确性

我们使用两种LLM判断协议来审计语义忠实性，它们共享一个评分标准，但在判断读取的内容上有所不同。

##### 每项目NL/Lean配对。
每个语料库以不同方式追踪形式化实体，因此我们通过三种方式提取每实体记录，将教材的NL语句与其Lean声明头配对。对于Butcher，我们使用一个带有提取NL的策划的`lean_status.json`。对于alg