Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 2411.16718

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

S P Sharan·Minkyu Choi·Sahil Shah·Harsh Goel·Mohammad Omama·Sandeep Chinchali
View original source ↗Read source document ↗Export metadata ↓

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.

Explore related subjects

cs.CVcs.AI

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

S P Sharan, Minkyu Choi, Sahil Shah, Harsh Goel, Mohammad Omama, Sandeep Chinchali. 2025-04-25. Neuro-Symbolic Evaluation of Text-to-Video Models using Formal Verification. https://arxiv.org/abs/2411.16718

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Lifelong Learning of Video Diffusion Models From a Single Video Stream

Video diffusion models can enable embodied agents to anticipate plausible futures from the recent past, but they are typically trained offline on curated datasets--a mismatch with the agents' learning setup at deployment: online, from a single video stream that sequentially outputs one frame at a time. We bridge this training gap and demonstrate that training autoregressive video diffusion models from such a stream, resembling the experience of embodied agents, is not only possible but can also perform comparably to standard offline training given the same number of gradient steps. We find that this robustness to video stream autocorrelation and nonstationarity can be achieved using experience replay methods that retain a subset of the video stream. To support training and evaluation in this setting, we introduce five new datasets for streaming lifelong generative video modeling: Lifelong Bouncing Balls (O), Lifelong Bouncing Balls (C), Lifelong 3D Maze, Lifelong Drive, and Lifelong PLAICraft, each consisting of one million consecutive frames from environments of increasing complexity. Together, our datasets and experiments lay the groundwork for video generative models and world models that continuously learn from single-sensor video streams rather than fixed datasets.

cs.CV↗
arXiv2026

Bayesian Fusion of Active Contour Models and ConvNet Priors for Standing Dead Tree Segmentation

Instance segmentation is a core computer vision task with great practical significance. Recent advances, driven by large-scale benchmark datasets, have yielded good general-purpose Convolutional Neural Network (CNN)-based methods. Natural Resource Monitoring (NRM) utilizes remote sensing imagery with generally known scale and containing multiple overlapping instances of the same class, wherein the object contours are jagged and highly irregular. This is in stark contrast with the regular man-made objects found in classic benchmark datasets. We address this problem and propose a novel instance segmentation method geared towards NRM imagery. We formulate the problem as Bayesian maximum a posteriori inference which, in learning the individual object contours, incorporates shape, location, and position priors from state-of-the-art CNN architectures, driving a simultaneous level-set evolution of multiple object contours. We employ loose coupling between the CNNs that supply the priors and the active contour process, allowing a drop-in replacement of new network architectures. Moreover, we introduce a novel prior for contour shape, namely, a class of Deep Shape Models based on architectures from Generative Adversarial Networks (GANs). These Deep Shape Models are in essence a non-linear generalization of the classic Eigenshape formulation. In experiments, we tackle the challenging, real-world problem of segmenting individual dead tree crowns and delineating precise contours. We compare our method to two leading general-purpose instance segmentation methods - Mask R-CNN and K-net - on color infrared aerial imagery. Results show our approach to significantly outperform both methods in terms of reconstruction quality of tree crown contours. Furthermore, use of the GAN-based deep shape model prior yields significant improvement of all results over the vanilla Eigenshape prior.

cs.CV↗
arXiv2026

Sonicmesh: Enhancing 3D Human Mesh Reconstruction in Vision-Impaired Environments With Acoustic Signals

3D human mesh reconstruction (HMR) from RGB images often degrades under poor illumination, occlusion, and non-line-of-sight conditions. Acoustic sensing provides complementary spatial cues but suffers from low spatial resolution. We propose SonicMesh, which, to the best of our knowledge, is the first acoustic--visual framework for robust 3D human mesh reconstruction. SonicMesh first converts ultrasonic echoes into range--azimuth acoustic images through an Inverse Synthetic Aperture Radar (ISAR)-based imaging process. It then introduces a cross-dimensional anatomical registration module that maps modality-specific 2D joint features into a common canonical 3D human space. The registered anatomical representations are further integrated with acoustic and visual features through a two-stage fusion network for final mesh reconstruction. Experiments demonstrate that SonicMesh achieves accurate and robust 3D human reconstruction across normal, poor-light, occluded, and non-line-of-sight environments, consistently outperforming existing RGB-, radio-frequency (RF)-, and mmWave-based approaches under challenging sensing conditions.

cs.CV↗