Formalizing Numerical Analysis: An Agent Pipeline and Quality Audit Beyond Kernel Acceptance

背景

近年来，基于大语言模型（LLM）的代码智能体（Coding Agents）在形式化数学领域取得了显著进展。已有研究证明，这些智能体能够自动将整本高等数学教材形式化为 Lean 4 代码。然而，现有的工作主要存在两个局限性：

1. 领域偏差：大多数努力集中在 mathlib（Lean 的标准数学库）中已有大量现成表示的数学分支上。这意味着智能体更多是在“复用”已有知识，而非从零开始构建新理论。
2. 评估单一：现有的成功标准几乎完全依赖于“内核接受度”（Kernel Acceptance），即代码能否通过 Lean 类型检查器的编译。这种基于编译的指标虽然必要，但不足以全面反映形式化证明的质量，因为它无法捕捉语义上的错误、逻辑漏洞或对原始数学意图的偏离。

为了突破这些局限，本文聚焦于数值分析（Numerical Analysis）这一在 mathlib 中相对缺失的领域，特别是常微分方程（ODEs）数值方法的形式化。研究旨在评估智能体从零开始开发新理论的能力，并引入一套超越单纯编译检查的质量审计框架。

核心内容

1. 研究对象与方法论：从零构建数值分析理论

本研究选取了《常微分方程数值方法》（Numerical Methods for Ordinary Differential Equations）作为目标教材。与代数或拓扑等成熟分支不同，数值分析在 mathlib 中的基础较为薄弱。因此，这项工作重点考察了编码智能体（Coding Agent）在缺乏现成库支持的情况下，如何从头构建新的数学理论和形式化证明。

2. 三维质量评估框架

传统的“编译通过即成功”的标准存在巨大盲区。为此，作者提出并应用了一个系统化、可复现的三维评估框架，用于评估智能体生成的形式化内容质量：

• 语义正确性（Semantic Correctness）：形式化代码是否忠实于原始数学文本的含义？是否存在逻辑谬误或表述不完整？
• Mathlib 复用（Mathlib Reuse）：智能体是否有效地利用了现有的 mathlib 库资源，还是不必要地重新发明轮子？
• 跨文件复用（Cross-file Reuse）：生成的形式化内容是否具有良好的模块化结构，能否在其他证明或模块中被有效复用？

为了量化评估“语义正确性”和“跨文件复用”，研究采用了 LLM-as-judge（以大语言模型作为裁判）的方法。这种方法允许通过自动化手段对形式化证明的深层质量进行审计，而不仅仅是检查语法。

3. 审计结果：揭示“内核接受”掩盖下的质量问题

作者将该评估框架应用于两个场景：

1. 本研究自身生成的 ODE 数值方法形式化代码。
2. 公开发布的其他自动形式化系统（如 RepoProver 和 M2F）的输出结果。

审计发现，尽管这些形式化代码都能通过 Lean 内核检查（即具备“内核接受度”），但其中普遍存在不忠实的形式化模式（Unfaithful Formalization Patterns）。具体包括：

• 不完整的多部分陈述：原始数学命题可能包含多个条件或结论，但形式化代码仅捕获了部分，导致逻辑信息丢失。
• 添加的弱化假设（Added Weakening Hypotheses）：为了使证明更容易通过编译，智能体可能无意中添加了比原始数学陈述更严格的限制条件，从而削弱了定理的通用性和强度。
• 参数限制（Parameter Restrictions）：对定义域或参数范围的不当限制，导致形式化结果无法覆盖原始数学理论的全部情况。

这些错误在传统的编译检查中是完全不可见的，因为只要代码符合类型规则，内核就会接受它。然而，从数学严谨性的角度来看，这些形式化是“有缺陷”的。

关键要点

• 突破领域限制：研究证明了编码智能体可以在 mathlib 覆盖不足的领域（如数值分析）中，从零开始构建复杂的数学理论，而不仅仅是复用现有知识。
• 编译指标的高估问题：基于编译（Kernel Acceptance）的指标严重高估了自动形式化系统的实际质量。通过编译并不等于数学上的正确或忠实。
• 三维审计框架的有效性：提出的“语义正确性、Mathlib 复用、跨文件复用”三维框架，结合 LLM-as-judge 方法，能够揭示传统方法无法检测的逻辑缺陷。
• 普遍存在的“不忠实”模式：在 RepoProver、M2F 以及本研究自己的产出中，均发现了诸如“弱化假设”和“信息丢失”等系统性错误。这表明当前的自动形式化技术仍倾向于生成“易于证明”而非“忠实原意”的代码。
• 可复现的审计方法论：研究提供了一套可复现的审计流程，为未来评估和改进自动形式化系统提供了更 rigorous（严谨）的标准。

意义与影响

这项工作对形式化验证和 AI 辅助数学领域具有深远意义：

1. 重新定义成功标准：它挑战了以“编译通过”为唯一成功标准的现状，呼吁社区关注形式化证明的语义忠实度和数学严谨性。
2. 推动更高质量的自动形式化：通过揭示当前系统（包括 RepoProver 和 M2F）的固有缺陷，研究为改进智能体架构提供了明确方向——即需要增强智能体对数学意图的理解能力，而不仅仅是代码生成能力。
3. 填补数值分析形式化的空白：在 mathlib 中系统性地引入常微分方程数值方法的形式化，为后续相关领域的研究奠定了坚实基础。
4. 提供通用评估工具：所提出的三维评估框架和 LLM-as-judge 审计方法，可被其他研究者应用于评估不同的自动形式化工具，促进该领域的标准化和透明化发展。

总之，本文不仅是一次具体的技术实践，更是一次对自动形式化系统评估范式的深刻反思，强调了在追求自动化效率的同时，必须坚守数学形式的严谨性与忠实性。