港科大团队发现：AI代码组合能力存在严重缺陷

这项由香港科技大学的徐旭、李鑫，曼彻斯特大学的瞿星伟，上海AI实验室的傅杰以及香港科技大学的袁斌航共同完成的研究发表于2025年9月，论文编号为arXiv:2509.23061v1。有兴趣深入了解的读者可以通过该编号在学术数据库中查询完整论文。

当我们谈到人工智能写代码时，大多数人可能会想到那些令人印象深刻的演示：AI助手轻松地写出一个排序算法，或者快速生成一个计算器程序。然而，就像一个厨师能够完美制作单道菜，但在准备整桌晚宴时却手忙脚乱一样，最新研究发现，当前最先进的AI模型在编写复杂、多功能组合的程序时表现出了令人震惊的能力缺陷。

这项研究聚焦于一个至关重要但长期被忽视的问题：当AI需要编写由多个相互依赖的功能组成的程序时，它们的表现会如何？为了回答这个问题，研究团队创建了一个名为DAFNYCOMP的全新测试基准。这个基准就像是给AI出了一道"组装家具"的考试——不是简单地制作一个螺丝或一块木板，而是要把多个零件按照正确的方式组装成一件完整的家具，并且要确保每个连接点都牢固可靠。

研究团队选择了Dafny这种特殊的编程语言作为测试平台。Dafny可以说是编程界的"严格老师"，它不仅要求程序能够运行，还要求程序员明确说明每个功能的输入要求、输出保证，以及各个部分之间如何安全地协作。这就像是要求厨师不仅要做出美味的菜肴，还要详细记录每道菜的食材要求、制作步骤和营养保证，确保整桌菜搭配合理、营养均衡。

为了构建这个测试基准，研究团队采用了一个巧妙的两阶段方法。首先，他们从包含1847个高质量编程题目的数据集中筛选出具有一定复杂度的单个功能。这个筛选过程就像是挑选优质食材——他们使用了麦卡布复杂度这个指标，专门选择那些包含复杂循环、条件判断和递归模式的功能，确保每个"食材"都有足够的挑战性。

接着，研究团队将这些独立的功能像搭积木一样组合起来，创造出包含2到5个相互依赖功能的复杂程序。这个过程特别有趣：他们采用了"链式组合"的方式，让第一个功能的输出成为第二个功能的输入，第二个功能的输出又成为第三个功能的输入，以此类推。这就像是创造一个"接力赛"，每个选手都必须完美地把接力棒传给下一个选手，任何一个环节出错都会导致整个比赛失败。

在程序组合完成后，研究团队面临着一个更大的挑战：如何将这些用Python编写的程序转换成Dafny语言，并添加必要的形式化规约。这个过程就像是把一份家常菜谱转换成专业厨师的标准作业程序——不仅要保持原有的味道和营养，还要添加详细的温度控制、时间管理和食品安全要求。

研究团队发现直接转换的成功率极低，只有不到5%。因此，他们开发了一个渐进式的转换流程：先将每个Python功能分别转换成Dafny代码，立即进行验证，然后再逐步组装。这个过程需要多达10轮的精细调整，就像是一个精密的手表组装过程，每个齿轮都必须完美配合。最终，他们从1200个候选程序中成功转换了564个，再从中精心挑选出300个作为最终的测试基准。

当研究团队用这个基准测试13个最先进的AI模型时，结果令人震惊。这些模型包括了我们熟悉的GPT-4、Claude-3.5、Gemini-2.5等当前最强大的AI助手。在语法正确性方面，这些AI表现得相当不错，平均能达到95.67%的正确率，就像是学生们都能正确拼写单词和使用标点符号一样。

然而，当涉及到真正的程序验证——也就是确保程序不仅能运行，还能按照承诺的方式正确工作时，结果却是灾难性的。这些AI模型的验证成功率暴跌到了仅仅3.69%，相比单功能程序的58%成功率，这是一个高达92%的性能落差。这就好比一个学生能够完美地回答单选题，但在需要综合运用多个知识点的论述题面前却几乎完全失败。

更令人担忧的是，即使给AI多次尝试的机会——从1次增加到8次——情况也没有明显改善。最好的模型（Claude-3.5）在8次尝试后也只能达到7%的成功率，而大多数模型仍然徘徊在2%以下。这表明问题不在于AI需要更多的思考时间或尝试次数，而是它们根本缺乏处理这类复杂组合问题的核心能力。

