卡内基梅隆大学与亚马逊联手揭秘：AI写代码越来越厉害，但它真的"懂"自己在写什么吗？

这项由卡内基梅隆大学与亚马逊研究院联合开展的研究，以预印本形式发布于2026年5月，论文编号为arXiv:2605.26457。感兴趣的读者可通过该编号在arXiv平台查阅完整原文。

当我们把一道菜的做法用文字写下来，厨师才能照着做出正确的菜——这个"写法"在软件世界里就叫做"规范"（specification）。近些年来，AI写代码的能力突飞猛进，但有一个关键问题一直被忽视：AI生成的代码是否真的做了它应该做的事？更深层的问题在于，AI能不能把一道用自然语言写成的"菜谱"，准确翻译成一份严格的、可被计算机验证的"标准食谱"？卡内基梅隆大学与亚马逊的研究团队决定正面回答这个问题，并为此专门建造了一套完整的测试系统。

研究团队搭建了一个名为VERUS-SPECGYM的测试环境，以及一套包含581道题目的题库VERUS-SPECBENCH，专门用来考察AI模型能否把编程竞赛题目的中文自然语言描述，转化为一份可被机器严格验证的"菜谱"——这个过程他们称之为"规范自动形式化"。结果发现，即便是最强的前沿AI模型，也只能完成不到八成的任务，而开源模型的成绩更是惨淡。这项研究揭示了一个容易被忽视的瓶颈：AI写出正确的代码，和AI真正"理解"任务要求，是两件截然不同的事。

一、为什么"菜谱写对了"和"菜做对了"是两回事

要理解这项研究的意义，先来思考这样一个场景：你去餐厅点了一份"不加辣的红烧肉"，厨师端来一盘确实没有辣椒的菜，但里面用了大量花椒——从严格意义上说，花椒也是辛辣调料，你的要求其实没有被满足。问题出在哪？不是厨师手艺不好，而是那份"不加辣"的要求本身描述得不够精确。

软件开发中的情况完全一样。当一个程序经过"形式化验证"（formal verification）之后，计算机会保证这个程序严格符合某份规范文件的要求。这种保证是数学级别的，非常可靠。但这份保证有一个前提条件——规范文件本身必须准确描述了用户的真实意图。如果规范写错了，哪怕程序通过了所有验证，它实际上仍然可能是个"错误的程序"。

研究团队用一个精妙的比喻来描述这个问题：规范太宽松，就像菜谱上写"加适量盐"——任何一个厨师都能说自己做对了，但菜可能完全不好吃；规范太严格，就像菜谱上写"每一粒米必须煮恰好七分钟"——正确的做法反而可能被判定为错误。

为了精确描述这个问题，研究团队把"规范是否正确"分解成四个维度来检验。第一是"前置条件完整性"：对于所有合法的输入，规范是否都接受？第二是"前置条件健全性"：对于所有非法的输入，规范是否都拒绝？第三是"后置条件完整性"：对于所有正确的输出，规范是否都接受？第四是"后置条件健全性"：对于所有错误的输出，规范是否都拒绝？只有当这四个维度全部通过测试，才能说这份规范真正"忠实地"反映了题目的要求。

用更直观的例子来说：假设有一道二分查找题，要求在一个有序数组中找到目标值第一次出现的位置，找不到则返回-1。前置条件完整性要求：给定一个合法的有序数组，规范必须接受它——如果规范只允许严格递增的数组，那么包含重复元素的合法数组就会被错误拒绝。前置条件健全性要求：一个无序数组不应该被接受。后置条件完整性要求：当答案确实是-1时，规范必须接受-1这个输出。后置条件健全性要求：如果目标值在数组中第二次出现的位置被作为答案返回，规范必须拒绝——因为题目要求的是"第一次出现"。

二、一套精妙的"自动阅卷机器"是如何建造出来的

要评判AI写出的规范是否正确，本身就是个难题。研究团队面临的困境类似于：如何在没有标准答案的情况下，判断一道填空题是否做对了？

一种方法是请专家来判断，但请专家为581道题各写一份参考答案，成本高得惊人。另一种方法是用另一个AI来当"评卷老师"，但AI评卷员可能和出题AI犯同样的错误，无法识别那些微妙的漏洞。

