VLA 中有多少能力来自 kNN 检索
研究发现，在无需策略训练的情况下，检索相近演示并复用其动作块即可在 LIBERO 上达到 91.7% 成功率，而 VLA 模型已超过 95%。在 LIBERO-Plus 扰动下，检索方法在所有受评策略中降幅最小；对九个公开 VLA 的分析显示，微调主要让视觉语言骨干成为更好的检索键，其动作仍接近演示数据。
推荐理由：通过无策略训练的检索基线与九个公开 VLA 对照，研究呈现了 LIBERO 高分中训练演示复用的潜在比重。
#论文/研究
arXiv 机器人论文摘要精选 Microsoft Research精选 Microsoft 研究利用休眠神经元向 AI 智能体植入 Lazarus 后门
Microsoft 研究人员发现 Lazarus 技术无需训练，只需重编程大语言模型中少于 10 个休眠神经元，即可为其智能体植入由隐藏条件触发的后门。模型平时表现正常并能通过标准评测，触发后却可生成命令，让具备工具或终端权限的智能体下载并运行攻击者代码。研究认为可靠检测需要与原始权重比对，Microsoft 正探索权重扫描、红队检测、模型签名及可验证来源审计等防御措施。
推荐理由：研究揭示少量休眠神经元即可植入隐蔽后门，并将模型权重完整性与来源追溯列为智能体部署的关键防线。
Google DeepMind精选 Google DeepMind 公布 AlphaProof Code 研究，形式化验证 Signal 核心加密代码
Google DeepMind 公布 AlphaProof Code 研究，利用多 LLM 智能体框架和 Lean，对 Signal 协议实际代码的关键安全属性进行形式化验证。
推荐理由：该研究给出人类专家、多种大语言模型与 Lean 协作验证生产级密码代码的流程，可供评估 AI 形式化验证的工程路径。
Microsoft Research精选 Microsoft Research 用 PDD Kit 形式化验证智能体编写的全栈 Web 应用
Microsoft Research 介绍了 PDD Kit 如何把开发者意图转为 Verus 形式化规格，证明智能体代码对所有输入满足规格，并在证明覆盖不到的部分使用测试。
推荐理由：案例展示了将自然语言意图转成形式化规格，并用证明与测试分层约束智能体代码的完整工作流。
Microsoft Research精选 Microsoft Research 研究人员解决提出31年的 KLS 猜想
Microsoft Research 的 Xinzhi Zhang 与合作者 Zhao Song 解决了提出31年的 Kannan–Lovász–Simonovits（KLS）猜想，给出与维度无关的固定界。
推荐理由：材料梳理了人类主导的多智能体筛选流程，以及递归收紧维度依赖直至常数界的关键思路。
GitHub Blog · AI & ML精选 GitHub 引入 ModernBERT 分类器，将推送保护扩展至非结构化密钥
GitHub 与 Microsoft Applied Sciences 开发了新的 ModernBERT 分类器，用代码上下文识别非结构化密钥，批量评估候选密钥耗时不到 2 ms，可使推送保护阻止的密钥数量增加一倍以上。
推荐理由：九个季度的数据将密钥泄露增长归因于代码规模而非单次推送风险上升，并说明自动拦截为何比人工补救更易扩展。
已经到底了