研究团队深入分析了900个失败案例，发现了三种主要的失败模式。第一种被称为"规约脆弱性"，占失败案例的39.2%。这就像是建筑工程中的"连锁反应"问题：一个功能的输出规约稍有不足，就会导致下一个功能无法确认其输入的有效性，进而引发整个程序链条的崩溃。比如，一个计算数字各位数之和的功能忘记说明结果总是非负数，那么依赖这个结果的下游功能就无法确保自己能正常工作。

第二种失败模式是"实现-证明不匹配"，占21.7%的失败。这种情况下，AI生成的代码本身可能是正确的，但它提供的规约和证明却与实际的代码逻辑不符。这就像是一个厨师做出了一道美味的菜，但菜谱上写的却是完全不同的制作方法。AI可能会生成看起来合理的循环不变式或断言，但这些断言实际上无法被程序验证器确认。

第三种失败模式是"推理不稳定性"，占14.1%。这反映了AI在维持长链推理逻辑时的根本性困难。正式验证需要严格的归纳推理：证明性质在初始状态成立，在每次迭代中保持不变，并且能够跨功能边界组合。AI模型在这种归纳推理上表现出了明显的局限性，就像是一个人能记住故事的开头和中间某些片段，但无法维持整个故事线的逻辑一致性。

这些发现揭示了当前AI技术的一个根本性盲点：它们擅长模式识别和局部推理，但在需要全局一致性和长距离依赖关系的任务上表现不佳。这就像是一个优秀的单科生，在每门课程上都能取得好成绩，但在需要综合运用多学科知识的项目中却力不从心。

研究团队还发现，即使是专门针对推理优化的AI模型（如QWQ-32B和DeepSeek-R1）也没有表现出明显优势。这表明问题不在于模型的训练策略或规模，而是当前transformer架构本身可能缺乏处理这类组合推理任务所需的内在机制。

这项研究的意义远远超出了编程领域。在我们日益依赖AI系统来处理复杂任务的时代，理解AI的这种局限性至关重要。当AI需要协调多个组件、确保系统级别的一致性时——无论是在软件开发、工程设计还是其他需要精确协调的领域——它们可能会遇到类似的困难。

从实用角度来看，这项研究为我们如何更好地利用AI提供了重要启示。在单个功能或局部任务上，AI确实可以成为强有力的助手。但对于需要多个组件精确协调的复杂系统，我们仍需要人类专家的介入和监督。这不是AI技术的失败，而是对其当前能力边界的清晰认识。

研究团队通过DAFNYCOMP基准不仅揭示了问题，也为未来的研究指明了方向。这个基准现在可以作为衡量AI组合推理能力的标准工具，帮助研究者开发出更好的模型和训练方法。就像体育比赛需要标准化的赛场和规则一样，AI研究也需要这样的标准基准来推动技术进步。

对于软件开发行业来说，这项研究提醒我们在关键系统的开发中仍需保持谨慎。虽然AI可以大大提高单个功能的开发效率，但在系统集成和整体验证方面，人类专业知识仍然不可替代。这不是要贬低AI的价值，而是要更智慧地使用这项技术。

随着我们对AI能力和局限性的理解不断加深，我们也在学习如何更好地与这些强大工具协作。DAFNYCOMP基准的建立标志着我们在这个学习过程中迈出了重要一步，它不仅揭示了当前的挑战，也为未来的突破奠定了基础。

Q&A

Q1：DAFNYCOMP基准是什么？它主要测试AI的什么能力？

A：DAFNYCOMP是由香港科技大学等机构开发的测试基准，专门用来测试AI在编写复杂多功能程序时的能力。它包含300个由2-5个相互依赖功能组成的程序，要求AI不仅要写出能运行的代码，还要提供正确的形式化规约，确保各个功能之间能够安全协作。

Q2：为什么AI在单个功能上表现很好，但在多功能组合时就失败了？

A：研究发现AI主要存在三个问题：规约脆弱性（一个功能的小疏漏会引发连锁反应）、实现-证明不匹配（代码和规约不符）、推理不稳定性（无法维持长链逻辑推理）。这就像厨师能做好单道菜，但在协调整桌宴席时就手忙脚乱一样。

Q3：这项研究对普通用户使用AI编程助手有什么启示？

A：这提醒我们AI编程助手在单个功能开发上很有用，但对于需要多个组件精确协调的复杂系统，仍需要人类专家的介入和验证。我们应该将AI作为强有力的辅助工具，而不是完全依赖它来处理关键系统的整体设计和验证。