# Quantum projective measurements and the CHSH inequality in Isabelle/HOL

Mnacho Echenim and Mehdi Mhalla
Université Grenoble Alpes, Grenoble INP
CNRS, LIG, F-38000 Grenoble, France

(March 2021)

###### Abstract

We present a formalization in Isabelle/HOL of quantum projective measurements,
a class of measurements involving orthogonal projectors that is frequently
used in quantum computing. We also formalize the CHSH inequality, a result
that holds on arbitrary probability spaces, which can used to disprove the
existence of a local hidden-variable theory for quantum mechanics.

##  1 Introduction

One of the (many) counterintuitive aspects of quantum mechanics involves the
measurement postulates, which state that:

  * •

Measurements of equally prepared systems such as photons or electrons do not
always output the same value, which implies that it is only possible to make
statistical predictions on properties of these objects;

  * •

Once the measurement of an object has produced an outcome $\lambda$, all
subsequent measurements of the same object also produce the outcome $\lambda$,
a phenomenon known as the _collapse of the wave function_.

These postulates are now widely accepted, but this has not always been the
case, as evidenced by the well known EPR paradox, named after Einstein,
Podolsky and Rosen, in a paper published in 1935, suggesting that quantum
mechanics was an incomplete theory [10]. In their thought experiment, the
authors considered two entangled particles that are separated. When one of
them is measured, the collapse of the wave function guarantees that the
measure of the other particle will produce the same result. Because
instantaneous transmission of information is impossible, the authors viewed
this phenomenon as evidence that there existed hidden variables that
predetermined the measurement outcomes but were not accounted for by quantum
mechanics. The search for so-called _local hidden-variable theories_ for
quantum mechanics came to a halt in 1964 when Bell proved [3] that these
theories entailed upper-bounds on the correlations of measure outcomes of
entangled particles, and that these upper-bounds are violated by the
correlations predicted by quantum mechanics; a violation that has since then
been experimentally confirmed [1].

In this paper we present the formalization in Isabelle/HOL of _projective_
measurements, also known as von Neumann measurement, along with the related
notion of _observables_. Projective measurements involve complete sets of
orthogonal projectors that are used to compute the probabilities of
measurement outcomes and to determine the _state collapse_ after the
measurement. Although there are more general forms of measurements in quantum
mechanics, projective measurements are quite common: for example, textbooks on
quantum mechanics frequently mention “measuring a state in a given orthonormal
basis”; an operation that means performing a projective measurement with the
projectors on the elements of the orthonormal basis. These measurements are
especially used in quantum computing and quantum information, and are thus of
a particular interest to computer scientists.

Next we formalize the _CHSH inequality_ , named after Clauser, Horne, Shimony
and Holt [6]. This inequality involving expectations of random variables can
be used to prove Bell’s theorem that quantum mechanics cannot be formalized in
a probabilistic setting involving local hidden variables, thus showing the
intrinsically statistical nature of quantum mechanics.

#### Related work.

There are several lines of ongoing research on the use of formal tools for the
analysis of quantum algorithms and protocols, such as an extension of attack
trees with probabilities [13], or the development of dedicated quantum Hoare
logics [23, 15]. Approaches closer to ours involve the formalization of
quantum notions and algorithms in proof assistants including Coq [4, 19] and
Isabelle [5]. In this paper we extend the effort started in [5] in two ways.
First, our formalization is based on so-called _density operators_ rather than
pure quantum states. Although both notions are equivalent, density operators
are a more convenient way of representing quantum systems that are in a mixed
state, i.e., in one of several pure quantum states with associated
probabilities that sum to 1. They also permit to obtain more general and
natural statements on quantum mechanics. Second, although notions related to
measurements are formalized in [5], these are specific and in particular, only
involve measurements in the standard basis. We develop the full formalization
of projective measurements and observables in this paper. To the best of our
knowledge, no such formalization is available in any proof assistant.

Our formalization is available on the _Archive of Formal Proofs_ , at the
address https://www.isa-afp.org/entries/Projective_Measurements.html. It is
decomposed in three parts:  (i) A formalization of necessary notions from
Linear Algebra. We heavily rely on the results developed in [15], especially
those involving complex matrices and the decomposition of Hermitian matrices
for this part, as well as the _types-to-sets_ transfer tool [14] to use
general results on types in our setting.  (ii) The formalization of projective
measurements and their relationship to observables. In particular we show how
to construct a projective measurement starting from an observable and how to
recover the observable starting from the projective measurement.  (iii) The
formalization of the CHSH inequality. Along with the proof of the inequality
on an arbitrary probability space, we prove that assuming the existence of a
local hidden variable to explain the outcome of measurements leads to a
contradiction.

##  2 Preliminaries

We review the formalization of probability theory in Isabelle, as well as
basic notions from linear algebra and quantum mechanics. A more detailed
presentation on this last topic can be found in, e.g., [21, 17]. As we will
only formalize quantum notions in finite dimension, we present the standard
general definitions and illustrate them in the finite dimensional case.

###  2.1 Probability theory in Isabelle

We begin by briefly presenting the syntax of the interactive theorem prover
Isabelle/HOL; this tool can be downloaded at https://isabelle.in.tum.de/,
along with tutorials and documentations. Additional material on Isabelle can
be found in [18]. This prover is based on higher-order logic; terms are built
using types that can be:

  * •

simple types, denoted with the Greek letters $\alpha,\beta,\ldots$

  * •

types obtained from type constructors, represented in postfix notation (e.g.
the type $\alpha$ set denotes the type of sets containing elements of type
$\alpha$), or in infix notation (e.g., the type $\alpha\rightarrow\beta$
denotes the type of total functions from $\alpha$ to $\beta$).

Functions are curried, and function application is written without
parentheses. Anonymous functions are represented with the lambda notation: the
function $x\mapsto t$ is denoted by $\lambda x.\,t$. We will use mathematical
notations for standard terms; for example, the set of reals will be denoted by
$\mathbb{R}$ and the set of booleans by $\mathbb{B}$. The application of
function $f$ to argument $x$ may be written $f\ x$, $f(x)$ or $f_{x}$ for
readability.

A recent tool [14] permits to transfer type-based statements which hold on an
entire type universe to their set-based counterparts. This tool is
particularly useful to apply lemmata in contexts where the assumptions only
hold on a strict subset of the considered universe. For example generalized
summation over sets is defined for types that represent abelian semigroups
with a neutral element. Such an algebraic structure is straightforward to
define on any set of matrices that all have the same dimensions. In our
formalization, we define a _locale_ [2] for such a set of matrices in which
the number of rows and columns is fixed:

$\begin{array}[]{l}\textbf{locale}\ \texttt{fixed-carrier-mat}\ =\
\textbf{fixes}\ \texttt{fc-mats}\ \texttt{dimR}\ \texttt{dimC}\\\
\quad\textbf{assumes}\ \texttt{fc-mats}\ =\ \texttt{carrier-mat}\
\texttt{dimR}\ \texttt{dimC}\end{array}$

The set of matrices with $n$ rows and $m$ columns is represented in Isabelle
by $\texttt{carrier-mat}\ n\ m$, all matrices in fc-mats thus admit dimR rows
and dimC columns. After proving that fc-mats along with the standard addition
on matrices and the matrices with dimR rows and dimC columns consisting only
of zeroes is an abelian semigroup with a neutral element, we can define a
generalized summation of matrices on this locale:

$\begin{array}[]{lcl}\texttt{sum-mat}&::&(\alpha\rightarrow\beta\
\texttt{mat})\rightarrow\alpha\ \texttt{set}\ \rightarrow\beta\
\texttt{mat}\\\ \texttt{sum-mat}\ \mathcal{A}\ I&=&\texttt{sum-with}\ (+)\
\mathbf{0}\ \mathcal{A}\ I\end{array}$

The types-to-sets transfer tool then permits with no effort to transfer
theorems that hold on abelian semigroups, and especially those involving sums,
to this locale.

A large part of the formalization of measure and probability theory in
Isabelle was carried out in [12] and is included in Isabelle’s distribution.
We briefly recap some of the notions that will be used throughout the paper
and the way they are formalized in Isabelle. We assume the reader has
knowledge of fundamental concepts of measure and probability theory; any
missing notions can be found in [8] for example. Probability spaces are
particular _measure spaces_. A measure space over a set $\Omega$ consists of a
function $\mu$ that associates a nonnegative number or $+\infty$ to some
subsets of $\Omega$. The subsets of $\Omega$ that can be measured are closed
under complement and countable unions and make up a _$\sigma$ -algebra_. In
Isabelle the measure type with elements of type $\alpha$ is denoted by
$\alpha\ \texttt{measure}$.

A function between two measurable spaces is _measurable_ if the preimage of
every measurable set is measurable. In Isabelle, sets of measurable functions
are defined as follow:

$\begin{array}[]{lcl}\texttt{measurable}&::&\alpha\,\texttt{measure}\rightarrow\beta\,\texttt{measure}\rightarrow\left(\alpha\rightarrow\beta\right)\texttt{set}\\\
\texttt{measurable}\ \mathcal{M}\ \mathcal{N}\
\mu&=&\left\\{f:\Omega_{\mathcal{M}}\rightarrow\Omega_{\mathcal{N}}\,\middle|\>\forall
A\in\mathcal{A}_{\mathcal{N}}.\,f^{-1}(A)\cap\Omega_{\mathcal{M}}\in\mathcal{A}_{M}\right\\}\end{array}$

Measurable functions that map the elements of a measurable space into real
numbers, such as random variables which are defined below, are measurable on
Borel sets:

$\begin{array}[]{l}\textbf{abbreviation}\ \texttt{borel-measurable}\
\mathcal{M}\ \equiv\ \texttt{measurable}\ \mathcal{M}\
\texttt{borel}\end{array}$

Probability measures are measure spaces on which the measure of $\Omega$ is
finite and equal to $1$. In Isabelle, they are defined in a locale.

$\begin{array}[]{l}\textbf{locale}\ \texttt{prob-space}=\texttt{finite-
measure}\ +\textbf{assumes}\ \mu_{\mathcal{M}}(\Omega_{\mathcal{M}})\ =\
1\end{array}$

A _random variable_ on a probability space $\mathcal{M}$ is a measurable
function with domain $\Omega_{\mathcal{M}}$. The average value of a random
variable $f$ is called its _expectation_ , it is denoted by111The superscript
is omitted when there is no confusion. $\mathbb{E}^{\mathcal{M}}[f]$, and
defined by $\mathbb{E}^{\mathcal{M}}[f]\stackrel{{\scriptstyle\mbox{\tiny
def}}}{{=}}\int_{\Omega_{\mathcal{M}}}f\mathrm{d}\mu_{\mathcal{M}}$.

In what follows, we will consider properties that hold _almost surely_ (or
_almost everywhere_), i.e., are such that the elements for which they do not
hold reside within a set of measure $0$:

lemmaAE-iff $\displaystyle:$ $\displaystyle\ (\textsc{AE}_{\mathcal{M}}\,x.\
P\ x)$ $\displaystyle\Leftrightarrow(\exists
N\in\mathcal{A}_{\mathcal{M}}.\,\mu_{\mathcal{M}}(N)=0\wedge\left\\{x\,\middle|\>\neg
P\ x\right\\}\subseteq N)$

We will formalize results involving local hidden-variable hypotheses under the
more general assumption that properties hold almost everywhere, rather than on
the entire probability space under consideration.

###  2.2 On linear algebra

We recap the core notions from linear algebra that will be used in our
formalism. A more detailed treatment can be found, e.g., in [11]. A _Hilbert
space_ $\mathcal{H}$ is a complete vector space over the field of complex
numbers, equipped with an _inner product_
$\langle\cdot|\cdot\rangle:\mathcal{H}\times\mathcal{H}\rightarrow\mathbb{C}$,
i.e., a function such that for all $\varphi,\psi\in\mathcal{H}$,
$\langle\varphi|\psi\rangle=\overline{\langle\psi|\varphi\rangle}$,
$\langle\varphi|\varphi\rangle\geq 0$ and $\langle\varphi|\varphi\rangle=0$
iff $\varphi=\mathbf{0}$. The _norm_ induced by the inner product is defined
by $\left\lVert\varphi\right\rVert\stackrel{{\scriptstyle\mbox{\tiny
def}}}{{=}}\sqrt{\langle\varphi|\varphi\rangle}$, and $\varphi$ is
_normalized_ if $\left\lVert\varphi\right\rVert=1$. The elements of a Hilbert
space of dimension $n$ are represented as column vectors, and the inner
product of $\varphi$ and $\psi$ is
$\langle\varphi|\psi\rangle=\sum_{i=1}^{n}\overline{\varphi_{i}}\psi_{i}$.

