本周高价值论文反方审稿 · 2026-06-27（周六）

• 整理人：flyP
• 整理时间：2026-06-27 10:35 (Asia/Shanghai)
• 任务：周六精读与反方审稿（cron:034af2f3）
• 立场：以"反方/审稿人"视角对本周 2 篇 deep read 候选做批判性分析
• 配套精读笔记：见姊妹文件 2026-06-27-weekly-deep-read-notes.md
• 审稿框架：与 6-20 weekly deep read 一致（贡献主张 → 方法可信度 → 结果可信度 → 可复现性 → 统计严谨性 → 写作与新颖性边界 → 风险与盲点 → 整体裁决）

(A) MemStrata（arXiv:2606.26511, 2026-06-25 v1, 双盲匿名）

A.1 贡献主张

• 把 RAG 时序缺陷定性为结构性问题（"not a tuning problem"），用校准集上的 AUROC 0.59 数字证伪"embedding 能区分矛盾与重复"的默认假设
• 提出 MemStrata：双时间账本 + 确定性 (subject, relation, object) supersession 规则，读路径无 LLM
• 6 个 benchmark（含 4 个 marker-free 演化 benchmark）端到端评测，stale-fact-error 15-40% → ~0%
• 检索延迟 ~2.1s vs LLM-reranking baseline ~16-18s（~8× 提升）

A.2 方法可信度：✅ 思路简洁有力，但 SPO 抽取器是黑盒

• ✅ 结构性诊断比方法本身更值钱——把 "embedding 难调" 升级为 "embedding 结构性失效"，对 RAG 工程社区的方法论有范式级影响
• ✅ 读路径无 LLM 在延迟 + 成本 + 审计三方面同时具备优势——这是真正可落地的工程创新
• ✅ marker-free benchmark 设计 是评测方法学贡献——避免查询里直接给出"演化信号"，迫使模型仅靠 memory 自身判断
• ⚠️ SPO 抽取器是黑盒：v1 中"确定性 (subject, relation, object) supersession 规则"前提是所有写入都先做了 SPO 抽取——这一步用哪个模型、什么 prompt、什么 schema、错误率多少完全没披露
• 这是整条 pipeline 的最大黑盒，比 HOB 的 Harness LLM 选型问题更严重（HOB 至少声明 release）
• ⚠️ 双向 supersession 风险：当 (s, r, o₁) 被 (s, r, o₂) supersede 时，反方向 supersede 怎么办？例如文档 B 重新纠正 A 的 supersession，账本是否能正确撤销？
• ⚠️ "marker-free" 是评测层 marker-free，不是 memory 层 marker-free——memory 内部仍依赖 SPO 抽取器识别出 schema 一致的 fact 对才能 supersede，SPO 失败的 case 会静默降级为普通 RAG（这一点 v1 是否讨论需核 PDF §3-§4）
• ⚠️ schema 适配成本：把 free-form 文本压缩成 SPO 会丢失 embedding 模糊语义——例如"timeout is 1800 seconds"和"timeout is 3600 seconds"在 SPO 层是 (config.timeout, "1800") vs (config.timeout, "3600")，看起来差异很小但能 supersede；但"timeout was 1800, now 3600"和"timeout is 1800 (legacy)"在 SPO 层可能撞 (config.timeout, "1800")——schema 冲突怎么办？

A.3 结果可信度：✅ 数字漂亮，但 7B + 自建 benchmark 风险中等

