使用形式验证的文本到视频模型进行神经符号评估

使用形式验证的文本到视频模型进行神经符号评估

Neuro-Symbolic Evaluation of Text-to-Video Models using Formal Verification

https://arxiv.org/pdf/2411.16718

摘要

近期，诸如 Sora、Gen-3、MovieGen 和 CogVideoX 等文本到视频生成模型的进展正在推动合成视频生成技术的边界，并已在机器人、自动驾驶和娱乐等领域得到应用。随着这些模型的普及，各种评估生成视频质量的指标和基准也相继出现。然而，这些指标主要关注视觉质量和流畅性，忽略了对安全性至关重要的时间保真度和文本到视频对齐性。

为弥补这一空白，我们提出了NeuS-V，这是一种全新的合成视频评估指标，使用神经符号形式化验证技术严格评估文本到视频的对齐性。我们的方法首先将文本提示转换为形式化的时序逻辑（Temporal Logic, TL）规范，并将生成的视频转换为自动机表示。然后，通过将视频自动机与 TL 规范进行形式化验证，来评估文本与视频之间的对齐程度。

此外，我们还提供了一个包含时间扩展提示的数据集，用于在我们的基准下评估最先进的视频生成模型。我们发现，与现有指标相比，NeuS-V 与人类评估的相关性高出5 倍以上。我们的评估还揭示出，当前的视频生成模型在处理这类时间复杂的提示时表现较差，突显了在提升文本到视频生成能力方面未来研究的必要性。

我们在 utaustin-swarmlab.github.io/NeuS-V 公开了基准测试、代码和数据集。

1. 引言

设想我们需要通过模拟一个场景来对自动驾驶（Autonomous Driving, AD）的运动规划系统进行压力测试或重新训练，例如：

“一辆卡车在第 10 帧出现，并在 2 秒钟内变道到我的车道前方。”

随着文本到视频（Text-to-Video, T2V）生成模型的最新发展，为这类场景生成合成视频具有巨大的潜力，可以显著提升此类工程系统的能力。

然而，为了使这些合成视频有效，它们必须在以下三个关键维度上与期望的提示保持一致：

• ➊ 语义一致性

  （Semantics）

• ➋ 空间关系

  （Spatial Relationships）

• ➌ 时间连贯性

  （Temporal Coherence）

例如，如果合成视频中卡车在自动驾驶车辆前的移动路径不准确，或者未能遵循正确的变道时间点，就可能在再训练过程中误导运动规划系统，导致在关键时刻做出错误决策。

近年来，出现了多种评估指标，用于从新开发的 T2V 模型 [4, 14, 20, 33, 57] 中识别出与提示高度对齐的合成视频。

虽然许多视频评估工具 [23, 39, 41] 主要关注视觉质量，但一些方法使用视觉语言模型（Vision-Language Models, VLMs）[50, 51] 或视频字幕模型（video captioning models）[9] 来评估生成视频与原始提示之间的语义对齐程度。

更值得注意的是，VBench[23] 可以从多个维度和类别对视频进行评估，最近已被用于排行榜*（leaderboards）中评估 T2V 模型。

然而，使用另一个神经网络去评估一个由神经网络生成的视频，这种方式既不够严谨，也缺乏可解释性。此外，当前的评估指标仍然忽略了视频数据固有的关键时空特性（见图1）。

我们的核心洞察是：利用近期在视频理解系统中的进展，这些系统结合了结构化的符号验证方法与神经网络[10]。

我们提出了Neuro-Symbolic Verification（NeuS-V），这是一种全新的 T2V 模型评估方法，它将神经网络输出与基于时序逻辑（Temporal Logic, TL）规范的结构化符号验证相结合。

具体流程如下：

1. 我们首先利用视觉语言模型（VLMs）来解析视频的空间和语义内容；

2. 然后通过按帧顺序处理，捕捉这些语义之间的时间关系；

3. 最后，我们构建一个合成视频的自动机表示（automaton representation），用以建立视频事件的结构化时间序列。

