CAPRI: 契约感知的Isabelle证明修复 精读

深度精读多国团队合作的 CAPRI——面向 Isabelle 证明修复的契约感知工作流。核心洞察是『假成功』问题:LLM 不修证明,而是把要证的结论直接加进假设再用 by assumption 一步证完,Isabelle 完全正确地接受了这个被改弱的定理——build 通过不等于修复发生在授权边界内。CAPRI 的解法是双接受规则:Build(Isabelle 构建)与 Conforms(独立契约检查器逐字节比对保护区)缺一不可,配合 proof-body-only 最小暴露接口把违规提案物理挡在证明器之外。180 次冻结运行中,144 个被 Isabelle 接受的终态候选里有 6 个动了保护文本,全部来自可编辑完整理论的迭代工作流;而接口受限的 C2 零契约违规。论文给一切 LLM 辅助修改场景立了一条铁律:权限边界的验证必须独立于能力验证。

August 16, 2026 · 3 min

DIVE: 多样性驱动的冻结模型技能进化 精读

深度精读佐治亚理工与 Cisco Research 合作的 DIVE 论文——让只能通过 API 访问的冻结大模型,把任务经验进化成可持续复用的自然语言技能。从三大挑战(自修订噪声、经验超上下文、进化路径依赖)出发,拆解其核心机制:多种群独立进化维持假设多样性、异构算子组合 + UCB 自适应分配进化预算、算子本身也能进化、验证集上联合选择互补技能集。GPT-5-nano 借此平均 81.5 分反超 GPT-5 + ICL 且推理成本降低 42.5%,小模型逆袭大模型的路径首次如此清晰。

August 16, 2026 · 2 min

ERSkill: 检索技能与路由器共进化 精读

Agent 记忆系统的进化大多发生在“写入侧”——怎么抽取、压缩、组织记忆。深圳国际工业与应用数学中心等机构的 ERSkill 把目光转向被忽视的“读取侧”:检索机制本身。它把检索行为表示为由固定原语(实体搜索/BM25/稠密检索 + 三种扩展 + LLM 处理)组合成的可执行技能,用训练好的 router 按查询的信息需求派发技能;进化时用经验 trie 记录所有探索过的原语路径以避免重复提议,用 Pareto 式双前沿把“能力探索”与“router 面向的部署”解耦。三大记忆基准上整体平均提升 31.3%(Qwen3-Next-80B-A3B 骨干),LongMemEval 零训练迁移仍居首。本精读逐部分拆解其机制,并建立“查询异构性→技能化→证据密集型任务受益”的因果链。

August 16, 2026 · 4 min

Full-bandwidth transformer 精读

Full-bandwidth transformer(微软+JHU+普林斯顿,含 John Langford)指出自回归 Transformer 的垂直反馈通道极窄:步间只回传一个采样 token(至多 log2|V| 比特),顶层隐状态被直接丢弃。论文提出潜反馈解码(latent feedback decoding),用门控线性单元把上一步顶层隐状态与 token 嵌入融合后回灌输入端,配合多 pass 训练目标、渐进调度与 prefix mixin,在 1B 模型 400B token 预训练中验证:Math500 超越 1T token 标准基线、GSM8K 指令调优后 71.8 逼近 1T 基线、约 2 倍数据效率、base 模型推理链显著变短且精度不降,每 token 推理开销不到 1%。本精读覆盖带宽视角的动机、可达集理论、训练配方、实验因果链与可推广灵感。

August 16, 2026 · 5 min

Practice Makes Unsafe: 技能误进化 精读

自我改进的 LLM Agent 会把成功轨迹蒸馏成可复用技能,但一次“不安全的成功”也可能被写进技能库,在触发它的输入消失后继续潜伏。本文精读香港城市大学与阿德莱德大学的论文《Practice Makes Unsafe: Skill Misevolution in Self-Improving LLM Agents》:它提出概念“技能误进化”,构建了生命周期感知的测试环境 SKILLMISEVO-GYM 与冻结基准 SKILLMISEVO-BENCH,用“写入—检索—执行”三道门指标把风险归因到具体环节,并提出方法无关的治理包装器 SAFEEVOLVE。实验覆盖 25 个配置、每个 525 个任务:21 个进化配置全部写入了不安全技能,仅 15 个到达干净会话伤害;3 个恶意任务就把残留攻击成功率从 16.0% 推到 35.3%;SAFEEVOLVE 将不安全检索与残留伤害分别降低 26.7 和 17.3 个百分点,而良性效用只变化 0.4 分。

