Bayesian Inference in Quantum Programs

TL;DR

This paper equips a quantum while-language with conditioning, defines its denotational and operational semantics over infinite-dimensional Hilbert spaces, and shows their equivalence.

Abstract

Conditioning is a key feature in probabilistic programming to enable modeling the influence of data (also known as observations) to the probability distribution described by such programs. Determining the posterior distribution is also known as Bayesian inference. This paper equips a quantum while-language with conditioning, defines its denotational and operational semantics over infinite-dimensional Hilbert spaces, and shows their equivalence. We provide sufficient conditions for the existence of weakest (liberal) precondition-transformers and derive inductive characterizations of these transformers. It is shown how w(l)p-transformers can be used to assess the effect of Bayesian inference on (possibly diverging) quantum programs.

Figures (5)

• Figure 1: Transition probability function of MC $\mathfrak{R}_{\rho}\llbracket S \rrbracket$ for all $\sigma \in \mathcal{D}(\mathcal{H})$ where $\downarrow;S_2 \equiv S_2$
• Figure 2: Quantum Fast-Dice-Roller. For the identity operator on $\mathcal{H}_2 \otimes \mathcal{H}_2$ we use $\textbf{I}_4$.
• Figure 3: Inner loop body $S_k$ of the quantum algorithm solving MAJ-SAT as presented in postbqp. $y,z$ are qubits, $\overline{q}$ is an $n$-qubit sized register (formally $n$ qubits $q_1,\dots,q_n$). We use $\overline{q} := 0^{\otimes n}$ to denote that all $n$ qubits of $\overline{q}$ are set of $0$. $R_k = \frac{1}{\sqrt{1+4^k}}1-2^k2^k1$ is a rotation matrix depending on the parameter $k$ and $CH$ is a controlled Hadamard.
• Figure 4: Maximum of $\Pr_{nsk}={\hat{tr}(qcwp\llbracket S_k \rrbracket (P,\textbf{I}^{\otimes n+2}) \odot \rho)}$ for $k\in [-n,n]$. The cases where $s<2^{n-1}$ are underlined.
• Figure 5: Operational semantics of the Quantum Fast-Dice-Roller with $\rho_1 =(H \otimes \textbf{I}_2 \otimes \textbf{I}_2) \rho (H \otimes \textbf{I}_2 \otimes \textbf{I}_2)^\dagger$$\rho_2 = (H \otimes H \otimes \textbf{I}_2) \rho (H \otimes H \otimes \textbf{I}_2)^\dagger$$\rho_3 = \frac{1}{tr(\rho_3')}\rho_3'$ with $\rho_3' = ((\textbf{I}_4 - \ket{11}\bra{11}) \otimes \textbf{I}_2)(H \otimes H \otimes \textbf{I}_2) \rho (H \otimes H \otimes \textbf{I}_2)^\dagger ((\textbf{I}_4 - \ket{11}\bra{11}) \otimes \textbf{I}_2)^\dagger$$\rho_4 = \frac{1}{tr(\rho_3')}((\textbf{I}_4 - \ket{11}\bra{11}) \otimes \textbf{I}_2)(H \otimes H \otimes H) \rho (H \otimes H \otimes H)^\dagger ((\textbf{I}_4 - \ket{11}\bra{11}) \otimes \textbf{I}_2)^\dagger$

Theorems & Definitions (29)

• Example 1
• Definition 2
• Definition 3
• Proposition 4
• Proposition 5
• Lemma 6
• Lemma 7
• Definition 8
• Proposition 9
• Definition 10