研究团队选择了第三条路：把规范变成可以运行的代码，然后用真实的测试数据来检验它。这个思路听起来简单，但实现起来颇有技巧。

规范在Verus（一种专门用于验证Rust代码的工具）中被写成逻辑谓词，类似于数学公式，并不能直接当作普通程序来运行。研究团队扩展了Verus内置的一个叫做`exec_spec`的机制，让它能够自动把这些逻辑公式"翻译"成可执行的Rust函数，进而在真实输入上运行，得到一个明确的"接受"或"拒绝"的答案。这就好比把一道数学定义题里的"充要条件"，自动转化成一段可以在电脑上运行的验证程序。

这套翻译机制支持了相当丰富的数据类型，包括序列（类似列表）、集合、多重集合和映射（类似字典），同时还支持多变量的量词表达式，比如"对所有满足某条件的下标i和j，都有某个性质成立"这样的语句。对于每一道题目的每一个测试样例，评卷流程分两步进行：先尝试用数学推理（SMT求解器）来直接证明规范是否接受或拒绝这个测试样例；如果数学推理在规定时间内无法得出结论，就转而把规范编译成可执行代码，直接运行一遍得到答案。

测试数据的来源同样经过精心设计。官方Codeforces题目自带的测试数据被用来填充"合法输入"和"正确输出"两个类别。但仅有这些还不够——这些官方测试数据往往无法覆盖所有边界情况，很容易让一个"差不多正确"的规范侥幸通过。研究团队的关键创新在于，他们额外引入了Codeforces竞赛平台上的"hack"数据。

在Codeforces竞赛中，当一名参赛者提交了代码并通过了官方测试之后，其他参赛者可以尝试构造一个特殊输入来"攻破"这份代码——这就叫做hack。能够成功hack的输入，往往是那些极其边缘的情况，比如违反了题目里某个容易忽视的隐含条件，或者能让一个功能上基本正确但细节有误的程序产生错误输出。这些由真实人类精心设计的对抗性测试样例，正好能精准识别规范中的细微漏洞。

研究团队把hack数据按照结果进行分类。如果Codeforces判断hack的输入本身是非法的，就把它加入"非法输入"测试集；如果输入合法但被攻击的程序给出了错误输出，就把这个"输入-错误输出"对加入"错误输出"测试集。这样，四个测试维度都有了充足且高质量的数据支撑。

三、从一道竞赛题到一份可验证的规范，中间有多少道工序

研究团队还需要解决一个工程层面的难题：Codeforces题目的测试数据都是纯文本格式，而Verus规范需要的是有类型的结构化数据。把文本格式的"5\n10 20 20 20 30\n20"翻译成一个包含数组和整数字段的Rust结构体，本身就需要相当精细的工作。

为了批量完成这项转换，研究团队训练了一个"转换代理"（基于gpt5.3-codex运行在SWE-AGENT框架上），让它自动为每道题目生成一对工具：一个"解析器"（把文本转成结构体）和一个"打印器"（把结构体转回文本）。判断这对工具是否正确的标准非常简单也非常严格：把原始测试数据用解析器转成结构体，再用打印器转回文本，结果必须和原始数据一字不差。

这个"解析-打印-比对"的回环检验，确保了每一个测试样例在类型转换过程中没有丢失任何信息。如果某道题目的转换失败率太高，或者某个测试维度的样例数量不足5个，这道题就会从题库中剔除。经过这一系列筛选，最终形成了包含581道题目的VERUS-SPECBENCH。这581道题目涵盖了从800分到2700分的难度范围，主题从基础实现题到数学、贪心、动态规划、图论等各类算法题均有覆盖，每道题平均拥有约21个"非法输入"样例、80个"合法输入"样例、55个"错误输出"样例和78个"正确输出"样例。

四、AI模型在这场考试里表现如何

研究团队选取了六个具有代表性的AI模型来接受这套测试系统的考核，包括三个闭源前沿模型（gemini-3.1pro、gpt5.3-codex、opus4.6）和三个开源模型（deepseek-v4pro、glm-5.1、kimi-k2.6）。每个模型在每道题上的预算是2.5美元，时间上限是75分钟，运行在SWE-AGENT交互框架中，可以读写文件、调用Verus验证器、查阅文档，并根据验证反馈反复修改规范。

