锐Owl 雷达 · 2026-10-23：删掉记录不等于删掉秘密，证明不崩不等于没有 bug

覆盖 2026-10-22 18:00 → 2026-10-23 18:00（北京时间）。

今天五条落在同一个位置：动作的「完成态」，正在从「我做了」变成「我能证明我做了」。删掉一条记忆记录，信息还留在它派生出的摘要里——删除得按行为审计；程序跑过数万亿次测试，该出的 bug 还出——正确性要交出证明；把推理候选砍到只剩几个，得先保证池子里还有对的答案——剪枝要直接对 pass@k 负责；一张海报「字排对没有」，比「好不好看」更能量化——生图开始对自己可度量的那部分负责；给 agent 开权限，人只会点「同意」——那就让策略变更先过一遍形式化预检。同一天里，验证的单价在往下走，而「可检验」正在变成新的交付标准。

① 删掉记忆记录不等于删掉秘密：单条提问就能从 Agent 里捞回已删内容，成功率约三分之二（arXiv 2610.31366，2026-10-22）

这篇论文测的不是模型能力，是「删除」这个动作有没有真的生效。《AfterDeleteBench: Auditing Post-Deletion Information Persistence in LLM Agents》（2610.31366，提交 2026-10-22，25 页 7 图 12 表，作者 Ehsan Saleh、Roozbeh Nahavandi、Sama Salarian、Raef Bassily、Andrew Perrault）指出一个结构性事实：现在的 agent 会在外部维护持久记忆，并从历史里派生出额外状态（摘要就是最典型的一种）；删掉原始记忆记录，并不等于删掉它的后裔携带的信息。为此团队做了一个受控行为审计：对每一条合成秘密，把「暴露过、然后被删除」的 agent 与「除了没暴露过、其余配置完全相同」的对照 agent 放在一起比，这样删除之后任何恢复都只能归因于那一次暴露。主设定下，一条查询就能从 Qwen2.5-7B-Instruct 里捞回已删秘密，成功率约三分之二，而匹配的未暴露对照组恢复率为 0。更关键的是，恢复不需要留着一份逐字副本：当完整秘密串已经不存在、只剩分开存放的若干片段加一条公开的拼接规则时，Qwen、Mistral、Phi-3 上的精确重建成功率仍有 62%–99%。论文还把「测量」本身算进了系统——当请求格式与解析器不对齐时，明明带答案的回复会被判成失败，也就是说评估接口本身就是测量仪器的一部分。修复侧给了个有效方向：按来源闭包（provenance-aware closure，连同由该记录派生出的状态一起清掉）在测试的正基线设定下消除了可观察的恢复；而「精确字面写入过滤器」只能拦住重新写回，抹不掉已经流到下游的信息。结论一句话：源删除应当按「agent + 记忆系统」的行为层面评估，而不是当成一次存储操作。

认知价值：① 删除是图操作，不是行操作。 摘要、画像、结论卡片都是原记录的「后裔节点」；删父节点不会自动改子节点。任何声称「已删除用户数据」的系统，只要存在派生态（摘要/embedding/缓存/preference），就必须回答「后裔怎么办」。② 为什么「逐字过滤器」注定失效： 信息可以以碎片 + 公开的拼接规则存在——这不是加密，是拼图。62%–99% 的重建率说明：只要每一块碎片都合法留存，整句就能被合法还原。这直接适用于 RAG 与 prompt 缓存场景下的「删文档」：删掉原文，不等于删掉模型能重建出的知识。③ 方法论比结论更值得抄：匹配未暴露对照。 没有对照组的删除审计无法区分「真泄漏」与「碰巧猜中」，而没有归因的指标上升，本身可能就是污染。我们的评测同理：任何「提升」在没有对照的条件下都不构成证据。 ④ 对自家知识库是一条硬提醒。 我们的知识库是「md 单源 + Obsidian 直读」，一条笔记删掉之后，索引、摘要、引用它的下游文档都还在；涉及个人信息与授权内容时，正确做法是闭包删除（连带下游派生），而不是只删那一行 md。⑤ 边界：合成秘密、固定权重 agent、7B 级模型、正基线设定有限；论文验证的是「能被单条查询恢复」，不是真实生产记忆库的泄漏面。另注意它把「重建 / 写回 / 新会话召回」三种失败分开测——这三件事在工程上的修法完全不同。