这种结构确保满足指定的 TL 要求，从而实现严格且可解释的视频评估。

此外，我们还引入了一个包含时间扩展提示的数据集，用于评估 T2V 模型在时间保真度和事件序列准确表达方面的能力。我们计划将NeuS-V、我们的提示语集合、人类评估结果以及当前最先进的（SOTA）T2V 模型的公开排行榜一并开源。

2. 相关工作文本到视频模型的评估

随着 T2V 模型的迅速发展，人们迫切需要专门的指标来评估生成视频的质量与连贯性。

该领域的初步研究使用了诸如FID、FVD 和 CLIPSIM等指标 [6, 21, 25, 38, 49, 55]，但这些方法在处理需要复杂推理和逻辑的提示时表现不佳。

最近的一些研究 [31, 32, 40, 58] 利用大语言模型（LLMs）将提示拆解为视觉问答对（VQA pairs），然后由 VLM 进行评分。

也有一些方法利用了视觉 Transformer和时间网络[11, 16, 22, 27]。

包括EvalCrafter[39]、FETV[41]、T2V-Bench[16] 以及其他一些研究 [18, 26] 在内的工作则结合了多种视觉质量指标的集成评估。

其中，VBench[23] 正逐渐成为该领域的事实基准，它从多个维度和类别对视频进行评估。

然而，所有当前的评估方法都侧重于视觉质量，忽略了视频的时间顺序。

尽管某些方法声称进行了时间方面的评估，但它们往往关注的是播放方式（如慢动作、延时摄影）或运动速度等，而不是真正的时间推理，且缺乏严谨性。

相比之下，NeuS-V通过在合成视频的自动机表示基础上，使用时序逻辑（TL）规范进行形式化验证，弥补了这些不足，从而实现对时间保真度的严格评估。

视频事件理解

近期的方法通常依赖于感知模型[15, 48] 或视觉语言模型（VLMs）[42, 56] 来分析视频中的事件。

尽管这些模型能够有效检测对象和动作，但它们并不能保证对视频时间动态的可靠理解。

Yang 等人 [53] 提出将视频表示为一种形式化模型——离散马尔可夫链，提供了一种更具结构化的方式来捕捉跨时间的事件。

这一思路的一个应用是NSVS-TL[10]，它采用神经符号方法来识别感兴趣的场景。

类似地，NeuS-V利用 VLM 和形式化验证技术来增强对生成视频中时间关系的理解并评估视频质量，从而为视频评估建立了可靠的基础。

3. 预备知识

在接下来的章节中，我们将通过一个运行示例来帮助说明我们的方法。

假设我们使用 T2V 模型生成一段自动驾驶场景的视频，其提示语为：

“一辆汽车在晴朗的阳光下沿道路行驶，与骑自行车的人互动，骑车人通过打手势转弯以避开障碍物。”

简而言之，时序逻辑（TL）是一种具有逻辑和时序操作符的表达性强的形式化语言[13, 43]。

一个 TL 公式由三个部分组成：

• ➊ 原子命题集合

  （Atomic Propositions）

• ➋ 一阶逻辑运算符

  （First-order Logic Operators）

• ➌ 时序运算符

  （Temporal Operators）

原子命题是不可再分的陈述句，其取值可以为“真”（True）或“假”（False），它们可以组合起来构造更复杂的表达式。

一阶逻辑运算符包括：

• 与（AND，记作 ∧）

• 或（OR，记作 ∨）

• 非（NOT，记作 ¬）

• 蕴含（IMPLY，记作 ⇒）等

时序运算符包括：

• 永远成立（ALWAYS，记作 □）

• 最终成立（EVENTUALLY，记作 ♢）

• 下一时刻（NEXT，记作 X）

• 直到（UNTIL，记作 U）等

我们示例中的原子命题 P和TL 规范 Φ如下：

这条 TL 规范说明了这样一个逻辑：如果一辆汽车在晴朗的天气中行驶，并且一名骑自行车的人发出转弯信号，那么这意味着骑车人最终会转弯并避开障碍物。

4. 方法论