考试结果分出了明显的梯队。最强的gemini-3.1pro能够通过77.8%的题目，gpt5.3-codex排在第二位，通过率为57.8%，opus4.6以51.1%的通过率位列第三。三个开源模型的表现则相当惨淡，通过率分布在21.5%到25.5%之间——差不多是闭源模型的三分之一。

更细致地看四个测试维度，gemini-3.1pro在"合法输入"测试上通过了92.6%的样例，在"正确输出"测试上通过了89.2%，在"非法输入"测试上通过了90.9%，在"错误输出"测试上通过了89.1%。gpt5.3-codex的四项数据分别是91.0%、87.8%、82.6%、76.6%。相比之下，开源模型的四项数据都在35%到42%之间徘徊，显示出根本性的能力差距。

一个非常有趣的发现出现在"写代码"和"写规范"的对比实验中。研究团队专门挑选了那些gpt5.3-codex写规范失败、但每个输入只对应唯一正确输出的题目（共187道），然后测试同一个模型能否用Python写出正确的代码来解决这些题目。结果，模型用Python写代码的成功率高达81.8%——换句话说，模型明明知道怎么解这道题，却仍然无法把正确的解题要求准确地写成规范。这说明"理解一道题的解法"和"精确描述这道题的要求"在认知层面是两件截然不同的任务，AI在后者上还有很长的路要走。

五、AI写规范时最容易在哪里翻车

研究团队通过大量案例分析，归纳出了三类最常见的失败模式，每一类都值得仔细了解，因为它们揭示了规范"失真"的不同机制。

第一类是"前置条件太宽松"——规范接受了本不应该接受的输入。一个典型案例来自Codeforces 1028C题目，要求在n个矩形中找到至少被n-1个矩形覆盖的一个整数坐标点。题目中有一个关键的隐含保证：这n个矩形里必然存在某n-1个共享一个公共点。gpt5.3-codex和gemini-3.1pro在写前置条件时，都只检查了每个矩形的坐标是否在合法范围内，完全没有捕捉到"某n-1个矩形必须有公共交点"这个全局性约束。于是，当hack数据给出三个互不相交的矩形时，两个模型的规范都错误地接受了这个非法输入。这个被遗漏的条件其实是整道题能够求解的核心前提，缺少了它，任何验证过的代码实际上都无法保证正确性。

第二类是"后置条件太宽松"——规范接受了本不应该接受的错误输出。Codeforces 1051B题要求把区间[l,r]内的所有整数配成若干对，每对的最大公约数必须等于1。gpt5.3-codex写的后置条件只检查了每对数字"不同时为偶数"——这是互质的必要条件，但远非充分条件。于是，(3, 6)这样一对数字，因为3是奇数，就通过了检验，但它们的最大公约数是3，完全不满足题目要求。另一个例子来自Codeforces 1027C，要求从一堆棍子里选出四根组成周长平方除以面积之比最小的矩形。gpt5.3-codex写的后置条件检查了输出的矩形是否可以由输入中的棍子组成，却完全没有检查这个矩形是否是比值最小的那个。结果，任何一个合法的矩形都能通过检验，包括那些远非最优解的结果。kimi-k2.6在同一道题上的表现更糟，写出的后置条件只要求四个输出数字构成"两对相等的数"，连"这四根棍子必须来自输入"这一基本要求都没有写进去。

第三类是"后置条件太严格"——规范拒绝了实际上正确的输出。Codeforces 2074D要求计算n个以x轴为圆心的圆所覆盖的整数坐标点总数。gemini-3.1pro为了精确表达"圆的并集覆盖了哪些点"，写出了一套基于水平区间的复杂计算逻辑：先收集每个y坐标上所有圆覆盖的x坐标区间，再排序、合并相邻区间、求和。这个逻辑在概念上是正确的，但实现上出现了问题——对于五个圆心都在原点、半径均为2的圆，正确答案显然是13个整数点（单个半径为2的圆覆盖的点），但gemini-3.1pro的规范在执行中拒绝了这个答案。相比之下，opus4.6用了一个更简洁的几何思路：对于每个整数x坐标，找出所有覆盖该x坐标的圆中最大的垂直覆盖高度，然后计算该高度对应的整数点数量，最后对所有x坐标求和。这种更高层次的数学抽象反而更不容易出错，也顺利通过了所有测试。