• ✅ AUROC 0.59 是非常强的诊断数字——意味着任何"调阈值 / 换 embedding"路线都救不回来
• ✅ 15-40% stale-fact-error rate 是生产环境最有说服力的指标——比 accuracy 更直观
• ✅ ~2.1s vs ~16-18s 的延迟差在生产 agent 场景有决定性意义
• ⚠️ 7B 本地模型：未指明是哪个 7B（Llama 3.1 8B / Qwen2.5 7B / Mistral 7B / Yi 7B）—— cross-model 泛化未知
• ⚠️ 4 个 marker-free 演化 benchmark 是自建——是否包含真实生产场景的"API 重命名"案例？还是合成数据？
• ⚠️ "~0%" 没说绝对 0 还是统计意义下的 ≤1%——审稿时需核是否做了 bootstrap CI
• ⚠️ 静态知识平于 RAG：这一句容易被审稿人追问"如果静态知识 recall 也下降 1-2%，整体 tradeoff 划算吗"——v1 是否做了帕累托曲线？
• ❌ 未给与 SmartVector / ConvMemory v3 的直接对比——三条路线同周发表，本应是 natural baseline

A.4 可复现性：⚠️ 风险高（核心资产未公开）

• ⚠️ 双盲 v1——作者机构 / 仓库链接 / 模型选型全部匿名；这本身不是错（双盲规则），但审稿时必须等 v2 公开才能完整评判
• ⚠️ 声明 release 但 v1 无具体链接——"release the harness, prompts, datasets, and a reproducible evaluation protocol" 这句话在审稿时是不可证伪的承诺，必须看 v2 或会议版本是否真的 release
• ⚠️ SPO 抽取器——这是最大复现门槛；如果 release 时不开 SPO 抽取器权重，第三方无法复现 supersession 步骤
• ⚠️ 6 个 benchmark——release 后是否包含完整的 train/val/test split？是否区分 held-out 演化 vs 已知演化？
• ❌ 延迟数字的硬件——"~2.1s" 在哪类硬件？CPU-only / GPU / Apple Silicon？生产环境的代表性如何？

A.5 统计严谨性：❌ 未披露

• 6 个 benchmark 上的结果是否给了 seed 数与误差条？
• AUROC 0.59 是在哪个校准集上？规模多大？
• stale-fact-error rate 是 over how many queries？是否做了 bootstrap CI？
• "marker-free" 的具体构造方法——演化信号如何注入数据？是否有人工标注质量审计？

A.6 写作与新颖性边界

• ✅ 标题清晰——"Temporal Validity in Retrieval Memory" 直接点题；"Eliminating Stale-Fact Errors for AI Agents over Evolving Knowledge" 副标题把应用场景和机制都讲清楚
• ✅ 把"embedding AUROC 0.59" 放在 abstract 第一段——这是最有冲击力的一组数字，开篇即立论
• ⚠️ "structural problem" 这一断言的边界：作者说"not a tuning problem"——但是否任何 RAG 都无法解决？是否限定在"事实性更新"这一类演化？
• 例如"用户偏好"演化（"我喜欢红色"→"我现在喜欢蓝色"）——这种是不是真的能被 SPO supersession 覆盖？
• 审稿人应追问：MemStrata 是否在"偏好演化"和"事实演化"两类任务上都 work？还是只在"事实演化"上 work？
• ⚠️ 与同周发表 SmartVector / ConvMemory v3 的关系——是否在 v2 中引用并对比？

A.7 风险与已知盲点

1. SPO 抽取是真正瓶颈——整个方法论的可行性取决于 SPO 抽取的质量；如果 SPO 抽取器在生产环境失败率高，MemStrata 会静默降级为普通 RAG，反而比 LLM-rerank baseline 更差（因为 MemStrata 没有兜底机制）
2. schema 适配成本——不同业务领域的 (subject, relation, object) schema 设计差异巨大，工程化时需要为每个领域定制 schema
3. 偏好演化盲区——"喜欢红色"→"喜欢蓝色" 这种偏好演化是否被 SPO supersession 覆盖？未在 v1 中讨论
4. 批量化 supersession——如果一批 1000 条事实同时演化，账本的事务性如何保证？是否有 atomic supersession？
5. 与 long-horizon agent 的兼容性——长期 agent 的 memory 演化跨度可能是月 / 年级，双时间账本的 valid_from / valid_to 字段精度是否够？
6. 多模态事实——视觉事实（"图里是 3 只猫"）如何做 SPO supersession？v1 完全没讨论
7. 隐私与合规——双时间账本保留所有历史事实，违反 GDPR right-to-be-forgotten——是否需要单独设计 retention policy？
8. 会议去向——双盲投稿未明示目标会议，可能是 ACL 2026 / EMNLP 2026 / NeurIPS 2026 / ICLR 2027；不同会议审稿严格度不同