An _operator_ is a linear map on a Hilbert space. We denote by $\mathbf{I}$
the identity operator; we may also write $\mathbf{I}_{n}$ to specify that the
considered Hilbert space is of dimension $n$. If $A$ is an operator on
$\mathcal{H}$, then the operator $B$ such that for all
$\varphi,\psi\in\mathcal{H}$, $\langle\varphi|A\psi\rangle=\langle
B\varphi|\psi\rangle$, is called the _adjoint of $A$_, and denoted by
$A^{\dagger}$. If $A=A^{\dagger}$ then we say that $A$ is _self-adjoint_ or
_Hermitian_ , and if $AA^{\dagger}=A^{\dagger}A=\mathbf{I}$, then we say that
$A$ is _unitary_. We identify operators with their matrix representation. The
set of complex matrices is represented in Isabelle by complex mat. For
convenience, we denote by $\mathbb{C}^{n\times m}$ the set of complex matrix
with $n$ rows and $m$ columns and by $\mathbf{0}_{n,m}$ the matrix in
$\mathbb{C}^{n\times m}$ containing only zeroes. When there is no ambiguity,
we will write $\mathbf{0}$ instead of $\mathbf{0}_{n,m}$. The adjoint of the
(square) matrix $A$ satisfies $(A^{\dagger})_{i,j}=\overline{A_{j,i}}$, and if
$A$ is self-adjoint then we say that $A$ is a _Hermitian matrix_. The _trace_
of a square matrix is the sum of its diagonal elements: if
$A\in\mathbb{C}^{n\times n}$ then $\mathrm{Tr}(A)=\sum_{i=1}^{n}A_{i,i}$. An
operator $A$ is a _projector_ if $A^{2}=A$, and $A$ is an _orthogonal
projection_ if $A^{\dagger}=A$. We say that $A$ is _positive_ if, for all
$\varphi\in\mathcal{H}$, we have $\langle\varphi|A\varphi\rangle\geq 0$.

We say that the vector $\varphi$ is an _eigenvector_ of operator $A$ is there
exists $\lambda\in\mathbb{C}$ such that $A\varphi=\lambda\varphi$. In this
case, we say that $\lambda$ is an _eigenvalue_ of $A$. The set of eigenvalues
of $A$ is called the _spectrum_ of $A$ and denoted by $\mathrm{spct}(A)$. When
$A$ is Hermitian, all its eigenvalues are necessarily real and it is possible
to associate every eigenvalue $\lambda\in\mathrm{spct}(A)$ with a projector
$P_{\lambda}$ such that

$P_{\lambda}\cdot P_{\lambda^{\prime}}=\mathbf{0}\ \text{if}\
\lambda\neq\lambda^{\prime},\
\sum_{\lambda\in\mathrm{spct}(A)}P_{\lambda}=\mathbf{I}\ \text{and}\ A\ =\
\sum_{\lambda\in\mathrm{spct}(A)}\lambda P_{\lambda}.$

The _tensor product_ of two vector spaces $U$ and $V$ is denoted by $U\otimes
V$. We also consider the tensor product of vectors $u\in U$ and $v\in V$, and
denote it by $u\otimes v$; similarly, for matrices $A$ and $B$, we denote by
$A\otimes B$ their tensor product. Two properties of interest in this context
are the following:

$\begin{array}[]{l}\textbf{lemma}\ \textsc{tensor-mat-hermitian}:\\\
\quad\textbf{assumes}\ A\in\texttt{carrier-mat}\ n\ n\ \textbf{and}\
B\in\texttt{carrier-mat}\ n^{\prime}\ n^{\prime}\\\ \quad\textbf{and}\ n>0\
\textbf{and}\ n^{\prime}>0\\\ \quad\textbf{and}\ \texttt{hermitian}\ A\
\textbf{and}\ \texttt{hermitian}\ B\\\ \textbf{shows}\ \texttt{hermitian}\
A\otimes B\vspace{0.5em}\\\ \textbf{lemma}\ \textsc{tensor-mat-unitary}:\\\
\quad\textbf{assumes}\ \texttt{dim-row}\ A>0\ \textbf{and}\ \texttt{dim-row}\
B>0\\\ \quad\textbf{and}\ \texttt{unitary}\ A\ \textbf{and}\ \texttt{unitary}\
B\\\ \textbf{shows}\ \texttt{unitary}\ A\otimes B\\\ \end{array}$

It is standard in quantum mechanics to represent the elements of $\mathcal{H}$
using the Dirac notation: these elements are called _ket-vectors_ , and are
denoted by $\left|u\right\rangle$. In what follows, we will represent the
tensor product $\left|u\right\rangle\otimes\left|v\right\rangle$ by
$\left|uv\right\rangle$. We also consider the dual notion of _bra-vectors_ ,
denoted by $\left\langle u\right|$. Formally, a bra-vector is the linear map
that maps the vector $\left|v\right\rangle$ to the complex number $\langle
u|v\rangle$. In the finite-dimensional setting, if

$\left|u\right\rangle=\begin{pmatrix}u_{1}\\\ u_{2}\\\ \vdots\\\
u_{n}\end{pmatrix}$

then $\left\langle
u\right|=(\overline{u_{1}},\overline{u_{2}},\ldots,\overline{u_{n}})$. We will
write $\left\langle uv\right|$ instead of $\left\langle
u\right|\otimes\left\langle v\right|$, and by a slight abuse of notation, we
will identify the application of $\left\langle u\right|$ to
$\left|v\right\rangle$ with the inner product $\langle u|v\rangle$. We define
the _outer product_ of two vectors, denoted by
$\left|u\right\rangle\\!\left\langle v\right|$, as the linear map such that,
for all $\left|v^{\prime}\right\rangle\in\mathcal{H}$,
$(\left|u\right\rangle\\!\left\langle
v\right|)\left|v^{\prime}\right\rangle=\left|u\right\rangle\cdot\langle
v|v^{\prime}\rangle=\langle v|v^{\prime}\rangle\cdot\left|u\right\rangle$. In
the finite-dimensional setting, this outer product is represented by the
matrix $M$, where $M_{i,j}=u_{i}\overline{v_{j}}$. When $\left|v\right\rangle$
is normalized, the outer product $\left|v\right\rangle\\!\left\langle
v\right|$ is called the _rank-1 projection on $v$_. It is in fact an
orthogonal projection with trace 1:

$\begin{array}[]{l}\textbf{lemma}\ \textsc{rank-1-proj-adjoint}:\\\
\textbf{shows}\ \texttt{adjoint}\ (\texttt{rank-1-proj}\ v)\
=\texttt{rank-1-proj}\ v\vspace{0.5em}\\\ \textbf{lemma}\ \textsc{rank-1-proj-
unitary}:\\\ \quad\textbf{assumes}\ \left\lVert v\right\rVert=1\\\
\textbf{shows}\ \texttt{projector}\ (\texttt{rank-1-proj}\ v)\vspace{0.5em}\\\
\textbf{lemma}\ \textsc{rank-1-proj-trace}:\\\ \quad\textbf{assumes}\
\left\lVert v\right\rVert=1\\\ \textbf{shows}\ \texttt{trace}\
(\texttt{rank-1-proj}\ v)\ =1\end{array}$

Many introductory textbooks on quantum computing present quantum postulates on
states, i.e., normalized vectors on the underlying Hilbert space. The more
general statement of these postulates involves so-called _density operators_ ,
which are represented by positive matrices of trace 1. This notion has already
been formalized in [15]:

$\begin{array}[]{lcl}\texttt{density-operator}&::&\texttt{complex
}\texttt{mat}\rightarrow\mathbb{B}\\\ \texttt{density-operator}\
\rho&\equiv&\texttt{positive}\ \rho\ \wedge\ \texttt{trace}\ \rho\
=1\end{array}$

######  Example 1.

Given a Hilbert space $\mathcal{H}$, consider a set of normalized vectors
$\left|u_{1}\right\rangle,\ldots\left|u_{n}\right\rangle$ and assume that for
$i\in[1,n]$, $p_{i}\geq 0$ and $\sum_{i=1}^{n}p_{i}=1$. Then

$\rho\ \stackrel{{\scriptstyle\mbox{\tiny def}}}{{=}}\
\sum_{i=1}^{n}p_{i}\left|u_{i}\right\rangle\\!\left\langle u_{i}\right|$

is a density operator (lemma rank-1-proj-sum-density). In quantum terminology,
when $n=1$, the matrix $\rho$ is referred to as a _pure state_ and otherwise,
to a _mixed state_.

A density operator that will be used in the formalization of the measurement
postulate is the so-called _maximally mixed state_. It is formalized as
follows in Isabelle:

$\begin{array}[]{lcl}\texttt{max-mix-
density}&::&\mathbb{N}\rightarrow\texttt{complex }\texttt{mat}\\\ \texttt{max-
mix-density}\ n&=&\frac{1}{n}\cdot\mathbf{I}_{n}\end{array}$

Intuitively, this density operator is the one with the maximal von Neumann
entropy; in other words, its spectrum admits the maximum Shannon entropy.

All the matrices we consider in what follows are nontrivial complex square
matrices, we thus define a locale to work in this context:

$\begin{array}[]{l}\textbf{locale}\ \texttt{cpx-sq-mat}\ =\ \texttt{fixed-
carrier-mat}\ (\texttt{fc-mats}::\texttt{complex }\texttt{mat}\
\texttt{set})\,+\\\ \quad\textbf{assumes}\ \texttt{dimR}=\texttt{dimC}\
\textbf{and}\ \texttt{dimR}>0\end{array}$

###  2.3 Quantum mechanics postulates

We present the postulates of quantum mechanics that are used in quantum
computation and information, following [17].

State postulate

Associated to an isolated physical system is a Hilbert space, which is
referred to as the _state space_. The system itself is completely described by
its density operator; we thus identify the state of a system with its density
operator.

Evolution postulate

The evolution of a closed quantum system is described by a unitary
transformation: the state $\rho$ at time $t$ of the system is related to the
state $\rho^{\prime}$ at time $t^{\prime}$ of the system by a unitary operator
$U\stackrel{{\scriptstyle\mbox{\tiny def}}}{{=}}U(t,t^{\prime})$, by the
equation $\rho^{\prime}=U\rho U^{\dagger}$.

Measurement postulate

Quantum measurements are described by collections of so-called _measurement
operators_. These collections are of the form
$\left\\{M_{\alpha}\,\middle|\>\alpha\in I\right\\}$, where $M_{\alpha}$ is
the matrix associated to the measurement outcome $\alpha$, and they satisfy
the completeness equation:

$\sum_{\alpha\in I}M_{\alpha}^{\dagger}M_{\alpha}\ =\ \mathbf{I}.$

When the state $\rho$ of a quantum system is measured with the collection
$\left\\{M_{\alpha}\,\middle|\>\alpha\in I\right\\}$, the probability that the
outcome $\alpha$ occurs is $\mathrm{Tr}(M_{\alpha}^{\dagger}M_{\alpha}\rho)$,
and the state after the measurement _collapses_ into

$\rho^{\prime}\ \stackrel{{\scriptstyle\mbox{\tiny def}}}{{=}}\
\frac{M_{\alpha}\rho
M_{\alpha}^{\dagger}}{\mathrm{Tr}(M_{\alpha}^{\dagger}M_{\alpha}\rho)}.$

Composite postulate

The state space of a composite physical system is the tensor product of the
state spaces of the component physical systems. If the system consists of $n$
individual systems and system $i$ is prepared in state $\rho_{i}$ for
$i\in[1,n]$, then the joint state of the composite system is
$\rho_{1}\otimes\rho_{2}\otimes\cdots\otimes\rho_{n}$.

######  Example 2.

The simplest quantum system is described by a two-dimensional Hilbert space.
It is standard to note an orthonormal basis for such a vector space as
$\left\\{\left|0\right\rangle,\left|1\right\rangle\right\\}$; the two elements
of this orthonormal basis are called the _computational basis states_. In the
density operator terminology, a _qubit_ is a state of the form
$\left|\varphi\right\rangle\\!\left\langle\varphi\right|$, where
$\left|\varphi\right\rangle=a\left|0\right\rangle+b\left|1\right\rangle$, for
some $a,b\in\mathbb{C}$ such that $\left|a\right|^{2}+\left|b\right|^{2}=1$.

In Section 4, we will consider composite systems involving two qubits.
Consider two physical systems $A$ and $B$, to which are associated the Hilbert
spaces $\mathcal{H}_{A}$ and $\mathcal{H}_{B}$. Although the state space of
the composite system consisting of $A$ and $B$ is simply
$\mathcal{H}_{A}\otimes\mathcal{H}_{B}$, properties of measurements involving
this composite system can be quite counterintuitive, because of the notion of
entanglement:

######  Definition 3.

A state $\rho$ is _separable_ if it can be written as

$\rho\ =\ \sum_{i=1}^{n}p_{i}\rho^{i}_{A}\otimes\rho^{i}_{B},$

where for $i\in[1,n]$, $0\leq p_{i}\leq 1$ and $\sum_{i=1}^{n}p_{i}=1$.
Otherwise, it is _entangled_. $\Diamond$

For systems involving two qubits, we have the _Bell states_ are examples of
entangled pure states:

