arXiv:2606.14000 — AI 智能体形式化数学教材：通过编译不等于保证正确性

宏大目标：在 Lean 4 中形式化整本教材

形式化数学验证——在 Lean 4、Coq 或 Isabelle 等系统中证明定理——传统上需要数千小时专业人员的手工工作。研究人员 Theodore Meek、Siyuan Ge、Di Qiu Xiang、Simon Chess 和 Vasily Ilin 将自动化智能体流水线应用于一个雄心勃勃的目标：在配备 Mathlib 库的 Lean 4 中形式化一本关于常微分方程数值方法的完整教材。

数值分析是尤其具有挑战性的目标，因为这一数学分支在现有形式化库中的覆盖相对薄弱——这意味着智能体无法简单地调用已有的引理，而必须从头构建形式化基础。

编译通过足以证明正确性吗？

评估形式化数学代码智能体的标准指标是内核接受——代码能否在无错误的情况下通过 Lean 验证器。乍看之下，这似乎是一个可靠的信号：内核接受的陈述在形式上是被证明了的。

然而本研究推翻了这一假设。作者发现内核接受在本质上掩盖了语义错误——智能体经常产出可以编译但在数学意义上不正确的陈述。更甚者，基于编译的指标在很大程度上高估了形式化的实际质量，这使得仅依赖此信号的评估协议的可靠性受到质疑。

三种系统性失败模式

智能体流水线呈现出三种编译无法捕捉的反复出现的错误模式。

添加假设削弱定理。 智能体在陈述定理时附加了原始定理中并不存在的额外前提条件。陈述在这些前提下在技术层面是正确的——但证明的是较弱的命题。例如，关于数值方法收敛性的一般定理可能被限制为正系数的特殊情形，Lean 会接受这个结果，但研究人员并不会。

多部分陈述的不完整覆盖。 当定理有多个结论或分支情形时，智能体可能只形式化了其中一部分。Lean 会将此作为有效但部分的形式化接受，原始定理的覆盖保持不完整，验证器也不会给出任何诊断信息。

幻象导入。 智能体引用了不存在或具有不同导出名称的 Mathlib 定义或引理。在某些情况下，Lean 会容忍或部分解析这类导入，让错误通过内核并留下虚假的有效性印象。

三维质量框架

作为回应，作者提出了一个三维评估框架，超越了简单的接受或拒绝二元方法。

第一个维度是语义正确性——形式化陈述是否符合教材中原始定理的语义，无论其是否通过内核验证。第二个维度是 Mathlib 复用——智能体是否使用了 Mathlib 库中现有的定义、引理和结构，还是在重新发明已有的证明。第三个维度是跨文件复用——定义在项目的不同文件中是否保持一致，或者是否存在隐藏逻辑漏洞的不一致对。

三个维度均通过 LLM-as-judge 方式评分——这是一种可复现且可扩展的自动化评估方法。该框架设计为可应用于未来的形式化智能体系统，而不仅限于这一特定流水线。

对 AI 编程基准的更广泛启示

这项研究的影响远超形式化数学领域。编译通过作为主要成功信号，同样被用于评估标准软件的 AI 编程智能体——HumanEval 或 SWE-bench 等基准依赖测试通过作为正确性的代理。

如果同样的问题在那里也存在——智能体通过了测试，但产出了在语义上被弱化或部分正确的实现——那么标准 AI 编程基准就是质量信号不足的指标。这项研究为这一担忧提供了正式论证，并以真实形式化项目中分类的具体错误样本作为佐证。

对于将 AI 智能体部署于编写或验证关键代码的团队而言，核心信息是明确的：编译通过和测试通过是必要但不充分的正确性指标。语义评估——无论代价多高、自动化难度多大——仍是不可或缺的步骤。