<p>亚马逊网络服务正在为其 Kiro AI 编码工具添加一项新功能，旨在在编写任何代码之前，数学证明软件需求没有矛盾和漏洞，从而解决 AI 辅助软件开发的核心风险之一。</p>
<p>该功能名为需求分析，旨在捕捉那些通常最难发现且修复成本最高的错误——这些问题并不是出现在最终代码中，而是出现在定义软件应做什么的初始需求中。</p>
<p>周二早上的公告是在亚马逊公开反驳《金融时报》关于其 AI 编码工具导致 AWS 中断的报道三个月后发布的，这一事件突显了在软件开发中给予 AI 代理过多自主权的风险。</p>
<p>这项公告还在 AWS 聘请前微软高管 Shawn Bice 回归亚马逊担任 AI 服务副总裁，领导其自动推理团队的前一天发布，正是该团队开发了这一新功能。Bice 将向亚马逊的代理 AI 副总裁 Swami Sivasubramanian 汇报。</p>
<p>需求分析结合了大型语言模型和一个称为 SMT 求解器的自动推理引擎。LLM 将自然语言需求翻译为形式逻辑。</p>
<p>然后，求解器通过数学证明检查这些需求是否相互矛盾或留下可能被 AI 编码工具错误填充的漏洞——随着 AI 生成软件的速度超过开发者审查的速度，这成为一个普遍问题。</p>
<p>“每个模糊的提示都会产生模糊的规格或计划，而实施该规格的 AI 代理则会生成充满未披露决策的代码，这些决策是在你不知情或未同意的情况下做出的，” AWS 应用科学家在伴随新闻发布的博客文章中写道。</p>
<p>Kiro 在一个竞争激烈且快速增长的 AI 编码工具市场中竞争，包括 Cursor、GitHub Copilot、Anthropic 的 Claude Code、谷歌的 Antigravity 和 OpenAI 的 Codex。</p>
<p>虽然这些工具越来越多地在代码生成的同时添加了规划和代理工作流程，但 Kiro 的身份建立在一种以规格为先的方法上，这要求开发者在 AI 开始构建之前正式化他们的意图。</p>
<p>AWS 还宣布了另外两个 Kiro 功能，旨在加快开发过程。</p>
<ul>
<li>并行任务执行同时运行独立的编码任务，而不是顺序执行，从而将大型项目的实施时间缩短约 75%。</li>
<li>AWS 表示，新推出的快速计划模式允许开发者跳过对已理解功能的逐步审批过程，一次性生成完整的需求、设计和任务。</li>
</ul>
<p><strong>之前：</strong> 亚马逊的意外独立热门：Kiro 广泛推出，旨在重塑 AI 驱动的软件开发。</p>

亚马逊每日 1 倍做空 ETF - Direxion

AMZZ

云计算 ETF - GlobalX

亚马逊每日 2 倍做多 ETF - Direxion

<p>亚马逊网络服务（AWS）正在增强其 Kiro AI 编码工具，推出一项名为需求分析的新功能，旨在确保软件需求在编码开始之前没有矛盾和漏洞。这一举措旨在应对与 AI 辅助软件开发相关的风险，特别是在 AWS 因其 AI 工具的可靠性受到审查后。该功能结合了大型语言模型和 SMT 求解器来验证需求。此外，AWS 还宣布了另外两个功能，以加快开发速度：并行任务执行和快速计划模式，这些功能简化了编码过程</p>