$\displaystyle\left|\Phi^{+}\right\rangle$
$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny def}}}{{=}}$
$\displaystyle\frac{1}{\sqrt{2}}\left(\left|00\right\rangle+\left|11\right\rangle\right)$
$\displaystyle\left|\Phi^{-}\right\rangle$
$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny def}}}{{=}}$
$\displaystyle\frac{1}{\sqrt{2}}\left(\left|00\right\rangle-\left|11\right\rangle\right)$
$\displaystyle\left|\Psi^{+}\right\rangle$
$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny def}}}{{=}}$
$\displaystyle\frac{1}{\sqrt{2}}\left(\left|01\right\rangle+\left|10\right\rangle\right)$
$\displaystyle\left|\Psi^{-}\right\rangle$
$\displaystyle\stackrel{{\scriptstyle\mbox{\tiny def}}}{{=}}$
$\displaystyle\frac{1}{\sqrt{2}}\left(\left|01\right\rangle-\left|10\right\rangle\right)$

The Bell state $\left|\Psi^{-}\right\rangle$ will be used in Section 4 to
contradict the local hidden variable hypothesis.

##  3 Projective measurements

###  3.1 The projective measurement postulate

A notion related to collections of measurement operations is that of
_observables_. Intuitively, an observable represents a physically measurable
quantity of a quantum system, such as the spin of an electron or the
polarization of a photon. Formally, observables are represented by Hermitian
operators; this is the approach that was used by von Neumann in his axiomatic
treatment of quantum mechanics. This is why it is common to see the
Measurement postulate stated as follows:

Projective measurement postulate

A projective measurement is described by an observable, which is a Hermitian
operator $M$ on the state space of the observed system. The measurement
outcomes for an observable are its eigenvalues. Given the spectral
decomposition

$M\ =\ \sum_{\lambda\in\mathrm{spct}(M)}\lambda\cdot P_{\lambda},$

where $P_{\lambda}$ is the projector onto the eigenspace of $M$ with
eigenvalue $\lambda$, the probability of obtaining outcome $\lambda$ when
measuring the density operator $\rho$ is $\mathrm{Tr}(\rho P_{\lambda})$, and
the resulting state is

$\rho^{\prime}\ =\ \frac{P_{\lambda}\rho P_{\lambda}}{\mathrm{Tr}(\rho
P_{\lambda})}.$

Projective measurements are also known as von Neumann measurements. The
Projective measurement postulate can be derived from the Measurement
postulate. Indeed, using the fact that projectors are Hermitian, by the
spectral theorem we have

$\sum_{\lambda\in\mathrm{spct}(M)}P_{\lambda}^{\dagger}P_{\lambda}\ =\
\sum_{\lambda\in\mathrm{spct}(M)}{P_{\lambda}}^{2}\ =\
\sum_{\lambda\in\mathrm{spct}(M)}{P_{\lambda}}\ =\ \mathbf{I},$

and by invariance of traces under cyclic permutations, we have:

$\mathrm{Tr}(P_{\lambda}^{\dagger}P_{\lambda}\rho)\ =\
\mathrm{Tr}(P_{\lambda}^{2}\rho)\ =\ \mathrm{Tr}(P_{\lambda}\rho)\ =\
\mathrm{Tr}(\rho P_{\lambda}),$

so that

$\frac{P_{\lambda}\rho
P_{\lambda}^{\dagger}}{\mathrm{Tr}(P_{\lambda}^{\dagger}P_{\lambda}\rho)}\ =\
\frac{P_{\lambda}\rho P_{\lambda}}{\mathrm{Tr}(\rho P_{\lambda})}.$

Projective measurements could be formalized in many ways. We chose to stick
with a formalization that is as close as possible to the one used in [15] for
their quantum programs, for the sake of future reusability. We consider a
measure outcome as a couple $(\lambda,P_{\lambda})$, where $\lambda$
represents the output of the measure and $P_{\lambda}$ the associated
projector, and introduce a binary predicate that characterizes projective
measurements. The first parameter of this argument represents the number of
possible measure outcomes and the second parameter is the collection of
measure outcomes. We require that the values of the measure outcomes are
pairwise distinct, that the associated projectors have the correct dimensions
and are orthogonal projectors, that sum to the identity. For the sake of
readability, if $M_{i}=(\lambda,P_{\lambda})$ is a measure outcome, then we
denote $\lambda$ by $M_{i}^{\mathrm{v}}$ and $P_{\lambda}$ by
$M_{i}^{\mathrm{p}}$.

$\begin{array}[]{l}\textbf{type-synonym}\ \texttt{measure-outcome}\ =\
\mathbb{R}\times\texttt{complex }\texttt{mat}\end{array}$
$\begin{array}[]{lcl}\texttt{proj-
measurement}&::&\mathbb{N}\rightarrow(\mathbb{N}\rightarrow\texttt{measure-
outcome})\rightarrow\mathbb{B}\vspace{0.5em}\\\ \texttt{proj-measurement}\ n\
M&\Leftrightarrow&\texttt{inj-on}\ (\lambda i.\ M_{i}^{\mathrm{v}})\ \
[0,n-1]\ \wedge\\\ &&\forall j<n.\,M_{j}^{\mathrm{p}}\in\texttt{fc-
mats}\wedge\texttt{projector}\ M_{j}^{\mathrm{p}}\ \wedge\\\ &&\forall
i,j<n.\,i\neq j\Rightarrow M_{i}^{\mathrm{p}}\cdot
M_{j}^{\mathrm{p}}=\mathbf{0}\ \wedge\\\
&&\sum_{j=0}^{n-1}M_{j}^{\mathrm{p}}=\mathbf{I}\end{array}$

According to the projective measurement predicate, the probability of
obtaining result $\lambda$ when measuring the density operator $\rho$ is
$\mathrm{Tr}(\rho P_{\lambda})$. We prove that, although $\rho$ and
$P_{\lambda}$ are complex matrices, these traces are real positive numbers
that sum to 1.

$\begin{array}[]{lcl}\texttt{meas-outcome-prob}&::&\texttt{complex
}\texttt{mat}\rightarrow(\mathbb{N}\rightarrow\texttt{measure-
outcome})\rightarrow\\\ &&\quad\quad\mathbb{N}\rightarrow\mathbb{C}\\\
\texttt{meas-outcome-prob}\ \rho\ M\ i&=&\mathrm{Tr}(\rho\cdot
M_{i}^{\mathrm{p}})\end{array}$

$\begin{array}[]{l}\textbf{lemma}\ \textsc{meas-outcome-prob-real}:\\\
\quad\textbf{assumes}\ \rho\in\texttt{fc-mats}\ \textbf{and}\ \texttt{density-
operator}\ \rho\\\ \quad\textbf{and}\ \texttt{proj-measurement}\ n\ M\
\textbf{and}\ i<n\\\ \textbf{shows}\ \texttt{meas-outcome-prob}\ \rho\ M\
i\in\mathbb{R}\vspace{0.5em}\\\ \textbf{lemma}\ \textsc{meas-outcome-prob-
pos}:\\\ \quad\textbf{assumes}\ \rho\in\texttt{fc-mats}\ \textbf{and}\
\texttt{density-operator}\ \rho\\\ \quad\textbf{and}\ \texttt{proj-
measurement}\ n\ M\ \textbf{and}\ i<n\\\ \textbf{shows}\ \texttt{meas-outcome-
prob}\ \rho\ M\ i\geq 0\vspace{0.5em}\\\ \textbf{lemma}\ \textsc{meas-outcome-
prob-sum}:\\\ \quad\textbf{assumes}\ \rho\in\texttt{fc-mats}\ \textbf{and}\
\texttt{density-operator}\ \rho\\\ \quad\textbf{and}\ \texttt{proj-
measurement}\ n\ M\\\ \textbf{shows}\ \sum_{j=1}^{n-1}(\texttt{meas-outcome-
prob}\ \rho\ M\ j)=1\end{array}$

When the result of the measurement of $\rho$ is $\lambda$, $\rho$ collapses
into $\frac{P_{\lambda}\rho P_{\lambda}}{\mathrm{Tr}(\rho P_{\lambda})}$. When
formalizing this collapse in Isabelle, some care must be taken to handle the
case of results that occur with probability zero. Although such cases are
never meant to be analyzed when reasoning on quantum algorithms, it is still
necessary to provide a reasonable definition of the state $\rho$ collapses
into. We have chosen to make $\rho$ collapse into the maximally mixed state in
this case:

$\begin{array}[]{lcl}\texttt{density-collapse}&::&\texttt{complex
}\texttt{mat}\rightarrow\texttt{complex
}\texttt{mat}\rightarrow\texttt{complex }\texttt{mat}\\\ \texttt{density-
collapse}\ \rho\ P&=&\textbf{if}\ \mathrm{Tr}(\rho\cdot P)=0\ \textbf{then}\
\texttt{max-mix-density}\ \texttt{dimR}\\\
&&\quad\quad\quad\quad\quad\quad\quad\textbf{else}\ \frac{P\cdot\rho\cdot
P}{\mathrm{Tr}(\rho\cdot P)}\end{array}$

###  3.2 Projective measurements for observables

We develop the construction of a projective measurement for an observable,
i.e., a Hermitian matrix. This construction relies on the fact that a
Hermitian matrix $A$ can be decomposed as $A=U\cdot B\cdot U^{\dagger}$, where
$B$ is a diagonal matrix and $U$ is unitary. A construction of $B$ and $U$
based on the Schur decomposition theorem is available in Isabelle; this
theorem was developed in [22] and extended in [15]. The projective measurement
for $A$ is constructed using the fact that the spectrum of $A$ consists of the
diagonal elements of $B$, and because $U$ is unitary, its column vectors are
necessarily normalized and pairwise orthogonal. More specifically, assume
$A\in\mathbb{C}^{n\times n}$, let $D_{B}\stackrel{{\scriptstyle\mbox{\tiny
def}}}{{=}}\left\\{B_{i,i}\,\middle|\>i=1,\ldots,n\right\\}$ (represented by
$\texttt{diag-elems}\ B$ in our formalization), and let
$p\stackrel{{\scriptstyle\mbox{\tiny def}}}{{=}}\left|D_{B}\right|$
(represented by $\texttt{dist-el-card}\ B$ in our formalization). The number
$p$ represents the size of the spectrum of $A$; we let $\mathcal{C}$
(represented by $\texttt{diag-idx-to-el}\ B$ in our formalization) be a
bijection between $[0,p-1]$ and $D_{B}$, and $\mathcal{E}$ (represented by
$\texttt{diag-elem-indices}\ B$ in our formalization) associate to $\lambda\in
D_{B}$ the set $\left\\{i\leq n\,\middle|\>B_{i,i}=\lambda\right\\}$. Then the
set
$\left\\{\mathcal{E}\circ\mathcal{C}(0),\ldots,\mathcal{E}\circ\mathcal{C}(p-1)\right\\}$
is a partition of $[1,n]$ (lemmas diag-elem-indices-disjoint and diag-elem-
indices-union in our formalization). This partition is used, along with the
unitary matrix $U$, to construct projectors for the eigenspaces of $A$ as
follows. We define the function project-vecs which, for $i\in[0,p-1]$,
constructs the matrix

$P_{i}\stackrel{{\scriptstyle\mbox{\tiny
def}}}{{=}}\sum_{j\in\mathcal{E}\circ\mathcal{C}(i)}\left|U_{j}\right\rangle\\!\left\langle
U_{j}\right|,$

where $U_{j}$ denotes column $j$ of $U$. For $i\in[0,p-1]$, the function
$\texttt{mk-meas-outcome}\ i$ constructs the couple $(\mathcal{C}(i),P_{i})$.
We obtain the definition of the projective measurement associated to the
Hermitian matrix $A$ whose eigenvalues are represented by $\texttt{eigvals}\
A$:

$\begin{array}[]{lcl}\texttt{make-pm}&::&\texttt{complex
}\texttt{mat}\rightarrow\mathbb{N}\times(\mathbb{N}\rightarrow\texttt{measure-
outcome})\\\ \texttt{make-pm}\ A&=&\textbf{let}\ (B,U,\\_)=\texttt{unitary-
schur-decomposition}\ A\ (\texttt{eigvals}\ A)\\\ &&\textbf{in}\
(\texttt{dist-el-card}\ B,\ \texttt{mk-meas-outcome}\ B\ U)\end{array}$

The resulting couple represents a projective measurement, and the original
matrix can be recovered by summing the projectors scaled by the corresponding
eigenvalues:

$\begin{array}[]{l}\textbf{lemma}\ \textsc{make-pm-proj-measurement}:\\\
\quad\textbf{assumes}\ A\in\texttt{fc-mats}\ \textbf{and}\ \texttt{hermitian}\
A\\\ \quad\textbf{and}\ \texttt{make-pm}\ A=(n,M)\\\ \textbf{shows}\
\texttt{proj-measurement}\ n\ M\vspace{0.5em}\\\ \textbf{lemma}\ \textsc{make-
pm-sum}:\\\ \quad\textbf{assumes}\ A\in\texttt{fc-mats}\ \textbf{and}\
\texttt{hermitian}\ A\\\ \quad\textbf{and}\ \texttt{make-pm}\ A=(n,M)\\\
\textbf{shows}\ \sum_{i=0}^{n-1}M_{i}^{\mathrm{v}}\cdot
M_{i}^{\mathrm{p}}=A\end{array}$

