聊天机器人能否编写正确代码？

我最近参加了在纽约举行的AI工程师代码峰会，这是一个仅限受邀参加的AI领导者和工程师聚会。在与正在使用AI构建产品的与会者交谈中，一个主题反复出现：我们正接近这样一个未来，开发者将永远不再需要查看代码。当我追问这些支持者时，他们给出了一个相似的论点：

四十年前，当像C这样的高级编程语言日益流行时，一些守旧派抵制它，因为C给你的控制力不如汇编语言。现在同样的事情正发生在LLM（大语言模型）身上。

表面上，这个类比似乎合理。两者都代表了抽象程度的提升。两者最初都遇到了阻力。两者最终都改变了我们编写软件的方式。但这个类比真的让我觉得不妥，因为它忽略了一个比抽象级别更根本的区别：确定性。

编译器和LLM之间的区别不仅仅是关于控制或抽象。它关乎语义保证。正如我将要论证的，这种差异对软件的安全性和正确性具有深远的影响。

编译器的契约：确定性与语义保留

编译器有一项工作：在改变语法的同时，保留程序员的语义意图。当你在C中编写代码时，编译器会将其转换为汇编语言，但你代码的含义保持不变。编译器可能会选择使用哪些寄存器、是否内联函数或如何优化循环，但它不会改变你程序的功能。如果语义被无意改变，那不是一个特性，而是一个编译器错误。

这种属性——语义保留——是现代编程的基础。当你在Python中写 result = x + y 时，语言保证了加法会发生。解释器可能会优化执行加法的方式，但不会改变要执行的操作。如果它改变了，我们会称之为Python中的一个错误。

从汇编语言到C，到Python，再到Rust的历史进程始终保持着这一属性。是的，我们增加了抽象程度。是的，我们放弃了细粒度的控制。但我们从未放弃过确定性。编程行为仍然是组合性的：你从更简单、定义明确的片段构建复杂系统，而且组合本身是确定且明确的。

在某些罕见的情况下，高级语言的抽象会妨碍程序员语义意图的保留。例如，密码学代码需要在所有可能的输入上以恒定的时间运行；否则，攻击者可以利用时间差异作为预言机来做诸如暴力破解密码之类的事情。像“恒定时间执行”这样的属性，大多数编程语言并不允许程序员指定。直到最近，还没有什么好方法来强制编译器生成恒定时间代码；开发者不得不求助于使用危险的内联汇编。但通过Trail of Bits对LLVM的新扩展，我们现在也能让编译器保留这种语义属性了。

正如我在2017年发表的《自动化的自动化》一文中写到，我们在自动化方面存在根本性的限制。但这些限制并没有消除我们所构建工具中的确定性；它们仅仅意味着我们无法自动证明每个程序的正确性。编译器并不试图证明你的程序是正确的；它们只是忠实地翻译它。

为什么LLM从根本上是不同的

LLM在设计上是非确定性的。这不是一个错误；这是一个特性。但它带来了一些我们需要理解的后果。

实践中的非确定性

将一个提示词运行两次通过同一个LLM，你可能会得到不同的代码。即使温度设置为零，模型的更新也会改变行为。相同的“为此函数添加错误处理”请求可能意味着捕获异常、添加验证检查、返回错误代码或引入日志记录，而LLM每次都可能做出不同的选择。

这对于创意写作或头脑风暴来说没问题。但当你需要代码的语义含义被保留时，就没那么好了。

模糊输入问题

自然语言本质上是模糊的。当你告诉LLM“修复认证漏洞”时，你假设它理解：

你在使用哪个认证系统
在这个上下文中，“漏洞”是什么意思
“修复”看起来是什么样子
必须保留哪些安全属性
你的威胁模型是什么

LLM将基于它认为你表达的意思，自信地生成代码。这与你实际表达的意思是否匹配，是概率性的。

明确输入的问题（其实并不明确）

你可能会说，“好吧，但如果我给LLM明确的输入呢？如果我给出确切的C代码，并说‘把这个C代码翻译成Python’呢？”

问题是：即使这样，也不像看起来那么明确。考虑这个C代码：

1
2
3
4


// C 代码
int increment(int n) {
    return n + 1;
}

我让Claude Opus 4.5（扩展思考）、Gemini 3 Pro和ChatGPT 5.2把这个代码翻译成Python，它们都产生了相同的结果：

1
2
3


# Python 代码
def increment(n: int) -> int:
    return n + 1

