软件里最贵的漏洞不在代码里，而在写代码之前的需求文档里。

AWS最新发布的数据显示，他们审查的软件需求中，60%存在漏洞。这些漏洞不是代码写错了，而是需求本身就有问题——自相矛盾、模棱两可、关键信息缺失。等到产品上线才发现不对劲，回溯排查往往要耗费数周。

打开网易新闻 查看精彩图片

AWS的解法出人意料：不是堆更多AI，而是搬出一台有50年历史的逻辑引擎。

这套方案藏在AWS新升级的Kiro智能开发平台里，核心功能叫"需求分析"。AWS人工智能产品管理总监Mike Miller向The New Stack解释，需求漏洞包括几种典型情况：两条需求互相矛盾、表述含糊让不同开发者理解出不同意思、或者干脆缺了关键信息。"沿着开发、测试、上线的路径走下去，最后发现不对劲，再往回倒查，"Miller说，这正是他们想要打断的恶性循环。

整个流程分三步走。首先，大语言模型把模糊的自然语言需求改写成精确、可测试的标准。然后，这些标准被翻译成形式化的数学逻辑——AWS称之为"形式化表征"。最后，一台SMT求解器登场。

SMT全称"可满足性模理论"，是一种自动推理引擎，诞生于1970年代。它不猜概率，而是做证明：给定一组逻辑规则，它能严格推导出是否存在矛盾、歧义、未定义行为或信息缺口。发现问题后，系统会向开发者抛出简单的二选一问题，Miller说每个问题大约10到15秒就能解决。

AWS反复强调一个词：prove（证明）。这不是大模型标出一个"可能有问题"的警示，而是形式化推理引擎在演示——没有任何可能的实现方式，能同时满足两条冲突的规则。

"大模型做它最擅长的，自动推理做它最擅长的，"Miller总结。

Moor Insights & Strategy分析师Jason Andersen评价，AWS在"用多样化算法模型评估大模型正确性"这条路上是先行者。"最早是把自动推理用在IAM这类访问控制产品上，成功之后开始蔓延到其他产品线。"他也指出，更常见的做法是用额外的大模型来检查输出是否合理，AWS这条路走的人不多。

这套技术组合有个学术名词：神经符号AI（neurosymbolic AI）。神经网络负责统计模式匹配，符号逻辑负责规则推演。一个处理"大概是这样"，一个确保"必须如此"。

50年前的老引擎，就这样被拉进了AI时代的开发流水线。