领域：agent-frameworks ｜ 去向：related（挂钩 10-22 ③ MemoryTax：那条讲记忆「写什么」的成本与上限，这条讲记忆「删不掉」的后果，两条可合成一篇「记忆系统的账本」）｜ 等级：🟡

来源：🟡 预印本（2026-10-23 直读摘要页）https://arxiv.org/abs/2610.31366 《AfterDeleteBench: Auditing Post-Deletion Information Persistence in LLM Agents》Submitted on 22 Oct 2026（原文含：25 页 / 7 图 / 12 表；单条查询从 Qwen2.5-7B-Instruct 恢复已删秘密约 2/3、匹配未暴露对照为 0；碎片 + 公开拼接规则的精确重建 62–99%（Qwen / Mistral / Phi-3）；「the response interface is part of the measurement system」；provenance-aware closure 消除可观察恢复、字面写入过滤器无法抹除已在下游的信息）

② Claude 在 123 个开源库里证明「不会崩」，能自己核的证明只公开了 25 个库、60 个入口（Anthropic × Theorem，2026-10-22）

这条最该看的不是「AI 会写证明了」，是这条命题的边界写在哪。 Anthropic 于 2026-10-22 发布研究帖《LLMs are making formal software verification feasible at a much larger scale》，与 Theorem 合作，用 Claude（文中为 Opus 5.5）在 RISC-V 汇编层为 123 个开源库证明了安全属性。命题写得很具体：这些程序对每一个小于 64MB 的输入、每一种被建模的 Linux OS 响应与内存布局，都会正常退出，不触发内存安全错误、不失败断言——前提是单线程静态二进制、固定内存预算、跑在 RISC-V CPU 上的 Linux。他们称这是「首个大规模用 AI 把形式化验证用到生产软件汇编层」的尝试（厂商口径）。写证明的过程中，Claude 还找到了多年、数万亿次测试运行都没发现的 bug：比如某库解压器副本里的计数器下溢导致越界写，只在约 20MB、且带一种罕见布局的输入上触发（模糊测试的典型输入上限是 1MB、靠覆盖率引导，基本碰不到）；另有一处图像解码器的越界读。效率侧给了可读的曲线：36 个形式化验证任务，每个任务三次独立的单 agent 尝试、每次 5M token 预算，按首次完成计为「已证明」，Opus 5.5 比更早模型完成得更快。产物也放出来了：证明子集在 theorem-labs/oss-verify-proofs（MIT，10-22 建仓、10-23 仍在推送），其 README 自报 25 个库、60 个入口点有证明，用 Rocq 9.2.0 检查，命题建立在 LPS（一个「跑 RISC-V 二进制的 Linux 进程」形式模型）上，并明确写着「LPS is best effort and not complete」；配套还有 RISC-V/OS 语义仓库 rocq-linux-process-semantics 与一个帮开发者上手的 Claude skill。另有几条探路：为 RFC 1950 写形式规范、并证明 Linux 内核里的 zlib 实现正确实现了该规范（同样在二进制层）；以及证明一个 Rust 写的 Python 解释器的行为等价。HN 上这条 348 分 / 205 评论（10-22 22:54Z）。参照系：seL4 内核实现用了 2 人年，形式化验证用了 20 人年。