这很微妙，但语义已经改变了。在Python中，有符号整数算术具有任意精度。在C语言中，有符号整数溢出是未定义行为：它可能环绕、可能崩溃、可能做任何事。在Python中，这是明确定义的：你会得到一个更大的整数。没有一个领先的基础模型注意到了这个区别。为什么呢？这取决于它们是否在训练中见过强调这种区别的例子，是否在推理时“记得”这个区别，以及是否认为它足够重要需要标记出来。

存在无限多个Python程序，对于所有有效输入，它们的行为都与C代码相同。LLM并不能保证产生其中任何一个。

事实上，如果不知道原始的C开发者期望或打算C编译器如何处理这个边缘情况，LLM不可能精确地翻译代码。开发者知道输入永远不会导致加法溢出吗？或者他们检查了汇编输出，得出结论：他们特定的编译器在溢出时回绕到零，而这种行为在代码的其他地方是必需的？

案例研究：当Claude“修复”了一个不存在的漏洞

让我分享一个最近的经历，它完美地具体化了这个问题。

一位开发者怀疑一个新的开源工具未经许可就复制并开源了他们的代码。他们决定使用Vendetect，一个我在Trail of Bits开发的自动化源代码抄袭检测工具。Vendetect正是为此用例设计的：你将它指向两个Git仓库，它会找出一个仓库中从另一个仓库复制的部分，包括具体的违规提交。

当开发者运行Vendetect时，它崩溃了，并输出了堆栈跟踪。

我被指派去审查这个PR。

不对。

Vendetect的输出现在变成空的了。当我运行单元测试时，它们都失败了。某些东西被破坏了。

我知道在Python中递归是有风险的。Python的栈帧足够大，以至于你在深度递归时很容易溢出堆栈。然而，我也知道，这个特定递归函数的输入被约束为永远只会递归几次。Claude要么错过了这个约束，要么没有被它说服。因此，Claude费力地将函数重写为迭代形式。

并且在这个过程中破坏了逻辑。

我恢复到主分支上的原始代码，并重现了崩溃。经过几分钟的调试，我发现了真正的问题：这根本不是Vendetect的漏洞。

开发者的输入仓库包含两个同名但大小写不同的文件：一个以大写字母开头，另一个以小写字母开头。开发者和我都在macOS上运行，macOS默认使用不区分大小写的文件系统。当Git试图在区分大小写有冲突的仓库上进行操作，而不区分大小写的文件系统上时，它会抛出错误。Vendetect忠实地报告了这个Git错误，但随后用堆栈跟踪显示了Git错误在代码中发生的位置。

我最终修改了Vendetect来处理这个边缘情况，并打印一个更易懂的错误消息，而不是被堆栈跟踪淹没。但Claude如此自信地诊断并“修复”的那个漏洞，根本不存在。Claude“修复”了正常工作的代码，并且在这个过程中破坏了实际功能。

这次经历具体化了问题：LLM对待代码的方式就像一个人第一次查看代码库时的样子：对事情为什么是这样毫无上下文。

那个递归函数在Claude看来是有风险的，因为在Python中递归可能有风险。如果没有上下文——不了解这个特定的递归受到Git仓库结构的限制——Claude做出了一个看似合理的更改。它甚至“有效”了，因为崩溃消失了。只有彻底的测试才揭示它破坏了核心功能。

规模问题：当上下文至关重要时

LLM在拥有清晰规范的新项目上表现相当好。一个简单的Web应用，一个标准的CRUD接口，样板代码。这些都是LLM见过成千上万次的模板。问题是，这些并不是开发者最需要帮助的情况。

把软件架构比作建筑架构。一个预制的棚屋用作存储没问题：需求简单，约束标准，设计可以模板化。这就是你拥有清晰规范的新Web应用。LLM可以生成一些功能性的东西。

但想象一下，用模块化构件迭代地拼凑一座摩天大楼，从一开始就没有连贯的计划。你最终得到的真的就是九龙城寨：功能性的，但难以维护。

图1：Gemini对迭代构建的摩天大楼可能样子的想象。

那么，改造一座有100年历史的建筑呢？你需要知道：

哪些墙是承重墙
公用设施管线在哪里
建造时适用哪些建筑规范
之前的改造如何影响了结构
使用了什么材料以及它们是如何老化的

建筑图纸——原始的、确定性的规范——是必不可少的。你不能仅仅派一个承包商，他第一次看到这栋楼，就开始挥舞大锤，基于看起来正确的东西开工。

遗留代码库正是如此。它们具有：

文档不全的内部API
无人完全理解的脆弱依赖
历史背景（这些无法放入任何上下文窗口）
通过阅读代码并不明显的约束
多年增量需求变化和功能累积而出现的业务逻辑