##  4 The CHSH inequality

The fact that a physical system is in a superposition of states and that,
instead of revealing a pre-existing value, a measurement “brings the outcome
into being” (Mermin, [16]) was the cause of many controversies between the
pioneers of quantum mechanics. Famously, Einstein did not believe in the
intrinsically statistical nature of quantum mechanics. According to him,
quantum mechanics was an incomplete theory, and the postulates on
probabilistic measure outcomes actually reflected statistical outcomes of a
deterministic underlying theory (see [7, 20] for detailed considerations on
these controversies). The EPR paradox [10] was designed to evidence the
incompleteness of quantum mechanics. It involves two entangled and separated
particles which are sent in opposite directions. If one of the particles is
measured, then the outcome of the measurement of the other particle will be
known with certainty. For example, if the entangled system is represented by
the Bell state
$\left|\Phi^{+}\right\rangle=\frac{1}{\sqrt{2}}\left(\left|00\right\rangle+\left|11\right\rangle\right)$
and a measurement of the first particle returns $0$, then it is certain that a
measurement of the second one will also output $0$. This phenomenon is known
as _nonlocality_ , and it may leave the impression that information traveled
from the first to the second particle instantaneously, which would contradict
the theory of relativity222Since then, it has been proven that this phenomenon
is in no contradiction with the theory of relativity and does not imply
faster-than-light communication.. Einstein called this phenomenon “spooky
action at a distance”. A suggested solution to this phenomenon is that the
measurement outcomes are actually properties that existed before the
measurement was performed, and that deterministic underlying theories for
quantum mechanics should thus be developed. Efforts to develop such theories
are called _hidden-variable programs_. The theories that take into account the
fact that information cannot travel instantaneously, thus also requiring that
distant events are independent, are called _local hidden-variable theories_.

The fact that there can be no local hidden-variable underlying theory for
quantum mechanics was proved by Bell [3] who derived inequalities (the _Bell
inequalities_), that hold in a probabilistic setting, and showed that they are
violated by measurements in quantum mechanics. Recently, Aspect [1] showed
that this violation can be experimentally verified, even when taking
experimental errors into account, i.e., regardless of the possible outcomes of
the particles lost during the experiment.

In what follows we formalize probabilistic an inequality that is violated in
quantum mechanics: the _CHSH inequality_ , named after Clause, Horne, Shimony
and Holt [6]. This inequality is an upper-bound involving expectations of
products of random variables. It involves two parties, Alice and Bob, who each
receive and measure a particle that is part of an entangled system originating
from a common source. After repeating this operation a large number of times,
they can compute the frequencies of the different outcomes. These frequencies
are referred to as _correlations_ , or _joint probabilities_ , and denoted by
$\mathrm{p}(a,b\mid A,B)$, where $a$ and $b$ represent the outcomes and $A$
and $B$ represent the measuring devices used by Alice and Bob, respectively.
In the CHSH setting, Alice and Bob have two measuring devices each,
represented by the observables $A_{1}$ and $A_{2}$ for Alice, and $B_{1}$ and
$B_{2}$ for Bob. All observables have $\pm 1$ as eigenvalues. At each round,
Alice and Bob independently choose one measuring device; running the
experimental sufficiently many times permits to construct the expectation
values for observables $A_{i}$ and $B_{j}$, where
$\left\\{i,j\right\\}\subseteq\left\\{1,2\right\\}$:

$\mathrm{E}(A_{i},B_{j})\ \stackrel{{\scriptstyle\mbox{\tiny def}}}{{=}}\
\sum_{a,b=\pm 1}a\cdot b\cdot\mathrm{p}(a,b\mid A_{i},B_{j}).$

Consider the quantity

$\mathrm{E}(A_{1},B_{1})+\mathrm{E}(A_{1},B_{0})+\mathrm{E}(A_{0},B_{1})-\mathrm{E}(A_{0},B_{0}).$

As we will see, under the local hidden-variable assumption, this quantity
admits an upper-bound, but for a suitable choice of density operator and
observables, this upper-bound is violated; a violation that has been confirmed
experimentally [1].

Under the local hidden-variable assumption, the quantities
$\mathrm{E}(A_{i},B_{j})$ are expectations in a suitable probability space. We
prove the following inequality which holds in any probability space
$\mathcal{M}$, with relaxed conditions on the upper-bounds of random variables
compared to standard statements of the result, which are assumed to hold
almost everywhere rather than for all samples:

$\begin{array}[]{l}\textbf{lemma}\ \textsc{chsh-expect}:\\\
\quad\textbf{assumes}\ \textsc{AE}_{\mathcal{M}}\,x.\
\left|A_{0}(x)\right|\leq 1\ \textbf{and}\ \textsc{AE}_{\mathcal{M}}\,x.\
\left|A_{1}(x)\right|\leq 1\\\ \quad\textbf{and}\
\textsc{AE}_{\mathcal{M}}\,x.\ \left|B_{0}(x)\right|\leq 1\ \textbf{and}\
\textsc{AE}_{\mathcal{M}}\,x.\ \left|B_{1}(x)\right|\leq 1\\\
\quad\textbf{and}\ \texttt{integrable}\ \mathcal{M}\ (A_{0}\cdot B_{0})\\\
\quad\textbf{and}\ \texttt{integrable}\ \mathcal{M}\ (A_{0}\cdot B_{1})\\\
\quad\textbf{and}\ \texttt{integrable}\ \mathcal{M}\ (A_{1}\cdot B_{0})\\\
\quad\textbf{and}\ \texttt{integrable}\ \mathcal{M}\ (A_{1}\cdot B_{1})\\\
\textbf{shows}\ \left|\mathbb{E}[A_{1}\cdot B_{0}]+\mathbb{E}[A_{0}\cdot
B_{1}]+\mathbb{E}[A_{1}\cdot B_{1}]-\mathbb{E}[A_{0}\cdot B_{0}]\right|\leq
2\end{array}$

The local hidden-variable assumption on a system states that there exists a
probability space and independent random variables such that, when performing
simultaneous measurements on the system, the probabilities of the outcomes,
the values of which are given by the Measurement postulate, are expectations
in the probability space. This statement is often found in articles and
textbooks under the assumption that the probability space admits a
density333Including in the original paper on the CHSH inequality [6]., but it
is defined in our formalization in a more general case, where no assumption on
the existence of a density is made, and properties on the considered random
variables are assumed to hold almost everywhere rather than on the entire
probability space.

$\begin{array}[]{lcl}\texttt{pos-rv}&::&\alpha\
\texttt{measure}\rightarrow(\alpha\rightarrow\mathbb{R})\rightarrow\mathbb{B}\\\
\texttt{pos-rv}\ \mathcal{M}\ X&\equiv&X\in\texttt{borel-measurable}\
\mathcal{M}\ \wedge\ \textsc{AE}_{\mathcal{M}}\,x.\ X(x)\geq
0\vspace{0.5em}\\\ \texttt{prv-sum}&::&\alpha\
\texttt{measure}\rightarrow\texttt{complex
}\texttt{mat}\rightarrow(\mathbb{C}\rightarrow\alpha\rightarrow\mathbb{R})\rightarrow\mathbb{B}\\\
\texttt{prv-sum}\ \mathcal{M}\ A\
X&\equiv&\textsc{AE}_{\mathcal{M}}\,x.\sum_{a\in\mathrm{spct}(A)}X_{a}(x)=1\vspace{0.5em}\\\
\texttt{lhv}&::&\alpha\ \texttt{measure}\rightarrow\texttt{complex
}\texttt{mat}\rightarrow\\\ &&\quad\texttt{complex
}\texttt{mat}\rightarrow\texttt{complex }\texttt{mat}\rightarrow\\\
&&\quad(\mathbb{C}\rightarrow\alpha\rightarrow\mathbb{R})\rightarrow(\mathbb{C}\rightarrow\alpha\rightarrow\mathbb{R})\rightarrow\mathbb{B}\\\
\texttt{lhv}\ \mathcal{M}\ A\ B\ \rho\ X\ Y&\equiv&\texttt{prob-
space}\mathcal{M}\ \wedge\\\ &&\texttt{prv-sum}\ \mathcal{M}\ A\ X\ \wedge\
\texttt{prv-sum}\ \mathcal{M}\ B\ Y\ \wedge\\\ &&\forall
a\in\mathrm{spct}(A).\,\texttt{pos-rv}\ \mathcal{M}\ X_{a}\ \wedge\\\
&&\forall b\in\mathrm{spct}(B).\,\texttt{pos-rv}\ \mathcal{M}\ Y_{b}\
\wedge\\\ &&\forall a\in\mathrm{spct}(A).\,\forall b\in\mathrm{spct}(B).\\\
&&\quad(\texttt{integrable}\ \mathcal{M}\ (X_{a}\cdot Y_{b})\ \wedge\\\
&&\quad\mathbb{E}[X_{a}\cdot Y_{b}]=\mathrm{Tr}(P_{a}\cdot
P_{b}\cdot\rho))\end{array}$

The _quantum expectation value_ of a measurement represents the average value
of the projective measurement of an observable. In other words, given an
observable $A$, if the probability of obtaining result $a\in\mathrm{spct}(A)$
after a measurement of some state is $p_{a}$, then the expectation value of
$A$ is $\sum_{a\in\mathrm{spct}(A)}a\cdot p_{a}$. More generally, given a
density operator $\rho$ and an observable $A$, the (quantum) expectation value
of $A$ is

$\langle A\rangle_{\rho}\ \stackrel{{\scriptstyle\mbox{\tiny def}}}{{=}}\
\mathrm{Tr}(A\cdot\rho).$

Under the local hidden-variable hypothesis, when $X$ represents observable
$A$, we can define the random variable related to the expectation value of
$A$:

$\begin{array}[]{lcl}\texttt{qt-expect}&::&\texttt{complex
}\texttt{mat}\rightarrow(\mathbb{C}\rightarrow\alpha\rightarrow\mathbb{R})\rightarrow\alpha\rightarrow\mathbb{R}\\\
\texttt{qt-expect}\ A\ X&=&\left(\lambda x.\,\sum_{a\in\mathrm{spct}(A)}a\cdot
X_{a}(x)\right)\end{array}$

We obtain the following equality relating the expectation of the product of
random variables and the quantum expectation of the corresponding observables:

$\begin{array}[]{l}\textbf{lemma}\ \textsc{sum-qt-expect}:\\\
\quad\textbf{assumes}\ \texttt{lhv}\ \mathcal{M}\ A\ B\ \rho\ X\ Y\\\
\quad\textbf{and}\ A\in\texttt{fc-mats}\ \textbf{and}\ B\in\texttt{fc-mats}\
\textbf{and}\ \rho\in\texttt{fc-mats}\\\ \quad\textbf{and}\
\texttt{hermitian}\ A\ \textbf{and}\ \texttt{hermitian}\ B\\\ \textbf{shows}\
\mathbb{E}[(\texttt{qt-expect}\ A\ X)\cdot(\texttt{qt-expect}\ B\
Y)]=\mathrm{Tr}(A\cdot B\cdot\rho)\end{array}$

The goal becomes finding a suitable density operator and suitable observables
so that the combination of their traces violates the CHSH inequality. To this
purpose, we consider the density operator

$\rho_{C}\ \stackrel{{\scriptstyle\mbox{\tiny def}}}{{=}}\
\left|\Psi^{-}\right\rangle\\!\left\langle\Psi^{-}\right|,\ \text{where
}\left|\Psi^{-}\right\rangle\ =\
\frac{1}{\sqrt{2}}\left(\left|01\right\rangle-\left|10\right\rangle\right)\text{
is one of the Bell states}.$

We consider bipartite measurements of this entangled state. These measurements
involve the following observables:

$\begin{array}[]{rclcrcl}\texttt{Z}&\stackrel{{\scriptstyle\mbox{\tiny
def}}}{{=}}&\begin{pmatrix}1&0\\\
0&-1\end{pmatrix}&&\texttt{X}&\stackrel{{\scriptstyle\mbox{\tiny
def}}}{{=}}&\begin{pmatrix}0&1\\\ 1&0\end{pmatrix}\vspace{0.5em}\\\
\texttt{XpZ}&\stackrel{{\scriptstyle\mbox{\tiny
def}}}{{=}}&-\frac{1}{\sqrt{2}}(\texttt{X}+\texttt{Z})&&\texttt{ZmX}&\stackrel{{\scriptstyle\mbox{\tiny
def}}}{{=}}&\frac{1}{\sqrt{2}}(\texttt{Z}-\texttt{X})\end{array}$

These are all Hermitian matrices, and they are also unitary. The corresponding
separated measurements are represented by the following tensor products:

$\begin{array}[]{rclcrcl}\texttt{Z-I}&\stackrel{{\scriptstyle\mbox{\tiny
def}}}{{=}}&\texttt{Z}\otimes\mathbf{I}&&\texttt{X-I}&\stackrel{{\scriptstyle\mbox{\tiny
def}}}{{=}}&\texttt{X}\otimes\mathbf{I}\\\
\texttt{I-XpZ}&\stackrel{{\scriptstyle\mbox{\tiny
def}}}{{=}}&\mathbf{I}\otimes\texttt{XpZ}&&\texttt{I-ZmX}&\stackrel{{\scriptstyle\mbox{\tiny
def}}}{{=}}&\mathbf{I}\otimes\texttt{ZmX}\end{array}$

Under the local hidden-variable hypothesis, we can compute the following
expectations:

$\begin{array}[]{l}\textbf{lemma}\ \textsc{Z-I-XpZ-chsh}:\\\
\quad\textbf{assumes}\ \texttt{lhv}\ \mathcal{M}\ \texttt{Z-I}\
\texttt{I-XpZ}\ \rho\ V_{z}\ V_{p}\\\ \textbf{shows}\ \mathbb{E}[(\texttt{qt-
expect}\ \texttt{Z-I}\ V_{z})\cdot(\texttt{qt-expect}\ \texttt{I-XpZ}\
V_{p})]=\frac{1}{\sqrt{2}}\vspace{0.5em}\\\ \textbf{lemma}\ \textsc{X-I-XpZ-
chsh}:\\\ \quad\textbf{assumes}\ \texttt{lhv}\ \mathcal{M}\ \texttt{X-I}\
\texttt{I-XpZ}\ \rho\ V_{x}\ V_{p}\\\ \textbf{shows}\ \mathbb{E}[(\texttt{qt-
expect}\ \texttt{X-I}\ V_{x})\cdot(\texttt{qt-expect}\ \texttt{I-XpZ}\
V_{p})]=\frac{1}{\sqrt{2}}\vspace{0.5em}\\\ \textbf{lemma}\ \textsc{X-I-ZmX-
chsh}:\\\ \quad\textbf{assumes}\ \texttt{lhv}\ \mathcal{M}\ \texttt{X-I}\
\texttt{I-ZmX}\ \rho\ V_{x}\ V_{m}\\\ \textbf{shows}\ \mathbb{E}[(\texttt{qt-
expect}\ \texttt{X-I}\ V_{x})\cdot(\texttt{qt-expect}\ \texttt{I-ZmX}\
V_{m})]=\frac{1}{\sqrt{2}}\vspace{0.5em}\\\ \textbf{lemma}\ \textsc{Z-I-ZmX-
chsh}:\\\ \quad\textbf{assumes}\ \texttt{lhv}\ \mathcal{M}\ \texttt{Z-I}\
\texttt{I-ZmX}\ \rho\ V_{z}\ V_{m}\\\ \textbf{shows}\ \mathbb{E}[(\texttt{qt-
expect}\ \texttt{Z-I}\ V_{z})\cdot(\texttt{qt-expect}\ \texttt{I-ZmX}\
V_{m})]=-\frac{1}{\sqrt{2}}\end{array}$

Summing the first three expectation values and subtracting the last one
returns $2\sqrt{2}>2$, and the CHSH inequality is violated. We conclude that
the local hidden-variable assumption cannot hold:

$\begin{array}[]{l}\textbf{lemma}\ \textsc{no-lhv}:\\\ \quad\textbf{assumes}\
\texttt{lhv}\ \mathcal{M}\ \texttt{Z-I}\ \texttt{I-XpZ}\ \rho\ V_{z}\ V_{p}\\\
\quad\textbf{and}\ \texttt{lhv}\ \mathcal{M}\ \texttt{X-I}\ \texttt{I-XpZ}\
\rho\ V_{x}\ V_{p}\\\ \quad\textbf{and}\ \texttt{lhv}\ \mathcal{M}\
\texttt{X-I}\ \texttt{I-ZmX}\ \rho\ V_{x}\ V_{m}\\\ \quad\textbf{and}\
\texttt{lhv}\ \mathcal{M}\ \texttt{Z-I}\ \texttt{I-ZmX}\ \rho\ V_{z}\ V_{m}\\\
\textbf{shows}\ \text{False}\end{array}$

##  5 Conclusion

We have formalized the essential notion of quantum projective measurements and
the way they are obtained from observables. This formalization was carried out
in a setting that is as general as possible. For example, the local hidden-
variable hypothesis is formalized with as few conditions as possible and
contrarily to many textbooks, makes no assumption on the existence of a
density function on the underlying probability space. We also took care of
formalizing necessary notions in a way that should make them simple to reuse
in other formalizations. For instance, the way projective measurements are
defined is close to their usage in the quantum language used in [15], which
could permit to consider extensions of this language in which it is possible
to reason about measurement outcomes. This is a direction we are currently
exploring: to the best of our knowledge, there are currently no formalized
quantum languages that permit to perform probabilistic reasoning on quantum
algorithms. Yet, this form of reasoning is common in textbooks on quantum
mechanics, where it is obvious that if a large number of systems in the state
$\frac{1}{\sqrt{2}}(\left|0\right\rangle+\left|1\right\rangle)$ are measured
in the standard basis, then approximately half of the outputs will be equal to
0; a simple consequence of the Law of large numbers which is formalized in
Isabelle [9]. Although the CHSH inequality shows that it is not possible to
model quantum mechanics in a probabilistic setting, we are currently
investigating how to associate a probability space to a quantum algorithm, in
order to use the large corpus of results on measure theory that have already
been formalized in Isabelle for the subsequent reasoning tasks.

The CHSH inequality turned out to be difficult to formalize, because although
it is presented in a similar way in [17, 21], we were unable to find a
justification why their presentation entails the required result without
making an additional assumption on the relationship between expectations of
the random variables they consider and the quantum expectations of the related
measurements. This is why the treatment of the CHSH inequality that is
formalized in this paper is the one from [20], in which the local hidden-
variable formulation is the same as in the original paper [6]. This inequality
is also an important first step toward the formalization of _device-
independent_ quantum cryptography protocols; i.e., protocols that are
_unconditionally secure_ , even in the case where the devices used are noisy
or malicious. Indeed a key point of these protocols is the notion of _self-
testing_ , which guarantees that the verification of inequality violations
with classical interaction is enough to certify quantum properties that are
stronger than entanglement.

#### Acknowledgments.

The authors thank Stéphane Attal for his feedback on the relationship between
quantum and standard probabilities. This work benefited from the funding
_“Investissements d’avenir”_ (ANR-15-IDEX-02) program of the French National
Research Agency.

## References

  * [1] A. Aspect.  Experimental tests of Bell’s inequalities in atomic physics.  In I. Lindgren, A. Rosén, and S. Svanberg, editors, Atomic Physics 8, pages 103–128, Boston, MA, 1983. Springer US.
  * [2] C. Ballarin.  Locales: A module system for mathematical theories.  J. Autom. Reasoning, 52(2):123–153, 2014.
  * [3] J. S. Bell.  On the Einstein Podolsky Rosen paradox.  Physics, 1(3):195–200, 1964.
  * [4] J. Boender, F. Kammüller, and R. Nagarajan.  Formalization of quantum protocols using Coq.  Electronic Proceedings in Theoretical Computer Science, 195:71–83, Nov 2015.
  * [5] A. Bordg, H. Lachnitt, and Y. He.  Isabelle marries Dirac: a library for quantum computation and quantum information.  Journal of Automated Reasoning, 2020.
  * [6] J. F. Clauser, M. A. Horne, A. Shimony, and R. A. Holt.  Proposed Experiment to Test Local Hidden-Variable Theories.  Phys. Rev. Lett., 23(15):880–884, Oct. 1969.
  * [7] B. J. Dalton, B. M. Garraway, and M. D. Reid.  Tests for einstein-podolsky-rosen steering in two-mode systems of identical massive bosons.  Phys. Rev. A, 101:012117, Jan 2020.
  * [8] R. Durrett.  Probability : theory and examples.  The Wadsworth & Brooks/Cole statistics/probability series. Wadsworth Inc. Duxbury Press, Belmont, California, 1991.
  * [9] M. Eberl.  The laws of large numbers.  Archive of Formal Proofs, Feb. 2021.  https://isa-afp.org/entries/Laws_of_Large_Numbers.html, Formal proof development.
  * [10] A. Einstein, B. Podolsky, and N. Rosen.  Can quantum-mechanical description of physical reality be considered complete?  Phys. Rev., 47(10):777–780, May 1935.
  * [11] P. A. Fuhrmann.  Linear systems and operators in hilbert space.  Proceedings of the Edinburgh Mathematical Society, 26(1):113–114, 1983.
  * [12] J. Hölzl.  Construction and Stochastic Applications of Measure Spaces in Higher-Order Logic.  PhD thesis, Institut für Informatik, Technische Universität München, October 2012.
  * [13] F. Kammüller.  Attack trees in Isabelle extended with probabilities for quantum cryptography.  Comput. Secur., 87, 2019.
  * [14] O. Kuncar and A. Popescu.  From types to sets by local type definition in higher-order logic.  J. Autom. Reason., 62(2):237–260, 2019.
  * [15] J. Liu, B. Zhan, S. Wang, S. Ying, T. Liu, Y. Li, M. Ying, and N. Zhan.  Formal verification of quantum algorithms using Quantum Hoare Logic.  In I. Dillig and S. Tasiran, editors, Computer Aided Verification, pages 187–207. Springer International Publishing, 2019.
  * [16] N. D. Mermin.  Hidden variables and the two theorems of john bell.  Rev. Mod. Phys., 65:803–815, Jul 1993.
  * [17] M. A. Nielsen and I. L. Chuang.  Quantum Computation and Quantum Information: 10th Anniversary Edition.  Cambridge University Press, USA, 10th edition, 2011.
  * [18] T. Nipkow and G. Klein.  Concrete Semantics: With Isabelle/HOL.  Springer Publishing Company, Incorporated, 2014.
  * [19] R. Rand, J. Paykin, and S. Zdancewic.  Qwire practice: Formal verification of quantum circuits in Coq.  Electronic Proceedings in Theoretical Computer Science, 266:119–132, 02 2018.
  * [20] V. Scarani.  Bell Nonlocality.  Oxford Graduate Texts. Oxford University Press, 2019.
  * [21] W. Scherer.  Mathematics of Quantum Computing: An Introduction.  Springer International Publishing, 01 2019.
  * [22] R. Thiemann and A. Yamada.  Formalizing jordan normal forms in isabelle/hol.  In J. Avigad and A. Chlipala, editors, Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016, pages 88–99. ACM, 2016.
  * [23] D. Unruh.  Quantum relational hoare logic.  Proceedings of the ACM on Programming Languages, 3(POPL):1–31, Jan 2019.


# A Diffusion-based Data Generator for Training Object Recognition Models in
Ultra-Range Distance

Eran Bamani, Eden Nissinman, Lisa Koenigsberg, Inbar Meir and Avishai Sintov
E. Bamani, E. Nissinman, L. Koenigsberg, I. Meir and A. Sintov are with the
School of Mechanical Engineering, Tel-Aviv University, Israel. Corresponding
Author<EMAIL_ADDRESS>
(November 2023)

###### Abstract

Object recognition, commonly performed by a camera, is a fundamental
requirement for robots to complete complex tasks. Some tasks require
recognizing objects far from the robot’s camera. A challenging example is
Ultra-Range Gesture Recognition (URGR) in human-robot interaction where the
user exhibits directive gestures at a distance of up to 25 m from the robot.
However, training a model to recognize hardly visible objects located in
ultra-range requires an exhaustive collection of a significant amount of
labeled samples. The generation of synthetic training datasets is a recent
solution to the lack of real-world data, while unable to properly replicate
the realistic visual characteristics of distant objects in images. In this
letter, we propose the Diffusion in Ultra-Range (DUR) framework based on a
Diffusion model to generate labeled images of distant objects in various
scenes. The DUR generator receives a desired distance and class (e.g.,
gesture) and outputs a corresponding synthetic image. We apply DUR to train a
URGR model with directive gestures in which fine details of the gesturing hand
are challenging to distinguish. DUR is compared to other types of generative
models showcasing superiority both in fidelity and in recognition success rate
when training a URGR model. More importantly, training a DUR model on a
limited amount of real data and then using it to generate synthetic data for
training a URGR model outperforms directly training the URGR model on real
data. The synthetic-based URGR model is also demonstrated in gesture-based
direction of a ground robot.

##  I Introduction

Visual object recognition is essential for robots to interact effectively with
their environment. Image resolution degradation caused by the increased
distance between the robot and the object of interest can significantly hinder
recognition performance due to the loss of discriminative visual features [1].
Furthermore, cluttered backgrounds with numerous objects can pose a
significant challenge for accurate object identification algorithms [2].
Recognition in long distances is imperative in various other applications such
as surveillance [3], and the detection of drones [4], drowning scenarios [5]
and ships [6]. Particularly in robotics and Human-Robot Interaction (HRI),
gesture recognition from a large distance is required for a user to
efficiently convey natural directives to a robot.

Figure 1: Two examples of generating synthetic images in DUR with gesture and
distance conditions. Across 150 iterations, Gaussian noise is transformed into
a comprehensive high-fidelity image according to the desired labels.

