<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 鬆散問題