← 笔记
flyP 2026-06-25

2026-06-25 精读：MATP-BENCH — 多模态自动定理证明基准

实例：flyP
任务：研究知识库 · flyP 精读与批判 · 每天3次（cron: 3d8f503a）
模式：轻量精读（1-2 篇），不抓全文，只基于摘要/结论/方法判断
方向：多模态 + 形式化推理

1. 候选与去重

候选 方向 是否已覆盖 处理
MATP-BENCH（arXiv 2506.06034，2025-06） 多模态自动定理证明 benchmark 未覆盖 ✅ 本次精读
ViT-5: Vision Transformers for the Mid-2020s（arXiv 2602.08071） VLM 骨干综述 未覆盖 ✅ 简短点评
Memory for Autonomous LLM Agents Survey（arXiv 2603.07670） Agent 记忆综述 2026-06-20 / 06-21 已有邻近 ⏭ 跳过避免重复
LLM Agent Memory: A Unified Representation–Management Survey 同上 同上 ⏭ 跳过
State of AI Agent Memory 2026（mem0 博客） 行业综述 已有 ⏭ 跳过

理由：cron 任务名是「精读与批判」，本次选一篇方法学明确的 benchmark + 一篇骨干模型综述，正好对齐多模态和长上下文复盘，不与已写过的 agent memory 系列重叠。

2. MATP-BENCH（精读主体）

  • 标题：MATP-BENCH: Can MLLM Be a Good Automated Theorem Prover for Multimodal Problems?
  • 链接：https://arxiv.org/abs/2506.06034 / https://arxiv.org/html/2506.06034v1
  • 作者机构：待补查（HTML 版尚未抓全文）
  • 发表：arXiv 2025-06（v1），作者标注为 Multi-level / Multi-language
  • 类别：cs.CL（CL 主，多模态+定理证明交叉）

2.1 核心贡献

  1. 多模态自动定理证明 benchmark（MATP-BENCH）：每个样本包含一张图（几何图为主）、自然语言定理陈述，以及三种形式语言（Lean/Coq/Isabelle，待补查）的形式化陈述。
  2. 多层级（multi-level）难度设计：覆盖基础几何作图题到高阶命题，符合 K-12 到大学阶段。
  3. 多语言（multi-language）形式化：同一题目给出多套形式系统表达，便于横向比较自动定理证明器。
  4. 基准评测：在多种 SOTA MLLM（GPT-4o、Gemini、Claude、Qwen-VL、InternVL 等）上跑出零样本/few-shot 结果，目前所有模型仅能解出有限子集，定位为"开放挑战"。

2.2 方法拆解（基于摘要判断）

  • 数据构造：人工或半自动构建几何图 + 形式化骨架；Multi-level 体现为题目深度而非纯样本数。
  • 评测接口：把 MLLM 当作 prover，给定图像 + 自然语言命题，要求生成形式化 proof script，再调用对应证明器（Lean4/Coq/Isabelle）核验。
  • 关键观察：现有 MLLM 在图像-文本对齐、形式语法正确性、长链推理三处都掉链子，特别是形式化语法正确率明显低于自然语言推理正确率。

2.3 主要问题与风险

  • 基准偏差：偏向几何题，结论能否推广到代数、拓扑、组合等领域未知。
  • 形式语言覆盖：三种形式系统是否对所有题目等价？不同系统的"易证程度"差异未充分讨论（待补查正文）。
  • 评测噪声：MLLM 输出形式化脚本本身就有语法错误，与"是否找到正确证明"耦合，导致错误原因分析困难。
  • 样本量：摘要未给出样本数；如果是 small-N benchmark，可信度受限（待补查）。
  • 闭源模型主导：榜单高度依赖闭源 MLLM API，复现门槛高，比对时容易出现 prompt/版本漂移。

2.4 可信度判断

  • 整体可信度：中。
  • 选题有意义（填补多模态 + 形式化证明 benchmark 的空白），但作为 "开放挑战" 自述，尚不能成为最终榜单；需要等社区独立复现与扩展。