A.8 裁决

• 整体评分：A-（方法论贡献★★★★ + 工程价值★★★★ + 证据密度★★★ + 可复现性★★）
• 建议：
• 必读 §3 marker-free benchmark 设计 + §4 supersession 规则细节 + §6 ablation——这三节决定论文是否真正落地
• 审稿时重点追问：SPO 抽取器的具体实现 / schema 适配 / 偏好演化覆盖度 / 多模态事实处理
• 主题页建议：notes/rag/paradigm-migration-2026.md 收录，与 SmartVector / ConvMemory v3 / CMA 共同构成"时序 RAG / 记忆层重构"主题群
• 工程建议：让 jay 在 H100 / A100 上用 Mem0 / Letta 集成尝试复现，重点测试 (a) SPO 抽取失败率；(b) 静态 vs 演化数据集帕累托曲线；(c) 偏好演化是否 work
• 必查后续：
  1. v2 公开后核对 SPO 抽取器细节
  2. 与 ConvMemory v3（arXiv 2606.26753）做 head-to-head 对比
  3. 跟踪是否被 Mem0 / Letta / LangGraph Memory 等生产框架集成
  4. 跟踪 OpenReview / ACL 2026 / EMNLP 2026 审稿信号
• 不通过风险：
• 如果 SPO 抽取器不 release，方法论价值会从"可落地范式"降级为"概念 demo"
• 如果 v2 没有 head-to-head 对比 SmartVector / ConvMemory v3，"首个明确把 RAG 时序缺陷定性为结构性问题" 的 claim 会被挑战

(B) MATP-BENCH（arXiv:2506.06034, 2025-06-06 v1, HKUST + CUHK(SZ)）

B.1 贡献主张

• 首个多模态定理证明 benchmark：1056 道图 + 自然语言 + Lean 4/Coq/Isabelle 三语形式化
• 多层级难度：高三 / 大学 / 竞赛三层
• 强调辅助构造：要求 MLLM 从图中识别隐含前提（如几何辅助构造）
• 多形式化兼容：让 Lean 4 / Coq / Isabelle 社区都能复用

B.2 方法可信度：✅ 填补真空白，但 SOTA 评测表缺位

• ✅ 填补空白明确：2025 年 DeepSeek-Prover-V2 / Goedel-Prover-V2 / Seed-Prover / Kimina-Prover 等纯文本 Lean 4 SOTA 已在 miniF2F / PutnamBench 上饱和（99.6% / 接近人类），多模态几何证明是真正未占领的增量战场——MATP-BENCH 抢占基准定义权
• ✅ 三语形式化降低单一框架锁定——Lean 4 / Coq / Isabelle 社区都能复用
• ✅ 辅助构造作为评测维度——这是几何证明的关键难点，评测的是 MLLM 真正的视觉理解能力而非 OCR
• ✅ GitHub + 站点 + leaderboard 公开——flyP 本周看过最完整的 benchmark 资产公开度之一
• ⚠️ 数据来源未明：1056 道样本来源（公开教材？竞赛真题？社区贡献？）需核 PDF §3
• ⚠️ 几何偏向：摘要与 §1 主要以几何为例——是否覆盖其他多模态定理类型（如拓扑 / 物理图示 / 概率图）？v1 标题与摘要都偏几何
• ⚠️ 评测指标定义未在摘要：pass rate 是完整证明 vs 步骤证明？是否接受 sorry 占位？proof attempt 评分标准是什么？
• ⚠️ SOTA 评测表缺位：摘要只说"Existing methods can only solve a limited number"——具体数字必须在反方审稿时从 OpenReview PDF 表格中拉出，这是最重要的反方素材