认知价值：① 边界即结论。 它没说「没有 bug」，说的是「在三条写明假设下，不出现某一类 bug」——64MB 上限、单线程静态二进制、固定内存预算。这三条把证明锚回工程可用的范围，也正好划出它管不到的领域（多线程、动态链接、超大输入）。看到一个「已被证明」的软件，先问四件事：证的是什么属性、假设是什么、模型可信到什么程度、谁来复核。② 123 库 vs 公开 25 库 60 入口，这个差不是问题，是常态。 宣传数是总数，可复核数是子集；判断价值的标准是公开集能不能被第三方跑起来（Rocq 9.2.0 + LPS 语义 + 仓库里的 release-check CI）。这也解释了为什么「论文 + 可跑产物」比「论文 + 视频」值钱一个量级。③ bug 的形态变了。 计数器下溢只在 20MB、特定布局下触发——这不在「更努力地测」的能力范围内，而在采样偏差之外的区域。数万亿次测试与一次证明不是同类证据：一个是采样，一个是全称量化（在给定上限内）。这一条对任何「我们测了很多遍」的论点都是直接反驳。④ 可操作性。 Theorem 把管线做成了招生式服务（开源项目可报名 oss-verify），并给了 Claude skill 让人从零搭。自己的项目更现实的第一步不是「证明整个程序」，而是给一个解析入口写「不越界」这种小命题——先跑通检查链，再扩属性。⑤ 风险要写清： LPS 自称不完备，证明只和模型一样可靠；证明生成用的是专有模型，社区能复核证明本体，不能复现生成过程；「首个大规模」是厂商口径，不是第三方认定。

领域：eval-evidence ｜ 去向：feeds（喂养「证据的可检验性」选题：与 10-22 ① PHP 那两个 CVE 的「数千个假 PoC 同分布」并置——一边是证据批量生产，一边是证据被机器检查，正反两面同一讲）｜ 等级：🟡

来源：🟡 厂商研究（2026-10-23 直读页面，JSON-LD datePublished = 2026-10-22、页面 <time> = Oct 22, 2026）https://www.anthropic.com/research/formal-verification 《LLMs are making formal software verification feasible at a much larger scale》（原文含：123 个开源库、RISC-V 汇编层、每个小于 64MB 的输入、单线程静态二进制 / 固定内存预算 / RISC-V + Linux 三条假设、数万亿次测试、Opus 5.5、36 个任务 × 3 次独立尝试 × 5M token 预算、seL4「2 人年实现 / 20 人年验证」、zlib + RFC 1950、Rust 版 Python 解释器行为等价）｜🟢 一手已核（GitHub API + 仓库 README 原文，2026-10-23）https://github.com/theorem-labs/oss-verify-proofs （MIT；建仓 2026-10-22、push 2026-10-23；README 原文：「60 entry points in 25 libraries have proofs」「checked with Rocq 9.2.0」「stated in LPS, a formal model of a Linux process that runs a RISC-V binary」「LPS is best effort and not complete」）｜🟢 HN Algolia（348 分 / 205 评论，2026-10-22T22:54:43Z，item 50202217）

③ 推理剪枝别再「质量」「多样性」二选一：直接在候选池上优化 pass@k，8 个开源推理模型超过两类既有方法（arXiv 2610.31667，2026-10-22）

测试时扩展最贵的一步不是采样，是把每一个候选都写到底。 现在通行的省钱办法是：只让模型生成很短的前缀，就砍掉大部分候选，把算力留给幸存者（2610.31667，提交 2026-10-22，作者 Mahdi Salmani、Adel Javanmard、Devansh Gupta、Meisam Razaviyayn）。既有剪枝分两派：质量型给每个部分解打分，丢掉那些被预测会走错的；多样性型挑推理轨迹彼此不同的，指望它们覆盖不同的最终答案。这两派的分歧本质是探索与利用的张力，但此前没有人把这个权衡直接暴露出来、更没人直接优化它。这篇的做法是：把「选哪些候选继续写」写成一个优化问题——选那个让「池子里至少有一个候选续写后得到正确答案」的概率最大的集合，也就是在选出的池上直接优化 pass@k。由于这个目标同时奖励高质量的部分解、又惩罚它们之间的冗余，质量与多样性是由准则本身平衡的，不靠两套 ad-hoc 的打分加权。结果：在 8 个开源权重推理模型上，该方法超过既有的质量型与多样性型剪枝策略；增益在「剪枝后保留中等数量候选继续生成」时最明显。

