RT-NeuS: Towards Real-Time Neuro-Symbolic Video Understanding via Adaptive Temporal Verification

Long-form video question answering (LVQA) requires answering natural-language queries about videos spanning minutes to hours, demanding temporal reasoning across thousands of frames. Standard vision-language models (VLMs) struggle with this task: their fixed frame budgets force aggressive downsampling that misses the temporal structure that complex queries depend on. Neuro-symbolic approaches address this by decomposing queries into atomic propositions, translating them into temporal logic specifications, and applying formal model checking to retrieve segments satisfying the specification. This yields up to 10% higher accuracy on temporally complex benchmarks, with interpretability and formal guarantees. However, constructing the video automaton requires grounding every proposition at every frame window via VLM calls, resulting in up to 130x slower inference than standard VLM prompting. We present RT-NeuS, a framework that preserves the accuracy and formal guarantees of temporal-logic-guided LVQA while closing this latency gap. RT-NeuS introduces coarse-to-fine adaptive sampling to identify the small set of query-relevant, visually distinct frames, and batched proposition detection with KV-cache reuse to evaluate all propositions per window in a single forward pass. We derive latency upper bounds as a function of video length, proposition count, and sampling density. Experiments on LongVideoBench, Video-MME, and MLVU reduce inference latency by up to 13x on a single NVIDIA H200 GPU, while matching or exceeding prior neuro-symbolic accuracy.