我们提出了NeuS-V，这是一种基于神经符号形式化验证框架的新型 T2V 模型评估方法。NeuS-V 从以下四个方面对合成视频进行评估：

• 对象存在性
• 空间关系
• 对象与动作对齐
• 整体一致性

其评估流程包括以下五个步骤：

• 步骤1

  ：通过PULS（基于时序逻辑规范的提示理解）将文本提示转化为一组原子命题和一个TL规范；

• 步骤2

  ：在每一帧序列上应用视觉语言模型（VLM），为每个原子命题获取一个语义置信度得分；

• 步骤3

  ：为合成视频构建一个视频自动机表示；

• 步骤4

  ：通过将构建的视频自动机与 TL 规范进行形式化验证，计算其满足概率；

• 步骤5

  ：最终通过映射将满足概率校准为 NeuS-V 的最终评估得分。

我们提出了基于时序逻辑的提示理解（Prompt Understanding via temporal Logic,PULS），这是一种新颖的方法，能够高效且准确地将文本提示转化为时序逻辑（TL）规范。

该方法保留了提示中的所有语义细节，并用于构建其 TL 规范。与以往仅关注单一对象之间的关系、孤立事件 [5, 8, 17] 或仅编码空间信息 [37, 47] 的方法不同，我们的 PULS 方法完整地捕捉了时间与空间两个维度的细节。

通过引入四种评估模式，我们在时空维度上提供了更全面的评估。

评估模式

PULS 将文本提示编译为在四种评估模式下不同的命题集合 P和 TL 规范 Φ：

4.2 来自神经感知模型的语义得分

为了计算标记概率，我们获取响应标记的 logits，并在应用 softmax 后计算该标记的概率。接着，语义置信度得分由这些概率的乘积得出，具体如下：

4.3 合成视频的自动机表示

4.4 对合成视频的形式化验证

5. 实验设置

PULS使用GPT-4o和o1-preview将文本提示翻译为 TL 规范，而NeuS-V在构建自动机时选用的视觉语言模型（VLM）为InternVL2-8B[25]。我们在提示 VLM 时使用连续三帧作为上下文。所有系统提示和示例输出可在附录中找到。我们还使用GPT-4o构建提示语集合。

T2V 模型

我们使用两个不同的提示集合来评估闭源与开源文本到视频模型的性能：

• 闭源模型

  ：我们选取了Gen-3†和Pika‡；

• 开源模型

  ：我们选取了T2V-Turbo-v2[35] 和CogVideoX-5B[54]。

实验在 8× A100 GPU 上使用默认超参数运行。

提示语与评估套件

我们观察到现有的 T2V 评估基准 [23, 26, 41] 缺乏明确的时间指令，因此我们提出了包含总共360 条提示的NeuS-V 提示语套件。

这些提示被设计用于严格评估模型在保持时间连贯性和准确遵循事件序列方面的能力。

该套件涵盖四个主题：

• “自然”（Nature）

• “人类与动物活动”（Human & Animal Activities）

• “物体交互”（Object Interactions）

• “驾驶数据”（Driving Data）

并根据时间与逻辑操作符的数量划分为三个复杂度等级：

• 基础级（Basic）

• 中级（Intermediate）

• 高级（Advanced）

为了建立无偏基线，我们进行了人类研究，指导标注者明确区分视觉质量与文本到视频对齐性。

我们的提示语套件以及人类评估结果将在论文被接收后公开发布。

更多细节请参见补充材料。

6. 实验结果

基于上述实验设置，我们现在对NeuS-V进行实证评估。我们的实验旨在回答以下三个核心问题，以说明我们方法的必要性：

1. 与强调视觉质量的基线方法相比，NeuS-V 对时间保真度的关注是否在与人类标注的相关性方面表现更优？

2. 基于时序逻辑和形式化验证的方法，在评估框架的鲁棒性方面，相较于仅依赖 VLM 的方法，能提升到什么程度？

3. NeuS-V 的可靠性是否能够超越我们设计的合成提示语集，推广到更大规模的现有数据集上？