六、几个关键设计选择为何至关重要

研究团队还通过一系列对比实验，验证了评测体系中几个关键设计选择的价值。

首先是"健全性测试必不可少"。如果只看"完整性测试"（即规范是否接受了所有合法情况），gpt5.3-codex的通过率会从57.8%上升到76.6%；gemini-3.1pro会从77.8%上升到82.4%；opus4.6会从51.1%上升到58.7%。这些虚高的数字说明，有相当一部分模型写出的规范虽然不会误判合法情况，却会把错误的情况也一并接受。没有健全性测试，这些漏洞就会被完全掩盖。

其次是"hack数据的价值"。研究团队发现，增加测试样例数量确实能暴露更多规范漏洞，但边际收益递减——测试样例从少量增加到约50-75个时效果显著，之后曲线趋于平缓。hack数据之所以特别有价值，恰恰在于它们是由人类针对真实提交代码的漏洞精心设计的，能够覆盖那些系统性随机测试很难发现的边缘情况。事实上，在实验中有相当比例的规范失败案例，只有在引入hack数据之后才被发现，官方测试数据无法独立暴露这些问题。

然后是`exec_spec`机制的关键作用。在整个评测过程中，有大量规范无法被纯数学推理（SMT求解器）直接判定——尤其是在后置条件的测试上，数学推理经常面对过于复杂的输出关系而无能为力。正是`exec_spec`的运行时执行能力补充了这一空缺。以gemini-3.1pro为例，在后置条件测试上，通过运行时执行得到判断的样例数量远多于纯数学推理得到判断的数量。如果没有这个运行时执行机制，大量测试样例会停留在"无法判断"的状态，整个评测系统就失去了意义。

最后是"AI评委远不如运行测试可靠"。研究团队还专门用gpt5.3-codex来评判它自己写的规范——把题目描述和生成的规范都提供给模型，让它判断规范是否正确。结果显示，在191个被运行测试判定为错误但编译通过的规范中，AI评委有49个（25.7%）被错误地判定为正确。换句话说，四分之一的规范错误逃过了AI评委的眼睛，但没有逃过运行测试。这清晰地说明，可执行的测试驱动评估比让AI自己"阅卷"要可靠得多。

七、这套测试环境本身是如何运作的

值得详细了解的是AI模型在这套系统中实际上的工作方式，因为它模拟了真实的软件开发场景，而不只是简单地要求模型输出一段文字。

每道题目对应一个工作目录，其中包含：题目的自然语言描述、一个预先定义好输入输出数据结构的Rust代码框架（agent只需填写两个函数的函数体）、三个可见的测试样例（仅来自完整性测试维度，不提供健全性测试样例）、一道其他题目的参考规范示例、Verus的完整文档、评测系统的源代码，以及一份由Verus专家撰写的详细任务说明。

Agent在工作时可以读写文件、在终端执行命令，通过运行`verus_gym_specgen_check`命令来对当前规范进行本地测试，并根据测试反馈（包括具体的Verus错误信息）修改规范，然后再次测试，形成迭代循环。当agent认为规范已经足够好时，可以提交。提交后，系统会用包含隐藏样例的完整测试集进行最终评判。

在代码框架中，agent需要填写的两个函数分别是`pre_spec`（前置条件，描述合法输入的特征）和`post_spec`（后置条件，描述对于给定输入什么样的输出是正确的）。框架里还预留了四个可选的"辅助证明函数"，agent可以在其中填写一些帮助Verus数学推理的提示，但这不是必须的。如果数学推理需要这些提示，agent可以选择填写；如果规范本身足够简单，留空也没有关系。

值得注意的是，输入输出的数据结构类型是由前期的转换流水线固定好的，agent不能修改这些类型定义——这确保了规范的评估是在统一的数据表示下进行的，不同agent的结果之间具有可比性。

八、这项研究指向的更大图景

