AI写代码越来越快，但一个老问题被放大了：需求本身的漏洞。

亚马逊云科技（AWS）本周二为其Kiro AI编程工具推出了一项新功能——Requirements Analysis（需求分析）。它的作用是在任何代码生成之前，用数学方法证明软件需求是否存在矛盾或缺失。AWS应用科学家在官方博客中写道："每一个模糊的提示都会产生模糊的需求或计划，而执行该计划的AI代理会在你不知情、不同意的情况下，替你做出大量未公开的决定。"

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

这项技术结合了大型语言模型与一种名为SMT求解器的自动推理引擎。LLM负责将自然语言需求转化为形式化逻辑，求解器则通过数学证明来检验这些需求是否自相矛盾，或存在可能被AI编码工具错误填补的空白。AWS称，这类源于需求定义阶段的缺陷，往往是最难发现、修复成本最高的。

发布时机耐人寻味。三个月前，AWS曾公开反驳《金融时报》关于其AI编码工具导致服务中断的报道，该事件凸显了赋予AI代理过多自主权的潜在风险。而在新功能发布前一天，AWS刚宣布聘请前微软高管Shawn Bice回归，担任AI服务副总裁，领导开发该功能的自动推理团队，向AWS代理式AI副总裁Swami Sivasubramanian汇报。

Kiro目前面临激烈竞争，对手包括Cursor、GitHub Copilot、Anthropic的Claude Code、Google的Antigravity以及OpenAI的Codex。与竞品侧重规划和代理工作流不同，Kiro的核心差异化在于"需求优先"——强制开发者在AI开始构建前将意图形式化。

同期推出的还有两项功能：Parallel Task Execution（并行任务执行）可并发运行独立编码任务，AWS称能将大型项目的实现时间缩短约75%；Quick Plan模式则允许开发者对成熟功能跳过逐步审批，一次性生成完整的需求、设计和任务集。