如第5节所述，我们在闭源与开源的最先进模型上进行了基准测试，包括：

• 闭源模型：Gen-3 和 Pika；
• 开源模型：T2V-Turbo-v2 [34, 35] 和 CogVideoX-5B [54]。与人类标注的相关性

  我们使用NeuS-V和专注于视觉质量的基准测试工具VBench，对所选视频生成模型进行了评估。为了衡量这些指标与人类对文本到视频对齐性的评分之间的相关性，我们在图4中绘制了相关结果。

  在所有模型中，NeuS-V与人类标注表现出更强的一致性，如最佳拟合线和皮尔逊相关系数所示，其表现优于 VBench。

  通过引入时序逻辑规范和合成视频的自动机表示，NeuS-V 实现了对文本到视频对齐性的严格评估。

  在我们的提示语套件上的表现

  我们将每个 T2V 模型在提示语套件上的表现进行分解分析，结果如表1所示，按主题和复杂度组织（基于160条子集提示）。

  结果显示，大多数模型在生成“自然”（Nature）和“人类与动物活动”（Human and Animal Activities）主题的视频时表现最佳。

  其中，Gen-3 模型在整个套件中得分最高，这一结果也得到了人类标注者的印证。

  此外，图5展示了 PULS 中四种评估模式在不同模型间的使用情况。不同的提示依赖于不同的评估模式，表明这些模式的结合能够全面捕捉提示中时间规范的多样性。

  6.2 对时序逻辑与验证机制的消融实验 —— 形式化语言有多重要？

  在本消融实验中，我们通过将形式化组件替换为缺乏严谨性的 VLM 替代方案，研究了基于时序逻辑与模型检测的形式化方法的作用。

  具体来说：

  这种设置反映了现有的从提示到视觉问答（prompt-to-VQA）的基线方法 [31, 32, 40, 58]。

  在本次实验中，我们使用GPT-4o[1] 作为 LLM，并搭配两种 VLM 配置：

  我们使用我们的提示语套件对这些方法进行评估，结果如图6所示。

  我们的研究发现：

  这些结果进一步表明：当 VLM 被置于时序逻辑和形式化验证框架下时，可以提供更鲁棒的评估框架。

• • 尽管这两种方法与人类标注之间存在正相关性（由皮尔逊相关系数体现），

  • 但它们的相关强度仍不及图4中基于形式化方法的结果；

  • 此外，LLaVA-Video 表现出过度自信（overconfidence），导致其相关性弱于仅处理图像的 LLaMa-3.2。

  • LLaMa-3.2-11B-Vision-Instruct§

    （可处理图像）

  • LLaVA-Video-7B-Qwen2¶

    （可处理完整视频）

  • 我们不再使用 PULS 将提示翻译为原子命题和规范，

  • 而是直接使用 LLM 将提示拆解为一组“是非问题”（yes/no questions），涵盖每个提示的内容与视觉特征；

  • 此外，我们也不再使用 NeuS-V 进行验证，

  • 而是使用 VLM 根据之前生成的问题独立地对每一帧打分。

6.3 在真实世界视频字幕数据集上的鲁棒性验证

尽管我们的提示语评估套件效果良好，但其规模有限，仅包含 160 条提示。有人可能会质疑：这种小规模的数据集，加上使用的是合成视频字幕，可能会影响我们指标的可靠性。

为解决这一问题，我们采用了MSR-VTT[52] 数据集，这是一个广泛使用的视频字幕数据集——该任务同样涉及评估视频与给定文本描述之间的对齐程度。

MSR-VTT 包含由 MTurk 工作者标注的大规模视频-字幕对。我们利用其标注的可信度，从中选取验证集来评估我们指标的可靠性。

我们构建了两个数据划分：

• 正样本集

  （Positive Set）：字幕与视频匹配；

• 负样本集

  （Negative Set）：字幕与视频不匹配。

随后，我们测试NeuS-V 指标是否能够有效区分对齐与不对齐的视频-字幕对。

实验结果

