AI 新闻·2026年10月25日·来源： Accu
变异 Lean 证明以寻找问题
大型语言模型（LLM）被用于生成机器可检查的 Lean 语言数学证明，但数学家们发现这些由 AI 衍生的证明程序包含错误。为解决此问题，一个团队尝试了变异测试，这是一种改变证明源代码并检查其是否仍然有效的技术，旨在识别潜在的缺陷部分。
对 AI 模型在复杂输出（例如数学证明）方面日益增长的依赖，凸显了对强大验证方法的需求。尽管 LLM 可以在像 Lean 这样的形式语言中生成证明，这些语言是为机器验证而设计的，但这些输出并非没有错误，这与 AI 生成的编程代码中发现的问题相呼应。对这些证明进行传统的手动审查通常不切实际，因为它们可能长达数千行。
变异测试提供了一种潜在的自动化解决方案来发现隐藏的缺陷。这种方法涉及在 Lean 证明的源代码中引入故意的、非琐碎的更改或“变异”。核心假设是，如果一个证明可以在不影响其被 Lean 证明助手验证的能力的情况下进行实质性更改，那么原始证明可能包含无效代码或过于宽泛的条件，这些条件掩盖了潜在的问题。
一项初步的、有限的实验使用一个基本的变异工具，成功地在一个小型测试案例中引入了 13 个变异，而证明仍然通过验证。这证明了该技术在突出可能被忽视的关注领域方面的潜力。然而，将这种方法扩展到更大、真实世界的证明，例如 OpenAI 为 Navier-Stokes 提供的 470,000 行 Lean 代码，面临着重大的计算挑战，因为即使是简短的证明，每次变异也需要几秒钟的验证时间，这对全面的测试提出了大量的处理能力要求。