While state-of-the-art in gesture recognition provides an effective distance
of up to seven meters and mostly indoor [7, 8, 9, 10, 11], recent work by the
authors have addressed the Ultra-Range Gesture Recognition (URGR) problem
demonstrating an effective distance of up to 25 meters in various indoor and
outdoor environments [12]. A central challenge in URGR, and in other ultra-
range object recognition problems, is the acquisition of data across varying
environmental conditions and distances, which is instrumental for feasible
model training. Constraints on data acquisition often originate from limited
time and human resources, insufficient equipment, or low variability in
environmental contexts.

Figure 2: Illustration of the Diffusion in Ultra-Range (DUR) framework. (a)
Dataset $\mathcal{D}$ for training DUR is acquired by collecting labeled RGB
images, cropping the user with YOLOv8, and improving image quality with HQ-
Net. (b) The generation of conditional synthetic samples starts with Gaussian
noise along with distance and gesture conditions. A non-Markovian diffusion
process denoises the noisy image and the ResNet filter removes failed images.

To effectively address these data acquisition challenges, a potential solution
emerged in the form of synthetic data generation [13]. The approach is based
on the simulation of data that closely resembles real-world samples. Some work
is based on a graphical simulator (e.g., Unity and Blender) [14, 15, 16, 17]
which, however, cannot provide sufficiently realistic images. Over the recent
years, numerous data-based techniques have arisen [18] including the prominent
Generative Adversarial Network (GAN) [19]. GAN has revolutionized the
landscape of artificial intelligence by introducing an intricate interplay
between a generative model and its discriminative counterpart. Consequently,
advanced versions of GAN were proposed such as Deep Convolutional GAN (DCGAN)
[20] and Progressive GAN [21]. Conditional GAN (CGAN) [22] is a relevant model
that can incorporate conditional variables, such as class labels, over the
generative process and thereby synthesizing specifically targeted data with
predefined attributes. In the context of object recognition, GAN variants have
been proposed to improve recognition in, for instance, low-quality images [23]
and strong lighting conditions [24]. In human gestures, several works used GAN
to augment the training data and improve recognition rates [25, 26, 27, 28,
29]. However, the approaches focus on close-range recognition where the
exerted gesture features are observable in high quality and quite easily
distinguishable.

While demonstrated efficacy in various applications, the training of GAN
requires substantial computational resources, extensive datasets, and long
training time [30]. In addition, the training of GANs may exhibit sensitivity
to hyperparameter selection, suffer from mode collapse, and demonstrate
reduced effectiveness in generating complex visual data, particularly for
objects viewed relatively far within the image [31]. To address these
challenges, diffusion models have recently been introduced and emerged as a
powerful tool for generative tasks [32]. Unlike GAN and other generative
methods, diffusion models are able to generate diverse high-quality data with
fewer stability issues [33]. In addition, they do not have a low-dimensional
latent space while modeling it as a random Gaussian distribution to maintain
the original image size. Diffusion models operate by iteratively adding noise
to data samples and then denoising them, thereby capturing the underlying data
distribution [34]. By simulating diffusion processes, intricate patterns
within the data are learned.

Due to their versatility and effectiveness, diffusion models are used in
various domains, including image denoising [35], super-resolution [36], and
inpainting [37]. Few attempts have used diffusion models in object detection
applications [38]. For instance, it was used to augment weed identification
[39]. In a different work, noisy bounding boxes on the image are denoised to
boxes on objects of interest [40]. Nevertheless, these applications do not
consider low-resolution images with specific importance to the detection of
small features. To the best of the authors’ knowledge, work is absent with
diffusion models for conditional and ultra-range image generation relevant to
object and gesture recognition. The inherent problem of generating synthetic
human gesture data across diverse environments is further challenged when
solely focusing on the distance variation from the viewpoint of the camera.

In this work, we address the generation of conditional synthetic images with
desired objects of interest located in the ultra range. Within this effort, we
propose a novel framework termed Diffusion in Ultra-Range (DUR). DUR is a
generator of conditional synthetic images that contain desired objects viewed
in ultra-range from the camera (Figure 1). Hence, the object in the synthetic
image is seen far from the viewpoint of the camera and in low quality, making
it difficult to identify fine details, as in the real-world case. DUR,
illustrated in Figure 2, is based on a Diffusion model and specifically on
non-Markovian Diffusion processes for enhanced performance [41]. With the DUR
generator, one can generate large-scale synthetic datasets for training ultra-
range object recognition models. As a test case, we explore the efficacy of
synthetic images generated by DUR, compared to real data, for training a URGR
model. In the URGR problem, the target object for recognition is small and
exhibits low-resolution characteristics, such as blurry hand features, within
a visually complex environment. This specific application presents a stringent
evaluation benchmark for the DUR generator’s capability to synthesize
realistic images suitable for training a robust object recognition model. The
key contributions of this work are:

  * •

We propose the novel DUR framework for generating synthetic and labeled
imagery datasets with objects of interest situated in an ultra-range distance
from the viewpoint of the camera.

  * •

As a rigorous test case, we show the ability of a DUR generator to synthesize
high-fidelity imagery data of individuals exhibiting directive gestures. The
generator offers control over two key conditions, allowing practitioners to
manipulate the model to produce images spanning distances from 4 to 25 meters,
across different gestures, environments, and human subjects.

  * •

A synthetic dataset of ultra-range gestures is used to train a URGR model,
exhibiting high performance compared to the same model trained with real data.

  * •

The trained URGR model is demonstrated in directing a ground robot.

  * •

The trained model and labeled dataset will be made available open-source for
the benefit of the community111The availability of the dataset and model will
be provided upon acceptance for publication, with images modified to safeguard
the privacy of participants..

##  II Methods

###  II-A Problem Formulation

For a robot to comprehend its environment, it is essential to train models
capable of recognizing objects across diverse and challenging environments,
and at varying distances in particular. Based on the URGR problem originally
presented by the authors [12], we define the general ultra-range object
recognition problem. Given an RGB image $\mathbf{x}_{i}$ taken while an object
is in a distance of $d\leq 25$ meters, it is required to classify the image
based on the exhibited object out of $m$ possible classes
$\\{\mathcal{O}_{1},\ldots,\mathcal{O}_{m}\\}$.

A significant challenge lies in generating a sufficient amount of reliable
data that can effectively generalize across different environments and
distances while accommodating the various object classes. To acquire accurate
recognition, a substantial amount of heterogeneous data is required, covering
different objects, poses, environments, camera angles and distances. However,
acquiring sufficient data may not be feasible due to limited resources and
time. Therefore, the objective of this work is to train a synthetic image
generator capable of generating diverse images in varied environments and
distances. In practice, the generator $\Theta(\mathcal{O}_{i},d)$ will output
a synthetic image exhibiting a desired object class $\mathcal{O}_{i}$ in
distance $d$. The ability to manipulate both the object classes and the
distance from which they are captured will provide the capacity for generating
a large amount of diverse training data. In this work, we specifically
evaluate a generator for the URGR problem where the distinction of finger
features during gesture is challenging.

###  II-B Data Collection

To train the generative gesture model, we collect a labeled dataset
$\mathcal{D}=\\{(\mathbf{x}_{i},o_{i},d_{i})\\}_{i=1}^{N}$. Each image
$\mathbf{x}_{i}$ in $\mathcal{D}$ is labeled with the gesture class index
$i\in\\{1,\ldots,m\\}$ and distance $d_{i}\in[4,25]$. Images are taken using a
simple web camera with several users in various environments. Particularly,
the dataset was acquired from diverse indoor and outdoor settings, with users
moving freely within the designated range while performing one of several
possible gestures. To have an image focused on the user, each image in the
dataset goes through pre-processing by detecting the user within it using
YOLOv8 and cropping out the background. When considering a general object
recognition problem, manual segmentation of the objects of interest would
replace the YOLO step. Since the cropped images are of low resolution, we
augment their quality with HQ-Net [12]. HQ-Net is a Super Resolution (SR)
method that uses a set of filters, self-attention mechanisms, and
convolutional layers to improve the compromised image fidelity of a distant
object in the image. The collection process is illustrated in Figure 2a.

###  II-C Diffusion models

The diffusion model is a fundamental technique for the generation of synthetic
images. An intricate interplay of diffusion processes contributes to the
creation of visually compelling and high-fidelity images. Unlike GAN, the
diffusion model excels in generating diverse and high-quality data. We briefly
discuss the fundamentals of the Denoising Diffusion Probabilistic Model (DDPM)
while an in-depth presentation can be reviewed in [35].

The DDPM captures information spread over time and space by gradually
introducing and then reversing noise in the data. Hence, DDPM encompasses two
processes where, in the first, a training image is destroyed by iteratively
adding noise over time, making it progressively less recognizable until it
transforms into pure noise. In the second process, the noising process is
reversed. The reverse process converts the complex distribution back to a
simple distribution using inverse transformations. Hence, the generation of a
synthetic image can be done by randomly sampling noise and passing it through
the reverse process.

The forward process can be considered as a Markov chain. An image is sampled
from the real data distribution $\mathbf{x}_{0}\sim q(\mathbf{x})$ and
corrupted by gradually adding Gaussian noise for $T$ steps yielding a sequence
of noisy samples $\mathbf{x}_{1},\ldots,\mathbf{x}_{T}$. Let
$\\{\beta_{t}\in(0,1)\\}_{t=1}^{T}$ be a sequence of learned or fixed variance
schedules regulating the noise level, the forward process is given by

$p(\mathbf{x}_{1:T}|\mathbf{x}_{0})=\prod^{T}_{t=1}p(\mathbf{x}_{t}|\mathbf{x}_{t-1})$
(1)

where

$p(\mathbf{x}_{t}|\mathbf{x}_{t-1})=\mathcal{N}(\mathbf{x}_{t};~{}\mathbf{x}_{t-1}\sqrt{1-\beta_{t}},\beta_{t}\mathbf{I}).$
(2)

In the reversed process, a noise sample
$\mathbf{x}_{T}\sim\mathcal{N}(0,\mathbf{I})$ is used to recreate an image
from the original distribution. However, an inverse probability map
$p(\mathbf{x}_{t-1}|\mathbf{x}_{t})$ is not available. Hence, a model
$p_{\theta}$ is learned to approximate the conditional probabilities as

$p_{\theta}(\mathbf{x}_{t-1}|\mathbf{x}_{t})=\mathcal{N}(\mathbf{x}_{t-1};~{}\mu_{\theta}(\mathbf{x}_{t},t),\Sigma_{\theta}(\mathbf{x}_{t},t))$
(3)

where $\mu_{\theta}$ and $\Sigma_{\theta}$ are time-dependent mean and
variance parameters of the Gaussian transition from $\mathbf{x}_{t}$ to
$\mathbf{x}_{t-1}$. While the variance is usually chosen to be
$\Sigma_{\theta}(\mathbf{x}_{t},t)=\beta_{t}\mathbf{I}$, the diffusion
posterior mean $\mu_{\theta}(\mathbf{x}_{t},t)$ is implemented using a neural
network model which is required to have equal dimensionality at both input and
output.

While Markovian diffusion models provide high generative capabilities,
sampling a synthetic image tends to be significantly slow in the reverse
process over thousands of iteration steps $T$. Hence, the Denoising Diffusion
Implicit Model (DDIM) model was proposed where a non-Markovian process is
considered [41]. In such case, the recovery iteration step in (2) is
reformulated to

$p_{\theta}(\mathbf{x}_{t-1}|\mathbf{x}_{t},\mathbf{x}_{0})=\mathcal{N}(\mathbf{x}_{t-1};~{}\tilde{\mu}_{\theta}(\mathbf{x}_{t},\mathbf{x}_{0}),\beta_{t}\mathbf{I})$
(4)

where $\tilde{\mu}_{\theta}(\mathbf{x}_{t},\mathbf{x}_{0})$ is learned using a
neural network. Such a formulation has been shown to provide high-quality
synthetic images in a faster time and provides deterministic synthesis.

The neural networks of both DDPM and DDIM are commonly based on the U-Net
architecture [42]. U-Net is trained to reverse the Markov transitions in the
forward process to maximize the likelihood of the training data. By leveraging
the U-Net architecture in the reverse process, the diffusion model can
effectively reconstruct high-fidelity images from the noise sequences
generated during the forward process. This integration highlights the synergy
between advanced neural network architectures and probabilistic models,
leading to robust and reliable image generation techniques.

###  II-D DUR framework

To synthesize labeled data for training a gesture recognition model in ultra-
range, we propose the Diffusion in Ultra-Range (DUR) framework illustrated in
Figure 2b. The framework uses the DDIM to generate conditional synthetic
images and a ResNet-based model [43] as an image quality control module. To
learn the transition component of DDIM in (4), the U-Net architecture was
used. The unique architecture of U-Net is characterized by a contracting path
followed by an expansive path. During the expansive path, high-resolution
features are gradually restored by combining information from multiple scales,
enabling the network to recover fine details lost during the diffusion
process. Furthermore, skip connections enable the direct flow of information
from the contracting path to the expansive path aiding in preserving spatial
information and ensuring precise reconstruction. This mechanism is
particularly beneficial in the reverse process of the diffusion model, where
the goal is to faithfully reconstruct an image from the noise-corrupted
version.