从实验数据中还能读出一些令人深思的规律。把三个闭源模型的解题结果画成韦恩图，可以发现有214道题三个模型都能解，但三个模型合并起来可以解486道题——远超任何单一模型的能力边界。这说明不同模型的失败模式有相当程度的互补性，gemini-3.1pro贡献了最多的独有成功案例（84道），而opus4.6的成功案例基本都被其他两个模型所覆盖。

重复实验的结果也揭示了一个稳定性问题。让gpt5.3-codex独立运行三次，成功率分别是57.8%、55.9%和56.6%，相差不大；但三次合并后的成功率（至少一次成功的题目比例）高达75.6%，而三次全部成功的题目比例仅有34.8%。这个巨大的落差说明，即便模型有能力解一道题，它也经常无法稳定地做到，失败往往是随机的而非系统性的。

随着题目难度的增加，所有模型的成功率都稳定下降。gemini-3.1pro在难度800-900的简单题上成功率高达90%，但在难度2400-2700的高难度题上跌至50%；gpt5.3-codex从73%跌至27%；开源模型在2100分以上的题目上几乎全军覆没。即便如此，"在最简单的题目上仍有10-16%的失败率"这个数字依然值得关注——这说明规范形式化的难点不完全来自算法理解，很多简单题目中也隐藏着容易被忽视的边界条件和隐含约束。

说到底，这项研究做的事情可以用一句话来概括：它建造了一面镜子，让我们第一次清晰地看到AI在"理解任务要求"这件事上究竟做到了什么程度。答案是：当前的前沿AI能做到相当不错，但还远未达到可以放心使用的水平——而且它最容易在那些"知道怎么做但没说清楚要做什么"的地方犯错。

对于软件开发的未来而言，这个发现的意义不容小觑。随着AI越来越多地介入代码生成，我们或许会进入一个"AI写代码、人类无法完全审查"的时代。在这种情况下，形式化验证本来可以作为一道重要的质量关卡——但如果连"质量标准"（规范）本身都是由AI来写，而AI写出的标准又不可靠，这道关卡就形同虚设。这项研究提出的问题，以及它提供的测试工具，正是对这一挑战的正面回应。

对于关心AI可靠性的普通人来说，一个值得思考的问题是：当银行的风控系统、医疗诊断软件或自动驾驶算法都开始由AI来生成时，我们如何确保它们真的在做我们希望它们做的事，而不只是做了一件"看起来差不多"的事？这项研究表明，回答这个问题需要的不只是更好的代码生成能力，还需要更好的"意图表达"能力——而目前，即便是最强的AI模型，在这一点上仍然存在明显的短板。有兴趣深入了解这套测试系统技术细节的读者，可以通过arXiv编号2605.26457查阅完整论文，或访问该项目的开源代码仓库进一步探索。

Q&A

Q1：规范自动形式化（specification autoformalization）是什么意思，和普通写代码有什么区别？

A：规范自动形式化指的是把用自然语言写的程序要求，翻译成一份计算机能够严格验证的"精确说明书"。普通写代码是告诉计算机"怎么做"，而规范是在说"做成什么样才算对"。两者看似相关，但在认知上有本质区别——实验发现，AI用Python写对代码的成功率高达81.8%，但写出正确规范的成功率却低得多，说明"会解题"和"能精确描述解题标准"是两种不同的能力。

Q2：VERUS-SPECBENCH里的Codeforces hack测试数据和普通测试数据有什么不同，为什么特别有用？

A：普通测试数据往往覆盖常见情况，而Codeforces hack数据是竞赛中人类玩家专门为了击破别人代码而设计的边缘案例，针对那些"基本正确但细节有误"的程序。实验证明，有相当比例的规范错误只有hack数据才能发现，普通测试数据完全无法暴露这些漏洞。

Q3：为什么用AI来评判AI写的规范不可靠？

A：实验中让gpt5.3-codex评判自己写的规范，发现它有25.7%的概率把错误规范误判为正确。AI评委和出题AI容易犯相同类型的错误，对那些看起来合理但实际有细微漏洞的规范缺乏辨别能力。相比之下，用真实测试数据直接运行规范得到的判断更客观、更可靠，能够发现AI评委看不出来的具体反例。