在表2中，我们将 NeuS-V 与 VBench 进行对比，报告了对齐和不对齐样本得分的均值与标准差。

结果显示：

• NeuS-V 成功地区分了正样本集与负样本集

  ，对对齐的视频-字幕对给出了更高的评分，而对不对齐的对则给出更低的评分；

• 相比之下，VBench 在对齐与不对齐样本间的得分差异较小，这进一步凸显了NeuS-V 在捕捉有意义的文本到视频对齐方面的优越能力。

在对架构选择的首次消融实验中，我们研究了使用更多帧数是否一定能提升 NeuS-V 的性能。

为了评估这一点，我们在提示 VLM（InternVL2-8B）时，比较了使用单帧与三帧作为输入的效果。

如表3所示，使用三帧时始终与文本到视频对齐标注表现出更高的相关性。

我们未测试超过三帧的情况，因为这会超出大语言模型（LLM）的上下文窗口限制。

VLM 模型选择的影响

在第二个消融实验中，我们考察了不同 VLM 的选择是否会影响自动机的构建质量。

我们测试了两种最新的 VLM：

• InternVL2-8B[45]
• LLaMa3.2-11B-Vision（使用单帧上下文）

如表4所示，InternVL2-8B在与文本到视频对齐标注的相关性方面始终表现更优。

尽管我们尝试对LLaMa3.2模型进行校准，但由于其输出概率分布存在严重偏移，该模型倾向于过度自信（overconfidence），导致其与人类标注的相关性较低。

7. 讨论严格的形式化方法是关键吗？

一个自然的问题是：是否可以用更简单的 if-else 判断和断言来替代形式化的时序逻辑？

从原则上讲，是可以的。

然而，随着提示语的长度和复杂度增加，这种基于规则的方法在扩展性上面临挑战，变得不切实际。

相比之下，符号化的时序操作符可以实现近似线性的扩展性，从而更高效地验证是否符合自动机模型。

如第6.2节图6所示，尽管替代方法可能展现出一定潜力，但它们最终仍无法达到形式化时序逻辑所提供的鲁棒性。

NeuS-V 是首个将形式化方法引入文本到视频（T2V）评估的工作，其意义超越了传统的基于视觉质量的评估指标。

重新思考文本到视频模型

表1中的评估结果显示，当前的文本到视频模型在处理时间扩展型提示时存在显著局限性。

尽管这些模型被宣传为“文本驱动”的视频生成工具，但它们往往难以生成真正符合提示要求的运动和事件序列。

许多所谓的“运动”其实只是简单的平移、缩放等效果，缺乏对交互行为或有意义场景转换的生成能力。

在实践中，视频生成流程通常需要进行多轮提示调整（reprompting）才能达到与提示的一致性。而理想情况下，我们应期望模型在大多数情况下都能与提示保持对齐。

局限性与未来工作

目前，NeuS-V 尚缺乏一种机制来惩罚生成视频中不相关的内容，因此难以区分“无关的伪影”与“未被明确要求但可能有用的辅助内容”。

未来，我们的方法可用于迭代优化生成视频，直到其满足设定的评估阈值，从而在不重新训练模型的情况下提升提示对齐性。

此外，来自 NeuS-V 的反馈信息还可用于优化提示语设计或模型训练，为文本到视频生成系统的改进提供新方向。

8. 结论

文本到视频模型正越来越多地应用于自动驾驶、教育和机器人等对安全性要求较高的领域，在这些场景中，保持时间上的保真度（temporal fidelity）至关重要。

然而，我们发现当前大多数评估方法更侧重于视觉质量，而忽视了文本与视频之间的对齐性。

为解决这一问题，我们提出了NeuS-V，这是一种全新的评估指标，它将文本提示转化为时序逻辑规范，并将视频表示为自动机，从而通过形式化验证对视频进行评分。

与 NeuS-V 一同，我们还发布了一个包含时间复杂性挑战的提示语基准测试集，用于评估当前最先进的 T2V 模型在遵循指定事件序列方面的能力。

