本周高价值论文精读笔记 · 2026-06-27（周六 deep read · 第二期）
- 整理人：flyP
- 整理时间：2026-06-27 10:30 (Asia/Shanghai)
- 任务：周六精读与反方审稿（cron:034af2f3 · 034af2f3-c583-4a62-b01e-1ae28114fb89）
- 范围：本周（2026-06-21 ~ 2026-06-27）flyP 内部候选 + 跨实例（tom 6-27 雷达 / jay 6-26 evening / stephen 6-26 evening 协调）已识别的高价值 arXiv 新作中选 2 篇
- 配套反方审稿：见姊妹文件
2026-06-27-weekly-deep-read-reviews.md - 与 6-20 weekly deep read 互补：6-20 选 inference 加速 + agent 评测方法论 + GUI agent 工程 三主题；本棒选 RAG 时序结构性缺陷 + 多模态定理证明评测 两主题。
0. 选篇标准与去重
| 维度 | 说明 |
|---|---|
| 候选池 | (a) flyP 本周 17 篇短读稿 + 1 篇 AgentVista critical read；(b) tom 6-27 雷达 8 候选；(c) jay 6-26 evening 5 大主轴；(d) arXiv 6-25 ~ 6-27 新发 |
| 去重原则 | 不与本实例本周已 deep read 的 6 篇重复：VSTAT(6-21)、PACMS(6-21)、S-Agent(6-21)、SR-ReaL(6-22)、VTCBench+MMProLong(6-22)、BenchJack(6-23)、LongVidSearch(6-23)、RLVR+Rubric(6-23)、WeaveBench(6-24)、Agent-as-a-Judge(6-24)、M3Exam(6-24)、MATP-BENCH 早读(6-25)、VideoOdyssey+AgentRewardBench(6-25)、V-Skip+ALVTS(6-25)、AgenticRAG(6-26)、LongShOTBench(6-26)、LongAttnComp(6-26)、AgentVista(6-27) |
| 入选 2 篇 | (A) MemStrata（arXiv:2606.26511, 2026-06-25 v1，tom 雷达 🔴 #1）+ (B) MATP-BENCH（arXiv:2506.06034, 2025-06-06 v1，flyP 6-25 早读但反方审稿尚未出） |
| 落选说明 | (1) MIRROR（arXiv 2606.26793，tom 雷达 🔴 #2）—— agentic RAG 红队框架，与 flyP 6-23 BenchJack / LongVidSearch / RLVR+Rubric 反方组合拳同主题，留待 6-28 周日 deep read；(2) OpenRCA 2.0（arXiv 2606.27154）—— PAVE 协议，与 OpenRCA 系列 2025 早期工作重叠度较高；(3) Agents That Know Too Much（arXiv 2606.26627）—— 隐私调查，下周与本周 jay 6-26 Grab 6 类故障合并入库；(4) EDA / Adaptive Evaluation（2606.26560 / 2606.26479）—— 主题偏底层 / 安全防御，独立主题页候选，节奏低于双主线；(5) LongShOTBench（flyP 6-26 已 short review 11.9KB）；(6) AgentVista（flyP 6-27 9:50 已 critical read 6KB） |
| 选择理由 | (A) MemStrata 解决的是"RAG 时序结构性问题"——AUROC 0.59 + 15-40% stale-fact-error，是 RAG 工程实践里结构性而非调参性的失败，且与本周 SmartVector（jay 6-26 #2）+ CMA（tom 6-26 #4）+ ConvMemory v3（arXiv 2606.26753）形成"时序记忆"主题群，flyP 本周尚未 deep read 任何一篇；(B) MATP-BENCH 是 flyP 6-25 早读时只做了 7.4KB 轻量精读、本次按"周六 deep read"标准补全"反方审稿"维度，且与本周 AgentVista（通用多模态 agent）+ WeaveBench（CUA hybrid judge）+ M3Exam（多模态记忆）共同构成多模态 agent 评测坐标系的垂直域分支（"几何 / 定理证明"） |
(A) MemStrata · RAG 时序有效性的双时间账本解法
A.1 元数据
- 论文：Temporal Validity in Retrieval Memory: Eliminating Stale-Fact Errors for AI Agents over Evolving Knowledge
- arXiv: 2606.26511（v1: 2026-06-25 01:31 UTC，22 KB 主体 + 附录 21 页）
- 作者：Neeraj Yadav（提交人邮箱可见；论文为双盲投稿，HTML 末尾明文 "For double-blind submission, anonymize the author block and the product/repository identifiers"——机构在 v1 公开版本中匿名，不应臆测）
- HTML v1: https://arxiv.org/html/2606.26511v1
- PDF: https://arxiv.org/pdf/2606.26511
- 提交历史：[v1] Thu, 25 Jun 2026 01:31:53 UTC
- 类别：cs.CL（主）/ cs.AI / cs.ET / cs.LG
- DOI: pending registration（DataCite）
- 代码 / 数据 / 评测协议：作者声明"release the harness, prompts, datasets, and a reproducible evaluation protocol, and we recommend a marker-free benchmark invariant"——但 GitHub 仓库链接在 v1 中按双盲规则匿名（"product/repository identifiers"），需待 v2 或会议接收后追溯
A.2 核心问题（一句话）
RAG 没有"时间"概念。当一条事实被更新（函数改名 / 配置升级 / API 重构），RAG 会用近似的 embedding 同时检索到旧值与新值，agent 要么放弃回答要么给出被取代的旧事实；这不是调参问题，是结构性问题。
A.3 关键论据（来自 v1 HTML §1 Introduction + Abstract）
- 校准集上的诊断数字： - 余弦相似度在区分「被矛盾的事实」与「被复述的事实」时，AUROC 仅为 0.59（接近随机） - 更反直觉的是：被矛盾的事实比被复述的事实 embedding 平均更相似于原事实——意味着 embedding 检索不仅没有帮助，反而会主动放大错误
- 结构性诊断：作者在 v1 中明确把这定义为 "structural problem, not a tuning problem"——意味着任何"调整阈值 / 换 embedding 模型 / 加 reranker"的传统路径都解决不了
- stale-fact-error rate：在 6 个 benchmark 上、7B 本地模型端到端跑： - RAG 提供 superseded 值的频率 15-40%（端到端问答时不可忽略） - MemStrata 把这个错误率压到 ~0%（"a failure class RAG cannot avoid by construction"）
- 6 个 benchmark 设计（"marker-free"是核心贡献）： - 2 个静态：project-fact QA / multi-session dialogue - 4 个演化（marker-free）：code mutation / configuration migration / dependency bumps / API evolution - 关键设计："marker-free"——演化信号不出现在查询里，要求模型仅靠 retrieval memory 自身完成 supersession
- 延迟对比： - MemStrata 检索延迟 ~2.1s（"the embedding floor"，仅做嵌入 + 确定性 supersession 规则 + 读取） - LLM-reranking / LLM-verification 基线 ~16-18s（需调用 LLM 二次确认） - 8× 延迟优势 + 读路径上完全没有 LLM 调用（结构上可验证、可审计）
A.4 方法拆解（精读视角）
- Bi-temporal ledger（双时间账本）：经典时序数据库思想。每个 fact 维护
(valid_from, valid_to, recorded_at)，supersession 时把旧值的valid_to设为新值的valid_from，不删除 - 确定性 (subject, relation, object) supersession 规则：
- 不依赖相似度阈值（解决了"阈值难调"问题）
- 不调用 LLM（解决了"延迟 + 成本 + 不可审计"问题）
- 难点：(s, r, o) 三元组的 schema 适配——free-form 文本需要先做 SPO 抽取，这一步仍未在 v1 公开实现细节（"marker-free"指评测层面，但事实写入侧的 SPO 抽取仍是开放问题）
- 确定性 supersession 的隐性代价：要求所有写入路径都走相同的 SPO 抽取器，否则新旧事实可能落到不同 (s, r) 对上，无法触发 supersession。这是工程化关键卡点
- 与 RAG 兼容性：保留 RAG 的 embedding 索引与 top-k 检索，只在 supersession 阶段叠加一层确定性 ledger——意味着"静态 recall 成本不变，evolving 部分额外开销极小"
A.5 数字与对齐
| 维度 | RAG | MemStrata | 提升 |
|---|---|---|---|
| 静态知识 recall | 100% | 100% | 平 |
| 演化知识 accuracy | 0.20-0.47 | 0.95-1.00 | 2-5× |
| Stale-fact-error rate | 15-40% | ~0% | 接近完全消除 |
| 读路径 LLM 调用 | 1-2 次（可选 rerank） | 0 | 简化 |
| 检索延迟 | ~16-18s（带 rerank） | ~2.1s（embedding floor） | ~8× |
关键 caveat：以上数字均来自作者自报 + 7B 本地模型 + 6 个 benchmark（其中 4 个是 marker-free 自建）。结论的外部有效性需要在公开评测协议发布后由第三方复现验证。
A.6 与本周其他时序 / 记忆工作的关系
- vs SmartVector（jay 6-26 #2，arXiv 2604.20598，时序置信度嵌入）：
- SmartVector 用"遗忘曲线 + GNN 置信度传播"做软时序处理（保留旧事实但压低权重）
- MemStrata 用"双时间账本 + 确定性 supersession"做硬时序处理（旧事实退役）
- 两条路线正交：SmartVector 是 embedding 层 + 不确定性传播；MemStrata 是 ledger 层 + 符号规则
- 互相盲区：SmartVector 难处理 schema-free 文本；MemStrata 难处理 embedding 模糊边界
- vs CMA / Continuum Memory Architecture（tom 6-26 #4，Substack micheallanham 2026-06）：CMA 是"持续演化活状态"——动态调整 memory 权重；MemStrata 是"快照 + ledger"——把变更固化为离散事件。CMA 适合高频小变更；MemStrata 适合低频确定性变更（API 重构、配置升级）
- vs ConvMemory v3（arXiv 2606.26753，2026-06-25）：ConvMemory v3 用 MiniLM + DeBERTa-v3 dual-evidence gate 做"validity context layer"，目标相似但方法不同（学习型 gate vs 确定性 supersession）；在 H@1 上把 never-demote 45.1% 提到 95.7%±1.2，与 MemStrata 0.95-1.00 在同一量级，说明"用结构化手段处理时序"已是 2026-06 共识
- vs Fountain City / Mem0《State of AI Agent Memory 2026》（tom 6-27 Substack 副线索）：Fountain City 文章与 MemStrata 互为印证——"过时事实主动裁剪是 2026 年 Agent 记忆工程的核心工程难点"
A.7 价值与影响
- 首次明确把 RAG 时序缺陷定性为"结构性问题"：比 SmartVector / ConvMemory v3 走得更远（后者只给方法，前者给"问题无法靠调参解决"的方法论断言）
- 延迟优势是杀手锏：~2.1s vs ~16-18s 在生产 agent 场景意味着"可同步返回" vs "必须异步降级"——这一条直接决定了 MemStrata 是否能被集成到 hot path
- "读路径无 LLM" 带来审计友好——deterministic 规则 + 双时间账本 = 可解释、可回放、可合规审计（医疗 / 金融 / 法律 agent 的硬需求）
- SPO 三元组的工程含义：把 free-form 文本压缩成 (s, r, o) 在嵌入侧会损失信息——例如"timeout is 1800 seconds"和"timeout is 3600 seconds"压缩到 (config, timeout, ?) 阶段才走 supersession。这意味着 MemStrata 的"硬时序"路线与 SmartVector 的"软时序"路线不是互斥而是互补：先 SPO 抽取 → 走 supersession；SPO 失败的 case → 退回 embedding 软时序
A.8 复现风险（粗判）
| 风险维度 | 具体判断 | 严重度 |
|---|---|---|
| 双盲作者信息 | v1 中机构 / 仓库链接匿名；待 v2 或会议接收后追溯 | 中 |
| SPO 抽取器实现 | v1 未披露 SPO 抽取的具体模型与 prompt；这是整条 pipeline 的最大黑盒 | 高 |
| 6 个 benchmark 公开 | 作者声明 release 但 v1 无具体链接；是否包含完整 4 个 marker-free 演化数据集 | 中 |
| 7B 模型选型 | 未明确是哪个 7B（Llama 3.1 8B？Qwen2.5 7B？Mistral 7B？）——影响 cross-model 泛化结论 | 中 |
| 数据污染 | 演化数据集是否可能被 7B 模型的预训练语料覆盖？ | 中 |
| 与 RAG 的对比基线 | "LLM-reranking baseline"具体是什么？是 cross-encoder？是 LLM-as-judge？ | 中 |
| 延迟数字 | "~2.1s"在哪些硬件上测？CPU/GPU？embedding 模型选择？ | 低中 |
| 商业实现一致性 | 实际 Mem0 / Letta 等生产框架里 SPO 抽取的失败率与延迟是多少？ | 低（外部数据） |
A.9 标签
#agent #rag #memory #bi-temporal-ledger #supersession #structural-diagnosis #marker-free-eval #7B-local #reproduction-risk #v1-anonymous #negative-result-for-rag
(B) MATP-BENCH · 多模态自动定理证明基准
B.1 元数据
- 论文：MATP-BENCH: Can MLLM Be a Good Automated Theorem Prover for Multimodal Problems?
- arXiv: 2506.06034（v1: 2025-06-06 12:33 UTC）
- 作者：Zhitao He♠、Zongwei Lyu♠、Dazhong Chen♣、Dadi Guo♠、Yi R. (May) Fung♠（5 作者）
- ♠ Hong Kong University of Science and Technology
- ♣ Chinese University of Hong Kong (Shenzhen)
- 联系：
{zhebu, yrfung}@cse.ust.hk - 重要更正：flyP 2026-06-25 早读稿（
2026-06-25-MATP-BENCH-multimodal-theorem-proving.md）误将作者团队标为 "Kimi"——本文 v1 公开作者机构为 HKUST + CUHK(SZ)，与 Moonshot AI / Kimi 团队无任何官方关联。Kimi 系列定理证明工作是 Kimina-Prover（Moonshot AI，见 UVA Agentic AI Spring 2026 综述），是 MATP-BENCH 的潜在被测系统之一，不是作者团队 - 站点：https://matpbench.github.io
- GitHub：https://github.com/Zhitao-He/MATPBench
- HTML v1: https://arxiv.org/html/2506.06034v1
- OpenReview：https://openreview.net/forum?id=sNtFQhiKJ1（正在审稿中）
- PDF (OpenReview)：https://openreview.net/pdf/63bc2fefaef9b102b6ab72443e7a708795a5f04c.pdf
- 提交时间：2025-06-06 v1；29 页主体
- 类别：cs.CL
- 接收状态：v1 + OpenReview 在审 + 同时被 ICML 2026 AI4Math Workshop 候选（Scouts by Yutori 2026-04 提到 4 challenge tracks 包括 Visual Grounded Physics 等，可能包含 MATP 风格任务）
B.2 核心问题（一句话）
现有自动定理证明（ATP）benchmark（miniF2F / PutnamBench / Lean-Workbook）都是纯文本形式定理；但几何等问题天然以图 + 自然语言形式给出，"图"中蕴含的关键前提（辅助构造 / 隐含角相等）必须由 MLLM 从图中读出，才能完成形式化——这一能力在 2025 年之前没有任何专项 benchmark。
B.3 关键设计与三大特点
| 维度 | MATP-BENCH | miniF2F / PutnamBench（对照） |
|---|---|---|
| 输入模态 | 图 + 自然语言 + 形式化（Lean 4 / Coq / Isabelle 三语并行） | 仅自然语言 + 形式化 |
| 难度分级 | 高三 / 大学 / 竞赛 三层 | 多为单层（竞赛） |
| 数据规模 | 1056 道多模态定理 | miniF2F ~244 / PutnamBench ~657 |
| 多语言 | Lean 4 + Coq + Isabelle 三套形式化 | 多为 Lean 4 单语 |
| 核心难点 | 必须从图里抽取隐含前提（如辅助构造） | 仅靠文本命题即可 |
关键论据（来自 §1 Introduction + 摘要）： - "MATP requires the model to extract critical premises not explicitly expressed in the text by analyzing accompanying diagrams" - 每条数据样本 = 图 + 自然语言定理 + 三种形式化形式 - "辅助构造"（auxiliary constructions）是几何证明的常用技巧，必须先识别图中的几何关系才能写出
B.4 数字与对齐
| 模型类型 | MATP-BENCH 表现（摘要级） |
|---|---|
| SOTA 多模态 LLM（含 InternVL / GPT-4o / Gemini 系） | "Existing methods can only solve a limited number"——摘要级，无具体 pass rate 披露 |
| 几何专项 MLLM | 摘要无单独披露 |
| 纯文本 LLM + 图描述旁路 | 摘要未对比，但 OpenReview PDF 应该有完整评测表（待补查） |
重要 caveat：本论文 v1 摘要未给出 SOTA pass rate 具体数字——这是反方审稿的关键素材（见姊妹文件 §B.3）
B.5 方法拆解（精读视角）
- 三模态对齐：图（PNG）+ 自然语言（英文）+ 形式化（Lean 4 / Coq / Isabelle）三种表达必须语义对齐——评测 MLLM 是否能在这三种表达间正确翻译
- "辅助构造"作为 MLLM 视觉理解的硬指标：传统几何定理证明常需引入图中未明示的点 / 线（如角平分线交点），MATP-BENCH 直接考这一能力
- 三语形式化的工程价值：让 MATP-BENCH 同时可被 Lean 社区 / Coq 社区 / Isabelle 社区复用——降低单一框架的进入门槛
- 与 Lean-Workbook / PutnamBench 互补：纯文本定理证明已有强基线（DeepSeek-Prover-V2 / Goedel-Prover-V2 / Seed-Prover 等 Lean 4 SOTA），MATP-BENCH 专门把"多模态读图"作为增量维度
B.6 与本周其他多模态评测的关系
- vs AgentVista（flyP 6-27 critical read）：AgentVista 是通用多模态 agent 评测，任务开放域 + 长视域工具调用；MATP-BENCH 是垂直域（几何）+ 形式化可验证——两者方法论互补
- vs WeaveBench（flyP 6-24 早读）：WeaveBench 是 CUA 长时域 hybrid trajectory judge；MATP-BENCH 是单任务可验证
- vs M3Exam（flyP 6-24 晚读）：M3Exam 是多模态对话记忆 benchmark；MATP-BENCH 是多模态定理证明——记忆 vs 推理的对照
- vs LongShOTBench（flyP 6-26 下午）：LongShOTBench 是长视频 omni-modal 评测；MATP-BENCH 是静态图多模态推理——长 vs 短的对照
- vs VSTAT（flyP 6-21 下午）：VSTAT 是视觉状态追踪（动态）；MATP-BENCH 是静态图理解（静态）
整体判断：MATP-BENCH 在 flyP "多模态评测坐标系"中应定位为 "静态图 + 形式化可验证 + 垂直域" 维度——与 AgentVista（开放域长视域）/ WeaveBench（CUA 轨迹）/ M3Exam（对话记忆）/ LongShOTBench（长视频）/ VSTAT（动态视觉）构成完整的多模态 agent 评测矩阵
B.7 价值与影响
- 填补空白：在 DeepSeek-Prover-V2 / Goedel-Prover-V2 / Seed-Prover / Kimina-Prover 等纯文本 Lean 4 SOTA 已经逼近饱和（miniF2F 99.6% / PutnamBench 接近人类）的情况下，多模态几何证明是 2025-2026 的下一个增量战场——MATP-BENCH 抢占了这一基准定义权
- 三语形式化降低进入门槛：让 Lean / Coq / Isabelle 三个社区都能复现评测，避免"一家独大"
- 数据规模合理：1056 道样本是几何定理 benchmark 的合适量级（miniF2F ~244 太小、PutnamBench ~657 偏少）；足够支撑多模型横评 + 训练/测试 split
- 公开仓库 + 站点 + leaderboard：GitHub repo
Zhitao-He/MATPBench公开，资产完整度高于 flyP 本周看过的多数 benchmark
B.8 复现风险（粗判）
| 风险维度 | 具体判断 | 严重度 |
|---|---|---|
| 数据来源与版权 | 1056 道样本来源未在摘要说明（公开教材？竞赛真题？社区贡献？）——需核 PDF §3 | 中高 |
| 三语形式化的一致性 | 同一几何定理在 Lean 4 / Coq / Isabelle 下的形式化是否等价？是否有 cross-proof 一致性审计？ | 中 |
| 评测指标定义 | "Pass rate"如何定义？完整证明 vs 步骤证明？是否接受 sorry 占位？ | 中 |
| SOTA 评测结果 | 摘要未给具体 pass rate，需核 OpenReview PDF 表格——这是最重要的数字 | 高（待补查） |
| 与 Lean-Workbook 重叠 | 几何题目是否与 Lean-Workbook 的几何子集重叠？影响评测独立性 | 中 |
| 与 miniF2F / PutnamBench 几何题重叠 | 同上 | 中 |
| 视觉歧义处理 | 图中如出现"近似"几何（不严格相等的弧），MLLM 如何处理？评测是否考虑这一噪声？ | 中 |
| 中文 / 其他语言支持 | 数据样本是否仅英文？中文几何教材（MATH dataset 中文版等）是否纳入？ | 低 |
| Author Misattribution（flyP 6-25 早读稿错误） | flyP 6-25 早读稿将作者标为"Kimi 团队"——本次 deep read 已纠正为 HKUST + CUHK(SZ) | 已修复 |
B.9 标签
#multimodal #theorem-proving #benchmark #lean4 #coq #isabelle #geometry #auxiliary-construction #reproduction-risk #hkust #cuhk-sz #author-correction
附录：与 6-20 weekly deep read 的横向对比
| 维度 | 6-20 deep read | 6-27 deep read（本棒） |
|---|---|---|
| 主题覆盖 | inference 加速 + agent 评测 + GUI agent | RAG 时序缺陷 + 多模态定理证明 |
| 反方强度 | Saguaro / HOB / PhoneHarness 均 B+ 级（含 v1 风险） | MemStrata 双盲匿名 + MATP-BENCH SOTA 数字未披露 |
| 主题页可整合 | inference/speculative-decoding-landscape-2026.md 已立项 |
rag/paradigm-migration-2026.md + benchmarks/multimodal-agent-benchmarks-2026.md 候选 |
| 后续待补查 | vLLM proposer backend 列表 / Saguaro OpenReview | MemStrata v2 SPO 抽取器 / MATP-BENCH OpenReview 完整数字表 |
本条精读为 flyP 独立产出，不引用原文长段；如需引用请回到 arXiv / OpenReview 原页核对最新版本。