The U-Net in DUR incorporates temporal encoding to generate accurate outputs
corresponding to specific time points in the diffusion process. This temporal
information is fed into the U-Net as a condition through sinusoidal positional
embedding. To constrain the model to generate images of desired classes and
distances, two additional conditions, e.g., gesture and distance, are added to
the time embedding. Hence, the input to the U-Net is an embedding of the data

$u_{emb}=\mathbf{x}_{emb}+o_{emb}+d_{emb}$ (5)

where $o_{emb}$ and $d_{emb}$ are the vector embeddings of the class and
distance conditions, respectively. These are added to $\mathbf{x}_{emb}$, a
down-sampled embedding of the noise image
$\mathbf{x}_{T}\sim\mathcal{N}(0,\mathbf{I})$. The sampling process of images
is required to be of low temperature. In other words, the probability of
sampling an image not in the desired class will be low in a rather
deterministic process. Hence, we employ the Classifier-Free Diffusion Guidance
(CFDG) [44]. The guidance enhances learning and improves sample quality.

With this diffusion formulation, one can generate high-fidelity and realistic
images while enforcing a desired gesture and user distance from the camera, as
seen in Figure 1. However, preliminary observations of the outputted images
from the diffusion model have revealed that some portions are partly
unrealistic or distorted. For instance, the user may be generated without a
limb or smeared. Examples of such images can be seen in Figure 3. Hence, the
DUR framework includes an image quality control model used to filter low-
quality images. A systematic evaluation of image quality is conducted to
optimize the results of the generative process. After training the DDIM, $K$
synthetic images are generated. Then, they are manually labeled as successful
or failed ones. An image is labeled as failed if the structural integrity of
the user in the image is distorted or missing. With the labeled images, we
train a 32-layer ResNet with embedding to recognize successful and failed
images. The trained ResNet is then a filter for unfit images generated by the
DDIM. Hence, it is used to mitigate low-quality data, such as images depicting
only partial body parts, diminished image quality, smoothing effects and other
complexities.

Figure 3: Examples of failed synthetic images generated by DUR.

##  III Model Evaluation

In this section, we evaluate the proposed DUR framework for generating
conditional synthetic data and using them for training URGR models. Our
analysis focuses on six distinct gesture classes that can be used to direct a
robot: pointing, thumbs-up, thumbs-down, beckoning, stop and null, observed
across a range extending from 4 to 25 meters. Null is the lack of an exhibited
gesture where the user can perform any other task. We next analyze the quality
of the generated images in DUR followed by assessing their usage in training
gesture recognition models. All computations were performed on a Linux Ubuntu
(18.04 LTS) machine with an Intel Xeon Gold 6230R CPU (consisting of 20 cores
operating at 2.1GHz) and four NVIDIA GeForce RTX 2080TI GPUs, each endowed
with 11GB of RAM.

###  III-A Dataset

Dataset $\mathcal{D}$ of real images with gesture and distance labels was
obtained using eight users of diverse ages and genders. The users alternately
executed different gestures out of the six in various in-door and out-door
environments. The exhibited gesture can be performed with either the right or
left arm. In addition, the data was collected in a nearly uniform distribution
along the $d\in[4,25]$ meters distance range. Image acquisition involved a web
camera producing images sized at $480\times 640$ pixels. The collection
yielded $N=175,000$ labeled samples with approximately 29,105 samples per
gesture. Furthermore, a separate test set comprising 5,821 labeled images was
gathered from 16 users not included in the training process and in different
environments.

###  III-B Synthetic image quality

Using dataset $\mathcal{D}$, the DUR framework is trained. We first analyze
the quality and realistic characteristics of the synthetic images from DUR
compared to synthetic images from other generative models. Our comparison
includes CGAN, Auxiliary Classifier GAN [45], DCGAN and Progressive GAN. While
CGAN and ACGAN can handle conditioning of the generated images, DCGAN and
Progressive GAN were modified to align with the specific input conditions of
gestures and distances. In brief, both the generators and discriminators of
these two GAN’s were added an input of the gesture class and distance. We also
compare to DUR without filtering out failed images with the ResNet model. The
ResNet was trained with $K=16,800$ manually labeled images.

All GAN models were trained with the same data in $\mathcal{D}$. Then, each
model, including DUR, generated a set of synthetic images with an amount equal
to the size of the test set. We evaluate the quality of the synthetic images,
some with respect to the test data, using three metrics: Inception Score (IS)
[46], Fréchet Inception Distance (FID) [47] and Structural Similarity Index
(SSIM) [48]. IS evaluates the quality of synthetic images and considers both
the variety and distinctiveness of the generated images, with a higher score
indicating more realistic and diverse outputs. On the other hand, FID is a
common pixel-level metric of domain adaptation that compares the statistical
features of real and generated images without requiring paired image datasets.
A lower FID score indicates that the generated images better capture the
complexity and realism of the real data. Similarly, SSIM does not require
paired images and evaluates how similar two images are in terms of luminance,
contrast, and structure, aiming to reflect how humans perceive the difference.
Hence, a score closer to 1 indicates high similarity. Table I summarizes the
comparative results for all generative models and metrics. DUR is shown to be
significantly superior compared to all GAN models across all metrics. In
addition, ResNet is validated to considerably improve the quality of synthetic
images in the DUR framework. Figure 4 provides a visual comparison of
synthetic image examples generated by the above generative models. The
examples show that DUR provides the most realistic and physically accurate
samples.

TABLE I: Comparative quality evaluation of generative models Models |  | IS | FID | SSIM
---|---|---|---|---
CGAN | [22] | 6.41 | 28.46 | 0.671
ACGAN | [45] | 7.13 | 25.91 | 0.711
DCGAN | [20] | 5.92 | 31.28 | 0.543
Progressive GAN | [21] | 7.86 | 26.26 | 0.698
DUR w/o ResNet |  | 8.07 | 25.31 | 0.745
DUR |  | 9.47 | 20.05 | 0.907
Figure 4: Visual comparison of synthetic image examples across several
generative models, including DUR, and for the trained gesture classes.

###  III-C Usage for Gesture Recognition

The effectiveness of synthetic images is next evaluated for training a gesture
recognition model. We base our analysis on GViT previously proposed by the
authors for URGR [12]. GViT combines the merits of two different models: Graph
Convolutional Network (GCN) [49] and Vision Transformer (ViT) [50]. This
allows effective analysis of both the visual features of gestures captured by
a camera and the relationships between different parts of the hand or body
involved in the gesture, even at extended distances. Since a user is observed
from a far distance, the captured image is of low resolution. Hence, the image
goes through the super-resolution HQ-Net model for quality enhancement before
recognition with GViT.

First, GViT was trained with 175,000 real images from $\mathcal{D}$ as done in
[12]. In addition, for DUR and for each of the GAN models discussed in Section
III-B, we generated a dataset of 175,000 labeled synthetic images. The
datasets have a uniform distribution of sampled gestures and distances. A GViT
model was trained with each dataset and evaluated on a real test set of 10,109
labeled images originating from the work in [12] and independent of any
training data. Table II presents the recognition success rate for the GViT
models trained with the different sources of labeled data. The success rate
for each model is averaged over five training trials. The results show that
all generative models provide better recognition accuracy compared to a model
with real data. This highlights the merit of investing real collected data in
a generative model, compared to directly using the data for training the URGR
model. Among the generative models, DUR provides a superior recognition
success rate by a significant margin. Figure 5 demonstrates several correct
gesture recognitions with GViT trained on synthetic data from DUR.

TABLE II: Gesture recognition success rate using GViT trained with synthetic data from different generative models Training data source |  | Success rate (%)
---|---|---
Directly w/ real data | [12] | 58.8 $\pm$ 8.30
CGAN | [22] | 78.3 $\pm$ 4.82
ACGAN | [45] | 83.8 $\pm$ 5.03
DCGAN | [20] | 64.7 $\pm$ 5.71
Progressive GAN | [21] | 81.4 $\pm$ 3.48
DUR |  | 95.8 $\pm$ 4.01
|  |  |  |  |
---|---|---|---|---|---
Figure 5: Examples of correct gesture recognition with GViT trained on
synthetic data from DUR (left to right): thumbs-up gesture from 10 meters
distance with model certainty of 95.6%; beckoning gesture from 12 meters
distance with model certainty of 95.1%; null gesture from 19 meters distance
with model certainty of 93.5%; pointing gesture from 15 meters distance with
model certainty of 94.7%; thumbs-down gesture from 20 meters distance with
model certainty of 92.8%; and stop gesture from 17 meters distance with model
certainty of 93.9%.

We further evaluate the merit of investing real collected data $\mathcal{D}$
directly to train GViT, or indirectly by first training DUR with $\mathcal{D}$
and then training GViT with synthetic data. Figure 6 presents the success rate
of gesture recognition over the test data with regard to the amount of real
data used to train either DUR or directly GViT. When DUR is trained with some
amount of real data, 220,000 synthetic images are then generated and used to
train a GViT model. The results emphasize a significant improvement
attributable to the use of a generative model. By using 175,000 real images to
train DUR, the success rate reaches 95.8%. To reach the same rate with direct
GViT training, 312,000 real labeled images are required. On the other hand,
using the 175,000 real images to directly train GViT yields a poor success
rate of 58.8%. Hence, it is significantly more advantageous to use the
collected data to train DUR than directly using it to train GViT. This result
can be explained by the high quality and rich images generated by DUR compared
to the real data which is rather limited. DUR is able to capture the gesture
image distribution with a limited number of real samples and, thus, generalize
to provide representative synthetic samples from the whole distribution.
Figure 7 presents the confusion matrix for the GViT trained with synthetic
data from DUR. The results show high success rates for all gestures.

Figure 6: Gesture recognition success rate for training GViT with regard to
the amount of real data points used to directly train GViT, or to train DUR
and then generate 220,000 synthetic data for training GViT. Figure 7:
Recognition confusion matrix for GViT trained on synthetic data from DUR and
evaluated on real test data.

In an opposite perspective, we are interested in the implication of generating
more synthetic samples to train GViT, with an already trained DUR. Hence, we
use a DUR trained with 175,000 real images to generate synthetic samples.
Figure 8 presents the mean success rate for gesture recognition in GViT
trained with an increasing number of synthetic data. The mean success rate is
evaluated over five training trials with newly generated synthetic data in
each trial. The results clearly show performance improvement with an increase
in synthetic samples, emphasizing the benefit of using DUR.

Figure 8: Mean success rate for Gesture recognition for GViT with regard to
the amount of synthetic training samples generated by DUR.

Next, an ablation study is provided. We compare the recognition success rate
of GViT trained with synthetic data from different configurations of DUR:
training DUR without passing the cropped images through HQ-Net, training DUR
without CFDG, and DUR without filtering out failed images using ResNet. In
addition, we also evaluate ill-trained GViT on failed synthetic test images.
That is, 10,176 failed images were added to the training of the GViT. Then, it
was evaluated on test images composed of 16,464 failed synthetic images. The
failed images are the ones acquired for training the ResNet (Figure 3). Table
III presents the results for the comparison along with the one for the full
DUR model. The results show that DUR, in all cases, is able to acquire
relatively successful training data for GViT. Nevertheless, the SR component
using HQ-Net and the ResNet are able to provide important improvements. The
CFDG provides a rather marginal improvement. When considering failed test
data, it seems that the gesture information remains observable by the model
despite the generation errors and smearing. Hence, the ill-trained model
tested on a failed test set is able to provide a sufficient recognition rate.
Conclusively, the GVIT model, when implemented within the complete proposed
methodology, attains a commendable 95.8% success rate.

TABLE III: Ablation study of DUR variations for training GViT model Models | Success rate (%)
---|---
DUR w/o HQ-Net | 91.2 $\pm$ 5.71
DUR w/o CFDG | 94.6 $\pm$ 3.32
DUR w/o ResNet | 90.03 $\pm$ 4.53
Failed data | 89.15 $\pm$ 2.24
DUR | 95.8 $\pm$ 4.01

###  III-D Robot demonstration

The effectiveness and feasibility of the GViT model, trained with only
synthetic images, are experimented in directing a Unitree Go1 quadruped robot
with gestures. We evaluate the real-time responses of a robot, equipped with a
simple RGB camera, to recognize gestures exhibited by a user positioned in
ultra-range. For demonstration purposes, a pointing gesture directs the robot
to walk sideways; a thumbs-up commands the robot to pitch tilt; a thumbs-down
makes the robot lie down; beckoning instructs the robot to walk toward the
user; a stop gesture will make the robot stop a previous directive; and with
null, the robot will not change its current actions. The robot experiments
were conducted in various indoor and outdoor environments as demonstrated in
Figure 9. A total of 32 gestures were exhibited to the robot with a successful
action response rate of 94%. The results show that the URGR model trained only
with data generated by DUR is capable of efficient real-world performance.

