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

Yunhao Yang1, Jean-Raphaël Gaglione1, Sandeep Chinchali1, Ufuk Topcu1

###### Abstract

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.

## Introduction

The increasing abundance of video data enables users to search for events of
interest, but existing approaches to searching through videos are either
inefficient or require manual inspection. Various cameras, such as security or
vehicle dash cameras, gather terabytes of video data, and manually searching
for events (e.g., vehicle crashes) over such large-scale data is impractical.
Existing automated video search approaches require either excessive human
annotations (Chang et al. 1998) or massive training for neural networks
(Chang, Ma, and Smeulders 2007; Li et al. 2019), which are inefficient.
Furthermore, none of these approaches provide guarantees on the correctness of
their search results.

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
efficiently with probabilistic guarantees. The method includes an algorithm
that maps texts to formal specifications and an algorithm to construct
automata encoding information from videos, as illustrated in Figure 1. In
practice, many events of interest are expressed in natural language. We
accordingly design an algorithm that sends the text-based event description to
a text generation model, e.g., GPT-series, and queries the model for the
formal specifications and propositions describing the event. This algorithm
converts texts to an interpretable format that we can use to search through
videos.

Figure 1: Demonstration of searching an event of interest—described in
texts—within a given video.

Meanwhile, we design an algorithm to construct automata encoding the video
information. The algorithm utilizes a vision-language model to determine
whether the event described by the proposition happens in the video, with a
score indicating the model’s confidence. The algorithm calibrates the
confidence to the prediction accuracy of the search query using uncertainty
quantification techniques for deep learning models. It uses the calibrated
confidence to compute the probability that the automaton satisfies the
specifications. Hence, we can obtain the probability of each video satisfying
the event description during video search and add videos with probabilities
above 0.5 to our search result. In contrast to existing approaches, this
method is fully automated, computationally inexpensive, and can provide
probabilistic guarantees through formal verification.

We provide case studies and quantitative analysis on privacy-sensitive videos
and the state-of-the-art autonomous driving dataset to demonstrate the video-
searching capability of the proposed pipeline. We use the ground truth
annotations from the datasets to evaluate the proposed pipeline, and the
search results achieve over 90 percent precision.

## Related Work

#### Symbolic Representations.

Video searching or understanding typically requires the videos to be converted
into some symbolic representations encoding the video information. Existing
works (Mavroudi, Haro, and Vidal 2020; Wu and Krähenbühl 2021) utilize object
detection models to form symbolic representations of videos that encode object
information (e.g., existence, features). Some other works (Ji et al. 2020; Rai
et al. 2021; Gorelick et al. 2007) construct graphs that represent each event
or object as a temporal sequence of spatial information, which improves the
interpretability of the raw data. However, none of the existing video
representations are capable of formal verification. We introduce a video
representation that can be formally verified against the provided
specifications.

Another work (Umili, Capobianco, and De Giacomo 2022) uses a deep learning
model to classify images and builds a deterministic finite automaton
representing an image sequence through the classification results. It then
verifies the automaton against temporal logic specifications. This work
neither considers potential image classification errors nor provides
probabilistic guarantees. In contrast, we incorporate the confidence scores
returned by the foundation model to provide probabilistic guarantees. In
addition to Umili et al., we propose a method to map natural language to
temporal logic specifications.

#### Video Understanding.

Video applications like video searching require understanding the content of
the videos. Many works focus on short-form video understanding (Feichtenhofer
et al. 2019; Tran et al. 2019; Wang et al. 2018), i.e., understanding videos
less than five seconds, and long-form video understanding (Wu and Krähenbühl
2021; Tapaswi et al. 2016; Huang et al. 2020; Xiong et al. 2019), e.g., movie
question-answering. The existing works interpret the videos to detect actions
in the video (Deng, Yang, and Chen 2023; Bertasius, Wang, and Torresani 2021;
Liu et al. 2021), track objects (Nam and Han 2016; Sun et al. 2020), or detect
shot transitions (Porter, Mirmehdi, and Thomas 2001). However, these works do
not provide any guarantees on their video understanding outcomes. The pipeline
we proposed provides guarantees by formally verifying videos against the text-
based descriptions of events of interest.

#### Formal Verification.

Formal verification is a technique to prove or disprove the satisfaction of a
system with respect to certain formal specifications or properties. Such a
technique requires a formal representation of the system, such as a finite-
state automaton (FSA) or a Markov Decision Process (MDP). Bai et al. (Bai et
al. 2019) propose a method to construct MDPs from driving behaviors and verify
the safety of the behaviors. Sai et al. (Narasimhan, Bhat, and Chinchali 2023)
use MDPs to represent robotic control systems and verify the safety of the
system. Yang et al. (Yang et al. 2022) construct FSAs for textual task
knowledge extracted from large language models. None of the existing works
apply to videos alone. We take advantage of the emerging foundation models to
build formal representations of videos.

## Preliminaries

#### Probabilistic Automaton.

We formally define a _probabilistic automaton_ (PA)(Rabin 1963) as a tuple
$\mathcal{Amissing}=\langle Q,q_{0},F,L,\delta,\lambda\rangle$, where $Q$ is
the set of states, $q_{0}\in Q$ is the initial state, $F\in Q$ is the set of
acceptance states, $L$ is the set of state labeling symbols, $\lambda:Q\to L$
is the label function, and $\delta:Q\times Q\to\\{0,1\\}$ is the transition
function indicating whether a given transition is allowed by the automaton.
Each transition ($q\xrightarrow{\sigma}q^{\prime}$) associates with a
probability $\mathbb{P}$, which means if we are at state $q$, we choose the
transition $q\xrightarrow{\sigma}q^{\prime}$ with a probability $\mathbb{P}$.
Note that for every state, the probabilities of all the outgoing transitions
of this state with the input symbol $\sigma$ sum up to 1.

We define a set of atomic propositions $P$ for the state labeling symbols
$L\coloneqq 2^{P}$. The propositional logic formula is based on these atomic
propositions.

We then define a _trajectory_ as a sequence of labels of states and the input
symbols of the transitions

$\lambda(q_{0}),\lambda(q_{1}),...,\lambda(q_{n})$, where $q_{i}\in Q$.

The trajectory starts from the initial state $q_{0}$ and ends at one of the
acceptance states $q_{n}\in F$. Each trajectory is associated with a
probability, which is the product of all the probabilities of the state
transitions in the trajectory.

#### Linear Temporal Logic over Finite Traces.

Temporal logic represents propositional and first-order logical reasoning with
respect to time. _Linear temporal logic over finite traces_ (LTLf)(Zhu et al.
2017) is a form of temporal logic that deals with finite sequences, i.e.,
finite-length trajectories. The syntax of LTLfformulas is defined as

