NeuS-V: Neuro-Symbolic Evaluation of Text-to-Video Models using Formal Verification¶

会议: CVPR 2025
arXiv: 2411.16718
代码: https://utaustin-swarmlab.github.io/NeuS-V (有)
领域: 自动驾驶 / 视频生成评估
关键词: 文本到视频评估, 时序逻辑, 模型检验, 形式化验证, VLM

一句话总结¶

提出 NeuS-V，首个用形式化验证（时序逻辑+概率模型检验）评估文本到视频（T2V）模型时序一致性的框架——将文本提示转为时序逻辑规范，用 VLM 评分原子命题，构建视频自动机后形式化验证满足概率，在 Gen-3 上与人类标注 Pearson 相关 0.71（VBench 仅 0.47）。

领域现状：T2V 模型（如 Gen-3、Pika、CogVideoX）的评估主要依赖 VBench 等基于 CLIP 相似度的指标。这些指标通过逐帧相似度求平均，无法捕捉时序动态——"先A后B"和"先B后A"会得到相同分数。

现有痛点：VBench 对时序对齐的评估与人类判断相关性低（Pearson 仅 0.47），因为它不理解时序逻辑（ALWAYS/EVENTUALLY/UNTIL 等）。单帧 CLIP 无法区分"一直存在"和"偶尔出现"。

核心矛盾：视频的语义不仅是帧级的（每帧正确）还是序列级的（时序关系正确），但现有评估只做前者。

切入角度：用计算机科学中的形式化验证技术——将提示转为时序逻辑（TL），将视频建模为离散时间马尔可夫链（DTMC），用概率模型检验器 STORM 计算满足概率。

核心 idea：提示→时序逻辑 → 视频→自动机 → 形式化验证满足概率 = 严格的时序一致性评估。

PULS（Prompt→TL 转换）：用 GPT-4o 将自然语言提示分解为原子命题+时序逻辑规范。如"A cat walks then sits"→ EVENTUALLY(walk) AND EVENTUALLY(sit) AND walk UNTIL sit
VLM 原子命题评分：用 LLaMA-3.2 对每帧打分（0/1），判断每个原子命题是否满足
视频自动机 + STORM 验证：将帧级评分构建为 DTMC 转移矩阵 \(\delta(q,q') = \prod_i (C_i^*)^{1_{q'_i=1}}(1-C_i^*)^{1_{q'_i=0}}\)，用 STORM 模型检验器计算时序逻辑规范的满足概率

无训练——纯评估框架。满足概率 \(\mathbb{P}[\mathcal{A}_\mathcal{V} \models \Phi]\) 由 STORM 精确计算。