Figure 9: Human directive to a robot through gestures: (left) indoor with
beckoning at 23 m, and (right) outdoor with a pointing gesture at 16 m.

##  IV Conclusions

In this paper, we have introduced a comprehensive framework for generating
synthetic data of objects in ultra-range distances, addressing the challenges
posed by diverse environments, varying distances, and the acquisition of
reliable data. The DUR framework seamlessly integrates the diffusion model
with the U-Net architecture featuring time embedding to generate high-quality
synthetic data. Through extensive experimentation and analysis, we have
demonstrated the efficacy of DUR in training a gesture recognition model
across different distances, environments and users. By leveraging synthetic
data generation, we overcome limitations associated with data acquisition,
providing a scalable solution for training gesture recognition models. The
major benefit of using DUR is, therefore, the significant reduction of the
requirements for real-world data, while capable of training a highly robust
recognition model. Future work may include the enforcement of background
conditions, enabling the augmentation of an object recognition model with more
complex environments. Moreover, exploring the integration of video data and
temporal information into the DUR framework holds promise for capturing
dynamic changes over time, enhancing the realism and temporal fidelity of
synthetic data for recognition models.

## References

  * [1] T. Serre, L. Wolf, S. Bileschi, M. Riesenhuber, and T. Poggio, “Robust object recognition with cortex-like mechanisms,” _IEEE Trans. on pattern analysis and machine intelligence_ , vol. 29, no. 3, pp. 411–426, 2007.
  * [2] P. David and D. DeMenthon, “Object recognition in high clutter images using line features,” in _IEEE International Conference on Computer Vision_ , vol. 2, 2005, pp. 1581–1588.
  * [3] S. D. Shirke and C. Rajabhushnam, “Biometric personal iris recognition from an image at long distance,” in _IEEE Inter. Conf. on Trends in Electronics and Informatics_ , 2019, pp. 560–565.
  * [4] R. A. Zitar, A. Mohsen, A. E. Seghrouchni, F. Barbaresco, and N. A. Al-Dmour, “Intensive review of drones detection and tracking: Linear kalman filter versus nonlinear regression, an analysis case,” _Archives of Comp. Methods in Engineering_ , vol. 30, no. 5, pp. 2811–2830, 2023.
  * [5] W. Lu and Y.-P. Tan, “A vision-based approach to early detection of drowning incidents in swimming pools,” _IEEE Transactions on Circuits and Systems for Video Technology_ , vol. 14, no. 2, pp. 159–178, 2004.
  * [6] X. Yang, H. Sun, K. Fu, J. Yang, X. Sun, M. Yan, and Z. Guo, “Automatic ship detection in remote sensing images from google earth of complex scenes based on multiscale rotation dense feature pyramid networks,” _Remote sensing_ , vol. 10, no. 1, p. 132, 2018.
  * [7] L. Zhou, C. Du, Z. Sun, T. L. Lam, and Y. Xu, “Long-range hand gesture recognition via attention-based ssd network,” in _IEEE International Conference on Robotics and Automation (ICRA)_ , 2021, pp. 1832–1838.
  * [8] K. Nickel and R. Stiefelhagen, “Visual recognition of pointing gestures for human–robot interaction,” _Image and vision computing_ , vol. 25, no. 12, pp. 1875–1884, 2007.
  * [9] J. P. Wachs, M. Kölsch, H. Stern, and Y. Edan, “Vision-based hand-gesture applications,” _Commun. ACM_ , vol. 54, no. 2, p. 60–71, 2011.
  * [10] Z. Xia, Q. Lei, Y. Yang, H. Zhang, Y. He, W. Wang, and M. Huang, “Vision-based hand gesture recognition for human-robot collaboration: A survey,” in _IEEE International Conference on Control, Automation and Robotics_ , 2019, pp. 198–205.
  * [11] C. Yi, L. Zhou, Z. Wang, Z. Sun, and C. Tan, “Long-range hand gesture recognition with joint SSD network,” in _IEEE international conference on robotics and biomimetics (ROBIO)_ , 2018, pp. 1959–1963.
  * [12] E. Bamani, E. Nissinman, I. Meir, L. Koenigsberg, and A. Sintov, “Ultra-range gesture recognition using a web-camera in human-robot interaction,” _Eng. Applications of Artificial Intelligence_ , In press, 2024.
  * [13] Y. Lu, M. Shen, H. Wang, X. Wang, C. van Rechem, and W. Wei, “Machine learning for synthetic data generation: A review,” _arXiv_ , 2024.
  * [14] J. Molina, J. A. Pajuelo, M. Escudero-Viñolo, J. Bescós, and J. M. Martínez, “A natural and synthetic corpus for benchmarking of hand gesture recognition systems,” _Machine Vision and Applications_ , vol. 25, no. 4, pp. 943–954, 2014.
  * [15] C.-J. Tsai, Y.-W. Tsai, S.-L. Hsu, and Y.-C. Wu, “Synthetic training of deep CNN for 3D hand gesture identification,” in _Inter. Conf. on Control, Artificial Intel., Robotics & Optimization_, 2017, pp. 165–170.
  * [16] C. M. de Melo, B. Rothrock, P. Gurram, O. Ulutan, and B. S. Manjunath, “Vision-based gesture recognition in human-robot teams using synthetic data,” in _IEEE/RSJ Inter. Conf. on Intelligent Robots and Systems_ , 2020, pp. 10 278–10 284.
  * [17] A. Ninos, J. Hasch, M. E. P. Alvarez, and T. Zwick, “Synthetic radar dataset generator for macro-gesture recognition,” _IEEE Access_ , vol. 9, pp. 76 576–76 584, 2021.
  * [18] W. Zhou and K. Chen, “A lightweight hand gesture recognition in complex backgrounds,” _Displays_ , vol. 74, p. 102226, 2022.
  * [19] I. Goodfellow, J. Pouget-Abadie, M. Mirza, B. Xu, D. Warde-Farley, S. Ozair, A. Courville, and Y. Bengio, “Generative adversarial nets,” _Advances in neural information processing systems_ , vol. 27, 2014.
  * [20] A. Radford, L. Metz, and S. Chintala, “Unsupervised representation learning with deep convolutional generative adversarial networks,” _arXiv preprint arXiv:1511.06434_ , 2015.
  * [21] T. Karras, T. Aila, S. Laine, and J. Lehtinen, “Progressive growing of gans for improved quality, stability, and variation,” _arXiv preprint arXiv:1710.10196_ , 2017.
  * [22] M. Mirza and S. Osindero, “Conditional generative adversarial nets,” _arXiv preprint arXiv:1411.1784_ , 2014.
  * [23] C. D. Prakash and L. J. Karam, “It GAN do better: GAN-based detection of objects on images with varying quality,” _IEEE Transactions on Image Processing_ , vol. 30, p. 9220–9230, 2021.
  * [24] L. Minciullo, F. Manhardt, K. Yoshikawa, S. Meier, F. Tombari, and N. Kobori, “DB-GAN: Boosting object recognition under strong lighting conditions,” in _IEEE/CVF Winter Conference on Applications of Computer Vision_ , 2021, pp. 2939–2949.
  * [25] H. Tang, W. Wang, D. Xu, Y. Yan, and N. Sebe, “GestureGAN for hand gesture-to-gesture translation in the wild,” in _ACM International Conference on Multimedia_ , 2018, pp. 774–782.
  * [26] W. Fang, Y. Ding, F. Zhang, and J. Sheng, “Gesture recognition based on CNN and DCGAN for calculation and text output,” _IEEE access_ , vol. 7, pp. 28 230–28 237, 2019.
  * [27] J. Liu, K. Furusawa, T. Tateyama, Y. Iwamoto, and Y.-W. Chen, “An improved hand gesture recognition with two-stage convolution neural networks using a hand color image and its pseudo-depth image,” in _IEEE International Conference on Image Processing_ , 2019, pp. 375–379.
  * [28] J. Shen, J. Dudley, and P. O. Kristensson, “The imaginative generative adversarial network: Automatic data augmentation for dynamic skeleton-based hand gesture and human action recognition,” in _IEEE International Conference on Automatic Face and Gesture Recognition_ , 2021, pp. 1–8.
  * [29] A. Waheed, M. Goyal, D. Gupta, A. Khanna, F. Al-Turjman, and P. R. Pinheiro, “CovidGAN: Data augmentation using auxiliary classifier GAN for improved Covid-19 detection,” _IEEE Access_ , vol. 8, pp. 91 916–91 923, 2020.
  * [30] A. Borji, “Pros and cons of GAN evaluation measures,” _Computer vision and image understanding_ , vol. 179, pp. 41–65, 2019.
  * [31] J. Hellermann and S. Lessmann, “Leveraging image-based generative adversarial networks for time series generation,” _arXiv preprint arXiv:2112.08060_ , 2021.
  * [32] J. Sohl-Dickstein, E. Weiss, N. Maheswaranathan, and S. Ganguli, “Deep unsupervised learning using nonequilibrium thermodynamics,” in _International Conference on Machine Learning_ , 2015, pp. 2256–2265.
  * [33] F.-A. Croitoru, V. Hondru, R. T. Ionescu, and M. Shah, “Diffusion models in vision: A survey,” _IEEE Transactions on Pattern Analysis and Machine Intelligence_ , vol. 45, no. 9, pp. 10 850–10 869, 2023.
  * [34] Y. Song and S. Ermon, “Generative modeling by estimating gradients of the data distribution,” _Advances in neural information processing systems_ , vol. 32, 2019.
  * [35] J. Ho, A. Jain, and P. Abbeel, “Denoising diffusion probabilistic models,” _Advances in neural information processing systems_ , vol. 33, pp. 6840–6851, 2020.
  * [36] Z. Yue, J. Wang, and C. C. Loy, “ResShift: Efficient diffusion model for image super-resolution by residual shifting,” in _Advances in Neural Information Processing Systems (NeurIPS)_ , 2023.
  * [37] A. Lugmayr, M. Danelljan, A. Romero, F. Yu, R. Timofte, and L. Van Gool, “Repaint: Inpainting using denoising diffusion probabilistic models,” in _IEEE/CVF Conference on Computer Vision and Pattern Recognition_ , 2022, pp. 11 461–11 471.
  * [38] L. Wang, J. Jia, and H. Dai, “OrientedDiffDet: Diffusion model for oriented object detection in aerial images,” _Applied Sciences_ , vol. 14, no. 5, 2024.
  * [39] D. Chen, X. Qi, Y. Zheng, Y. Lu, Y. Huang, and Z. Li, “Synthetic data augmentation by diffusion probabilistic models to enhance weed recognition,” _Computers and Electronics in Agriculture_ , vol. 216, p. 108517, 2024.
  * [40] S. Chen, P. Sun, Y. Song, and P. Luo, “DiffusionDet: Diffusion model for object detection,” in _IEEE/CVF International Conference on Computer Vision (ICCV)_ , 2023, pp. 19 830–19 843.
  * [41] J. Song, C. Meng, and S. Ermon, “Denoising diffusion implicit models,” _arXiv preprint arXiv:2010.02502_ , 2020.
  * [42] O. Ronneberger, P. Fischer, and T. Brox, “U-Net: Convolutional networks for biomedical image segmentation,” in _Medical Image Computing and Computer-Assisted Intervention_. Springer, 2015, pp. 234–241.
  * [43] K. He, X. Zhang, S. Ren, and J. Sun, “Deep residual learning for image recognition. corr abs/1512.03385 (2015),” 2015.
  * [44] J. Ho and T. Salimans, “Classifier-free diffusion guidance,” _arXiv preprint arXiv:2207.12598_ , 2022.
  * [45] A. Odena, C. Olah, and J. Shlens, “Conditional image synthesis with auxiliary classifier gans,” in _International conference on machine learning_. PMLR, 2017, pp. 2642–2651.
  * [46] T. Salimans, I. Goodfellow, W. Zaremba, V. Cheung, A. Radford, and X. Chen, “Improved techniques for training gans,” _Advances in neural information processing systems_ , vol. 29, 2016.
  * [47] M. Heusel, H. Ramsauer, T. Unterthiner, B. Nessler, and S. Hochreiter, “GANs trained by a two time-scale update rule converge to a local nash equilibrium,” _Advances in Neural Information Processing Systems_ , vol. 30, 2017.
  * [48] Z. Wang, A. C. Bovik, H. R. Sheikh, and E. P. Simoncelli, “Image quality assessment: from error visibility to structural similarity,” _IEEE transactions on image processing_ , vol. 13, no. 4, pp. 600–612, 2004.
  * [49] I. Ullah, M. Manzo, M. Shah, and M. G. Madden, “Graph convolutional networks: analysis, improvements and results,” _Applied Intelligence_ , pp. 1–12, 2022.
  * [50] A. Dosovitskiy, L. Beyer, A. Kolesnikov, D. Weissenborn, X. Zhai, T. Unterthiner, M. Dehghani, M. Minderer, G. Heigold, S. Gelly, J. Uszkoreit, and N. Houlsby, “An image is worth 16x16 words: Transformers for image recognition at scale,” in _International Conference on Learning Representations_ , 2021.