ArticleMetadataMain page

source · 2026-04-17

通过形式化验证评测文本到视频模型的神经符号方法（CVPR 2025）

#near-cvpr-2025#evaluation#benchmarking#video-generation#primary-source

通过形式化验证评测文本到视频模型的神经符号方法（CVPR 2025）

会议：CVPR 2025
发表日期：2025-01-01
资料加入日期：2026-04-14
深分析稿：raw/ingest/2026-04-14-neuro-symbolic-eval-t2v/analysis

一句话结论

这篇论文把 formal verification 引进 text-to-video 评测，说明视频评测可以从“看起来像不像”推进到“是否真的满足 prompt 中的时间逻辑与事件关系”。

论文定位

它是“formal verification evaluator”路线里的代表作。与 AIGV-Assessor 和 Video-Bench 不同，这篇论文更强调可验证性与时序逻辑完整性。

问题定义

作者认为现有 T2V 评测存在一个核心缺口：

  • 视频可能看起来合理，但在时间顺序、动作逻辑和关系约束上仍然违背 prompt
  • 传统指标和一般 VLM 打分很难严格表达这类要求

因此需要把 prompt 形式化，再用更严格的验证框架来评测视频。

方法概述

方法有三层：

  1. Prompt → temporal logic specification

    2. 将 prompt 转写成显式时间逻辑规范。

  1. Video → automaton / DTMC representation

    2. 将视频解析成带状态与转移的时序表示，便于后续验证。

  1. Probabilistic model checking

    2. 对视频是否满足规范进行概率模型检测，计算满足度分数。

关键发现

  • 这条路线让评测不再只是软分数，而开始具备可验证约束。
  • Neu-SV 比 VBench 更能识别 temporal alignment / misalignment。
  • 它与人工标注相关性更高，说明形式化验证路线具备更强可信度。
  • 这篇论文清楚地把“时间逻辑是否满足”从评测盲区拉到了前台。

关键图示

论文总览图

!900

这一页同时展示 prompt、temporal spec、video automata、验证结果以及与 VBench 的直观对比，是最适合作为 source note 首图的页面。

formal verification 方法页

!900

这一页解释 temporal logic、video automaton/DTMC 和 neuro-symbolic pipeline 的组合方式，是理解方法的关键页。

主结果与讨论

!900

这一页集中展示与 VBench 的对比、与人工标注的相关性以及模型与上下文设置消融，是说明方法有效性的关键证据页。

核心实验与结果

  • Neu-SV 相比 VBench 更能区分 temporally aligned 与 misaligned 的视频。
  • 结果页说明它与人工标注相关性更高，也更适合复杂 prompt 评测。
  • VLM 选择、上下文长度等因素都会影响 formal verification evaluator 的表现。
  • 这篇论文使“可信评测”成为 T2V 评测中的一条独立路线。

局限或疑问

  • 形式化验证覆盖的能力维度不一定像人类判断那样全面。
  • 它更偏可信评测，不等于真实用户偏好。
  • 这条路线补的是“评测可信度”，而不单独构成完整评测体系。

对当前 wiki 判断的影响

  • 它显著补强了 topics/generative-model-evaluation 中“评测路线正在分化”这条判断。
  • 对 questions/question-do-benchmarks-track-real-video-editing-understanding 来说，它提供了一条比人类偏好和感知质量更严格的“时间逻辑验证”路线。
  • 它帮助我们把“看起来好”“人类喜欢”“逻辑满足”这三类评测坐标分开。

相关页面

原始链接

  • https://openaccess.thecvf.com/content/CVPR2025/html/Sharan_Neuro-Symbolic_Evaluation_of_Text-to-Video_Models_using_Formal_Verification_CVPR_2025_paper.html
  • https://openaccess.thecvf.com/content/CVPR2025/papers/Sharan_Neuro-Symbolic_Evaluation_of_Text-to-Video_Models_using_Formal_Verification_CVPR_2025_paper.pdf

Metadata

{
  "id": "2026-04-14-neuro-symbolic-eval-t2v",
  "type": "source",
  "title": "通过形式化验证评测文本到视频模型的神经符号方法（CVPR 2025）",
  "status": "reviewed",
  "created": "2026-04-14",
  "updated": "2026-04-17",
  "venue": "CVPR 2025",
  "ingested_at": "2026-04-14",
  "tags": [
    "near-cvpr-2025",
    "evaluation",
    "benchmarking",
    "video-generation",
    "primary-source"
  ],
  "note_status": "reviewed",
  "source_type": "paper",
  "authors": [
    "S P Sharan",
    "Minkyu Choi",
    "Sahil Shah",
    "Harsh Goel",
    "Mohammad Omama",
    "Sandeep Chinchali"
  ],
  "published_at": "2025-01-01",
  "canonical_links": [
    "https://openaccess.thecvf.com/content/CVPR2025/html/Sharan_Neuro-Symbolic_Evaluation_of_Text-to-Video_Models_using_Formal_Verification_CVPR_2025_paper.html",
    "https://openaccess.thecvf.com/content/CVPR2025/papers/Sharan_Neuro-Symbolic_Evaluation_of_Text-to-Video_Models_using_Formal_Verification_CVPR_2025_paper.pdf"
  ],
  "raw_entry": "raw/ingest/2026-04-14-neuro-symbolic-eval-t2v/",
  "analysis_note": "raw/ingest/2026-04-14-neuro-symbolic-eval-t2v/analysis.md",
  "image_index": "raw/ingest/2026-04-14-neuro-symbolic-eval-t2v/images/index.md",
  "topics": [
    "topics/generative-model-evaluation",
    "topics/video-generation"
  ],
  "entities": [],
  "claims": [],
  "questions": [
    "questions/question-do-benchmarks-track-real-video-editing-understanding"
  ]
}