认知价值：① 别再为代理指标调参，直接优化你在意的那个量。 想提高「至少一个对」的概率，就把这个概率当目标函数；「质量分 × α + 多样性分 × β」这种两段式设计，本质是把张力藏在两个超参里，让人永远调不到头。这是「指标即目标函数」最干净的一个实例，可以迁移到检索（要的是「召回里至少有一条能回答」而不是「平均相关度最高」）、数据合成（要的是「池子里覆盖了所有子类」而不是「平均质量分」）。② 「中等数量」这个细节是部署参数。 保留太少，没有可选的；保留太多，等于没剪，白花钱。既然增益集中在中间区间，就该拿它去定「前缀长度 × 保留数 × 完成预算」这组预算三角，而不是拍一个 k。③ 对我们自己的评测是硬约束： 如果一边用 pass@1、一边用 n 个样本取均值来比较两个方案，剪枝策略一换，结论就可能整体翻转——跨方案比较必须固定候选池、预算与前缀长度，否则测的是预算，不是能力。④ 边界：预印本；8 个开源推理模型、数学/代码类推理基准；摘要未给具体增益幅度，也未给延迟与显存实测（若要写进视频，这两个数得回论文表里核）；判分依赖标准答案，开放式任务不直接适用。

领域：inference-efficiency ｜ 去向：feeds（喂养「测试时扩展的真实成本」选题：与 10-21 ① DeepInfer 的「读缺口清单再决定算力往哪花」同题不同层——那条讲预算怎么分，这条讲候选怎么砍）｜ 等级：🟡

来源：🟡 预印本（2026-10-23 直读摘要页）https://arxiv.org/abs/2610.31667 《Direct Pass@$k$ Optimization for Thought Pruning: Balancing Quality and Diversity in Test-Time Reasoning》Submitted on 22 Oct 2026（原文含：短前缀后剪枝候选池、质量型 vs 多样性型两派、「optimizing pass@$k$ over the selected solution pool」、8 个开源权重推理模型上超过两类基线、「gains are particularly pronounced when the pruning procedure keeps a moderate number of partial solutions」）

④ 5B 生图模型把「文字和版式」当主战场：Comfy 镜像仓一周 160 万次下载，官方自评的覆盖率 96.3% 不等于逐字正确（MOSS-Image，技术报告 2026-10-16）

它没去争「谁画得更美」，它去争「谁把字排对」。 OpenMOSS 团队的 MOSS-Image（模思智能 + OpenMOSS）核心里是一个从零预训练的 5B 单流 DiT，分 Base 与 SFT 两版，权重 Apache-2.0，HF / ModelScope / GitHub 全放。技术报告（arXiv 2610.23374，提交 2026-10-16）把目标写得很直白：开放权重模型在密集文字与复杂版式上仍然不行，所以两条腿走——一边是能渲染双语长文本、支持精确布局控制的 5B 主干，一边是一个「意图感知」的 agentic 提示增强模块，把用户的一句话翻成内容规格与布局规格（summary + items + bounding box，文本条件最长 4096 token）。为了让这件事可测，团队自己造了两个基准：LLTB（LongLongTextBench，长文本中英渲染）与 RLA（RealLayoutArena，端到端富版式生成）。自评结果：LLTB 上平均文本覆盖率 96.3%、开放权重第一；RLA 端到端系统对比第二，主干在「共享增强提示词」条件下第一。生态侧的数字可以直接核（HF API，2026-10-23 直读）：Comfy-Org 镜像仓累计 1,606,363 次下载（10-16 建仓）、官方 MOSS-Image-SFT 仓 7,658 次下载 / 612 likes、GitHub OpenMOSS/MOSS-Image 1,548★（Apache-2.0，10-16 建仓、10-20 最后推送）；量子位 10-23 的报道口径是「上线 4 天超 130 万下载」。社区衍生件已经铺开：8 步 / 4 步加速、INT8 量化、GGUF、摄影与动漫 LoRA、ComfyUI 工作流。两个工程细节值得记：官方 quickstart 要求 NVIDIA GPU + CUDA（PyTorch 2.9+），Mac 本地只能走社区路径（未验证）；训练据团队对媒体披露用了国产 PPU 算力平台（技术报告未见此描述）。

