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

TL;DR

NeuS-V introduces a formal, neuro-symbolic framework for evaluating text-to-video models by converting prompts into Temporal Logic specifications and verifying generated videos against a video automaton using probabilistic model checking. The method combines neural perception scores with TL-based reasoning (via PULS) to produce a calibrated NeuS-V score across four evaluation modes (object existence, spatial relations, action alignment, overall consistency). A dedicated NeuS-V Prompt Suite benchmarks temporally extended prompts, and results show NeuS-V correlates with human judgments much more strongly than visual-quality baselines, highlighting gaps in current T2V models for temporally coherent generation. The work also provides a detailed calibration pipeline, ablation studies, and a real-world robustness check on MSR-VTT, underscoring the practical significance of temporal-formal evaluation for safety-critical applications and guiding future improvements in T2V research.

Abstract

Recent advancements in text-to-video models such as Sora, Gen-3, MovieGen, and CogVideoX are pushing the boundaries of synthetic video generation, with adoption seen in fields like robotics, autonomous driving, and entertainment. As these models become prevalent, various metrics and benchmarks have emerged to evaluate the quality of the generated videos. However, these metrics emphasize visual quality and smoothness, neglecting temporal fidelity and text-to-video alignment, which are crucial for safety-critical applications. To address this gap, we introduce NeuS-V, a novel synthetic video evaluation metric that rigorously assesses text-to-video alignment using neuro-symbolic formal verification techniques. Our approach first converts the prompt into a formally defined Temporal Logic (TL) specification and translates the generated video into an automaton representation. Then, it evaluates the text-to-video alignment by formally checking the video automaton against the TL specification. Furthermore, we present a dataset of temporally extended prompts to evaluate state-of-the-art video generation models against our benchmark. We find that NeuS-V demonstrates a higher correlation by over 5x with human evaluations when compared to existing metrics. Our evaluation further reveals that current video generation models perform poorly on these temporally complex prompts, highlighting the need for future work in improving text-to-video generation capabilities.

Figures (8)

• Figure 1: Current generative video evaluation methods struggle with temporal fidelity.NeuS-V converts prompts into Temporal Logic specifications and formally verifies them against a video automaton. The upper video aligns with the prompt's temporal sequencing, while the lower video, despite being visually appealing, fails to do so. Unlike VBench, NeuS-V effectively differentiates between them.
• Figure 2: Video automaton from the running example. Above is an automaton of a video generated by the Gen-3 model constructed with a TL specification (See \ref{['eq:running_example_tl_spec']}). Every state $q_t$ from a frame $\mathcal{F}$ is labeled and has incoming and outgoing transition probabilities $\delta(q,q') \in [0,1]$. For example, in frame $\mathcal{F}_8$, we have probabilities $P(p_4)=0.8$ and $P(p_5)=0.9$, where $p_4$ represents the atomic proposition "cyclist turns", and $p_5$ represents "cyclist avoids obstacle". These probabilities are assigned because the cyclist (red-dotted circle) has turned left to avoid obstacles on the road. In the state $q_{256}$, we have an incoming probability $0.72 = P(p_1) \times P(p_2) \times P(p_4) \times P(p_5) \times (1-P(p_3))$ from the previous state $q_{224}$, where that label is true for $p_1,p_2,p_4$, and $p_5$, and false for $p_3$ denoted as $\neg\{p_3\}$.
• Figure 3: Spatio-temporal and semantic measurements between a text prompt and a video by NeuS-V. We first decompose the text prompt to TL specification $\Phi$, then transform the synthetic video into an automaton representation $\mathcal{A}_{\mathcal{V}}$. Finally, we calculate the satisfaction probability by probabilistically checking the extent to which $\mathcal{A}_{\mathcal{V}}$ satisfies $\Phi$.
• Figure 4: Correlation with Human Annotations.NeuS-V consistently shows a stronger alignment with human text-to-video annotations (Pearson coefficients displayed at the top of each plot).
• Figure 5: Distribution of scores across the four modes of $\textit{PULS}$