# Specification-Driven Video Search via Foundation Models and Formal Verification

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

## Key facts

- Cited by 10 papers in the map (data through 14 Oct 2026).
- Builds on 29 of its 46 references that are in the map.
- First posted on arXiv 18 Sep 2023.

## Builds on (most cited first, 29 of 29)

- [Learning Transferable Visual Models From Natural Language Supervision](https://mlsanity.com/paper/2103.00020/) (2021)
- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [Swin Transformer: Hierarchical Vision Transformer using Shifted Windows](https://mlsanity.com/paper/2103.14030/) (2021)
- [Faster R-CNN: Towards Real-Time Object Detection with Region Proposal Networks](https://mlsanity.com/paper/1506.01497/) (2015)
- [ImageNet Large Scale Visual Recognition Challenge](https://mlsanity.com/paper/1409.0575/) (2014)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Segment Anything](https://mlsanity.com/paper/2304.02643/) (2023)
- [You Only Look Once: Unified, Real-Time Object Detection](https://mlsanity.com/paper/1506.02640/) (2015)
- [nuScenes: A multimodal dataset for autonomous driving](https://mlsanity.com/paper/1903.11027/) (2019)
- [Grounding DINO: Marrying DINO with Grounded Pre-Training for Open-Set Object Detection](https://mlsanity.com/paper/2303.05499/) (2023)
- [Non-local Neural Networks](https://mlsanity.com/paper/1711.07971/) (2017)
- [SlowFast Networks for Video Recognition](https://mlsanity.com/paper/1812.03982/) (2018)
- [Is Space-Time Attention All You Need for Video Understanding?](https://mlsanity.com/paper/2102.05095/) (2021)
- [Grounded Language-Image Pre-training](https://mlsanity.com/paper/2112.03857/) (2021)
- [Open-vocabulary Object Detection via Vision and Language Knowledge Distillation](https://mlsanity.com/paper/2104.13921/) (2021)
- [A Primer in BERTology: What we know about how BERT works](https://mlsanity.com/paper/2002.12327/) (2020)
- [MovieQA: Understanding Stories in Movies through Question-Answering](https://mlsanity.com/paper/1512.02902/) (2015)
- [Video Classification with Channel-Separated Convolutional Networks](https://mlsanity.com/paper/1904.02811/) (2019)
- [Action Genome: Actions as Composition of Spatio-temporal Scene Graphs](https://mlsanity.com/paper/1912.06992/) (2019)
- [Learning Multi-Domain Convolutional Neural Networks for Visual Tracking](https://mlsanity.com/paper/1510.07945/) (2015)
- [MovieNet: A Holistic Dataset for Movie Understanding](https://mlsanity.com/paper/2007.10937/) (2020)
- [Towards Long-Form Video Understanding](https://mlsanity.com/paper/2106.11310/) (2021)
- [Home Action Genome: Cooperative Compositional Action Understanding](https://mlsanity.com/paper/2105.05226/) (2021)
- [A Graph-Based Framework to Bridge Movies and Synopses](https://mlsanity.com/paper/1910.11009/) (2019)
- [Fast Template Matching and Update for Video Object Tracking and Segmentation](https://mlsanity.com/paper/2004.07538/) (2020)
- [Symbolic LTLf Synthesis](https://mlsanity.com/paper/1705.08426/) (2017)
- [A Large-scale Study of Spatiotemporal Representation Learning with a New Benchmark on Action Recognition](https://mlsanity.com/paper/2303.13505/) (2023)
- [Automaton-Based Representations of Task Knowledge from Generative Language Models](https://mlsanity.com/paper/2212.01944/) (2022)

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

- [Towards Neuro-Symbolic Video Understanding](https://mlsanity.com/paper/2403.11021/) (2024)
- [Fine-Tuning Language Models Using Formal Methods Feedback](https://mlsanity.com/paper/2310.18239/) (2023)
- [We'll Fix it in Post: Improving Text-to-Video Generation with Neuro-Symbolic Feedback](https://mlsanity.com/paper/2504.17180/) (2025)
- [Neuro-Symbolic Evaluation of Text-to-Video Models using Formal Verification](https://mlsanity.com/paper/2411.16718/) (2024)
- [NeuS-QA: Grounding Long-Form Video Understanding in Temporal Logic and Neuro-Symbolic Reasoning](https://mlsanity.com/paper/2509.18041/) (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)
- [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)
- [LogSTOP: Temporal Scores over Prediction Sequences for Matching and Retrieval](https://mlsanity.com/paper/2510.06512/) (2025)

## Abstract (arXiv)

The increasing abundance of video data enables users to search for events of interest, e.g., emergency incidents. Meanwhile, it raises new concerns, such as the need for preserving privacy. Existing approaches to video search require either manual inspection or a deep learning model with massive training. We develop a method that uses recent advances in vision and language models, as well as formal methods, to search for events of interest in video clips automatically and efficiently. The method consists of an algorithm to map text-based event descriptions into linear temporal logic over finite traces (LTLf) and an algorithm to construct an automaton encoding the video information. Then, the method formally verifies the automaton representing the video against the LTLf specifications and adds the pertinent video clips to the search result if the automaton satisfies the specifications. We provide qualitative and quantitative analysis to demonstrate the video-searching capability of the proposed method. It achieves over 90 percent precision in searching over privacy-sensitive videos and a state-of-the-art autonomous driving dataset.