过去五年，LLM 在软件工程界引发了巨大的震荡，其中大部分讨论都围绕着一个核心问题：我们的职业将走向何方？
一系列对人类介入和控制程度各有取舍、彼此竞争的范式由此出现。一端是几乎没有人类参与闭环的智能体，以及最近流行起来的“氛围编程”：它不鼓励手动修改代码，而是让人通过 LLM 与代码库交互；还有负责实现独立模块或功能的聊天机器人，它们有时甚至会借助代码解释功能运行代码。另一端则是预测用户想要实现什么、充当“超级自动补全”的编程助手。
人们对这些模型的极限、用途和潜力有着各种看法。有人相信，只要投入前所未有的时间和资源，模型就能达到人类水平，并自动构建生产级软件系统；怀疑者则贬低这些模型，声称它们写出的代码平庸而简单，无法扩展到任何生产环境。
我并不是来讨论模型本身的极限或能力。在理论知识和实践经验上，外面有远胜于我的专家。不过，我想提出下面这个观点。
世界上的每一款软件，都必须依据某种正确性定义做到“正确”。在 LLM 出现之前，我们的时间分配在编写、阅读和验证代码上。有了 LLM，我们可以把代码编写阶段交给它们，却无法外包验证过程，只能把验证推到另一个层次。
你会看到有人争辩说，正确性只在火箭或密码学等少数领域才重要。不要误解：不同领域对正确性严谨程度的要求会改变，但对正确性本身的要求不会消失。软件总是带着目的被创造出来，无论是消费和转换数据、向用户提供信息，还是让用户交互并创建新数据。所谓正确性，就是创建的软件符合创建者的意图，而创建者必须验证这种一致性。
在重要性较低的应用和领域中，正确性可以通过试用来判断。如果我要做一个网站，展示自己举办的一场聚会的信息，我会检查网站是否呈现了所有想要的信息。如果只是朋友间的聚会，这大概已经足够。如果是工作聚会，除了电脑，我还会在手机上试用，甚至可能请几位使用不同设备的朋友检查，确保一切正常。
即使在这个例子中，正确性的重要程度也取决于具体情境。领域和规模不同，验证正确性的机制也会随之改变。为商业应用开发软件时，公司会聘请专门负责“试用”的人员，也就是 QA，让他们走遍程序中的许多路径，找出意外行为，也就是bug。除了试用，典型公司还会投入大量时间测试代码；测试的严谨程度取决于用户规模、所涉资金和应用领域的重要性。一家小型 SaaS 公司可能只会编写覆盖若干场景的集成测试，或为部分组件实现单元测试；AWS 则会用数学方法证明 S3 实现的正确性，因为它每天要处理 PB 级数据。
根据目前的讨论，LLM 似乎应该能够生成不要求严格正确性的代码库。它或许还能生成测试，甚至为自己写的代码编写证明，对吧？也许 LLM 真能把人类排除在流程之外，由一组智能体自行协作；即便现在还不行，等它们能力更强时或许可行。我在讨论中多次听到这种论点。问题在于，我们尚未考虑代码的可验证性。我们谈到了严谨程度和规模，但要衡量一个领域有多适合 LLM，仅有严谨程度这个参数还不够；我们还需要讨论如何验证 LLM 生成的代码，其中也包括测试代码本身。
让我们退一步，看看 UI 编程，也就是通常所说的前端开发。许多从业者的经验表明，LLM 能根据一条提示词，甚至一张餐巾纸上的草图，生成完整的前端应用。我们也看到 V0 这类专门聚焦 UI 生成的工具。然而，它们在其他领域并没有取得同样的成功，至少没有得到同等程度的普及。对此，一种流行的朴素解释是：LLM 在公共代码仓库上接受训练，而 UI 编程在这些代码中占了很大比重。但这无法解释为什么 LLM 在 Web 服务器应用，也就是通常所说的后端开发中没有那么流行。后端代码或许与 UI 编程一样普遍，而且多样性更低、结构更加规整。
前后端受欢迎程度的差异也有一些心理层面的解释，主要是因为做出光鲜、令人惊艳的 UI，比做出能吸引同等关注的后端容易。因此，对于前后端受欢迎程度或可用性的比较，零散的经验之谈不应受到太多重视。不过，我的假设是：与我们编写代码的其他任何领域相比，UI 都更容易验证。
验证 UI 几乎就是字面意义上的“看”。看到一个网页时，我们几乎可以立刻识别生成的代码在哪些地方偏离了自己的意图，并立即向 LLM 反馈。验证 Web 服务器则需要准备一组测试输入，把它们发送到服务器，可能还要创建某些临时状态，然后检查输出是否符合预期。实际上，后者更适合通过编写测试来验证，而不是靠人试用；相比之下，编写 UI 测试是一个延续了三十年、至今仍未解决的痛点。
上周兴起的“氛围编程游戏”似乎也源于同一个原因。生成的游戏确实令人印象深刻，但它们可以通过试用来验证。这些游戏通常运行在单台服务器上，不保存持久状态；面对复杂的网络或性能问题，它们往往以牺牲用户体验或删除引发问题的功能来绕开，而不是解决问题。这并不是说这种选择无效，但之所以这样选择，并非因为那些问题不重要，而是因为验证其正确性更加困难，需要定制测试基础设施或依靠领域知识。
回到标题：可验证性决定了上限。
**这个上限告诉我们，哪些东西无法通过 LLM 实现，而且智能体方法也解决不了它。**理论上，安全智能体可以为应用添加安全检查，但如果打算产出这段代码的人不亲自验证，这种检查就毫无价值。测试智能体可以为程序添加测试，但在我们确认这些测试符合自身意图之前，测试本身没有意义。
到目前为止，为了说明自己的观点，我一直在从理论层面讨论 LLM 和我们生产软件的方式。现在，我要开始宣讲自己认为我们应该采取的行动。
如果可验证性决定了上限，如果它是使用 LLM 编程的瓶颈，那么自然要问：我们该如何抬高上限，让验证变得更容易？
我认为，我们首先需要承认“软件智能体可以拥有无限能力和无限扩展性”这一理念已经失败。如果可验证性真是上限，再多的智能体也解决不了问题。在我看来，我们需要更好的验证工具和界面。例如，程序员不必亲自阅读 LLM 生成的每项测试，而可以把这些测试归纳成人类可读的形式，当然，归纳本身也有丢失信息的风险。我们还应该更多地采用声明式随机测试方法，例如基于属性的测试：程序员定义一个对所有可能输入都应成立的谓词，再生成随机输入并传给程序，以检验这个谓词。这类方法已经用于提高许多领域中程序的可靠性，却尚未在软件工程界普及。它的优势在于，一个通用谓词比大量单元测试更容易检查和理解，同时还能提供更强的测试能力。
我们需要扩充讨论正确性时使用的词汇。我们需要更广泛地理解性能、安全性、无障碍性和灵活性，理解如何衡量程序的这些品质。只有这样，我们才知道自己希望应用具备什么，也才有验证这些品质的机制。在当前实践中，正确性通常被等同于功能正确性，基本上就是“输入和输出符合预期”；应用的其他大多数要求则被统称为“非功能属性”，而软件工程界总体上一直没有认真衡量和验证它们。
**最后，让我用一个预测作结。**很长时间以来，我一直认为，即使继续改进，LLM 也不会成为优秀的程序员。它们在竞赛编程中的成功改变了我的看法。作为一个已经退役的竞赛程序员，那或许就是我的“李世石时刻”。现在，我虽然仍有所保留，但确实相信，只要拥有完美预言机，LLM 就能在所有领域取得成功。
需要理解的是，这并不意味着 LLM 会成为能够产出百倍之多代码的神，因为在软件工程发挥作用的领域中，几乎没有任何领域拥有完美预言机。所谓完美预言机，是一种每次都能给出“正确或错误”答案的反馈。它几乎只会出现在游戏中，因为现实世界通常不存在完美的正确性模型。游戏的胜负就是一种完美预言机，编写一段能够通过竞赛编程评测系统的程序也是如此。
即使是编程中形式化程度最高的领域，也就是让用户证明代码正确性的定理证明器，也不是完美预言机。它无法告诉你证明进行到一半时是否走在正确道路上，只能告诉你证明是否正确，或你是否陷入困境。我希望这种不完美的预言机已经足以赢下证明这场游戏，也希望 LLM 在自动证明方面能超越我们。如果那一天到来，我们接下来的工作或许是创造新定理，让 LLM 生成代码和证明，再把这类系统安全、可靠地扩展为生产级代码库。
欢迎通过 [email protected] 告诉我你的看法；如果觉得本文有趣，也请分享给其他人。