<p>Amazon Web Services is adding a feature to its Kiro AI coding tool designed to mathematically prove that software requirements are free of contradictions and gaps before any code gets written, addressing one of the core risks of AI-assisted software development.</p>
<div class="lb-trans"><p>亚马逊网络服务正在为其 Kiro AI 编码工具添加一项新功能，旨在在编写任何代码之前，数学证明软件需求没有矛盾和漏洞，从而解决 AI 辅助软件开发的核心风险之一。</p>
</div><p>The feature, called Requirements Analysis, is designed to catch the kind of bugs that can often be the hardest to spot and most expensive to fix — problems that start not in the resulting code but in the initial requirements that define what the software is supposed to do.</p>
<div class="lb-trans"><p>该功能名为需求分析，旨在捕捉那些通常最难发现且修复成本最高的错误——这些问题并不是出现在最终代码中，而是出现在定义软件应做什么的初始需求中。</p>
</div><p>The announcement Tuesday morning comes three months after Amazon publicly pushed back on a Financial Times report that its AI coding tools contributed to AWS outages, an episode that highlighted the risks of giving AI agents too much autonomy in software development.</p>
<div class="lb-trans"><p>周二早上的公告是在亚马逊公开反驳《金融时报》关于其 AI 编码工具导致 AWS 中断的报道三个月后发布的，这一事件突显了在软件开发中给予 AI 代理过多自主权的风险。</p>
</div><p>It also comes a day after AWS hired former Microsoft exec Shawn Bice to return to Amazon as VP of AI Services leading its Automated Reasoning Group, the team behind the new feature. Bice will report to Swami Sivasubramanian, Amazon’s VP of Agentic AI.</p>
<div class="lb-trans"><p>这项公告还在 AWS 聘请前微软高管 Shawn Bice 回归亚马逊担任 AI 服务副总裁，领导其自动推理团队的前一天发布，正是该团队开发了这一新功能。Bice 将向亚马逊的代理 AI 副总裁 Swami Sivasubramanian 汇报。</p>
</div><p>Requirements Analysis combines large language models with an automated reasoning engine called an SMT solver. The LLM translates natural-language requirements into formal logic.</p>
<div class="lb-trans"><p>需求分析结合了大型语言模型和一个称为 SMT 求解器的自动推理引擎。LLM 将自然语言需求翻译为形式逻辑。</p>
</div><p>The solver then checks those requirements by mathematically proving whether they contradict each other or leave gaps that could be filled in erroneously by the AI coding tool — a common problem as AI increasingly generates software faster than developers can review it.</p>
<div class="lb-trans"><p>然后，求解器通过数学证明检查这些需求是否相互矛盾或留下可能被 AI 编码工具错误填充的漏洞——随着 AI 生成软件的速度超过开发者审查的速度，这成为一个普遍问题。</p>
</div><p>“Every vague prompt produces a vague spec or plan, and the AI agent implementing that spec produces code full of undisclosed decisions made on your behalf, without your awareness or agreement,” wrote AWS applied scientists in a blog post accompanying the news.</p>
<div class="lb-trans"><p>“每个模糊的提示都会产生模糊的规格或计划，而实施该规格的 AI 代理则会生成充满未披露决策的代码，这些决策是在你不知情或未同意的情况下做出的，” AWS 应用科学家在伴随新闻发布的博客文章中写道。</p>
</div><p>Kiro competes in a crowded and fast-growing market for AI coding tools that includes Cursor, GitHub Copilot, Anthropic’s Claude Code, Google’s Antigravity, and OpenAI’s Codex.</p>
<div class="lb-trans"><p>Kiro 在一个竞争激烈且快速增长的 AI 编码工具市场中竞争，包括 Cursor、GitHub Copilot、Anthropic 的 Claude Code、谷歌的 Antigravity 和 OpenAI 的 Codex。</p>
</div><p>While those tools have increasingly added planning and agent workflows alongside code generation, Kiro has built its identity around a spec-first approach that requires developers to formalize their intent before the AI starts building.</p>
<div class="lb-trans"><p>虽然这些工具越来越多地在代码生成的同时添加了规划和代理工作流程，但 Kiro 的身份建立在一种以规格为先的方法上，这要求开发者在 AI 开始构建之前正式化他们的意图。</p>
</div><p>AWS also announced two other Kiro features designed to speed up the development process.</p>
<div class="lb-trans"><p>AWS 还宣布了另外两个 Kiro 功能，旨在加快开发过程。</p>
</div><ul>
<li>Parallel Task Execution runs independent coding tasks concurrently rather than sequentially, cutting implementation times for large projects by roughly 75 percent, according to the company.</li>
<li>AWS says a new Quick Plan mode lets developers skip the step-by-step approval process for well-understood features, generating a full set of requirements, design, and tasks in one pass.</li>
</ul>
<div class="lb-trans"><ul>
<li>并行任务执行同时运行独立的编码任务，而不是顺序执行，从而将大型项目的实施时间缩短约 75%。</li>
<li>AWS 表示，新推出的快速计划模式允许开发者跳过对已理解功能的逐步审批过程，一次性生成完整的需求、设计和任务。</li>
</ul>
</div><p><strong>PREVIOUSLY:</strong> Amazon’s surprise indie hit: Kiro launches broadly in bid to reshape AI-powered software development</p>
<div class="lb-trans"><p><strong>之前：</strong> 亚马逊的意外独立热门：Kiro 广泛推出，旨在重塑 AI 驱动的软件开发。</p>
</div>

AWS targets AI slop with new spec check in Kiro coding tool, amid scrutiny of agent reliability

GeekWire

GraniteShares 2x Long AMZN Daily ETF

亚马逊

微软

谷歌-C

谷歌-A

OpenAI

在代理可靠性受到审查的背景下，AWS 在 Kiro 编码工具中推出新的规格检查，以解决 AI 松散问题