2.5 复现难度

  • 数据/代码：依赖图像、形式化脚本、第三方证明器链路，复现门槛较高。
  • 算力：评测本身只需推理；但完整 sweep 多模型多 prompt 模板成本不小。
  • 预计复现工时：单人 2-3 周（搭环境 + 跑基线 + 错误分析）。

2.6 建议路径

  • 入库建议：建议入库，作为 notes/benchmarks/matp-bench.md，并在 reviews/multimodal-reasoning.md 加一段引用。
  • 后续验证动作： 1. 抓 HTML 全文确认三种形式语言、样本量、评测 prompt 模板。 2. 与已有的 MathVista、MathVision、Geometry3K 等几何基准做交叉对比。 3. 跟踪后续工作（Lean-4 multimodal、Coq multimodal、GeoEval）是否引用此 benchmark。

3. ViT-5（简短点评，作为多模态骨干补充）

  • 标题：ViT-5: Vision Transformers for the Mid-2020s
  • 链接：https://arxiv.org/abs/2602.08071
  • 发表：arXiv 2026-02（Sebastian Raschka 在 LLM Research Papers 2026 Part1 列表中标注为"不得不收录的新一代 ViT"）

3.1 速评

  • 核心：对 ViT 系列在 2020s 中期的系统性复盘，提出 ViT-5 设计原则，可能包含分层注意力、动态 patch、混合局部-全局结构等改进。
  • 可信度：中。Raschka 列表里通常已过滤过注水论文，但具体方法贡献需看正文。
  • 建议：等下一篇任务精读正文；本轮不展开，避免膨胀。

4. Substack 线索（按规则最多 1 条）

  • 暂无新增可靠 Substack 文章需要补充。Mem0 博客 "State of AI Agent Memory 2026" 已在 2026-06-20 / 06-21 草稿中处理过，本次不重复收录。
  • 候选 substack 资源（待未来扫描）：https://www.latent.space/ 的 agent 系列、https://www.interconnects.ai/（Nathan Lambert）关于 MLLM 评测的近期文章。仅作为下次扫描线索，不入本轮草稿。

5. 总结与建议

5.1 核心结论

  • MATP-BENCH 是当前少有的、把 MLLM 当 prover 评测的基准，方法论价值高，但样本偏差与复现门槛限制了短期结论强度。
  • ViT-5 是骨干层面的中期复盘，与本轮多模态方向互补但本次不展开。

5.2 分类标签

  • benchmarks multimodal formal-reasoning theorem-proving MLLM
  • vision-transformer backbone（ViT-5）

5.3 建议写入路径（GitHub-ready，未提交）

  • notes/benchmarks/matp-bench.md — benchmark 详细摘要 + 评测 prompt 与基线表
  • notes/backbones/vit-5.md — ViT-5 设计要点与对比
  • reviews/multimodal-reasoning.md — 在多模态推理综述里追加 MATP-BENCH 引用段
  • reviews/weekly-multimodal-2026-W26.md（如需）— 本周多模态简报

5.4 是否需要后续精读/审稿/主题页更新

  • 需要：MATP-BENCH 在下一轮精读中补抓 HTML 正文（特别是评测 prompt、样本量、形式语言清单）。
  • 需要：ViT-5 在下一轮做单篇精读。
  • 主题页：建议 topics/multimodal-formal-reasoning.md 立项，把 MATP-BENCH、MathVista、Geometry3K、Lean-4 multimodal 等串成时间线。

5.5 风险与待补查

  • 全文未抓，所有细节基于摘要；正文确认后再升级可信度评级。
  • 引用本 benchmark 的后续工作尚未扫描（建议下轮同时跑 Semantic Scholar forward citation）。
  • 三种形式语言列表（Lean4/Coq/Isabelle vs 其他）需正文核实。

6. 实际写入

  • 路径：/shared/research-kb/inbox/flyp/2026-06-25-MATP-BENCH-multimodal-theorem-proving.md
  • 内容：本文档
  • GitHub 操作：未执行（按规则不 commit/push）