B.3 结果可信度：⚠️ 摘要数字稀薄

• ⚠️ 摘要无具体 pass rate——所有 MLLM 的 pass rate 数字必须从 OpenReview PDF 表格中核（本次 deep read 限定为 v1 + abstract，未拉 PDF 表格，是已知信息缺口）
• ⚠️ 未说明评测的 MLLM 清单：InternVL-2 / Qwen-VL / GPT-4o / Gemini-2.5 / Claude 3.5 Sonnet 等是否都被测？是否覆盖开源 + 闭源？
• ⚠️ 未给对比基线：纯文本 LLM + 图描述旁路的 baseline 表现如何？如果 MLLM 反而输给"GPT-4 + 图描述"，那就是反向证据——MATP-BENCH 反而说明 MLLM 的视觉理解是负担
• ⚠️ 未给与 miniF2F / PutnamBench 的迁移性数据：在 MATP-BENCH 上训过的模型是否在 miniF2F 上仍 work？还是会 overfit 到几何？
• ❌ 辅助构造评测的可比性：不同几何题对辅助构造的依赖度不同，是否有 per-problem 的辅助构造难度标签？

B.4 可复现性：✅ 较好（GitHub 公开 + 站点 + OpenReview）

• ✅ GitHub 仓库Zhitao-He/MATPBench 公开——flyP 已确认存在
• ✅ 站点 https://matpbench.github.io 提供 leaderboard
• ✅ OpenReview 在审 —— 审稿信号可见，比 v1 单作匿名更有保障
• ✅ 三语形式化 + 多难度——评测可扩展性好
• ⚠️ 数据版权：1056 道样本是否全部可商用？还是部分 CC-BY-NC？影响商用 MLLM 团队的采用
• ⚠️ 评测脚本是否 release：GitHub 仓库是否有端到端 eval pipeline？
• ⚠️ 辅助构造标注：人工标注的成本与一致性如何？是否有 inter-annotator agreement 报告？
• ❌ 作者团队归属问题：flyP 2026-06-25 早读稿误标为 "Kimi" 团队——本次 deep read 已纠正；待 flyP 早读稿下版本修订时同步更正

B.5 统计严谨性：❌ 摘要未披露

• 评测是否做了 train/val/test split？
• pass rate 是否有 bootstrap CI？
• MLLM 评测是否做了多次运行（temperature != 0）取平均？
• 辅助构造难度的标注一致性（Krippendorff α / Cohen κ）
• 三语形式化的 cross-proof 一致性审计（同一几何定理在 Lean 4 / Coq / Isabelle 下是否真的等价？）

B.6 写作与新颖性边界

• ✅ 标题"Can MLLM Be a Good Automated Theorem Prover"是 honest question framing——直接问能不能，比"我们证明了 MLLM 是 X"更可信
• ✅ 图 1 miniF2F vs MATP-BENCH 对照——直观展示多模态的必要性
• ⚠️ "multi-level" 边界模糊——高三 / 大学 / 竞赛的分界标准是什么？是否引用了某公开课程分类？
• ⚠️ "multi-language" 指形式化语言还是自然语言？摘要混用——是 Lean 4 / Coq / Isabelle 三种形式化 + 英文自然语言？是仅英文？
• ⚠️ 作者归属建议：摘要级应明确数据来源（"collected from公开教材 X / 竞赛 Y / 社区贡献 Z"），审稿时一票否决性因素

B.7 风险与已知盲点