认知价值：① 生图竞争的重心正在从审美转向可测量的版面正确性。 「文字覆盖率」和「bbox 定位 mIoU」是能被机器判的，而「好看」不能。凡是能被判的部分，都会先被卷到饱和——这对做封面、海报、信息图的人是最直接的红利，也是判断一个生图模型该不该换的唯一硬指标。② 96.3% 是覆盖率，不是正确率，这个区别必须说清。 覆盖率衡量「目标文字有没有出现」，不等于逐字无误；量子位原文也这么写。媒体在转述时最容易把这层抹掉——「参评第一」+「覆盖率」两个词放在一起，读者会自动读成「字都对」。这跟我们自己写评测的口径同一条红线：指标名与指标含义必须同时给。③ 自建基准的双刃： LLTB / RLA 是团队自己提的，好处是补了空白（此前没有长文本中英渲染的统一测法），坏处是无人复核、也不排除对自己有利的分布。可采信的做法是等第三方把 FLUX.3-klein、Krea2、Qwen-Image 2.1 拉到同一提示词下复测（社区已经在做，但都还是零散的 Reddit/X 帖）。④ 160 万次下载里有很大一部分是镜像与 CI 拉取，不能当用户数读。 真正说明问题的是分发路径：Comfy-Org 原生打包让它在 4 天内被看见，这比参数规模更决定采用度。⑤ 对我们的用法： 写实照片级继续走 M5 的 klein-9B；MOSS-Image 的差异化在带字的海报/图表/封面——正好是自牧封面与锐Owl 图文里最痛的一环。但官方管线 CUDA-only，Mac 侧要先用社区 GGUF/ComfyUI 路径验证一遍再谈进产线。

领域：industry-model ｜ 去向：feeds（喂养「带字封面」的产线实验：以自牧封面为题做 MOSS-Image vs M5 klein-9B 的同提示词对照，判据只取「文字正确率 + 版式命中」，不取观感分）｜ 等级：🟡

来源：🟡 厂商报告（2026-10-23 直读摘要页）https://arxiv.org/abs/2610.23374 《MOSS-Image Technical Report》Submitted on 16 Oct 2026（原文含：5B single-stream DiT 从零预训练、双语长文渲染与精确布局控制、agentic prompt enhancement、自建 LLTB 与 RLA、LLTB 平均文本覆盖率 96.3%、RLA 端到端第二 / 共享增强提示词下主干第一）｜🟢 一手已核（HF API，2026-10-23）https://hf-mirror.com/api/models/Comfy-Org/MOSS-Image （downloads 1,606,363、createdAt 2026-10-16、lastModified 2026-10-22）｜🟢 一手已核（HF API）https://hf-mirror.com/api/models/OpenMOSS-Team/MOSS-Image-SFT （downloads 7,658 / likes 612 / createdAt 2026-10-11 / license apache-2.0 / arxiv:2610.23374）｜🟢 一手已核（GitHub API）https://github.com/OpenMOSS/MOSS-Image （1,548★、Apache-2.0、created 2026-10-16、pushed 2026-10-20）｜🟡 媒体口径 https://www.qbitai.com/2026/10/504930.html 量子位《国产5B生图模型海外突然爆火，4天超百万下载》2026-10-23 16:50（「上线仅4天…收获130万次下载」、「1.4k Stars」、LLTB Mean-6 覆盖率 96.3%、7Bench 布局 0.88 mIoU / 0.70 AUC、RLA Elo 1698.70 第二 / 统一增强提示词下 1807.34 第一、4096 token、Qwen3.5-9B 文本编码器 + FLUX.2 VAE、国产 PPU 训练、官方 quickstart 需 NVIDIA GPU + CUDA）

⑤ NVIDIA 给 agent 运行时上了「内核级策略 + 策略变更形式化预检」：给权限这件事，开始要求出证明（OpenShell，v0.1.5 于 2026-10-20 发版）