当你拥有一个复杂的系统，内部API模糊不清，不清楚哪个服务与什么对话或为什么对话，而文档已经过时多年且太大无法放入LLM的上下文窗口时，这正是LLM最有可能自信地做出错误事情的时候。

Vendetect的故事是这个问题的缩影。那些重要的上下文——递归受到Git结构的限制、真正的问题是文件系统的一个怪癖——从代码中看不出来。Claude用看似合理的假设填补了空白。这些假设是错的。

前进之路：形式化验证与新框架

我并不是反对LLM编码助手。在我广泛使用LLM编码工具进行代码生成和漏洞查找的经历中，我发现它们确实有用。它们擅长生成样板代码、建议方法、作为调试时的“橡皮鸭”，以及总结代码。生产力的提升是真实的。

但我们需要对其根本局限性有清晰的认识。

LLM目前表现良好的地方

LLM在最有效时，你拥有：

干净、文档完善、使用惯用语的代码库
全新项目（greenfield projects）
优秀的测试覆盖率，能立即捕获错误
错误能迅速显现的任务（它崩溃了、输出错了），允许LLM迭代地接近目标
由理解上下文的经验丰富的开发者进行结对编程式的审查
由经验丰富的开发者编写的清晰、明确的规范

最后两点对于成功是绝对必要的，但往往还不够。在这些环境中，LLM可以加速开发。生成的代码可能不完美，但错误能很快被捕获，迭代成本很低。

我们需要构建什么

如果最终目标是将开发者的抽象层次提高到无需审查代码，那么我们将需要这些框架和实践：

LLM输出的形式化验证框架。我们需要能够证明语义保留的工具——即LLM的更改保持了代码的预期行为。这很难，但并非不可能。我们已经对某些领域有形式化方法；需要将它们扩展到覆盖LLM生成的代码。
更好的编码上下文和约束的方式。LLM需要的不仅仅是代码；它们需要理解不变量、假设、历史背景。我们需要更好的方法来捕获和传达这些信息。
超越“它崩溃了吗？”的测试框架。我们需要测试语义正确性，而不仅仅是语法有效性。代码是否做了它应该做的事？安全属性是否得到维护？性能特性是否可以接受？单元测试是不够的。
衡量语义正确性的指标。“它能编译”是不够的。甚至“它通过了测试”也是不够的。我们需要量化语义是否已被保留的方法。
可组合、安全设计的构建块。与其允许LLM编写任意代码，我们更需要LLM使用经过验证的安全的、模块化的、可组合的构建块来构建。有点像工业用品已经被商品化成乐高一样的零件。需要一个带D形轴的NEMA 23方形机身步进电机？不需要自己设计和制造——你可以从十几个不同的制造商那里购买商用现货电机，它们都能很好地安装到你的项目中。同样，LLM不应该实现自己的认证流程。它们应该编排预制的认证模块。

信任模型

在我们拥有这些框架之前，我们需要一个清晰的LLM输出心智模型：将其视为来自第一次看到代码库的初级开发者的代码。

这意味着：

始终彻底审查
未经测试绝不合并
理解“看起来正确”并不意味着“就是正确”
记住LLM即使在错误时也很自信
验证解决方案解决了实际问题，而不是一个听起来合理的问题

作为一个概率性系统，LLM总是有可能引入一个漏洞或误解其提示词。（这两者本质上是同一件事。）这个概率需要多小？理想情况下，它应该比人类的错误率更小。我们还没有达到那个水平，还差得远。

结论：在AI时代拥抱验证

自从我在2017年写到这些，自动化的根本计算限制并没有改变。改变的是，我们现在有了工具，使得大规模、自信地生成错误代码变得更加容易。

当我们从汇编语言转向C语言时，我们没有放弃确定性；我们构建了保证语义保留的编译器。随着我们迈向LLM辅助开发，我们需要类似的保证。但解决方案不是拒绝LLM！它们确实为某些任务提供了真正的生产力提升。我们只需要记住，它们的输出只和第一次看到代码库的人写的代码一样可信。就像我们不会在没有审查和测试的情况下合并来自新开发者的PR一样，我们也不能把LLM的输出当作自动正确的。

如果你对形式化验证、自动化测试或构建更可信的AI系统感兴趣，请联系我们。在Trail of Bits，我们正在致力于解决这些问题，并且我们很乐意听到你使用LLM编码工具的经验，无论是成功还是失败。因为现在，我们都在共同学习什么有效、什么无效。我们分享的经验教训越多，我们就越有能力构建我们需要的验证框架。