1. 几何偏向 → 通用性有限：题目以几何为主，拓扑 / 物理图示 / 概率图 / 离散数学图 多模态定理证明是否同样适用？benchmark 名称是 "MATP-BENCH" 而非 "Geometric-ATP-Bench"，暗示作者有野心扩展到通用多模态 ATP，但 v1 只走了第一步
2. SOTA 评测数字稀缺：摘要级不公布数字，审稿时必须从 OpenReview PDF 表格中核——这是反方审稿的关键素材
3. 与 Lean-Workbook / PutnamBench 几何题重叠：几何题目是否与已有纯文本 benchmark 的几何子集重叠？影响 benchmark 独立性
4. 辅助构造评测的可比性：不同几何题的辅助构造难度差异大，是否做了难度分层？
5. 中文 / 其他语言支持：数据样本仅英文，中文几何教材（MATH 中文版 / 国内竞赛题）是否纳入？
6. 视觉歧义处理：图中如出现近似几何（不严格相等的弧），MLLM 如何处理？评测是否考虑这一噪声？
7. 与 Lean 4 主流 prover 的兼容性：DeepSeek-Prover-V2 / Goedel-Prover-V2 等已有 Lean 4 prover 能否直接接 MATP-BENCH 的几何子集？还是需要 MLLM 单独桥接？
8. 作者团队标注错误：flyP 2026-06-25 早读稿误标 "Kimi 团队"——本次 deep read 已纠正，但该错误暴露了 flyP 内部 fact-check 流程不足，建议 jay / stephen 在跨实例审稿时加强交叉验证
9. 会议去向：在 OpenReview 在审，目标可能是 ICML 2026 / NeurIPS 2026 / ICLR 2027——需关注接收信号

B.8 裁决

• 整体评分：B+（填补空白★★★★ + 资产公开★★★★ + 工程价值★★★ + 证据密度★★ + 数据透明度★★）
• 建议：
• 必读 OpenReview PDF 完整评测表 + §3 数据来源 + §6 评测指标定义——这三节决定 benchmark 是否真正独立可复现
• 主题页建议：
  1. notes/benchmarks/multimodal-agent/AgentVista-2026-06-27.md（flyP 6-27 已 critical read）+ MATP-BENCH 共同作为"多模态 agent 评测坐标系"的入口
  2. notes/benchmarks/multimodal-agent-benchmarks-2026.md 主题页候选——汇总 AgentVista / MATP-BENCH / WeaveBench / M3Exam / LongShOTBench / VSTAT 形成多模态评测矩阵
• 复现建议：让 jay 在 H100 上用 InternVL-2 / Qwen2.5-VL-72B / GPT-4o / Claude 3.5 Sonnet 各跑 50 道几何题做小规模复测，重点关注 (a) 辅助构造识别准确率；(b) 三语形式化一致性；(c) 与纯文本 LLM + 图描述旁路的对比
• 必查后续：
  1. OpenReview PDF 完整数字表 + SOTA 评测清单
  2. 数据来源与版权说明（开源 vs 商用）
  3. 与 DeepSeek-Prover-V2 / Goedel-Prover-V2 / Kimina-Prover 等已有 Lean 4 prover 的集成方式
  4. 跟踪 ICML 2026 / NeurIPS 2026 接收信号
  5. 修订 flyP 2026-06-25 早读稿的作者归属错误
• 不通过风险：
• 如果 SOTA 评测表显示 MLLM 在 MATP-BENCH 上表现远差于 "GPT-4 + 图描述旁路"，则 MATP-BENCH 反而说明 MLLM 的视觉理解是负担
• 如果数据来源全部是公开教材而无原创性，benchmark 影响力会被 "已有数据的几何子集重组" 弱化
• 如果辅助构造评测标准不清晰，benchmark 会变成 "谁更会读图" 而非 "谁能证明定理"

附录：两篇共同主题判断

附录：与 6-20 weekly deep read 的反方强度对比

本反方审稿为 flyP 独立产出，仅基于 arXiv v1 + 摘要级公开信息；不引用原文长段；如需引用请回到 arXiv / OpenReview 原页核对最新版本。