agent 一旦能读文件、装包、调 API、拿凭证，它缺的就不是能力，是边界。 NVIDIA 的 OpenShell 把自己定位成「一群自主 agent 的安全私有运行时」：你声明每个 agent 能碰什么（policy），运行时负责强制执行。它靠两条腿：① 内核级执行——每个 agent 跑在隔离沙箱里，内核控制限制它能访问哪些文件、能发哪些系统调用，每一条网络连接在离开沙箱前都要过策略检查；agent 永远看不到真凭证，只有在请求发往已批准端点时，运行时才把凭证加进去。② 策略变更的形式化预检——一条策略改动在生效之前，先用形式化验证算一遍它会新放开什么，并把组合风险标出来（比如「能连一个新主机、同时还带着凭证」「能调一个新的 API 方法」），这类变更必须等人复核。仓库事实可以直接核：18,172★ / 1,848 fork，Apache-2.0，2026-02-24 建仓、10-23 当天仍有推送；最新 v0.1.5（2026-10-20）、上一版 v0.1.4（10-13），0.1.x 起给了稳定发版节奏与新隔离原语。**10-22 17:44Z（北京时间 10-23 01:44）**它上了 HN 首页，398 分 / 194 评论。运行环境：Linux、Apple Silicon 上的 macOS、或 Windows + WSL2（实验性），需要 Docker / Podman / 宿主虚拟化；上 K8s 时要求 CNI 真的执行 NetworkPolicy。默认沙箱是极简 Ubuntu、不预装任何 agent，官方教程用 OpenCode 配一个免费 OpenRouter 模型演示「agent 边走边申请、人逐条批」。

认知价值：① 权限的粒度问题被摆到台面上了。 大多数 agent 框架给的权限包是「一串 API key + 一个 shell」，等于把整台机器交出去；OpenShell 把权限拆成文件 / 系统调用 / 网络三类分别执行，并且凭证不进沙箱（只在出站请求上注入，且限定端点）。这是最小权限原则在 agent 上的落地形态，比「用完删 key」这种事后办法靠谱。② 最值钱的是那个「策略变更先证明」的设计。 agent 要新权限时，人的默认动作是点同意——因为不看懂 diff、也算不出组合后果。把 diff 送进形式化预检，把「新主机 + 凭证」「新 API 方法」这种单看每一项都无害、组合起来才有风险的变更提前标出来，等于给「同意」按钮加了一层证据。这跟今天 ② 是同一件事的两端：证明的单价下降之后，验证会被塞进日常流程，而不是留在论文里。③ 一条必须说清的反例：沙箱挡的是「越权」，挡不住「被说服」。 prompt injection 里的调用往往是合法的——用的是被批准的端点、被允许的文件。隔离与最小权限降低的是爆炸半径，不是注入成功率；这两件事经常被混为一谈。④ 运维视角： 本机在 Apple Silicon + Docker/Podman 这条路被官方列为支持（未实测）；默认沙箱不装 agent，意味着「装上就能用」不成立，得先想清楚镜像里放什么、policy 从哪来、谁复核变更。对夜间无人值守跑批这类场景，这种可审计的运行时比自建 docker + 手工白名单更值得试。

领域：agent-frameworks ｜ 去向：feeds（喂养「无人值守 agent 的权限边界」选题：可与本机夜间跑批的实际需求对照——policy 怎么写、变更谁来批、出问题怎么回滚）｜ 等级：🟢

来源：🟢 一手已核（仓库原文 + GitHub API，2026-10-23 直读）https://github.com/NVIDIA/OpenShell 《OpenShell is the safe, private runtime for fleets of autonomous AI agents》（README 原文含：kernel-level enforcement（文件 / 系统调用 / 网络逐条过策略）、「Agents never see real credentials; OpenShell adds them only to requests bound for approved endpoints」、「Before a policy change is approved, OpenShell uses formal verification to flag risky new access…so those changes wait for human review」；支持 Linux / Apple Silicon macOS / Windows WSL2（experimental）+ Docker / Podman / host virtualization；K8s 需 CNI 执行 NetworkPolicy；默认沙箱为极简 Ubuntu 且不预装 agent）｜🟢 一手已核（GitHub API）18,172★ / 1,848 fork / Apache-2.0 / created 2026-02-24 / pushed 2026-10-23T08:31Z；releases：v0.1.5 = 2026-10-20T17:28Z、v0.1.4 = 2026-10-13T20:48Z、dev = 2026-03-18｜🟢 HN Algolia（398 分 / 194 评论，2026-10-22T17:44:06Z，item 50198675）