Case study: solving P-99 with LPTP and an LLM

想象一个这样的世界：计算机不再仅仅遵循僵化、机械的指令，而是能够真正理解人类描述问题时那种凌乱、模糊的方式。这就是人工智能的前沿领域，特别是被称为**大语言模型（LLM）**的一个分支。把 LLM 想象成一个超级聪明、博览群书的学生，他几乎读遍了互联网上的所有内容。如果你让他写故事，他能写；如果你让他写代码，他也能写。但问题在于：这个学生容易产生“幻觉”，这意味着他可能会自信满满地捏造事实，或者编写看起来完美无缺、但在实际运行时却会秘密崩溃的代码。

为了解决这个问题，科学家们使用了形式化验证（Formal Verification），这就像是一位极其严厉的数学老师，会检查学生作业中的每一个步骤，以确保在逻辑上绝不可能出错。在计算机科学领域，有一套著名的挑战被称为 99 Prolog 问题（或简称 P-99）。这些问题就像是逻辑编程的“健身训练”，逻辑编程是一种描述“想要发生什么”而非“如何一步步实现”的编码风格。研究人员提出的核心问题是：我们能否让这个 AI 学生根据一段简单的英文描述来编写代码，然后让这位数学老师立即检查其是否正确？本论文探讨的正是在这种背景下的实验——将 AI 的创造性自由与形式逻辑的铁律结合在一起。

---

实验：拥有严格老师的编程搭档

在这项研究中，一个研究小组决定测试一种新的工作方式，即将**“氛围编码”（vibe-coding）与“验证编码”（vericoding）**相结合。想象一下，“氛围编码”就像是请一位富有创意的朋友根据你在餐巾纸上画的草图为你搭建一个树屋。你说：“我想要一个带滑梯和暗门的树屋，”然后他们就开始动手建造了。这很快也很有趣，但结果可能会摇摇晃晃。“验证编码”则恰恰相反：它像是聘请了一位建筑师，在钉下第一颗钉子之前，就要求提供蓝图、进行压力测试并完成安全检查。

研究人员想要看看能否将这两种方法结合起来。他们使用了一个名为 Claude（具体为 Opus 4.6 版本）的 AI 模型来充当那位富有创意的建造者。他们给它提供了著名的 P-99 列表中的前 33 个问题，这些问题是用简单、非正式的英语编写的。例如，其中一个问题仅仅是：“找到列表中的最后一个元素。”

AI 的任务是：

1. 编写解决该问题的 Prolog 代码。
2. 编写一个测试文件来检查代码是否有效。
3. 编写一个形式化证明，从数学上保证代码是安全、正确且一定会运行结束的。

为了检查这些证明，他们使用了一个名为 LPTP（逻辑程序定理证明器）的工具。把 LPTP 想象成那位严厉的数学老师，他拒绝接受“看起来没错”这种说法，而是要求为每一个主张提供一步步的逻辑推导。

结果：魔法与数学的结合

实验取得了成功，但这并非一剂万灵药。团队通过这种方法成功解决了 33 个 88 个练习题（约占 37.5%）。以下是幕后的情况：

• 创意部分（氛围编码）： AI 在初始编码方面表现得非常出色。它在短短几分钟内就生成了 58 个逻辑过程（实际的代码）和 508 个测试用例。它理解了英文指令，并生成了可以正确运行的代码。
• 严谨部分（验证编码）： 这是真正的重头戏。AI 必须证明其代码的正确性。它生成了 257 个引理（微小的数学事实），并写下了惊人的 11,800 行证明。
• 人工干预： 研究人员并没有任由 AI 肆意妄为。他们手动检查了每一个文件。他们运行测试，阅读逻辑语句，并使用 LPTP 重新运行证明。如果 AI 卡住了或者写的证明不合逻辑，人类就会介入并给予提示。例如，对于一个关于寻找列表中最后一个元素的问题，人类不得不询问 AI：“嘿，这与 append 函数是如何关联的？”以帮助它构建正确的证明。

主要发现

论文揭示了关于这种新工作方式的几个关键点：

1. AI 擅长“氛围编码”： AI 可以非常迅速地将模糊的英文描述转化为可运行的 Prolog 代码。它甚至避免了现实世界中 Prolog 代码常使用的“不纯”技巧，而是坚持使用一种严格的逻辑风格，以便数学老师（LP 老师）能够理解。
2. AI 在“验证编码”方面需要引导： 虽然 AI 可以轻松生成代码，但证明其“为什么正确”却更难。对于复杂的函数属性（例如证明代码确实完成了预定任务），AI 有时需要人类研究人员先用白话文解释逻辑。一旦人类给出了提示，AI 就能将其形式化并完成证明。
3. 这还不是一个“已解决”的问题： 团队并没有解决全部 99 个问题。有些问题 AI 只用了 15 分钟（如简单的“最后一个元素”问题），而另一些则耗费了数小时（如“质因数分解”问题）。研究人员指出，对于最难的问题，AI 在没有人类指导的情况下，仍然难以自主构思出正确的证明策略。

对未来的展望：“MCP”的联系

论文还描述了他们正在开发的一个新工具，称为模型上下文协议（Model Context Protocol, MCP）。目前，AI 和数学老师（LPTP）通过文件和文本文档进行交流，这有点像在互相寄信。新的 MCP 工具就像是给了他们一条直接的电话线。这使得 AI 能够实时向数学老师寻求帮助，即时检查自己的工作，并在无需人类介入的情况下修复错误。他们用其他 AI 模型（如 Gemini）测试了这一点，发现虽然有些模型可以生成证明的“想法”，但只有 Claude 能够成功生成通过严格检查的“有效”证明。

总结

这篇论文表明，我们正进入一个 AI 可以作为编写复杂逻辑代码的创意伙伴的时代，但它仍然需要一名人类“飞行员”来引导它度过最艰难的部分。AI 可以编写代码甚至起草数学证明，但有时会在细节中迷失方向。通过将 AI 的速度和创造力与像 LPTP 这样的形式化证明检查器相结合，研究人员创建了一个能够在错误变成真正的 Bug 之前将其捕捉到的系统。它目前还不是一个完全自动化的“万能修理机”，但它是一个强大的新工具，让编写可靠软件变得比以往任何时候都更快、更安全。