August 16, 2026 · 3 min

RippleMem: 从孤立检索到联想式回忆 精读

问一个 Agent’该不该听 Sam 的推荐带 Maya 去 Harbor Grill 吃饭’,正确的回答需要三条分散在不同会话里的证据:晚餐计划、Maya 的海鲜过敏、这家店是海鲜餐厅——直接检索只命中第一条,无向图扩展可能带出无关的订座偏好却恰恰漏掉过敏这条安全约束。本文精读中国传媒大学联合智联英才科技的 RippleMem:它把记忆访问从’一次性查找’重构为’证据条件化的联想式回忆’——已召回的记忆不是检索的终点,而是寻找缺失支持的线索。系统把交互历史写成线索丰富的情景记忆单元,组织成事件中心图,查询时从初始锚点沿语义与结构双通道局部扩散,定向找回缺失证据。在 LoCoMo 上 F1 52.49、LLM 裁判准确率 87.14 均为最佳,temporal 类超 SimpleMem 9.66 分,multi-session 从 60.92 提到 78.20;建图成本约为 Mem0g/Zep 的 1/30。本精读重点拆解其写读两阶段设计,并用因果链解释’evidence-distributed 题型为何增益最大’与'30 倍成本下降为何来自延迟建图’。

August 16, 2026 · 3 min

SkillEvo: 多轮交互反馈的自更新进化梯度 精读

深度精读腾讯云 Andon 与浙江大学合作的 SkillEvo 论文——把多轮用户模拟从评估终点反转为反馈生成器,让 Agent 技能在生产工单上自进化。从梯度衰减机制、可信反馈三条件(意图状态机、双侧正交评估、集体归因)到双层治理(有界修订、结构退化主动修复),全面拆解这套在腾讯云 9 个生产 Skill 上将 TSR 从 30.0 提升到 81.8 并落地生产环境的自进化框架。

August 16, 2026 · 2 min

SkillShapley: 技能步级Shapley归因 精读

深度精读北航与山东大学合作的 SkillShapley——首个面向 LLM Agent 技能的步级归因框架。它把 skill.md 的语义步骤视为合作博弈中的『玩家』,保留子集视为『联盟』,benchmark 成功率视为收益函数,用 Shapley 值量化每一步的真实贡献。针对『每个新联盟都要真实跑一遍 LLM agent』的高昂配置成本,BAES 用『warmup 锚点覆盖 + cache 感知自适应采集』两阶段策略,在同预算下产出远多于蒙特卡洛采样的可复用边际证据(99 配置预算下 206 条 vs 130 条)。案例研究给出一条朴素的技能写作启示:高价值步骤是连接任务条件与可执行决策的『程序性桥梁』,而背景解释性文本往往贡献为负。

August 16, 2026 · 3 min

【每日AI前沿追踪】2026年08月15日 核心技术与产业动态速递

8月15日(周六):HF/Arxiv无新批次,深挖8月14日批次未被覆盖的前沿论文——微软全带宽Transformer用潜变量反馈把垂直通道拓宽到全带宽,1B模型等效1.5倍训练数据;DFM Mimir以纯合规数据在1B规模逼近Qwen 3.5 4B;Agent记忆与技能两条主线集中爆发,RippleMem联想式回忆、ERSkill检索技能共进化、SkillEvo多轮反馈梯度、SkillShapley步级归因、DIVE多样性技能进化、Practice Makes Unsafe首次量化技能误进化风险;产业面GLM-5.3发布、Qwen3.8-27B开源生态刷屏、Anthropic营收破115亿美元首度运营盈利、英伟达5000亿美元AI融资平台落地、OpenAI年化收入破400亿但高管持续流失。

August 15, 2026 · 4 min

A Programming Paradigm for Spatiotemporal Composability 精读

北大与 DeepSeek-AI 合作的 88 页长文,为「插件系统、自进化 Agent Harness」这类动态组合软件给出了第一个完整的编程范式级形式化基础:把经典效应系统提升为可逆效应、把协同效应系统提升为响应式协同效应,统一成一个递归上下文类型,再配上动态组合演算与全套元理论(保持性、恢复精确性、活性、合流性),实现为 Cordis 元框架并在 Koishi(4000+ 社区插件)上验证。本文按背景、定位、问题、解法、评估、根源解释、知识反推、通用灵感八个层面完整拆解。

August 15, 2026 · 5 min