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

arXiv: https://arxiv.org/abs/2411.16718 · HTML: https://mlsanity.com/paper/2411.16718/

## Key facts

- Cited by 9 papers in the map (data through 14 Oct 2026).
- Builds on 35 of its 55 references that are in the map.
- First posted on arXiv 22 Nov 2024.

## Builds on (most cited first, 30 of 35)

- [Denoising Diffusion Probabilistic Models](https://mlsanity.com/paper/2006.11239/) (2020)
- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [Visual Instruction Tuning](https://mlsanity.com/paper/2304.08485/) (2023)
- [CogVideoX: Text-to-Video Diffusion Models with An Expert Transformer](https://mlsanity.com/paper/2408.06072/) (2024)
- [VBench: Comprehensive Benchmark Suite for Video Generative Models](https://mlsanity.com/paper/2311.17982/) (2023)
- [Align your Latents: High-Resolution Video Synthesis with Latent Diffusion Models](https://mlsanity.com/paper/2304.08818/) (2023)
- [Video-LLaMA: An Instruction-tuned Audio-Visual Language Model for Video Understanding](https://mlsanity.com/paper/2306.02858/) (2023)
- [Microsoft COCO Captions: Data Collection and Evaluation Server](https://mlsanity.com/paper/1504.00325/) (2015)
- [Video-ChatGPT: Towards Detailed Video Understanding via Large Vision and Language Models](https://mlsanity.com/paper/2306.05424/) (2023)
- [DSPy: Compiling Declarative Language Model Calls into Self-Improving Pipelines](https://mlsanity.com/paper/2310.03714/) (2023)
- [Structure and Content-Guided Video Synthesis with Diffusion Models](https://mlsanity.com/paper/2302.03011/) (2023)
- [I2VGen-XL: High-Quality Image-to-Video Synthesis via Cascaded Diffusion Models](https://mlsanity.com/paper/2311.04145/) (2023)
- [EvalCrafter: Benchmarking and Evaluating Large Video Generation Models](https://mlsanity.com/paper/2310.11440/) (2023)
- [Optimizing Instructions and Demonstrations for Multi-Stage Language Model Programs](https://mlsanity.com/paper/2406.11695/) (2024)
- [VideoScore: Building Automatic Metrics to Simulate Fine-grained Human Feedback for Video Generation](https://mlsanity.com/paper/2406.15252/) (2024)
- [T2V-CompBench: A Comprehensive Benchmark for Compositional Text-to-video Generation](https://mlsanity.com/paper/2407.14505/) (2024)
- [FETV: A Benchmark for Fine-Grained Evaluation of Open-Domain Text-to-Video Generation](https://mlsanity.com/paper/2311.01813/) (2023)
- [Make It Move: Controllable Image-to-Video Generation with Text Descriptions](https://mlsanity.com/paper/2112.02815/) (2021)
- [T2V-Turbo: Breaking the Quality Bottleneck of Video Consistency Model with Mixed Reward Feedback](https://mlsanity.com/paper/2405.18750/) (2024)
- [PEEKABOO: Interactive Video Generation via Masked-Diffusion](https://mlsanity.com/paper/2312.07509/) (2023)
- [The Probabilistic Model Checker Storm](https://mlsanity.com/paper/2002.07080/) (2020)
- [NL2TL: Transforming Natural Languages to Temporal Logics using Large Language Models](https://mlsanity.com/paper/2305.07766/) (2023)
- [T2V-Turbo-v2: Enhancing Video Generation Model Post-Training through Data, Reward, and Conditional Guidance Design](https://mlsanity.com/paper/2410.05677/) (2024)
- [Grounding Complex Natural Language Commands for Temporal Tasks in Unseen Environments](https://mlsanity.com/paper/2302.11649/) (2023)
- [Towards A Better Metric for Text-to-Video Generation](https://mlsanity.com/paper/2401.07781/) (2024)
- [TC-Bench: Benchmarking Temporal Compositionality in Text-to-Video and Image-to-Video Generation](https://mlsanity.com/paper/2406.08656/) (2024)
- [Subjective-Aligned Dataset and Metric for Text-to-Video Quality Assessment](https://mlsanity.com/paper/2403.11956/) (2024)
- [Data-Efficient Learning of Natural Language to Linear Temporal Logic Translators for Robot Task Specification](https://mlsanity.com/paper/2303.08006/) (2023)
- [Reward Guided Latent Consistency Distillation](https://mlsanity.com/paper/2403.11027/) (2024)
- [PyTorchVideo: A Deep Learning Library for Video Understanding](https://mlsanity.com/paper/2111.09887/) (2021)

## Built on by (most cited first, 9 of 9)

- [We'll Fix it in Post: Improving Text-to-Video Generation with Neuro-Symbolic Feedback](https://mlsanity.com/paper/2504.17180/) (2025)
- [A Challenge to Build Neuro-Symbolic Video Agents](https://mlsanity.com/paper/2505.13851/) (2025)
- [Real-Time Privacy Preservation for Robot Visual Perception](https://mlsanity.com/paper/2505.05519/) (2025)
- [VideoVerse: Does Your T2V Generator Have World Model Capability to Synthesize Videos?](https://mlsanity.com/paper/2510.08398/) (2025)
- [ObjectAlign: Neuro-Symbolic Object Consistency Verification and Correction](https://mlsanity.com/paper/2511.18701/) (2025)
- [RT-NeuS: Towards Real-Time Neuro-Symbolic Video Understanding via Adaptive Temporal Verification](https://mlsanity.com/paper/2602.23553/) (2026)
- [Incentivizing Vision Language Models to Search for Long Video Question Answering](https://mlsanity.com/paper/2607.02959/) (2026)
- [Plan-and-Verify Video Reward Reasoning with Spatio-Temporal Scene Graph Grounding](https://mlsanity.com/paper/2606.11838/) (2026)
- [VeriPhy: Agentic Physical Reasoning for World Model Evaluation and Refinement](https://mlsanity.com/paper/2609.03153/) (2026)

## Abstract (arXiv)

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.