工程实践 Amazon Science 2026/08/11
文章回顾了 AWS 自动推理组十年间将数学逻辑、形式验证和程序分析从研究原型推向生产服务的历程。核心方法包括使用 SMT 求解器、证明助手（如 Lean）和规范证明，对 VPC 网络、IAM 策略、TLS 握手、Nitro 隔离引擎及授权引擎等关键系统给出数学保证。文中列举了 Tiros/Zelkova、Reachability Analyzer、IAM Access Analyzer 和 Amazon Bedrock Guardrails 等落地成果，并指出自动推理不仅提升安全与可靠性，还通过精确规范帮助团队简化系统设计。作者进一步认为，该技术正被用于验证 AI 生成代码和约束智能体行为，为可证明安全的 AI 系统提供基础。文章主要作为 Amazon 内部视角的成就回顾，未深入介绍具体算法、失败案例或量化局限。
本文作为工业界形式化方法落地的一手回顾，提供了多个真实生产案例（如 IAM Access Analyzer、Reachability Analyzer、Bedrock Guardrails）和可迁移的洞察：精确规范能简化设计，自动推理可用于验证 AI 输出。适合关注形式验证、云安全、AI 安全的读者了解从研究到工程化的路径。主要风险是 Amazon 自我视角、缺乏技术细节和失败分析，需结合其他深度材料使用。
科研议题 Amazon Science 2026/07/30
文章提出 ControlG 框架，将工业 PID 控制器引入多任务图自监督学习，将多目标协调重新定义为时间分配问题，避免逐步梯度混合带来的冲突、漂移和饥饿。框架包含三个时间尺度的闭环：感知环估计目标难度（谱需求与干扰），规划环基于对数超体积敏感性生成计算资源分配计划，控制环利用 PID 控制器跟踪分配并修正偏差。在 9 个图基准（含同配、异配及大规模图）上的节点分类、链接预测和节点聚类任务中，ControlG 的平均排名显著优于随机调度及多种多任务基线，效率开销可控，且训练过程可解释、可审计。消融实验证实各组件贡献，方法主要适用于共享参数的多目标场景，当前验证限于图 SSL，作者正探索其在 LLM 持续学习与多任务微调中的应用。
本文来自亚马逊科学博客，详细介绍了 ICML 论文 ControlG，以控制理论重构多任务学习中的梯度冲突问题，方法新颖且有扎实的理论与实验支撑。适合从事多任务学习、图神经网络或自监督学习的研习者。其感测-规划-控制的分解及可解释调度记录，为克服目标冲突提供了可迁移的设计范式，具有长期参考价值。
科研议题 Amazon Science 2026/07/29
文章介绍了PatientAgentBench，一个面向患者健康AI智能体的临床安全评估基准。针对医学AI基准缺乏对多轮对话、工具使用和实际患者场景评估的问题，作者设计了合成患者档案、临床场景和状态化医疗工具，通过多轮对话评估AI系统。评估采用LLM陪审团，依据经临床医生验证的六个维度（临床安全、分诊质量、工作流准确性、任务完成度、临床有用性、对话质量）的复用标准进行打分。实验发现，当前最强基础模型在常规但存在潜在风险的任务中仍表现不足，主要失败模式包括忽略危机资源提供和临床信息捏造；模型能力无法自动保证安全，最棘手的案例往往不是紧急情况而是隐藏风险的日常请求。该框架可动态生成新场景，无需额外医生标注，且未使用真实病人数据，可扩展至新领域和人群。
推荐收录。该工作填补了患者侧AI智能体评估的空白，提供了一个可复现、经临床验证的基准框架，并揭示了当前模型在安全关键场景下的普遍短板。对从事AI安全、医疗AI和LLM研究的读者具有直接参考价值，其可复用的评估维度和动态场景生成设计也为其他安全敏感领域的AI评估提供了可迁移的方法论。
科研议题 Amazon Science 2026/07/10
文章提出一种名为 HydroShear 的触觉仿真方法，在现有水弹性接触模型中增加路径依赖的力追踪机制，从而准确模拟剪切力，用于训练机器人灵巧操作策略。该方法通过采集真实传感器数据校准关键参数，并支持 GPU 并行，能以低成本在仿真中大规模训练强化学习策略。在四个接触密集型任务上，仿真训练的策略直接部署到真实机器人，平均成功率达 93%，远超简化力近似和基于学习的基线方法。实验表明，精确模拟触觉剪切对于需要感知滑动、对准和接触力的任务至关重要。当前方法基于 GelSight 视觉触觉传感器，未来可扩展到更高分辨率或其他触觉模态。
本文详细阐述了一种新颖的触觉仿真方案，提供从问题建模、参数校准到真机验证的完整技术链路，实证结果扎实。适合从事机器人灵巧操作、仿真到真实迁移或强化学习应用的研究者和工程师阅读。其路径依赖力追踪的设计思想和低成本训练范式，对开发类似触觉感知系统具有明确的借鉴价值。
工程实践 Amazon Science 2026/07/09
文章介绍 Turnstile，一个用 Rust 编写的轻量级代理，旨在解决在智能体强化学习（RL）训练中由于文本重解析导致的 token 漂移问题。作者分析了现有智能体框架在记录 rollout 时，因重新分词、聊天模板变化和历史压缩等操作会丢失模型实际看到的精确 token 序列和路由信息，导致训练信号失真。Turnstile 位于智能体框架与推理后端之间，在生成时刻捕获准确的 token ID、log 概率、损失掩码，并支持多轮轨迹合并、MoE 路由记录和多模态图像处理。文章展示了 Turnstile 与开源框架 OpenHands 等集成，在不改动业务代码的情况下驱动两个不同智能体完成 RL 训练，验证了方案的有效性。当前 Turnstile 仍处于早期阶段，仅支持 SGLang 后端，但设计上保持与具体智能体逻辑解耦，可迁移到不同训练栈。
推荐收录，因为文章不仅提出了一个具体工程方案，还深入剖析了智能体 RL 训练中 token 漂移的根源、影响及解决思路。该代理设计优雅，将复杂训练数据捕获问题下沉到协议边界，对正在构建 RL 训练基础设施或需要可靠 rollout 管线的工程师有直接借鉴意义。其核心思想——在生成边界捕获精确状态而非事后重构——可迁移到其他需要确定性快照的分布式训练系统。
工程实践 Amazon Science 2026/06/10
这篇文章介绍了 AWS Graviton5 的整体设计升级，包括从 96 核提升到 192 核、采用 3nm 工艺、支持 DDR5-8800 与 PCIe Gen6，以及更大的 L3 缓存和改进后的芯粒互联。作者进一步解释了这些变化如何通过更好的分支预测、缓存层级、NUMA 划分和芯粒内互联来提升真实负载表现，尤其是数据库、Web 应用和机器学习推理等场景。文章还补充了 Nitro Isolation Engine 的正式验证隔离机制，强调了硬件设计与云安全之间的结合。
推荐收录，因为它不仅是产品发布，更提供了 CPU、缓存、芯粒互联、NUMA 和云安全隔离的具体设计思路，适合关注云基础设施和处理器演进的读者。尽管带有厂商宣传色彩，但其中关于真实工作负载优化与形式化验证安全性的论述具有较强的迁移价值。
科研议题 Amazon Science 2026/06/10
这篇文章介绍了 AWS 将 EC2 的隔离核心拆分为独立的 Nitro Isolation Engine，并用 Isabelle/HOL 对其进行形式化验证，从而为虚拟机隔离提供数学级别的正确性保证。文中重点解释了验证对象的边界、规格与证明的关系，以及如何分别处理功能正确性、内存安全、运行时错误和机密性/完整性等性质；还介绍了 μRust、分离逻辑、最弱前置条件和非干扰等关键方法。文章的价值在于，它不仅展示了一个可落地的商用云形式化验证案例，也清楚说明了这类证明适用的前提、复杂度和局限。
推荐收录，因为它把“形式化验证如何进入商用云基础设施”这件事讲得很完整，既有系统边界设计，也有证明方法和安全性质定义，具有很强的长期参考价值。对做操作系统、云基础设施、安全隔离和程序验证的读者来说，这篇文章能直接提供可迁移的建模与证明思路。
科研议题 Amazon Science 2026/06/08
文章围绕“如何把 agentic AI 可靠地锚定到现实世界”展开，提出四条互补路线：物理先验驱动的深度学习、带校准的不确定性推理、通过数值模拟弥合文本到数值执行的鸿沟，以及借助外部 verifier 进行验证增强。作者结合仓储、天气、数学证明和物理科学等场景说明这些方法如何降低幻觉、提升安全性与可执行性，并给出若干实验结果作为支撑。文章进一步指出，未来更复杂的多保真模拟、把不确定性作为训练信号、以及将物理约束编入形式化验证流程，可能成为构建可靠物理 AI 的关键方向。
推荐收录，因为它不是泛泛谈“AI 代理很重要”，而是系统总结了把 LLM/agent 接入物理世界时的四类关键机制，兼具研究脉络和工程边界。对关注 AI 代理、可靠性、科学计算和物理世界自动化的读者，这篇文章能提供可迁移的设计框架与问题分解方式。
工程实践 Amazon Science 2026/06/08
这篇文章讨论的是智能体系统中的“意图-执行鸿沟”：模型真正要做的事，和 harness 实际执行出来的事之间存在偏差，而这个偏差往往比模型本身的推理能力更能决定最终表现。作者结合论文与实测，给出了一套轻量级单智能体 harness 设计思路，包括更安全的编辑工具、更明确的 diff 反馈、对工具输出长度的处理、以及按不同模型家族调整 reasoning nudges 和工具接口。文章还强调 benchmark 分数会受到基础设施、超时、并发、网络和评测环境等因素显著影响，因此“benchmaxing”并不等于真实能力提升。
推荐收录，因为它不是泛泛讨论“怎么做 agent”，而是把智能体性能拆解为模型、工具、反馈与评测环境之间的系统问题，并给出可复用的工程原则。对于做 LLM agent、代码修复、工具调用和基准评测的人，这篇文章能直接帮助理解为什么同一模型在不同 harness 下表现会差很多。
科研议题 Amazon Science 2026/06/03
这篇文章讨论的是 AI 生成深度研究报告的事实核查与评测问题，核心观点是“ground truth 不是静态数据集，而是一个可审计、可修正的过程”。作者提出 audit-then-score 评测协议，并介绍了 DeepFact-Bench 和 DeepFact-Eval：前者作为共享基准，后者通过上下文阅读、检索多篇文献、追问缺失信息来判断报告中的主张是否被证据支持。文章还给出实验结果，说明在复杂事实核查任务中，专家一开始直接标注并不稳定，但在“审计争议答案”的角色下准确率显著提升，评测系统也因此优于若干传统事实核查与深度研究系统。
推荐收录，因为它不只是介绍一个新模型，而是系统性讨论了复杂 AI 任务中“如何构造可持续有效的评测”这一长期关键问题。文章提出的审计式基准维护思路，对生成式搜索、深度研究、事实核查和高不确定性评测场景都有可迁移价值。
工程实践 Amazon Science 2026/05/28
文章介绍了 AWS 在数据中心网络中用“准随机”平面网络替代传统 fat-tree 的方案，核心包括拓扑设计 RNG、路由算法 Spraypoint，以及用于落地布线的被动光学组件 ShuffleBox。作者不仅解释了为什么随机平面拓扑在理论上更优，还给出了可计算的性能模型、530 个 CPU 年规模的仿真实证，以及在真实生产环境中的部署结果。文章最后总结了该方案在路由器数量、吞吐量和能耗上的收益，同时说明其适用前提是需要配合专门的物理布线与路由机制。
推荐收录，因为它把网络拓扑理论、路由算法设计、物理布线约束和生产验证完整串联起来，属于典型的高质量工程研究案例。对做数据中心网络、系统架构和高性能基础设施的读者来说，这篇文章提供了可迁移的设计思路：如何把“理论最优”转化为“可部署、可验证、可规模化”的方案。
科研议题 Amazon Science 2026/05/26
这篇文章介绍了一项关于大语言模型推理训练的研究：作者不再把同一道题只绑定单一“标准推理链”，而是用多个多样化的推理轨迹共同监督模型，并通过全局分叉 token 让模型学习不同的推理模式。文中提出了 set-supervised fine tuning（SSFT）来避免模式坍塌，再结合 global forking policy optimization（GFPO）在推理时选择更合适的推理策略，从而在数学推理和代码任务上同时提升单次准确率与多样性。文章给出了 AIME、LiveCodeBench 等基准上的结果，显示该方法在 pass@1 上优于常见的 SFT+GRPO 管线，且在 pass@k 上也保持更好的多样性；其适用前提是能够获得同题多轨迹监督，并且主要证据来自基准评测。
推荐收录，因为它不是泛泛讨论“让模型更会思考”，而是明确提出了多推理轨迹监督、模式专门化和策略选择三个可复用机制，并给出清晰的实验验证。对关注 LLM 推理、后训练和多样性-准确率权衡的读者，这篇文章能提供可迁移的方法框架与评估视角。
科研议题 Amazon Science 2026/05/15
这篇文章基于一篇 ICLR 论文，讨论如何在不牺牲准确率的前提下提升大语言模型推理效率。作者指出，传统 Chinchilla scaling law 只覆盖参数量与训练数据量，而没有把隐藏维度、MLP 与注意力参数比例、以及 GQA 这类架构选择纳入优化框架；因此他们进一步建立了“条件缩放律”，把这些架构变量与损失和吞吐量直接关联起来。文章还通过训练 200 多个不同架构模型验证了该方法，给出了 Panda 与 Surefire 两类在准确率或准确率-效率帕累托前沿上更优的模型家族，并说明这些结论在不同 GPU 和推理框架上具有较强一致性，但仍主要适用于 Transformer 风格的 LLM 及其服务场景。
推荐收录，因为它不是泛泛介绍模型加速，而是把缩放规律、架构设计与推理吞吐放进同一个可计算框架里，具有很强的方法论价值。对做 LLM 训练、架构搜索和推理系统优化的读者来说，这类“如何在精度与效率之间做定量权衡”的结论很有迁移性。
科研议题 Amazon Science 2026/05/14
这篇文章介绍了 Promptimus，一种用于自动优化“已经相当不错”的 LLM 提示词的方法，重点解决企业场景中提示词迁移到新模型、以及在保留业务规则前提下继续提升性能的问题。文章给出了四步迭代流程：基于用户自定义指标做评估、用 metric analyzer 生成可分解的检查点、通过反馈与策略生成器定位失败模式、再以全量重写或局部 edit mode 生成候选提示词并迭代选择最佳方案。作者还用 20 个公开基准和多个企业任务验证了其效果，显示该方法在多数任务上优于现有自动提示优化基线，并且在多模态与结构化提示场景中，局部编辑往往比重写更稳健。
推荐收录，因为它不是泛泛介绍提示词优化，而是提出了完整的方法框架、系统架构和跨基准实验结果，适合长期参考。文章对“如何在保留复杂业务约束的同时自动改进提示词”给出了可迁移的研究与工程思路，尤其适合做企业 LLM 应用、提示迁移和自动调优的人阅读。
工程实践 Amazon Science 2026/05/06
这篇文章讲的是 Amazon 中段物流网络（middle-mile network）如何在需求波动、路况变化、设施故障等不确定性下进行网络设计与调度优化。核心思路不是追求对每一种异常都“鲁棒化”到完全免疫，而是通过“可选性（optionality）”设计、粗粒度优化加时间边界约束、以及 Monte Carlo 生成场景来评估方案的脆弱性，从而筛选出在常态和扰动下都更稳定的网络方案。文章还介绍了用图注意力网络同时建模站点图和起讫点图，以捕捉空间相关性与流量耦合关系，帮助生成更真实的需求场景。
推荐收录，因为它把大规模物流网络中的不确定性优化问题讲得比较具体，展示了优化、机器学习与仿真场景生成如何组合起来服务真实业务。虽然是博客形式，但其中关于“不要只优化平均情况、要为扰动保留可选性”的方法论，对做供应链、运筹优化和大规模决策系统的读者有较强迁移价值。
科研议题 Amazon Science 2026/05/05
这篇文章介绍了 Amazon 如何用机制设计理论优化与供应商的协作，核心是将 VCG 机制与分布式协同优化协议 CPP 结合，在信息不对称的前提下寻找对双方整体成本更优的供给计划。文章不仅解释了静态场景下如何通过迭代式 best response 近似实现“真报即最优”的性质，还进一步扩展到滚动时间窗的动态机制，并用成本-收益转移（CBT）来刻画参与各方的激励与补偿关系。文中还提出了适用于低维决策空间的 menu-of-contracts 替代方案，并讨论了缺货、双向承诺和不确定性下的设计边界。
推荐收录，因为它把机制设计、分布式优化和供应链协同三个领域连接起来，给出了从理论到系统实现的完整路径，而不是停留在概念介绍。对研究机制设计、协同优化、AI/运筹系统工程的人都具有较强的迁移价值，尤其适合理解“激励相容如何落到大规模系统里”。
工程实践 Amazon Science 2026/05/04
这篇文章系统介绍了 Amazon 如何把 responsible AI 嵌入 AI 全生命周期：从预训练阶段注入安全、隐私、公平等原则，到 RLHF 阶段用奖励模型和 judge 机制塑形行为，再到评测阶段构建可击穿模型的测试集，并在第三方监测与高风险场景中持续追踪风险。文章还展示了政策制定、红队、外部合作和法规变化如何反向影响模型训练与部署，强调“可信 AI”不是附加功能，而是产品设计和组织流程的一部分。整体上它更像一篇面向大模型治理与工程落地的案例梳理，适合关注 AI Safety、AI Engineering 和模型评测体系的读者参考。
推荐收录，因为它不是泛泛谈“负责任 AI”，而是把预训练、后训练、评测、第三方监测和政策制定串成了一条可复用的工程链路。对做大模型、评测、红队和安全治理的人来说，文章提供了跨团队协作、风险分层和验证闭环的参考框架。
科研议题 Amazon Science 2026/04/29
文章聚焦 AI 训练数据的隐私风险，系统梳理了三类典型攻击：针对单模型的成员推断、联邦学习中从梯度重建样本，以及从共享全局模型中提取他人训练数据。作者结合相关论文与自测实验说明，这些攻击并非理论猜想：例如成员推断可利用模型对训练样本的高置信度，联邦学习梯度本身也会泄露可重建信息。文章进一步给出两条核心防线：差分隐私通过向训练梯度注入噪声来削弱单个样本影响，安全多方计算则让各方只看到聚合结果而不暴露原始梯度。实验显示，DP-SGD 在 EMNIST 上以一定精度损失换来可量化隐私预算，而 MPC 能阻断梯度恢复，但若全局模型本身不加 DP 仍可能被继续利用。文章强调隐私保护必须在攻击规模化前前置部署，且 ε 与精度之间的权衡高度依赖任务、数据集和合规要求。
收录价值高，因为文中明确给出了成员推断、梯度反演和全局模型提取三类可操作攻击，并用 EMNIST、ResNet-50 等实验验证了风险与防线。适合做 AI 隐私、联邦学习和差分隐私的长期参考，尤其适用于需要在精度、合规与可部署性之间做权衡的团队。
科研议题 Amazon Science 2026/04/27
文章介绍了一篇关于大语言模型安全评估的研究，核心问题是传统红队测试只覆盖少量固定提示，难以刻画多轮对话中真实且最坏情况下的灾难性风险。作者与 UIUC 提出 C3LLM 框架，把对话建模为语义相关的图结构，并设计随机节点、图路径、带目标约束的图路径以及自适应采样四种威胁分布，以覆盖不同攻击能力。框架先用独立的 ChatGPT 评审器标注模型回复是否“灾难性”，再用 Clopper-Pearson 方法把攻击成功率转成置信区间，从而给出风险概率的上下界，而不是单点分数。实验在化学/生物与网络犯罪基准上比较了多款前沿闭源和开源模型，显示所有模型都存在非平凡风险，但安全性差异明显。该方法适合做更原则化的安全基准，但其结论仍受图构建方式、评审器可靠性和所选威胁模型覆盖范围限制。
推荐收录，因为文章明确给出了 C3LLM 的问题定义、对话图建模、四类采样威胁模型和置信区间认证方法，属于可复用的 LLM 安全研究框架。适合做安全评测、红队设计和基准构建的读者参考，但也要注意它依赖特定对话图与自动裁判，结论并非对所有真实场景都完全外推。
工程实践 Amazon Science 2026/04/17
文章介绍 AWS 如何用 Isabelle/HOL 对 Nitro Isolation Engine（NIE）做形式化验证，证明其在云隔离与客户数据保护上的正确性和安全保证。作者解释选择 Isabelle/HOL 的原因：它在表达力、自动化、证明可读性和可扩展性之间更平衡，且支持可控的中间目标、定制解析器、locale、sledgehammer、反例搜索和代码生成。为验证 NIE，他们在 Isabelle/HOL 上实现了 separation logic，将 Graviton-5 架构规范、Rust hypercall 代码及安全性质组织成约 25 万行证明。文章还说明该证明可在普通笔记本上约半小时运行，显示工具能处理大规模目标。同时作者也强调，高阶逻辑无法完全自动化，实际部署仍需测试覆盖未形式化部分与前提假设，因而其价值主要在高风险系统的关键路径验证。
推荐收录，因为它给出了选择 Isabelle/HOL 的直接工程证据：不是抽象地谈形式化验证，而是落到云 hypervisor、25 万行证明和实际运行性能。适合做云安全、系统软件和证明辅助器选型参考，但也要注意它依赖严格规格与大量人工交互式证明。
科研议题 Amazon Science 2026/04/15
文章介绍了 Amazon 与 Nimbus Therapeutics 合作的实验：把通用大模型 Nova 2 Lite 通过监督微调（SFT）和强化微调（RFT）改造成分子性质预测器，用于药物发现中的脂溶性、渗透性和清除率等 11 项属性。作者先证明未定制的 Claude Sonnet 4 与 Nova 2 Lite 在该任务上明显落后于专用 GNN，误差可高出 40% 到 200% 以上；随后用 55,000 个带实验标签分子做 SFT，再在 15,000 个未见样本上用 RFT 优化。文中重点比较了指数衰减、二值奖惩和 Huber reward 三种奖励设计，指出 Huber 在大误差和小误差区间都更稳定，最终取得最佳结果。最佳模型在 11 项性质上平均 RMSE 接近或部分超过多模型 GNN 方案，并把原本需要多套模型与接口的流程简化为单一对话式系统。文章也明确边界：当前成果主要是性质预测，向分子生成与可解释推理扩展仍是下一步，且效果依赖领域数据、奖励设计和持续微调。
收录价值在于它给出了可复现的迁移路径：SFT 负责补足领域知识，RFT 通过 Huber reward 稳定优化回归任务，并用明确指标对比 GNN 基线。适合做 LLM 行业定制、科学计算与 AI4Science 的方法参考，但其结论主要针对分子性质预测，外推到其他科学任务仍需重新验证。
科研议题 Amazon Science 2026/04/14
这篇文章介绍了 AWS 与约翰斯·霍普金斯工程学院 Gray Lab 联合发布的抗体可开发性基准数据集，核心问题是：当前用于抗体 AI/ML 设计的公开数据太少、太单一，导致模型难以被可靠比较。新基准强调用湿实验验证的真实标签来构建训练与评测基础，避免只依赖私有数据或单一靶点数据带来的偏差。数据集包含 50 个种子抗体、4 种结构格式、42 个抗原及大量系统性突变体，覆盖表达量、纯度、热稳定性、聚集、交叉反应性和疏水性等关键属性。它刻意纳入可开发与不可开发样本，并对 pLM 引导与非引导突变、插入/删除等策略做了区分，便于零样本评测和模型横向对比。文章也指出该基准仍局限于特定抗体空间与若干可开发性指标，后续扩展能否保持代表性仍是关键。
这篇内容有明确的收录证据：它不是单纯产品新闻，而是给出了公开数据集的设计原则、样本构成、标签体系和评测用途，适合作为蛋白/抗体 AI 研究的长期参考。对做生物计算、机器学习基准和模型评测的读者尤其有价值，但其结论主要适用于抗体可开发性这一特定任务域。
工程实践 Amazon Science 2026/04/08
文章介绍 AWS 的 RuleForge：用多智能体 AI 将新 CVE 的利用代码、威胁情报和日志分析串成检测规则生成流水线。系统先自动抓取公开 PoC 并按威胁优先级排序，再由生成代理并行产出候选 JSON 规则，随后由独立的 judge 模型按敏感性和特异性评估，而不是让生成模型自评。通过合成测试、MadPot 和内部日志验证，并把失败原因回传迭代，最后仍由人工复审后上线。实践结果显示，规则产出与验证速度提升 336%，独立评审还能把误报降低 67% 且保持命中率。文章同时指出该方案主要适用于已有公开利用样本、需要高精度生产落地的高危漏洞检测，边界在于仍依赖人工最终批准和域内提示设计。
收录，因为文中给出了可验证的生产级方案：将生成与评估拆分、采用负向提问和分阶段验证，并用 336% 提速与 67% 降误报作为直接证据。适合做 AI 安全、检测工程和 agent 工作流设计参考，但结论主要来自已知 CVE 与 PoC 场景，迁移到缺少样本或强对抗环境时需谨慎。
工程实践 Amazon Science 2026/04/07
文章介绍 Amazon 围绕后量子密码 ML-KEM（原 Kyber）构建高保障实现 mlkem-native 的工程实践。作者将前端高层逻辑与面向不同架构的性能后端拆分，前端保留可维护性，后端针对 AArch64、x86_64、RISC-V64 做汇编/内建优化。为同时保证安全与性能，团队用 CBMC 为 C 代码添加可机检契约，证明内存安全和整数边界安全；对关键汇编则结合 SLOTHY、HOL Light 和 s2n-bignum 做形式化正确性证明，并尽量让证明对指令调度和寄存器分配不敏感。文章还专门说明了形式化验证的可信边界，公开 SOUNDNESS.md 记录假设、残余风险和缓解措施。该实现已集成进 AWS-LC，并在 c7i/c7g 上相对参考实现取得明显吞吐提升，但文章也强调验证仍依赖模型、工具链和人工桥接，不能被理解为绝对无风险。
收录价值明确：文章给出了从参考实现到高性能、可验证生产代码的完整链路，且用 CBMC、HOL Light、SLOTHY 等工具说明了具体做法。适合密码工程、系统安全和高性能基础设施读者，尤其可迁移到需要同时兼顾正确性、性能与可维护性的关键代码场景。
工程实践 Amazon Science 2026/04/01
这篇文章讨论了基于 LLM 的文本转语音系统在真实应用中的三个主要问题：多语种语音克隆时的口音泄漏、表达力不足，以及自回归生成带来的幻觉、截断和发音不稳定。作者给出了一组组合式方案：用面向目标地区的数据增强和 LoRA 微调缓解口音串扰；用 classifier-free guidance 生成更具情感和韵律的参考音频，以提升可表达性；再通过在生成前预测音素序列与时长，引入守卫检查和失败重试来提升可靠性。文章还补充了数据过滤策略，结合 ASR 指标与注意力机制筛掉对齐不良样本，同时尽量保留表达性。实验结果显示，九个语言/地区上的 MUSHRA 评分较前代模型提升约 5% 到 20%，长文本上的关键错误率降到每小时不足 1 秒。其方法主要适用于 LLM 自回归 TTS 体系，对传统显式时长建模的 TTS 架构不一定直接适用。
收录价值明确，因为文章不仅描述了 LLM-TTS 的新问题，还给出了 LoRA、CFG、链式预测、guardrails 和数据过滤等可复用方案，并用 MUSHRA 与错误率量化了收益。适合做语音生成、AI 工程化和模型可靠性设计的参考，但读者也应注意这些技巧主要针对自回归 LLM-TTS 场景。
工程实践 Amazon Science 2026/03/20
这篇文章介绍了 Amazon 将 Arm64 汇编实现的 AES-XTS 加密/解密加入 s2n-bignum，并用 HOL Light 对其做形式化验证的过程。作者先从 AWS-LC 的现有实现出发，重整了原本为避免 buffer overread 而非常复杂的 5x 展开循环，把轮密钥常驻寄存器、拆分尾块处理，以便 SLOTHY 进一步优化指令调度。随后，他们依据 IEEE 1619 写出可测试的规格，再证明汇编代码与规格一致，并补充常量时间与内存安全性质。文章还说明了用 CI 持续约束证明、用硬件随机测试校验指令模型的做法。结果是在部分 Arm 核心上获得小幅性能收益，同时把高风险密码实现纳入可维护、可复用的证明框架。
推荐收录，因为它直接给出了“优化汇编 + 形式化证明 + CI 持续约束”的完整证据链，且落地在真实的 AES-XTS 密码库实现上。适合密码工程、系统安全和形式化验证读者参考，尤其对需要兼顾性能与正确性的底层实现有可迁移价值。
科研议题 Amazon Science 2026/03/19
本文围绕 LoRA 微调中“把适配器插到哪些模块”这一关键问题展开，基于 Amazon Nova 2.0 Lite 做了系统性消融实验。作者比较了 qkv、o_proj、fc1/fc2 以及多种组合在文本、长上下文、结构化 JSON 和多模态任务上的效果，评估指标覆盖准确率、ROUGE 和延迟。结果显示，o_proj 作为单模块目标最稳健，几乎不失手且通常接近最佳；qkv-only 波动较大，容易在复杂任务上欠拟合。对于更难的任务，o_proj + fc2 往往能取得更高精度，但相对单独 o_proj 只带来小幅收益。文章最终给出面向效率与精度的配置建议，并指出模块选择仍受基座模型、任务类型和模态影响，难以一刀切。
文中明确给出了跨 7 个数据集的消融结果、延迟对比和可落地的模块选择建议，不是泛泛而谈的 LoRA 介绍。适合做 LLM 微调、推理成本优化和生产化适配器设计的参考，但结论主要基于 Nova 2.0 Lite，迁移到其他基座模型仍需复验。
科研议题 Amazon Science 2026/03/16
本文讨论一种面向遗留系统的 agentic AI 思路：不去重建银行、航司、政府审批等难以停机的旧系统，而是让智能体在高保真模拟环境中学习这些系统真实的延迟、错误状态、强顺序约束和隐藏依赖。Amazon AGI Lab 将这类环境做成 RL gym 和 synthetic web environment，让 agent 不只学会“成功流程”，还要学会在失败、回退、重试和部分提交等场景中恢复操作。文章提出，足够成熟的 agent 可以把不稳定的 UI 语义抽象成稳定的“合成 API”，充当跨系统的接口层，逐步吸收现代化迁移期的脆弱性。它强调这不是简单的流程自动化，而是为无法替换的关键基础设施提供一种渐进式升级路径。文章的边界在于主要是理念与研究方向阐述，缺少公开实验指标和可复现细节，但对理解 agent、RL 训练环境与企业遗留系统改造的结合很有参考价值。
推荐收录，因为文章明确给出了 Amazon AGI Lab 在遗留系统模拟环境中训练 agent 的方法，并提出“agent 作为通用接口层”的架构判断。适合关注 agent、企业自动化和系统现代化的读者；可迁移价值在于如何用高保真仿真覆盖失败模式与历史包袱，但它更偏概念阐述，缺少公开基准与实验细节。