我们的评估揭示了现有模型的局限性——它们往往依赖于简单的摄像机运动，而非真正的时间动态。

我们希望 NeuS-V 能够为未来文本到视频生成模型的发展铺平道路，使其在时间对齐性方面达到更高的水平。

附录

补充材料

11. 视觉语言模型校准

在本节中，我们提供具体的实现细节，用于检测通过PULS得到的命题是否存在于合成视频的每一帧中。首先，我们描述视觉语言模型（VLM）如何进行推理，然后介绍用于获取最优阈值以校准视觉语言模型的方法。

11.1 通过视觉语言模型进行推理

如第4.2节所述，我们将 VLM 用作语义检测器。

11.2 误检阈值识别校准数据集

我们使用COCO Captions[7] 数据集对以下开源视觉语言模型进行校准，以用于 NeuS-V：

• InternVL2 系列

  （1B、2B、8B）[45]

• LLaMA-3.2 Vision Instruct

由于该数据集中每张图像与对应描述构成一个正样本对，我们通过将图像与其他图像的描述随机配对，构建一组负样本图像-描述对。

在构建包含40,000 对图像-描述的校准数据集后，我们使用 VLM 对每对输出“是”（Yes）或“否”（No）。

阈值设定方法

我们可以通过将上述问题视为单分类或多分类任务来识别 VLM 的最佳阈值。我们选择后者。

具体流程如下：

1. 首先将检测结果整理为一个置信度得分列表和一个one-hot 编码的真实标签；

2. 然后遍历所有可用的置信度得分，寻找最优阈值；

3. 对于每一个候选阈值，我们计算其正确预测的比例（见图7）；

4. 最优阈值

   通过最大化准确率（Accuracy）来确定，即真阳性（True Positive）与真阴性（True Negative）预测数量的比值。

此外，为了全面评估模型行为，我们还计算了接收者操作特征曲线（ROC），如图7所示。该曲线通过计算所有阈值下的真阳性率（TPR）和假阳性率（FPR）来实现。

在获得最优阈值后，我们使用它对 VLM 的预测结果进行校准。

图7中展示了校准前后准确率与置信度得分的关系曲线。

12. 视频自动机生成函数

13. NeuS-V 提示套件

创建数据集：我们的数据集经过精心设计，用于评估生成视频中的时间保真度和事件排序。它涵盖了四个主题——“自然”“人类与动物活动”“物体交互”和“驾驶数据”，每个主题包含 40 个提示。这些提示的复杂程度各不相同，根据时间运算符和逻辑运算符的数量，被分为 20 个基础提示、15 个中级提示和 5 个高级提示（见表 5）。这些提示是使用 GPT-4o 以及提示 4 中的系统提示生成的。为确保质量，每个提示都经过手动验证，以确保其清晰性、完整性和相关性。

从提示生成视频：我们使用开源模型和闭源模型为所有160个提示生成了视频。对于开源模型，我们通过克隆它们的HuggingFace Spaces并使用huggingface客户端查询它们，利用了预训练的权重和代码。对于闭源模型（Gen3和Pika），我们实现了一个自定义的命令行界面（CLI），通过逆向工程它们的前端接口来自动化视频生成请求。总共，我们制作了640个视频（160个提示×四个模型）。在接受后，我们还计划在HuggingFace上启动一个公开可用的排行榜，这将允许对新出现的文本到视频（T2V）模型进行持续评估。

注释：注释是通过众包从20名参与者那里收集的，包括来自像X（前身为Twitter）和LinkedIn这样的社交媒体平台的贡献者。如图8所示，注释者被指示在将视觉质量与文本到视频的对齐分开的同时，评估视频与其相应提示的一致性。

对提示的见解：我们在表6和表7中展示了我们数据集中的代表性示例，突出了提示的多样性和复杂性。这些示例提供了提示，以在不同模式中代表它们。在未来，我们计划通过在现有主题中添加更多提示并引入新类别来扩展数据集，以进一步增强其实用性和范围。

原文链接： https://arxiv.org/pdf/2411.16718