AI 生成代码的验证方案
两周前我开始讨论我们为非人类代码创建"非人类"测试和验证系统的潜在前进路径。我们不可能把大量AI生成代码的精灵塞回瓶子里。没有"逆转"这个行业工作方式的结构性变化。我们需要一个向前修复的方案。
我也一直在遭受"AI吸血鬼"问题的困扰。由于没有合理管理自己的工作量和休息，使用氛围编码工具让我感到有些倦怠。解决方案不是"完全不用这些工具"。我们同样需要一个向前修复的方案，它看起来会很像运动员的做法。我们将在通讯的后半部分讨论这一点。
上周我在YouTube上看了Anthropic的"Code with Claude"大会直播，在多个演讲中我看到了测试和验证方面潜在的前进修复方案的证据。Datadog的演讲是最好的一个。
在与Boris Cherny和Jarred Sumner的一个环节中，他们提到Bun包管理器正在进行一个从Zig到Rust的移植。自我最初写这篇文章以来，他们已经合并了这个PR！我让Claude看一下这个PR以获取一些经验教训，虽然他们不使用形式化验证方法，但他们确实有一个相当广泛的多代理驱动的规范和验证移植过程。
我还在最近一期Joe Rogan与Chamath Palihapitiya（All-in播客）的节目中听到了验证改进的证据。Chamath深入讲述了他如何将8090公司参与的政府合同项目，将遗留代码转化为英文规范，并确保他们编码的行为确实是他们想让代码做的事情。Chamath声称这将帮助消除浪费，更准确地自动化政府的更多工作。
1、一个公开的秘密
在我看来，这似乎几乎是一个公开的秘密——每个人都在推进验证作为行业方向，但没有人对他们特别自豪或准备好公开讨论的答案。没有人站在屋顶上大声宣扬他们伟大的方法，或者至少登上Hacker News的头条。
我只看到人们使用规范和验证语言的暗示（这将在本文后半部分变得重要）。比如"不变量"和"属性测试"。我在Hacker News上看到的关于"形式化验证"的唯一实际提及是Martin Kleppman在2025年12月预测形式化方法成为主流的帖子以及围绕它的讨论。我没有看到一个明确的"嘿，这就是我们正在做的，以及你也可以这样做"的声明。
我认为非常有趣的是，这仍然可能有一些alpha（或"优势"）。人们可能在把守如何使AI代理编码对其公司比竞争对手更有效的方法。或者也许这个过程是如此针对每个公司定制化，以至于发布你的方法对其他人可能根本不适用。或者也许没有人真正知道自己在做什么。我倾向于第一种和第三种解释。
2、为时过早还是过度杀戮？
传统上，只有处理健康、安全或密码学基础的高度任务关键系统才使用形式化验证来证明规范被正确实现。但就像我们现在处于AI生成代码的挂果林中一样，形式化验证软件的门槛也从未如此之低。
如果有人为你的软件付了很多钱，他们会期望它正常工作。你可以通过各种级别的测试覆盖率来实现这一点，但形式化证明某些功能按照你的规范运作会增加另一层信心。我们可能会看到更多公司和团队朝这个方向前进，特别是如果你要淡化或完全移除人工代码审查，因为每个PR生成的代码量现在是非人类的。作为一个行业，我们需要开发一个非人类的过程来处理非人类数量的代码。
3、一个非人类的、"不人道"的过程
形式化验证当然还没有成为整个行业的标准实践。对于错过我上一期通讯的人来说，形式化验证是——在咨询了Claude之后——一组证明你的代码与你规范中所写的内容匹配的方法。
想想高中几何课上的数学证明。升级版是大一计算机科学课上的离散数学证明。基本上，我们不只是测试，而是数学上证明代码完全按照我们的规范工作，这是一个比任何单个测试都强得多的断言。输入、输出以及它们之间的转换完全符合我们在规范中定义的；不多也不少。
15年前作为大学新生那是一种不人道的痛苦，现在它可能是AI生成代码管道中的一个基本必需品。
我只思考了两周，但这个问题在过去六个月左右——自从代理成为每家公司的标配以来——已经开始困扰整个行业。人类应该审查多少？如果没有人真正编写了代码，人类甚至能做好审查工作吗？
如果我要开始一个新项目，并且有依赖我的应用程序做我说它要做的事情的客户，我肯定会使用一定数量的形式化验证方法。它只是在开发过程的开头和结尾增加一个额外的阶段，如果你正在使用任何编排程度的代理，这对你来说并不重要。
4、瑞士奶酪层
Datadog的Sesh Nalla在他的"Code with Claude"演讲中描述他们的代码发布过程具有"瑞士奶酪层"。你以为瑞士奶酪上有很多洞，但如果你有不同的洞在不同位置的切片，那么它就是一个有效的过滤机制，可以希望在问题进入生产之前捕获许多（如果不是全部）不同类型的问题。
这或多或少是我在上一期通讯中提出的：我们需要非人类代码的非人类管道。我一直说我们需要将测试、验证和确认提高10倍，但这只是模糊的说法。好消息是，让我们的AI代理编写代码来加强我们防御bug的能力使得这变得更容易、更具体。因为我们可以让代理管理测试，所以几乎不管我们添加多少测试都没关系。
当然，我们仍然希望能够在一小时内从代码变更到生产部署（或者我们需要吗？这重要吗？那是AI之前的DORA指标标准，但部署速度听起来仍然很好，能够修复变更）。这只是关于每次代码变更我们想在计算和token上花费多少美元的问题。这是一个经济学问题，对每个项目都不同。
前进中企业面临的关键问题是：你每投入1美元的token，能获得多少美元的商业价值？
SaaS企业以前将云支出中的美元翻转为商业价值。前进中的企业现在正在将token支出中的美元翻转为商业价值。这是前进中的关键技巧。
你能在token上添加什么别人不能的东西？你的视角。
5、不要过早优化
我发现当开发者听到"优化支出"时，他们默认认为这意味着"最小化支出"。我试图提醒开发者，我们的时间和理智仍然是任何企业最高的持续成本。我们需要继续倡导节省我们时间和劳苦的工具，这样我们就能专注于交付最高的ROI商业价值。
我们不想在我们甚至还没弄清楚需要花费多少的时候就考虑节省token支出。我不主张为了花钱而花钱，但当我们甚至还没有实现六个月前模型的价值时，我们应该摆脱斤斤计较的心态。你需要花钱才能赚钱。
到目前为止我用了许多软件开发行业特有的词。如果你完全不知道这些词，读起来会有什么不同？我几乎不记得大一离散数学课程中的"形式化验证"这个词了。但我仍然模糊地知道它是什么，并且我可以把这个术语输入LLM开始取得进展。
6、关于魔法的一点说明
知识仍然是力量，即使Sam Altman想要对你的AI访问进行计量。以下是我对LLM最终推动世界上人类智能增长的看好理由。你知道或至少意识到的越多，使用这些工具的效果就越好。
仅仅知道有一个叫做"形式化验证"的事情可以做，就能让你用AI代理释放一个新的魔法咒语。你甚至不需要知道它"数学上证明规范可以准确地转化为代码"。如果你知道魔法词或者接近"形式化验证"的概念，LLM就能给你这个定义。否则，这是模型中一个完全无法触及的部分。
我在与非技术的氛围编码兄弟交谈时注意到了这一点：他不知道他不知道什么。我可以给他一些关于项目下一步该怎么走或者什么可以做得更好的提示，但仅仅通过让Claude让他的项目更接近他想要的样子，他已经走得很远了。
我认为这种在细节中的自我引导、超个性化的战术学习方法是非常有用和颠覆性的，但我们还需要为在LLM之外的、人类可以引导我们通过他们对某个主题的视角的战略性、大局性的高层次学习腾出时间。又出现了那个词。
他最近抱怨说他必须用各种氛围编码云托管服务"把所有东西连接起来"。我问他说的"连接"是什么意思，听起来他必须手动将应用程序的不同部分部署到不同的服务，然后更新每个服务上的一堆环境变量来让它们互相指向——他竟然知道什么是"环境变量"这件事太疯狂了，而且对他项目目前的阶段来说可能仍然是一个合适的解决方案。
我大致告诉他："如果我告诉你所有这些都以某种方式托管在AWS上，而AWS才是所有这些真正的底层基础设施呢？如果你只想让所有东西自动连接在一起，你可以写一些Terraform然后自己部署到AWS。托管的氛围编码服务是有观点的封装，可以防止你搬起石头砸自己的脚。"
我的兄弟：🤯
他只是不知道他不知道什么。
7、未知的未知
我觉得形式化验证也是同样的道理。我注意到行业中有些人在描述规范时使用了不同的术语，比如"不变量"。我对"不变量"的主要理解是在运动训练的约束主导方法（CLA）中。听到它们被用在这个计算机科学上下文中很令人震惊。我不知道的是，使用这些词的人都在指向同一件事：更好的规范，从而带来更好的、更形式化的验证。
行业中没有人明确大声地说，"嘿，这就是我们在做的来验证我们的AI生成代码！"。现在只是一个灰色地带，因为它仍然很新。没有人真正知道自己在做什么，从而有信心说他们的方法明确是最佳实践，尤其是当这是一个有许多博士生花了毕生精力的深度领域时。
我相信我们前进工作中的很大一部分将是阅读技术和非技术材料，以获得关于LLM可以实现什么的新想法和视角。也就是说，为了学习而学习。如果LLM已经阅读了所有现存书籍和公共互联网的每个角落，我们如何调用最高的alpha，即最少已知的部分？
有类似我兄弟经历的未知未知，我们前进的工作可能是将这组知识缩小到尽可能小。我们现在只能通过掌握书面语言及其描述的所有概念来做到这一点。我们需要拓宽我们对可能性的视野，以调用LLM的不同部分，让它以不同方式"思考"。
8、什么……所以我必须一直学习？一辈子？！？
我们现在处于全人类知识的学习曲线上。我们一直都是，但现在由于AI代理的存在，它对每个人都更加明显和可及。爬升这条学习曲线比以往任何时候都更重要、更有回报。
我认为所有学习曲线都是"指数级的"[2]，或者为了讨论起见至少是二次的（来源：相信我兄弟）。指数可以是任何大于1的数字，比如1.1或1.00001，但下面用2来更好地说明例子。需要记住的重要概念是，学习在人类和机器中都是复利的。
你学得越多，你的学习速度就越快。你的心智模型脚手架越多，你就越能附加新想法并让它们记住。记住的想法越多，它们就能交叉授粉，使未来学习新事物变得更容易，等等。我相信学习的"二阶导数"或"加速度"是正的。
给那些忘记的人一个快速的微积分课。别担心，它超级简单且拓展思维。你读到这里是因为你已经喜欢学习了。数学只是一种结构化的思考方式。
一个简单的"二次"（指数中的2）方程是 y = x²
这意味着y的值等于x乘以x。例如，y = 1×1，y = 2×2，y = 3×3，等等。
你可以看到，对于x的每个值，它以越来越快的速度上升。注意在x = 12时，y = 12×12 = 144。线性关系看起来像y = x，其中x = 12，y也等于12。
在物理学中，我们称第一个图为物体的"位置"。你可以把它想象成跟踪汽车旅行距离的里程表。在x = 10小时时，你已经行驶了100英里。在x = 20小时时，你已经行驶了400英里。在40小时时会是多少？
那是一辆不断加速的汽车，工程设计上根本不可能！剧透：这是你的大脑。
微积分的部分是这个图的导数或变化率可以通过将2移到x旁边来表示。y = 2x。别问我为什么，我老实说我忘了。这就是一个数学事实。
y = 2x这个图代表的概念是"你知道得越多，每次向现有知识库添加新东西时建立新连接的速度也在增加"。为了讨论起见，你每学到1件事，建立连接的速度可以增加2，或者每单位时间等等。
再做一次求导。二阶导数是y = 2。x消失了。规则就是这样。
这显示了在我们整个"汽车旅行"过程中持续的正加速度。加速度显示变化率的变化率。每次我们学到新东西时，学习速度增长率上升2。实际上，这种学习加速可能在童年达到顶峰，然后在我们的余生中随着认知健康的变化而波动。
这个值 > 1 只是说明学习是复利的。如果这个"加速"值为0，那么我们将以线性方式学习，知道更多东西不会让学习新东西变得更容易。学习新事物将需要恒定的努力量。既然我想我们都同意，你知道得越多，添加知识就越容易，我们可以同意这个值大于1。
再说一次，上面的数字都是编造的，但这是一个赋予力量的、方向正确的学习模型。
9、学习类比的TL;DR
学习进度在时间上（x轴）看起来是线性的，但y轴的值有一个大于1的指数，这意味着学习是复利的。二阶导数或学习加速度是正的，这意味着学习更多能提高你未来的学习速度。
鉴于所有关于学习的解释，我们如何将其应用于与AI代理合作？
10、要想变好，我们必须断联
我认为每个人花大量时间与AI代理在一起，试图弄清楚如何最有效地使用它们，这很好。然而，这现在只是一个有效工程师的入场门槛。
LLM说的语言是书面文字。如果你不擅长用文字表达自己，你如何才能访问LLM和它包含的知识的深层部分？
你可以尝试通过递归地问它问题来自我探索。你能够持续问出越来越好的问题，这就是这项技术令人难以置信的自我引导力量。
我也相信有一种互补的方式：阅读LLM以人类编写书籍形式编码的大量知识。这给了我们从特定人类视角出发的新想法和更好的问题。
"技术宅发现了老式阅读"
令人震惊，我知道，但我认为有意识地每周腾出时间来断开代理的使用，对我们长期追求的可持续性将非常重要。
直到两周前，我甚至都没有想过形式化验证或就此询问LLM。直到我有了这个想法这样做，它才向我揭示了它的秘密。这有点像我在2025年11-12月的一个想法的延伸：如果我们将成为这些LLM的管理者，我们必须知道该要求它什么才能充分利用它。我相信我们可以通过阅读书籍来做到这一点：技术的、商业的以及其他方面的。
如果你能让代理"嘿，优化这个AWS网络配置的负载均衡"，你必须至少知道这些词中一些的存在才能问它。一旦你知道了这些词，如果你能朝那个方向推动它，它可能大部分都能解决问题。
这意味着我们需要大量的技术和领域特定术语词汇，以对代理拥有最大的选择性和掌控力。这不仅意味着对技术概念的掌握，还意味着对我们试图为之编写代码的领域特定概念的掌握。这些领域特定的想法可能与你试图解决的特定问题是正交的或互补的。任何可以帮助访问模型最深处的信息。
因为每个人都在使用这些工具并问它们类似的事情，如果你能问一个代理不同的事情，你会得到不同的结果。这就是字面意义上的商业差异化。通过吸收新信息和接受新想法，你可能会受到启发，创造出不像其他人正在做的事情的东西。
我们可以仅仅通过与LLM自我引导和自学就走出相当远，只需问它"嘿，我们应该做什么？"如果我们成为更好的学生，我们将有更好的问题问它，而这需要先验知识。
提出更好的问题是需要培养的关键技能。
我认为更多地断联和做更多模拟活动将使我们保持身心健康，最终使我们在氛围编码这件事上做得更好。这是一场马拉松，不是短跑。
11、像运动员一样对待氛围编码
当我连续训练巴西柔术太多天时，它总是压垮我的中枢神经系统（CNS）然后我就生病了。尤其是当我报名参加比赛时。仅仅知道前方有一场比赛就是对我的系统的额外巨大压力源。我经常在比赛前或比赛后生病。
在没有任何特定月份或年份的高峰点，没有任何可以借此休息的比赛，氛围编码将成为一个持续的、不断增加的压力源，对于不善于管理的人来说肯定会引向倦怠和健康问题。长时间无调节的高表现是不健康的。一周七天不做任何休息地做任何要求高的事情都是不健康的。
我们需要休息日。我们需要拔掉插头。我们都还在摸索中。我认为这是长期使用这些工具最重要的事情：我们必须与它们保持健康的距离，把它当作我们可以控制的刺激。
举重的一句格言是我们要刺激，而不是毁灭。我们必须将周期化训练原则应用于氛围编码，因为正如Stevie Yegge在"AI吸血鬼"一文中所说，使用代理编码会加剧工作。我们不能再假装它和手动编码是一样的了。
我们需要建立断联日甚至每日断联时间，以保持身心健康。我想通过说通过阅读，我们仍然在推进我们的代理软件开发技能，即使我们没有直接做这件事本身，来给你一点甜头。
就像运动员不能仅仅通过他们的运动来维持身体一样。运动员需要做补充性的力量和体能训练，以保持健康并拥有成功的长期职业生涯。
我知道现在很可怕，到处都在谈论K型经济，裁员和大规模失业的威胁迫在眉睫。只要记住，如果你没有身心健康，其他一切都不重要。你的健康是所有这些有趣的、令人兴奋的、要求高的、具有挑战性的和有回报的事情的基础。
我一度忽略了自己的健康，因为我想在这个AI编码趋势中保持领先。现在我正在重新专注于每天运动身体和吃好的食物，这最终将支持我的长期氛围编码表现。我认为我用AI编码的初始冲刺已经完成，真正的长期收益将在未来几年以可持续的方式，日复一日地实现。
原文链接：The Fix-Forward Solutions to AI Coding Problems
汇智网翻译整理，转载请标明出处