$\varphi\coloneqq p\in
P\mid\lnot\varphi\mid\varphi_{1}\land\varphi_{2}\mid\operatorname{\leavevmode\hbox
to6.09pt{\vbox to6.09pt{\pgfpicture\makeatletter\hbox{\hskip
3.04527pt\lower-3.04527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{{{}} {}{}{}{}{}{}{}{}
}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.84528pt}{0.0pt}\pgfsys@curveto{2.84528pt}{1.57141pt}{1.57141pt}{2.84528pt}{0.0pt}{2.84528pt}\pgfsys@curveto{-1.57141pt}{2.84528pt}{-2.84528pt}{1.57141pt}{-2.84528pt}{0.0pt}\pgfsys@curveto{-2.84528pt}{-1.57141pt}{-1.57141pt}{-2.84528pt}{0.0pt}{-2.84528pt}\pgfsys@curveto{1.57141pt}{-2.84528pt}{2.84528pt}{-1.57141pt}{2.84528pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi\mid\varphi_{1}\operatorname{\mathcal{U}}\varphi_{2}$.

LTLfconsists of all operations from propositional logic, such as AND
($\land$), OR ($\vee$), XOR ($\oplus$), NOT ($\neg$), IMPLY ($\rightarrow$),
etc., and the following temporal operations:

  * •

Always ($\operatorname{\square}\phi_{1}$): $\phi_{1}$ is true for every step
in the trajectory.

  * •

Sometimes ($\operatorname{\lozenge}\phi_{1}$): $\phi_{1}$ is true for at least
one step in the trajectory.

  * •

Next ($\operatorname{\leavevmode\hbox to6.09pt{\vbox
to6.09pt{\pgfpicture\makeatletter\hbox{\hskip 3.04527pt\lower-3.04527pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{{{}} {}{}{}{}{}{}{}{}
}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.84528pt}{0.0pt}\pgfsys@curveto{2.84528pt}{1.57141pt}{1.57141pt}{2.84528pt}{0.0pt}{2.84528pt}\pgfsys@curveto{-1.57141pt}{2.84528pt}{-2.84528pt}{1.57141pt}{-2.84528pt}{0.0pt}\pgfsys@curveto{-2.84528pt}{-1.57141pt}{-1.57141pt}{-2.84528pt}{0.0pt}{-2.84528pt}\pgfsys@curveto{1.57141pt}{-2.84528pt}{2.84528pt}{-1.57141pt}{2.84528pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\phi_{1}$):
$\phi_{1}$ is true in the next step.

  * •

Until ($\phi_{1}\operatorname{\mathcal{U}}\phi_{2}$): $\phi_{1}$ has to be
true until $\phi_{2}$ becomes true, $\phi_{2}$ has to be true at one of the
future steps.

$\phi_{1}$ and $\phi_{2}$ are LTLfformulas. An LTLfformula is composed of
variables in $P$ and logic operations, as we call a _specification_. Each
formula can be satisfied by a finite sequence of truth valuations of variables
in $P$, as we call a trajectory. If a trajectory $T$ satisfies the
specification $\Phi$, we denote $T\models\Phi$.

#### Foundation Model.

Foundation models are large-scale machine learning models that are trained on
a vast amount of data and can be directly applied or fine-tuned to a wide
range of downstream tasks. _Large language models_ (LLMs)such as BERT (Rogers,
Kovaleva, and Rumshisky 2020), CodeX (Chen et al. 2021), and GPT-series (Brown
et al. 2020; OpenAI 2023) are text foundation models. LLMs are capable of
downstream language processing tasks like text generation (next-word
prediction), question-answering, text classification and summarization,
machine translation, etc.

Beyond text capability, several multimodal foundation models can understand
and process both visual and textual inputs. CLIP (Radford et al. 2021)
measures the similarity or consistency between the input texts and images.
Object detection models such as Yolo (Redmon et al. 2016), Grounded-Segment-
Anything (Grounded-SAM) (Liu et al. 2023; Kirillov et al. 2023), ViLD (Gu et
al. 2022), GLIP (Li et al. 2022) and R-CNN (Ren et al. 2017) can detect the
existences and positions of objects described in the textual inputs from a
given image. In the later parts, we refer to these models as _vision-language
models_ (VLMs)in the later parts.

## Methodology

We develop a method to search for events of interest in video. For each video
clip, the method takes in a set of text-based event descriptions and outputs a
score indicating the probability of the description being satisfied in the
video. The method has two components: The first is an algorithm to map text-
based event descriptions into LTLfspecifications. The second component is an
algorithm to construct a probabilistic automaton encoding the video
information. Then, the method verifies the automaton against the
specifications to obtain a probability that the automaton satisfies the
LTLfspecifications. By applying this method to a set of videos, we can
efficiently search for events of interest in these videos by finding all the
videos whose automata satisfy the specifications.

### Text-Based Description to LTLfSpecification

We develop an algorithm to map text-based descriptions of events of interest
to LTLfspecifications. The algorithm first extracts a set of atomic
propositions and by querying the LLMto extract _noun phrases_ from the texts:

⬇

1 Extract noun phrases from the following rules:

2 A list of rules.

3 1. noun phrase 1

4 2. noun phrase 2...

Note that a noun phrase is a group of words that functions as a single unit
within a sentence and centers around a noun. We consider these noun phrases as
atomic propositions. Then, the algorithm queries the LLMagain to transform the
textual rules to a set of LTLfspecifications with respect to the atomic
propositions:

⬇

1 Define the following rules in temporal logic with atomic propositions noun
phrase 1, noun phrase 2, ...:

2 A list of rules.

3 1. Temporal logic formula 1

4 2. Temporal logic formula 2...

Now we have the sequence of frames $\mathcal{F}$, a set of atomic propositions
$P$, and LTLfspecifications $\Phi$.

### Video to Probabilistic Automaton

We develop an algorithm to extract information from videos and construct
probabilistic automata encoding those information. The algorithm starts from a
provided video and a set of textual rules regarding the video. We extract
frames from the video at regular intervals, where each frame is an image. We
denote the number of frames extracted in each second of the video as _frame
frequency_ , with a unit of _frames per second_.

#### Calibrating Confidence and Accuracy

We use a VLM, e.g., an open-domain object detection model, to evaluate each
atomic proposition at each frame. In particular, a VLMthat can take text-based
propositions and the frame as inputs and returns _confidence score_ for each
proposition. A confidence score is a softmax score that indicates how certain
the model is about its prediction. These scores are between 0 and 1, where a
value close to 1 indicates high confidence and a value close to 0 means low
confidence.

The model detects whether the object or scene described by the atomic
proposition appears in the image with a certain confidence. We evaluate the
proposition as true only if the object or scene is detected. However, the
VLMcan raise detection errors. We consider a detection result to be _correct_
only if the VLMdetected an object that actually exists in the image.
Therefore, we utilize the confidence scores returned by the model and estimate
a mapping between confidence scores and the percentage of correct detection
over all the detection results, as we call _classification accuracy_.

######  Definition 1.

Let $N$ be the number of detection results whose confidence scores returned by
the VLMfall into a particular range $[c_{1},c_{2})$, $C$ be the number of
correct detection results (the detected object actually appears in the image)
with confidence scores between $[c_{1},c_{2})$, we define the classification
accuracy $A_{C}$ of confidence interval $(c_{1},c_{2}]$ as

$A_{C}=\frac{C}{N}$.

We assume that a VLMperforms consistently on data outside its training
dataset. Under this assumption, we consider the classification accuracy at
each confidence interval on a validation dataset as the probability of the
detection result being correct on realistic data. Therefore, we apply the
model to an image classification task on the validation dataset to estimate a
confidence-accuracy mapping and assume it also applies to realistic data.

We apply the VLMon a validation dataset independent of the video to obtain the
classification accuracies at each confidence interval. Hence, we get a set of
confidence-accuracy pairs. Then, we use a logistic function

$f(x)=\frac{1}{1+\exp(-k\cdot(x-x_{0}))}$ (1)

to estimate a mapping function $\mathcal{M:C\mapsto A}$ that maps confidence
scores to an accuracies. We use these accuracies in constructing probabilistic
automata.

#### Constructing Probabilistic Automaton

We now have a VLM$M_{V}:\mathcal{F}\times P\mapsto C$ that takes in a frame
and a proposition and returns a confidence score, a sequence of frames
$\mathcal{F}$, atomic propositions $P$, and a mapping function $\mathcal{M}$.
We use them to construct a probabilistic automaton and verify it against the
LTLfspecifications $\Phi$.

We start by creating an initial state $q_{0}$ whose label is _none_ , meaning
that the initial state’s label will not be counted into the trajectory during
verification. Then, we process the sequence of frames in order to construct a
probabilistic automaton. This procedure includes four steps:

We process each frame in four steps: We first send the frame and all atomic
propositions to the VLMand obtain a list of confidence scores associated with
the propositions. In the second step, we map the confidence scores into
accuracies through the function $\mathcal{M}$. In the third step, we create
$2^{|P|}$ ($|P|$ is the number of atomic propositions) new automaton states,
each corresponding to a conjunction of propositions in $2^{P}$. The
corresponding conjunction of propositions is the label for the state. As an
example, if an atomic proposition set $P=\\{p_{1},p_{2}\\}$, we build four
states with labels $p_{1}\land p_{2}$, $\neg p_{1}\land p_{2}$,
$p_{1}\land\neg p_{2}$, and $\neg p_{1}\land\neg B$, respectively.

In the fourth step, we compute a probability score for each newly created
state at frame $\mathcal{F}_{j}$. For a new state $q_{j,k}$, the probability
is the product of the probabilities for all the propositions

$\mathbb{P}_{j,k}=\prod_{p_{i}}\mathcal{M}(M_{V}(\mathcal{F}_{j},p_{i}))\quad\text{for
all }p_{i}\in P,$ (2)

where $\mathcal{F}_{j}$ is the current frame. The probability of the negation
of a proposition ($\neg p_{i}$) is
$1-\mathcal{M}(M_{V}(\mathcal{F}_{j},p_{i}))$. For every new state $q_{j,k}$
whose probability $\mathbb{P}_{j,k}>0$, we construct transitions from all the
states from the previous frame $\mathcal{F}_{j-1}$ to $q_{j,k}$ with
probability $\mathbb{P}_{j,k}$. After constructing the transitions, we remove
all the new states that do not have incoming transitions. If $\mathcal{F}_{j}$
is the first frame (j=1), we add transitions from the initial state $q_{0}$ to
every new state.

We repeat the four steps for all the frames in $\mathcal{F}$ and add the
states created from the last frame to the set of acceptance states. Hence, we
complete the automaton construction. We present the complete procedure in
Algorithm 1.

However, the resulting automaton will consist of $|\mathcal{F}|\times 2^{|P|}$
($|\mathcal{F}|$ is the number of frames) states, which could lead to high
computational complexity. We set two thresholds $t_{T}$ and $t_{F}$ and modify
the mapping function to

$\mathcal{M}^{\prime}(c)=\begin{cases}1\text{ if }c\geq t_{T}\\\
\mathcal{M}(c)\text{ if }t_{F}<c<t_{T}\\\ 0\text{ if }c\leq t_{F},\end{cases}$
(3)

where $c\in C$ is the confidence score. We use $\mathcal{M}^{\prime}$ as the
mapping function for Algorithm 1 instead of $\mathcal{M}$. By doing so, we can
eliminate a proportion of states due to zero-probability incoming transitions.

Algorithm 1 Automaton Construction from Video Frames

1:procedure Frames2Automata(Vision-language model $M_{V}$, Frames
$\mathcal{F}$, Output propositions $P$, Mapping function $\mathcal{M}$, True
threshold $t_{T}$, False threshold $t_{F}$)

2: $\Sigma,L,Q,F,\lambda,\delta$ = $A$, $2^{P}$, [$q_{0}$], [],
[$(q_{0}:none)$], []

3: prev = [$q_{0}$]

4: for $\mathcal{F}_{j}$ in $\mathcal{F}$ do

5: probability = dictionary()

6: for $p_{i}$ in $P$ do

7: $c=M_{V}(\mathcal{F}_{j},p_{i})$

8: probability[$p_{i}$] = $\mathcal{M}(c)$

9: probability[$\neg p_{i}$] = $1-\mathcal{M}(c)$

10: end for

11: current = []

12: for $conj_{k}$ in conjunctions of $2^{P}$ do

13: $\mathbb{P}_{j,k}=\prod_{p_{i}\in conj_{k}}$ probability[$p_{i}$]

14: if $\mathbb{P}_{j,k}>0$ then

15: $Q$.append($q_{j,k}$)

16: current.append($q_{j,k}$)

17: $\lambda$.append(($q_{j,k}:conj_{k}$))

18: $F$.append($q_{j,k}$) if $j=|\mathcal{F}|$

19: for $q_{j-1}$ in current do

20: $\delta$.append(($q_{j-1},q_{j,k},\mathbb{P}_{j,k}$))

21: end for

22: end if

23: end for

24: prev = current

25: end for

26: return $Q,I,F,\Sigma,L,\delta,\lambda$

27:end procedure

### Verification and Video Search

After we construct probabilistic automata for all the videos and convert event
descriptions into LTLfspecifications, we verify each automaton against the
specification. If an automaton satisfies all the specifications with
probability above a certain threshold (typically 0.5), we add the video
corresponding to this automaton to our search result. By doing so, we can
efficiently obtain all the videos containing the provided events of interest
with probabilistic guarantees.

## Empirical Demonstration

We empirically demonstrate the video search method on multiple proof-of-
concept examples. For each video clip, we verify it against the provided
specifications and add it to the search result if the verification probability
is above 50 percent. Then, we provide quantitative analysis on a privacy-
annotated video dataset and on a state-of-the-art autonomous driving dataset.
Both datasets consist of ground truth annotations which we can use to evaluate
the performance of our video search results.

### Confidence-Accuracy Mapping: Grounded-SAM

We choose an open-domain object detection model—Grounded-SAM (Kirillov et al.
2023; Liu et al. 2023)—as the VLMfor the experiments and estimate the
confidence-probability mapping on a validation dataset ImageNet (Russakovsky
et al. 2015).

$0$$0.2$$0.4$$0.6$$0.8$$1$$0$$0.2$$0.4$$0.6$$0.8$$1$confidence returned by
Grounded-SAMclassification accuracyGounded-SAMBenchmarkMapping Estimation

Figure 2: Confidence score returned by the Grounded-SAM versus its
classification accuracy (blue line). The estimated mapping function (green
dotted line) is $\mathcal{M}(x)=1/(1+\exp(-50\cdot(x-0.56)))$. The orange line
is the benchmark mapping, which is an identity function
$\overline{\mathcal{M}}(x)=x$.

We send each image and the complete list of labels from the validation dataset
to the Grounded-SAM to obtain a confidence score with a label for each image.
If the object detected by the Grounded-SAM is identical to the image’s label,
then we consider this case as a correct prediction. Figure 2 shows the
confidence-accuracy mapping. We estimate this mapping using a logistic
function

$\mathcal{M}(x)=\frac{1}{1+\exp(-50\cdot(x-0.56))},$ (4)

which will be used for all the experiments in the later sections.

According to Figure 2, the classification accuracy is consistently equal to
one when the confidence is greater than 0.64 and consistently equal to zero
when the confidence is less than 0.38. For the purpose of simplifying the
constructed automaton, we set a true threshold $t_{T}=0.64$ and a false
threshold $t_{F}=0.38$.

### Proof-of-Concept Demonstrations

We first demonstrate the proposed method through two proof-of-concept
examples, where we search through recorded videos that satisfy manually
generated rules.

Figure 3: Object detection results on the frames from college introductory
videos. -startFFTFTFTF1.01.00.380.620.620.620.380.380.970.970.030.03 Figure 4:
Automaton corresponding to the frames of the video in Figure 3. ‘T’ and ‘F’ in
each state indicate the state’s label, either “faces = True” or “faces =
False.”

#### Single-Rule Verification on College Introductory Videos

We start with an example that searches for videos that satisfy a single
privacy rule: never show faces in the video. We follow the procedure of
processing textual rules to LTLfspecifications and obtain the specification
$Phi$, where

$\Phi=\operatorname{\square}\neg faces$.

During this procedure, we query GPT-4 (OpenAI 2023) to transform textual rules
into LTLfspecifications.

We randomly select college introductory videos from YouTube and break each
video into frames with a frequency of one frame per second. Next, we apply the
Grounded-SAM object detection model to detect “faces” in each frame and
present the detection results in Figure 3. Then, we follow Algorithm 1 to
construct an automaton from the frames of each video.

Figure 4 shows one sample automaton constructed from the frames of a college
introductory video in Figure 3. We use a probabilistic model checker
implemented by Stormpy (Junges and Volk 2021) to compute the probability that
$\Phi$ is satisfied. The model checker returns a probability of $0.7\%$, which
is the probability of the video satisfying $\Phi$. This means the video in
Figure 3 will not be added to the search result since its probability of
satisfying $\Phi$ is below 0.5. We repeat the verification procedure to all
other college introductory videos and add videos whose probability of
satisfying $\Phi$ is greater than 0.5 to the search result. We present more
college introductory videos in Appendix C.1.

#### Multiple-Rule Verification on Traffic Recordings

Figure 5: Sample frames from the Driving Control Dataset with the object detection results. We present the label under each frame. -start1234.14.25.15.267.17.281.01.01.00.270.730.970.970.030.031.01.00.950.051.01.0 Figure 6: Automaton constructed from the frames in Figure 5. The labels for each state are in Table 1.  State | Label | State | Label
---|---|---|---
1,3,7.2 | accelerate | 2 | brake, stop sign
4.2 | no-op | 4.1 | no-op, red light
5.1,6 | brake, red light | 5.2 | brake
7.1, 8 | accelerate, green |  |
Table 1: State labels of the automaton in Figure 6.

We have so far demonstrated the algorithm’s capability in single-rule
verification. We now search for traffic recording clips that satisfy multiple
rules. We send the following prompt to GPT-4 to obtain the LTLfspecifications
regarding the traffic rules:

⬇

1 Given the propositions: pedestrian, stop sign, red light, green light,
accelerate, and brake.

2 Transform the following rules into temporal logic formulas:

3 1. Yield to pedestrians.

4 2. Slow down after seeing the stop sign or red light.

5 3. Accelerate sometime after the light turns from red to green.

The specifications are

$\Phi_{1}=\operatorname{\square}$ (pedestrian $\rightarrow$ brake),

$\Phi_{2}=\operatorname{\square}$ ((stop sign $\vee$ red light)
$\rightarrow\operatorname{\leavevmode\hbox to6.09pt{\vbox
to6.09pt{\pgfpicture\makeatletter\hbox{\hskip 3.04527pt\lower-3.04527pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{{{}} {}{}{}{}{}{}{}{}
}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.84528pt}{0.0pt}\pgfsys@curveto{2.84528pt}{1.57141pt}{1.57141pt}{2.84528pt}{0.0pt}{2.84528pt}\pgfsys@curveto{-1.57141pt}{2.84528pt}{-2.84528pt}{1.57141pt}{-2.84528pt}{0.0pt}\pgfsys@curveto{-2.84528pt}{-1.57141pt}{-1.57141pt}{-2.84528pt}{0.0pt}{-2.84528pt}\pgfsys@curveto{1.57141pt}{-2.84528pt}{2.84528pt}{-1.57141pt}{2.84528pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$ brake),

$\Phi_{3}=\operatorname{\square}$ ((red light
$\land\operatorname{\leavevmode\hbox to6.09pt{\vbox
to6.09pt{\pgfpicture\makeatletter\hbox{\hskip 3.04527pt\lower-3.04527pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{{{}} {}{}{}{}{}{}{}{}
}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.84528pt}{0.0pt}\pgfsys@curveto{2.84528pt}{1.57141pt}{1.57141pt}{2.84528pt}{0.0pt}{2.84528pt}\pgfsys@curveto{-1.57141pt}{2.84528pt}{-2.84528pt}{1.57141pt}{-2.84528pt}{0.0pt}\pgfsys@curveto{-2.84528pt}{-1.57141pt}{-1.57141pt}{-2.84528pt}{0.0pt}{-2.84528pt}\pgfsys@curveto{1.57141pt}{-2.84528pt}{2.84528pt}{-1.57141pt}{2.84528pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$ green light)
$\rightarrow\operatorname{\leavevmode\hbox to6.09pt{\vbox
to6.09pt{\pgfpicture\makeatletter\hbox{\hskip 3.04527pt\lower-3.04527pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{{{}} {}{}{}{}{}{}{}{}
}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.84528pt}{0.0pt}\pgfsys@curveto{2.84528pt}{1.57141pt}{1.57141pt}{2.84528pt}{0.0pt}{2.84528pt}\pgfsys@curveto{-1.57141pt}{2.84528pt}{-2.84528pt}{1.57141pt}{-2.84528pt}{0.0pt}\pgfsys@curveto{-2.84528pt}{-1.57141pt}{-1.57141pt}{-2.84528pt}{0.0pt}{-2.84528pt}\pgfsys@curveto{1.57141pt}{-2.84528pt}{2.84528pt}{-1.57141pt}{2.84528pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}(\operatorname{\lozenge}$
accelerate) ).

We collect a set of driving recordings and extract one frame per second from
the recordings. Then, we manually label each frame with driving operations
1-accelerate, 2-brake, or 0-no operation and construct a small-scale _Driving
Control Dataset_. We present some sample data from the dataset in Appendix B.

We apply the method to find recording clips that satisfy our selected traffic
rules. We have the set of symbols $L=\\{$ accelerate, brake, no operation,
pedestrian, stop sign, red light, green light $\\}$, where the first three
symbols are labels from the dataset, and the others are evaluated through the
VLM. An example of the frames from the dataset is presented in Figure 5, and
the corresponding constructed automaton is presented in Figure 6.

In this example, the probabilities of the three specifications being satisfied
are 100%, 73%, and 100%, respectively. Since this recording clip satisfies all
three specifications with probabilities greater than 0.5, we add this
recording clip to the search result. We can apply this procedure to search for
video clips from a long video, as presented in Appendix B.

### Quantitative Analysis over Realistic Datasets

#### Search over Privacy-Sensitive Videos.

Figure 7: Object detection results on the HMDB-51 dataset.

$0$$0.2$$0.4$$0.6$$0.8$$1$$0$$0.2$$0.4$$0.6$$0.8$$1$precision$\Phi_{1}^{P}$$\Phi_{2}^{P}$$\Phi_{3}^{P}$Ideal
Case

$0$$0.2$$0.4$$0.6$$0.8$$1$$0.2$$0.4$$0.6$$0.8$$1$probability returned by the
model checkerrecall$\Phi_{1}^{P}$$\Phi_{2}^{P}$$\Phi_{3}^{P}$Ideal Case

Figure 8: The top and bottom figures show the verification precision and
recall of verification results whose probabilities fall into each particular
range.

We apply the proposed method on a realistic video dataset HMDB-51 (Kuehne et
al. 2011) to verify the videos against several privacy rules and find all the
videos that violate any of the privacy rules. We evaluate the proposed method
in the metrics defined in Definition 2.

######  Definition 2.

Let $\Phi$ be an LTLfspecification, $N$ be the number of videos whose
verification probabilities returned by the model checker are between an
interval $[c_{1},c_{2})$, $T_{P}$ be the number of videos whose verification
probabilities are between $[c_{1},c_{2})$ that actually satisfy $\Phi$,
$T_{P}*$ be the number of videos whose verification probabilities are between
$[c_{1},1]$ that satisfy $\Phi$, $A_{P}$ be the total number of videos in the
dataset that satisfy $\Phi$, we define precision $P_{c}$ and recall $R_{c}$ as

$P_{c}=\frac{T_{P}}{N}$ and $R_{c}=\frac{T_{P}*}{A_{P}}$.

In the experiments, we equally divide the probabilities into 20 intervals:
$[0,0.05),[0.05,0.1),...,[0.9,0.95),[0.95,1]$.

In this setting, we obtain privacy annotations of the HMDB-51 dataset from PA-
HMDB51 (Wu et al. 2022), which include characters’ genders, races, etc., from
the videos. We use these annotations as the ground truth to compute the
accuracies.

As for the first step, we take some of the annotations from PA-HMDB51 as the
propositions and build a set of privacy rules by querying GPT-4:

⬇

1 Given the propositions: female, male, face, nude, black skin, white skin.

2 Transform the following rules into temporal logic formulas:

3 1. Never reveal gender.

4 2. Don’t show the faces of nude people.

5 3. Never reveal races.

We then transform these rules above into LTLfspecifications:

$\Phi_{1}^{P}=\operatorname{\square}(\neg\text{male }\land\neg$ female),

$\Phi_{2}^{P}=\operatorname{\square}$ (nude $\rightarrow\neg$ face),

$\Phi_{3}^{P}=\operatorname{\square}(\neg\text{black skin }\land\neg$ white
skin).

We extract all the frames from videos and apply the Grounded-SAM to detect
whether the objects described in the propositions appear in each frame. We
obtain the confidence scores from the Grounded-SAM and follow Algorithm 1 to
construct a probabilistic automaton for each video. The privacy annotations
from the dataset are static scenes. Hence, we only consider the detection
results from the VLMwhen constructing the automaton. Next, we use a
probabilistic model checker to compute the probability that each video
satisfies the LTLfspecifications. By doing so, we can efficiently find all
videos that violate any of the specifications, i.e., verification probability
below 50%.

We evaluate our verification results (probabilities) using the ground truth
privacy annotations from the dataset. We only select the following annotations
to avoid ambiguity: race-black, race-white, gender-female, gender-male,
gender-coexist, and nudity-semi-nudity. We evaluate the verification results
over the metrics in Definition 2. For each interval, we compute the precision
and recall, as presented in Figure 8. If we use 0.5 as the threshold to
determine whether we should add the video to the search result, the precision
is approximately 90%, and the recall is over 80%, indicating the reliability
of our verification results.

#### Search over Autonomous Driving Videos.

Figure 9: Examples of the object detection results on images from the NuScenes
Dataset. The top row shows the object detection results by the Grounded-SAM,
and the bottom row shows the annotated segments provided by the dataset.

$0$$0.2$$0.4$$0.6$$0.8$$1$$0$$0.2$$0.4$$0.6$$0.8$$1$precision$\Phi_{1}^{T}$$\Phi_{2}^{T}$$\Phi_{3}^{T}$Ideal
Case

$0$$0.2$$0.4$$0.6$$0.8$$1$$0.2$$0.4$$0.6$$0.8$$1$probability returned by the
model checkerrecall$\Phi_{1}^{T}$$\Phi_{2}^{T}$$\Phi_{3}^{T}$Ideal Case

Figure 10: The top and bottom figures show the verification precision and
recall of verification results whose probabilities fall into each range.

We use the proposed method to search videos that satisfy the provided
specifications within the NuScenes Dataset (Caesar et al. 2020). The NuScenes
Dataset consists of 93,000 images with annotations of objects. We group 10
images and consider them as frames for one video clip. Then, we want to search
for the video clips that satisfy our manually generated specifications:

$\Phi_{1}^{T}=\operatorname{\square}$ bicycle $\rightarrow$ human,

$\Phi_{2}^{T}=\operatorname{\square}$ truck
$\rightarrow(\operatorname{\lozenge}$ car),

$\Phi_{3}^{T}=\operatorname{\lozenge}$ car
$\land(\operatorname{\leavevmode\hbox to6.09pt{\vbox
to6.09pt{\pgfpicture\makeatletter\hbox{\hskip 3.04527pt\lower-3.04527pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{{{}} {}{}{}{}{}{}{}{}
}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.84528pt}{0.0pt}\pgfsys@curveto{2.84528pt}{1.57141pt}{1.57141pt}{2.84528pt}{0.0pt}{2.84528pt}\pgfsys@curveto{-1.57141pt}{2.84528pt}{-2.84528pt}{1.57141pt}{-2.84528pt}{0.0pt}\pgfsys@curveto{-2.84528pt}{-1.57141pt}{-1.57141pt}{-2.84528pt}{0.0pt}{-2.84528pt}\pgfsys@curveto{1.57141pt}{-2.84528pt}{2.84528pt}{-1.57141pt}{2.84528pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\neg$ human ).

From the specifications, we extract a set of propositions $\\{$ bicycle,
human, truck, car$\\}$. We apply the Grounded-SAM to detect objects described
by these propositions and follow Algorithm 1 to construct a probabilistic
automaton for each 10-frame video clip. Then, we use the probabilistic model
checker to compute the probabilities of each video clip satisfying each
specification. If a video satisfies all three specifications with a
probability above 50%, we extract it as one of the search results.

Since the dataset contains annotations of objects described by the
propositions, we take these annotations to evaluate our verification results.
We present both the object detection results and the annotations provided by
the dataset in Figure 9. We evaluate the probabilistic verification results
over the metrics in Definition 2. We indicate the reliability of the method in
Figure 10. The precision of verification results whose probabilities are
greater than 0.5 is around 95%, and the recall is above 80%. Although there
exist small gaps between the empirical results and the ideal case, these gaps
can be filled by the future development of VLMs.

## Conclusions

We design a method for efficient video search, which consists of an algorithm
that maps text-based event descriptions into LTLf formulas and an algorithm
for constructing a probabilistic automaton encoding the video information. We
calibrate the confidence and accuracy of the vision and language foundation
model and use the calibrated confidence as probabilities in the probabilistic
automaton. Hence, we can apply formal verification to compute the probability
that the automaton of each video satisfies the LTLf formulas. By doing so, we
can efficiently find all the videos that satisfy the event description with
formal guarantees, i.e., probabilities above a certain threshold. Due to the
limitation of the selected foundation model, our method only works for static
event descriptions. As a future direction, we can incorporate action
prediction models for searching dynamic events.

## References

  * Bai et al. (2019) Bai, X.; Xu, C.; Ao, Y.; Chen, B.; and Du, D. 2019.  Learning-based Probabilistic Modeling and Verifying Driver Behavior using MDP.  In Méry, D.; and Qin, S., eds., _International Symposium on Theoretical Aspects of Software Engineering_ , 152–159. IEEE.
  * Bertasius, Wang, and Torresani (2021) Bertasius, G.; Wang, H.; and Torresani, L. 2021.  Is Space-Time Attention All You Need for Video Understanding?  In Meila, M.; and Zhang, T., eds., _International Conference on Machine Learning_ , volume 139 of _Proceedings of Machine Learning Research_ , 813–824. PMLR.
  * Brown et al. (2020) Brown, T. B.; Mann, B.; Ryder, N.; Subbiah, M.; Kaplan, J.; Dhariwal, P.; Neelakantan, A.; Shyam, P.; Sastry, G.; Askell, A.; Agarwal, S.; Herbert-Voss, A.; Krueger, G.; Henighan, T.; Child, R.; Ramesh, A.; Ziegler, D. M.; Wu, J.; Winter, C.; Hesse, C.; Chen, M.; Sigler, E.; Litwin, M.; Gray, S.; Chess, B.; Clark, J.; Berner, C.; McCandlish, S.; Radford, A.; Sutskever, I.; and Amodei, D. 2020.  Language Models are Few-shot Learners.  _Advances in Neural Information Processing Systems_ , 33: 1877–1901.
  * Caesar et al. (2020) Caesar, H.; Bankiti, V.; Lang, A. H.; Vora, S.; Liong, V. E.; Xu, Q.; Krishnan, A.; Pan, Y.; Baldan, G.; and Beijbom, O. 2020.  nuScenes: A Multimodal Dataset for Autonomous Driving.  In _IEEE/CVF Conference on Computer Vision and Pattern Recognition_ , 11618–11628. Computer Vision Foundation / IEEE.
  * Chang et al. (1998) Chang, S.; Chen, W.; Meng, H. J.; Sundaram, H.; and Zhong, D. 1998.  A fully automated content-based video search engine supporting spatiotemporal queries.  _IEEE Trans. Circuits Syst. Video Technol._ , 8(5): 602–615.
  * Chang, Ma, and Smeulders (2007) Chang, S.; Ma, W.; and Smeulders, A. W. M. 2007.  Recent Advances and Challenges of Semantic Image/Video Search.  In _IEEE International Conference on Acoustics, Speech, and Signal Processing_ , 1205–1208. IEEE.
  * Chen et al. (2021) Chen, M.; Tworek, J.; Jun, H.; Yuan, Q.; Ponde, H.; Kaplan, J.; Edwards, H.; Burda, Y.; Joseph, N.; Brockman, G.; Ray, A.; Puri, R.; and et al. 2021.  Evaluating Large Language Models Trained on Code.  _ArXiv preprint arXiv:2107.03374_.
  * Deng, Yang, and Chen (2023) Deng, A.; Yang, T.; and Chen, C. 2023.  A Large-scale Study of Spatiotemporal Representation Learning with a New Benchmark on Action Recognition.  _arXiv preprint arXiv:2303.13505_.
  * Feichtenhofer et al. (2019) Feichtenhofer, C.; Fan, H.; Malik, J.; and He, K. 2019.  SlowFast Networks for Video Recognition.  In _IEEE/CVF International Conference on Computer Vision_ , 6201–6210. IEEE.
  * Gorelick et al. (2007) Gorelick, L.; Blank, M.; Shechtman, E.; Irani, M.; and Basri, R. 2007.  Actions as Space-Time Shapes.  _IEEE Trans. Pattern Anal. Mach. Intell._ , 29(12): 2247–2253.
  * Gu et al. (2022) Gu, X.; Lin, T.; Kuo, W.; and Cui, Y. 2022.  Open-vocabulary Object Detection via Vision and Language Knowledge Distillation.  In _International Conference on Learning Representations_. OpenReview.net.
  * Huang et al. (2020) Huang, Q.; Xiong, Y.; Rao, A.; Wang, J.; and Lin, D. 2020.  MovieNet: A Holistic Dataset for Movie Understanding.  In Vedaldi, A.; Bischof, H.; Brox, T.; and Frahm, J., eds., _European Conference on Computer Vision_ , volume 12349 of _Lecture Notes in Computer Science_ , 709–727. Springer.
  * Ji et al. (2020) Ji, J.; Krishna, R.; Fei-Fei, L.; and Niebles, J. C. 2020.  Action Genome: Actions As Compositions of Spatio-Temporal Scene Graphs.  In _IEEE Conference on Computer Vision and Pattern Recognition_ , 10233–10244. Computer Vision Foundation / IEEE.
  * Junges and Volk (2021) Junges, S.; and Volk, M. 2021.  Stormpy - Python bindings for Storm.
  * Kirillov et al. (2023) Kirillov, A.; Mintun, E.; Ravi, N.; Mao, H.; Rolland, C.; Gustafson, L.; Xiao, T.; Whitehead, S.; Berg, A. C.; Lo, W.-Y.; Dollár, P.; and Girshick, R. 2023\.  Segment Anything.  _arXiv preprint arXiv:2304.02643_.
  * Kuehne et al. (2011) Kuehne, H.; Jhuang, H.; Garrote, E.; Poggio, T. A.; and Serre, T. 2011.  HMDB: A large video database for human motion recognition.  In Metaxas, D. N.; Quan, L.; Sanfeliu, A.; and Gool, L. V., eds., _IEEE International Conference on Computer Vision_ , 2556–2563. IEEE Computer Society.
  * Li et al. (2022) Li, L. H.; Zhang, P.; Zhang, H.; Yang, J.; Li, C.; Zhong, Y.; Wang, L.; Yuan, L.; Zhang, L.; Hwang, J.; Chang, K.; and Gao, J. 2022.  Grounded Language-Image Pre-training.  In _Conference on Computer Vision and Pattern Recognition_ , 10955–10965. IEEE.
  * Li et al. (2019) Li, X.; Xu, C.; Yang, G.; Chen, Z.; and Dong, J. 2019.  W2VV++: Fully Deep Learning for Ad-hoc Video Search.  In Amsaleg, L.; Huet, B.; Larson, M. A.; Gravier, G.; Hung, H.; Ngo, C.; and Ooi, W. T., eds., _International Conference on Multimedia_ , 1786–1794. ACM.
  * Liu et al. (2023) Liu, S.; Zeng, Z.; Ren, T.; Li, F.; Zhang, H.; Yang, J.; Li, C.; Yang, J.; Su, H.; Zhu, J.; et al. 2023.  Grounding dino: Marrying dino with grounded pre-training for open-set object detection.  _arXiv preprint arXiv:2303.05499_.
  * Liu et al. (2021) Liu, Z.; Lin, Y.; Cao, Y.; Hu, H.; Wei, Y.; Zhang, Z.; Lin, S.; and Guo, B. 2021\.  Swin Transformer: Hierarchical Vision Transformer using Shifted Windows.  _arXiv preprint arXiv:2103.14030_.
  * Mavroudi, Haro, and Vidal (2020) Mavroudi, E.; Haro, B. B.; and Vidal, R. 2020.  Representation Learning on Visual-Symbolic Graphs for Video Understanding.  In _European Conference on Computer Vision_ , volume 12374 of _Lecture Notes in Computer Science_ , 71–90. Springer.
  * Nam and Han (2016) Nam, H.; and Han, B. 2016.  Learning Multi-domain Convolutional Neural Networks for Visual Tracking.  In _IEEE Conference on Computer Vision and Pattern Recognition_ , 4293–4302. IEEE Computer Society.
  * Narasimhan, Bhat, and Chinchali (2023) Narasimhan, S. S.; Bhat, S.; and Chinchali, S. P. 2023.  Safe Networked Robotics via Formal Verification.  _ArXiv preprint arXiv:2302.09182_.
  * OpenAI (2023) OpenAI. 2023.  GPT-4 Technical Report.  arXiv:2303.08774.
  * Porter, Mirmehdi, and Thomas (2001) Porter, S. V.; Mirmehdi, M.; and Thomas, B. T. 2001.  Detection and Classification of Shot Transitions.  In Cootes, T. F.; and Taylor, C. J., eds., _British Machine Vision Conference_ , 1–10. British Machine Vision Association.
  * Rabin (1963) Rabin, M. O. 1963.  Probabilistic Automata.  _Information and Control_ , 6(3): 230–245.
  * Radford et al. (2021) Radford, A.; Kim, J. W.; Hallacy, C.; Ramesh, A.; Goh, G.; Agarwal, S.; Sastry, G.; Askell, A.; Mishkin, P.; Clark, J.; Krueger, G.; and Sutskever, I. 2021.  Learning Transferable Visual Models From Natural Language Supervision.  In Meila, M.; and Zhang, T., eds., _International Conference on Machine Learning_ , volume 139 of _Proceedings of Machine Learning Research_ , 8748–8763.
  * Rai et al. (2021) Rai, N.; Chen, H.; Ji, J.; Desai, R.; Kozuka, K.; Ishizaka, S.; Adeli, E.; and Niebles, J. C. 2021.  Home Action Genome: Cooperative Compositional Action Understanding.  In _IEEE Conference on Computer Vision and Pattern Recognition_ , 11184–11193. Computer Vision Foundation / IEEE.
  * Redmon et al. (2016) Redmon, J.; Divvala, S. K.; Girshick, R. B.; and Farhadi, A. 2016.  You Only Look Once: Unified, Real-Time Object Detection.  In _Conference on Computer Vision and Pattern Recognition_ , 779–788. IEEE Computer Society.
  * Ren et al. (2017) Ren, S.; He, K.; Girshick, R. B.; and Sun, J. 2017.  Faster R-CNN: Towards Real-Time Object Detection with Region Proposal Networks.  _IEEE Transaction Pattern Analysis Machine Intelligence_ , 39(6): 1137–1149.
  * Rogers, Kovaleva, and Rumshisky (2020) Rogers, A.; Kovaleva, O.; and Rumshisky, A. 2020.  A Primer in BERTology: What We Know About How BERT Works.  _Transactions of the Association for Computational Linguistics_ , 8: 842–866.
  * Russakovsky et al. (2015) Russakovsky, O.; Deng, J.; Su, H.; Krause, J.; Satheesh, S.; Ma, S.; Huang, Z.; Karpathy, A.; Khosla, A.; Bernstein, M. S.; Berg, A. C.; and Fei-Fei, L. 2015\.  ImageNet Large Scale Visual Recognition Challenge.  _Int. J. Comput. Vis._ , 115(3): 211–252.
  * Sun et al. (2020) Sun, M.; Xiao, J.; Lim, E. G.; Zhang, B.; and Zhao, Y. 2020.  Fast Template Matching and Update for Video Object Tracking and Segmentation.  In _IEEE Conference on Computer Vision and Pattern Recognition_ , 10788–10796. Computer Vision Foundation / IEEE.
  * Tapaswi et al. (2016) Tapaswi, M.; Zhu, Y.; Stiefelhagen, R.; Torralba, A.; Urtasun, R.; and Fidler, S. 2016.  MovieQA: Understanding Stories in Movies through Question-Answering.  In _IEEE Conference on Computer Vision and Pattern Recognition_ , 4631–4640. IEEE Computer Society.
  * Tran et al. (2019) Tran, D.; Wang, H.; Feiszli, M.; and Torresani, L. 2019.  Video Classification With Channel-Separated Convolutional Networks.  In _IEEE/CVF International Conference on Computer Vision_ , 5551–5560. IEEE.
  * Umili, Capobianco, and De Giacomo (2022) Umili, E.; Capobianco, R.; and De Giacomo, G. 2022.  Grounding LTLf Specifications in Images.  In _Proceedings of the 16th International Workshop on Neural-Symbolic Learning and Reasoning_ , 45–63.
  * Wang et al. (2018) Wang, X.; Girshick, R. B.; Gupta, A.; and He, K. 2018.  Non-Local Neural Networks.  In _IEEE Conference on Computer Vision and Pattern Recognition_ , 7794–7803. Computer Vision Foundation / IEEE Computer Society.
  * Wu and Krähenbühl (2021) Wu, C.; and Krähenbühl, P. 2021.  Towards Long-Form Video Understanding.  In _IEEE Conference on Computer Vision and Pattern Recognition_ , 1884–1894. Computer Vision Foundation / IEEE.
  * Wu et al. (2022) Wu, Z.; Wang, H.; Wang, Z.; Jin, H.; and Wang, Z. 2022.  Privacy-Preserving Deep Action Recognition: An Adversarial Learning Framework and A New Dataset.  _IEEE Transactions on Pattern Analysis and Machine Intelligence_ , 44(4): 2126–2139.
  * Xiong et al. (2019) Xiong, Y.; Huang, Q.; Guo, L.; Zhou, H.; Zhou, B.; and Lin, D. 2019.  A Graph-Based Framework to Bridge Movies and Synopses.  In _IEEE/CVF International Conference on Computer Vision_ , 4591–4600. IEEE.
  * Yang et al. (2022) Yang, Y.; Gaglione, J.-R.; Neary, C.; and Topcu, U. 2022.  Automaton-Based Representations of Task Knowledge from Generative Language Models.  _arXiv preprint arXiv:2212.01944_.
  * Zhu et al. (2017) Zhu, S.; Tabajara, L. M.; Li, J.; Pu, G.; and Vardi, M. Y. 2017.  Symbolic LTLf Synthesis.  In Sierra, C., ed., _International Joint Conference on Artificial Intelligence_ , 1362–1369. ijcai.org.

##  Appendix A Additional Preliminaries

###  A.1 Probabilistic Verification

Probabilistic verification is a procedure of verifying a finite state machine
(e.g., probabilistic automaton) against some provided specifications and
returning a score indicating the probability of the specifications being
satisfied.

In practice, each trajectory from the probabilistic automaton is associated
with a probability and may or may not satisfy the specification. The model
checker sums up the probabilities of all the trajectories that satisfy the
specification and obtains a probability that the automaton satisfies the
specification.

We use the College Introductory Videos as an example: According to the
specification $\Phi$, we expect the label of every state in the trajectory to
be “faces = False.” Hence, there is only one trajectory in each automaton that
will satisfy $\Phi$, whose states only consist of the label “faces = False.”

Figure 11: Sample video frames and their labels from the Driving Control
Dataset.

$2$$4$$6$$8$$10$$0.4$$0.6$$0.8$$1$chunk numberprobability of satisfying
$\Phi$$\Phi_{2}$$\Phi_{3}$$\Phi_{1}$

Figure 12: Probability of each chunk of frames (30 frames) from the Driving
Control Dataset satisfying each of the provided specifications (traffic
rules). We record the probabilities of 10 chunks.

##  Appendix B Driving Control Dataset

We record a set of driving videos and extract one frame per second from the
videos. Then, we manually label each frame with driving operations
1-accelerate, 2-brake, or 0-no operation and construct a small-scale _Driving
Control Dataset_. Some examples are presented in Figure 11.

We verify the videos from the dataset against the following specifications:

$\Phi_{1}=\operatorname{\square}$ (pedestrian $\rightarrow$ brake),

$\Phi_{2}=\operatorname{\square}$ ((stop sign $\vee$ red light)
$\rightarrow\operatorname{\leavevmode\hbox to6.09pt{\vbox
to6.09pt{\pgfpicture\makeatletter\hbox{\hskip 3.04527pt\lower-3.04527pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{{{}} {}{}{}{}{}{}{}{}
}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.84528pt}{0.0pt}\pgfsys@curveto{2.84528pt}{1.57141pt}{1.57141pt}{2.84528pt}{0.0pt}{2.84528pt}\pgfsys@curveto{-1.57141pt}{2.84528pt}{-2.84528pt}{1.57141pt}{-2.84528pt}{0.0pt}\pgfsys@curveto{-2.84528pt}{-1.57141pt}{-1.57141pt}{-2.84528pt}{0.0pt}{-2.84528pt}\pgfsys@curveto{1.57141pt}{-2.84528pt}{2.84528pt}{-1.57141pt}{2.84528pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$ brake),

$\Phi_{3}=\operatorname{\square}$ ((red light
$\land\operatorname{\leavevmode\hbox to6.09pt{\vbox
to6.09pt{\pgfpicture\makeatletter\hbox{\hskip 3.04527pt\lower-3.04527pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{{{}} {}{}{}{}{}{}{}{}
}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.84528pt}{0.0pt}\pgfsys@curveto{2.84528pt}{1.57141pt}{1.57141pt}{2.84528pt}{0.0pt}{2.84528pt}\pgfsys@curveto{-1.57141pt}{2.84528pt}{-2.84528pt}{1.57141pt}{-2.84528pt}{0.0pt}\pgfsys@curveto{-2.84528pt}{-1.57141pt}{-1.57141pt}{-2.84528pt}{0.0pt}{-2.84528pt}\pgfsys@curveto{1.57141pt}{-2.84528pt}{2.84528pt}{-1.57141pt}{2.84528pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$ green light)
$\rightarrow\operatorname{\leavevmode\hbox to6.09pt{\vbox
to6.09pt{\pgfpicture\makeatletter\hbox{\hskip 3.04527pt\lower-3.04527pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{{{}} {}{}{}{}{}{}{}{}
}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.84528pt}{0.0pt}\pgfsys@curveto{2.84528pt}{1.57141pt}{1.57141pt}{2.84528pt}{0.0pt}{2.84528pt}\pgfsys@curveto{-1.57141pt}{2.84528pt}{-2.84528pt}{1.57141pt}{-2.84528pt}{0.0pt}\pgfsys@curveto{-2.84528pt}{-1.57141pt}{-1.57141pt}{-2.84528pt}{0.0pt}{-2.84528pt}\pgfsys@curveto{1.57141pt}{-2.84528pt}{2.84528pt}{-1.57141pt}{2.84528pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}(\operatorname{\lozenge}$
accelerate) ).

Our video search method can search for video clips that satisfy the
specifications within a long video. We select a five-minute driving video from
the Driving Control Dataset, which is presented as 300 frames. We further
divide them into ten half-minute chunks (each chunk has 30 frames) and verify
each chunk against the three specifications. We present verification results
in Figure 12. By doing so, we can search for video clips that satisfy the
specifications.

##  Appendix C Additional Results

###  C.1 Privacy Search on College Introductory Videos

Figure 13: Object detection results on the frames from college introductory
videos.
-startFFTFTFTF1.01.00.380.620.620.620.380.380.970.970.030.03-startFFFFF1.01.01.01.01.0-startTFTFT1.01.01.01.01.0
Figure 14: Automata corresponding to the frames of the videos in Figure 13.
‘T’ and ‘F’ in each state indicate the state’s label, either “faces = True” or
“faces = False.”

We collect a set of college introductory videos from YouTube and verify each
video against the following specifications:

$\Phi=\operatorname{\square}\neg faces$.

We break each video into frames with a frequency of one frame per second.
Next, we apply the Grounded-SAM object detection model to detect “faces” in
each frame and present the detection results in Figure 13. Then, we follow
Algorithm 1 to construct an automaton from the frames of each video, as
presented in Figure 14.

We apply the Stormpy model checker to verify each video against the
specification. From top to bottom, the automaton in Figure 14 satisfies the
specification with probabilities 0.007, 1.0, and 0, respectively. Among these
three videos, the second video is the only one to be added to the search
result.

###  C.2 Verification on Traffic Recordings

Figure 15: Object detection results on the frames of a manually recorded video
from a road intersection.
-startTTTTTFTTTTTFTFTTTTTTFTTT0.980.020.940.050.010.940.050.010.970.970.970.030.030.031.01.0
Figure 16: Automaton constructed from the frames in Figure 15. ‘T’ and ‘F’ in
each state indicate the “True” and “False” value of the corresponding label.
The three values correspond to “traffic light,” “road sign,” and “car,”
respectively. E.g., if a state is labeled as “TTF,” the label of this state is
“traffic light = True $\land$ road sign = True $\land$ car = False.”

We collect traffic recording videos, extract frames in a frequency of one
frame per second, and manually generate several rules regarding what may
happen in a traffic recording:

⬇

1 1. Never reveal any road signs.

2 2. At some point, simultaneously show a traffic light and a road sign.

3 3. There are cars after seeing the traffic light.

We transform the rules above into the following LTLfspecifications:

$\Phi_{1}=\operatorname{\square}\neg$ road sign,

$\Phi_{2}=\operatorname{\lozenge}$ traffic light $\land$ road sign,

$\Phi_{3}=\text{ traffic light }\rightarrow\operatorname{\leavevmode\hbox
to6.09pt{\vbox to6.09pt{\pgfpicture\makeatletter\hbox{\hskip
3.04527pt\lower-3.04527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{{{}} {}{}{}{}{}{}{}{}
}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.84528pt}{0.0pt}\pgfsys@curveto{2.84528pt}{1.57141pt}{1.57141pt}{2.84528pt}{0.0pt}{2.84528pt}\pgfsys@curveto{-1.57141pt}{2.84528pt}{-2.84528pt}{1.57141pt}{-2.84528pt}{0.0pt}\pgfsys@curveto{-2.84528pt}{-1.57141pt}{-1.57141pt}{-2.84528pt}{0.0pt}{-2.84528pt}\pgfsys@curveto{1.57141pt}{-2.84528pt}{2.84528pt}{-1.57141pt}{2.84528pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$ car.

The specification $\Phi_{3}$ consists of a NEXT operator. Since we need to
break the continuous timeline into discrete states to make the NEXT operation
meaningful, we manually define NEXT as the next frame in this experiment.

While obtaining the specifications, we also get the atomic propositions
$P=\\{\text{road sign, traffic light, car}\\}$. We break each recording video
into frames with a constant frequency of two frames per second. Then, we send
each frame and the propositions as the input to the Grounded-SAM and obtain
object detection results, as presented in Figure 15.

Given the object detection results with confidence scores and the estimated
mapping function, we construct a probabilistic automaton following Algorithm 1
and present it in Figure 16. Note that all the constructed automata have a set
of input symbols $\Sigma=\\{\epsilon\\}$. Then, we use the probabilistic model
checker to compute the probability of each specification being satisfied.

The probability of $\Phi_{1}$ being satisfied is 0, as all the trajectories
have to reach the acceptance state while the “road sign” is only evaluated to
be true in the acceptance state. The probability of $\Phi_{2}$ being satisfied
is 1, as all three propositions are evaluated to be true according to the
detection result of the last frame. The specification $\Phi_{3}$ is satisfied
with a probability of 1. The proposition “traffic light” is true according to
the third frame in Figure 15, and the proposition “road sign” is true
according to the fourth frame. We define the NEXT operation as the next frame.

$0$$0.2$$0.4$$0.6$$0.8$$1$$0$$0.5$$1$$1.5$Count (by thousand)Probability Count

$0$$0.2$$0.4$$0.6$$0.8$$1$$0.4$$0.6$$0.8$$1$probability returned by the model
checkerverification accuracy$\Phi_{1}^{P}$$\Phi_{2}^{P}$$\Phi_{3}^{P}$

Figure 17: The top figure shows the number count of verification results whose
probabilities fall into each particular range. The bottom figure shows the
accuracy of verification results within each range.

###  C.3 Search over Privacy-Sensitive Videos

In addition to the precision and recall in Definition 2, we present the video
search accuracy and number count of videos whose probability of satisfying the
specifications is between a particular range. We define _video search
accuracy_ as the follow:

######  Definition 3.

Let $\Phi$ be an LTLfspecification, $N$ be the number of videos whose
verification probabilities returned by the model checker are between an
interval $[c_{1},c_{2})$, $T_{P}$ be the number of videos whose verification
probabilities are between $[c_{1},c_{2})$ that actually satisfy $\Phi$, we
define video search accuracy $A_{V}$ as

$A_{V}=\begin{cases}\frac{N-T_{P}}{N}\text{ if }c_{2}\leq 0.5\\\
\frac{T_{P}}{N}\text{ if }c_{1}\geq 0.5.\end{cases}$

We present the number count and video search accuracies in Figure 17 and
denote $N$ as the _count_ in the figure.

We observe that most of the videos have verification probabilities close to 0
or 1. The video search accuracy is above 95 percent when the verification
probability is close to 0 or 1. And the accuracy reaches the lowest point
(lower than 40 percent) when the probability is 0.5. Overall, our search
method achieves above 90 percent accuracy over the privacy-annotated HMDB-51
dataset.

###  C.4 Search over Autonomous Driving Videos

$0$$0.2$$0.4$$0.6$$0.8$$1$$0$$0.1$$0.2$$0.3$$0.4$$0.5$Count (by
thousand)Probability Count

$0$$0.2$$0.4$$0.6$$0.8$$1$$0.4$$0.6$$0.8$$1$probability returned by the model
checkerverification accuracy$\Phi_{1}^{T}$$\Phi_{2}^{T}$$\Phi_{3}^{T}$

Figure 18: The top figure shows the number count of verification results whose
probabilities fall into each particular range. The bottom figure shows the
accuracy of verification results within each range.

We additionally present the number count and accuracy versus the verification
probability over the object-annotated autonomous driving dataset. We observe
that more verification results have probabilities close to 0 or 1, and fewer
results have probabilities in the middle. The search accuracy for the videos
with verification probability close to 0 or 1 is above 95 percent. However,
the search accuracy is lower than 50 percent when the verification probability
is approaching 0.5. In general, the overall search accuracy for the entire
dataset is approximately 90 percent, which indicates the reliability of our
video search method.