Quantum Information

Motivation

Many recent quantum algorithms for linear algebra and optimization take their input as a block-encoding: a unitary circuit whose top-left block, after projecting a set of ancilla qubits onto $|0\rangle$, approximates the matrix of interest. The quantum semidefinite-programming solver of van Apeldoorn and Gilyén (arXiv:1804.05058) introduces the quantum operator model, in which every constraint matrix of the SDP is given this way (Definition 2, p. 4). Block-encodings are also the input format of quantum singular value transformation and of Hamiltonian simulation by qubitization (Low and Chuang, arXiv:1610.06546).

A natural question is where block-encodings come from in applications. In §4.1, on shadow tomography, the constraint matrices are the elements $E_j$ of two-outcome measurements, and what a user can do is perform those measurements, not write down their matrices. The closing remark of §4.1 (pp. 24–25) answers the question for that setting: if a two-outcome measurement can be implemented on a quantum computer with small bias, then a block-encoding of its measurement operator can be built from the same circuit with one extra qubit and one CNOT gate. The remark is credited to the same observation by Low and Chuang (arXiv:1707.05391).

Setting

A two-outcome POVM on a finite-dimensional system is a pair $\{M, I - M\}$ of operators with $M$ and $I - M$ positive semidefinite. A mixed state (density matrix) is a positive semidefinite operator $\rho$ with $\operatorname{Tr}\rho = 1$; outcome $M$ occurs with probability $\operatorname{Tr}(M\rho)$.

An implementation of the measurement on a quantum computer, as the paper fixes it, takes the input $\rho$, attaches $a$ ancilla qubits in the state $|0\rangle^{\otimes a}$, applies a unitary $U$ to system and ancillas, measures in the computational basis, and accepts when the last qubit reads $|0\rangle$:

$$\rho \to \rho\otimes|0\rangle\langle 0|^{\otimes a} \to U\big(\rho\otimes|0\rangle\langle 0|^{\otimes a}\big)U^\dagger \to \operatorname{Tr}\Big((I\otimes|0\rangle\langle 0|)\,U\big(\rho\otimes|0\rangle\langle 0|^{\otimes a}\big)U^\dagger\Big).$$

The implementation has bias at most $\varepsilon$ if, for every state $\rho$,

$$\Big|\operatorname{Tr}\Big((I\otimes|0\rangle\langle 0|)\,U\big(\rho\otimes|0\rangle\langle 0|^{\otimes a}\big)U^\dagger\Big) - \operatorname{Tr}(M\rho)\Big| \le \varepsilon. \qquad (14)$$

Write $K = (I\otimes\langle 0|^{\otimes a})\,U^\dagger(I\otimes|0\rangle\langle 0|)U\,(I\otimes|0\rangle^{\otimes a})$, an operator on the system. A unitary $V$ on $a'$ ancilla qubits and the system is an $(\alpha, a', \varepsilon)$-block-encoding of $A$ (Definition 2) if $\|A - \alpha(\langle 0|^{\otimes a'}\otimes I)V(|0\rangle^{\otimes a'}\otimes I)\| \le \varepsilon$ in the operator norm. Finally $U' = U\otimes I_2$ adds one fresh qubit, and $I\otimes\mathrm{CNOT}$ is a CNOT gate whose control is the measured qubit and whose target is the fresh qubit.

Formalization targets

Goal (§4.1, p. 25)

$$\text{(14)} \;\Longrightarrow\; U'^\dagger(I\otimes\mathrm{CNOT})U' \text{ is a } (1,\ a+1,\ \varepsilon)\text{-block-encoding of } M .$$

The subnormalization is $1$, the ancilla count is $a' = a + 1$ and the error is the same $\varepsilon$ as the bias; none of these is weakened.

Milestones (all p. 25, in the order of the derivation)

1. The trace identity: $\rho\otimes|0\rangle\langle 0|^{\otimes a} = (I\otimes|0\rangle^{\otimes a})\rho(I\otimes\langle 0|^{\otimes a})$, hence the acceptance probability equals $\operatorname{Tr}(K\rho)$.
2. The equivalence $\forall\rho:\ |\operatorname{Tr}([K - M]\rho)| \le \varepsilon \iff \|K - M\| \le \varepsilon$, with $\rho$ over density matrices.
3. The CNOT identity $K = (I\otimes\langle 0|^{\otimes a'})\,U'^\dagger(I\otimes\mathrm{CNOT})U'\,(I\otimes|0\rangle^{\otimes a'})$.

Significance

The result. It converts an operational primitive, performing a measurement, into the input format that block-encoding algorithms consume, with an additive error equal to the measurement's bias and at the cost of one qubit and one CNOT. In the paper it is what makes the shadow-tomography application of §4.1 meaningful: the cost of the SDP solver is stated in terms of block-encodings of the $E_j$, and this remark lets one replace that by the cost of controlled implementations of the measurements. More generally it shows that the quantum operator model is no stronger than the ability to measure.

Formalizing it. The paper proves the remark in a few displayed lines, one of which ("it is easy to see") is left to the reader and whose CNOT direction is not printed. No machine-checked version exists. A formal proof fixes the register conventions, makes the direction of the CNOT explicit, and contributes a reusable fact about matrices: for a Hermitian $X$, $\sup_\rho |\operatorname{Tr}(X\rho)| = \|X\|$ over density matrices. The block-encoding predicate itself is already published on the platform and is reused.

Difficulty

The algebra of milestones 1 and 3 is bookkeeping over tensor-product index sets, and the main cost there is choosing representations that make the registers line up.

The one step with mathematical content is the direction "$\Rightarrow$" of milestone 2. The bias condition controls $|\operatorname{Tr}(X\rho)|$ only for density matrices $\rho$, that is, it bounds the numerical radius of $X = K - M$, while a block-encoding needs the operator norm. For a general matrix these differ by up to a factor of two, so the step needs $X$ to be Hermitian: $M$ is Hermitian as a POVM element, and $K$ is Hermitian because it is a compression of the projector $I\otimes|0\rangle\langle 0|$. A formal proof must use both facts and exhibit a state that attains the norm.

Formalization scope

The Lean development lives in the namespace QuantumSDP18.MeasureBE. Its conventions are:

• The system register is an arbitrary finite type $\iota$ (a $w$-qubit system is $\iota = \{0,1\}^w$). Operators are complex matrices; $\dagger$ is the conjugate transpose; the operator norm is the platform's QAlgorithms.specNorm.
• The ancilla register is Qubits c × Bool, so $a = c + 1 \ge 1$ and the Bool factor is the last, measured qubit. The basis state $|0\rangle$ of any register is its all-false index.
• (14) ranges over all density matrices (PosSemidef with trace $1$), and its absolute value is the modulus of a complex trace.
• The CNOT is the platform's QAlgorithms.cnot (control first), placed on the measured qubit (control) and the fresh qubit (target). With the opposite direction the block is $U^\dagger U$ and the goal is false; the chosen direction is the only reading under which the page's identity holds.
• The block-encoding predicate is the platform's QAlgorithms.IsBlockEncoding, which puts the ancilla register first, as Definition 2 does; the circuit, written system-first as on p. 25, is reindexed to match.
• Added hypothesis: $\varepsilon \ge 0$ (a bias is nonnegative). It matters only for a zero-dimensional system, where (14) holds vacuously.

The goal keeps both POVM hypotheses ($M \succeq 0$ and $I - M \succeq 0$), and the bias condition quantifies over all states rather than one fixed state, under which the conclusion would be false. A formalization in which (14) ranges over arbitrary matrices, or which drops the CNOT and states only $\|K - M\| \le \varepsilon$, is a different theorem.

Needed infrastructure: Kronecker products and reindexing of matrices, the unitarity of permutation matrices and of Kronecker products, and the variational characterization of the operator norm of a Hermitian matrix through its eigenvectors. The last is reusable beyond this mission. Proofs of the three milestones are welcome independently.

Selected references

• J. van Apeldoorn, A. Gilyén, Improvements in quantum SDP-solving with applications, arXiv preprint, 2018 (ICALP 2019). https://arxiv.org/abs/1804.05058
• G. H. Low, I. L. Chuang, Hamiltonian simulation by qubitization, arXiv preprint, 2016 (Quantum 3, 163, 2019). https://arxiv.org/abs/1610.06546
• G. H. Low, I. L. Chuang, Hamiltonian simulation by uniform spectral amplification, arXiv preprint, 2017. https://arxiv.org/abs/1707.05391
• S. Aaronson, Shadow tomography of quantum states, STOC 2018. https://arxiv.org/abs/1711.01053

Motivation

The quantum approximate optimization algorithm (QAOA) of Farhi, Goldstone and Gutmann (arXiv:1411.4028, 2014) is a family of shallow quantum circuits, indexed by an integer depth $p \ge 1$, that prepare states whose computational-basis measurements are biased toward good solutions of a combinatorial optimization problem. It became the standard candidate for optimization on near-term quantum hardware, and its performance on MaxCut is the benchmark against which later analyses and experiments are measured.

The original paper proves one concrete performance guarantee: at depth $p = 1$, on 3-regular graphs, the algorithm achieves an approximation ratio of at least $0.6924$. Short timeline:

• 2014, Farhi–Goldstone–Gutmann: the $p = 1$ bound $0.6924$ on 3-regular graphs, by reducing the expected cut to three subgraph functions and a numerical minimization (arXiv:1411.4028).
• 2018, Wang, Hadfield, Jiang and Rieffel: closed-form expressions for the $p = 1$ MaxCut expectation on arbitrary graphs (arXiv:1706.02998, Phys. Rev. A 97, 022304).
• Classically, Goemans and Williamson's semidefinite rounding achieves $0.878$ on all graphs (J. ACM 42, 1995), so the $p = 1$ guarantee is, as the paper itself notes, below the best classical algorithms.

Setting

A graph $G$ has vertex set $\{0, \dots, n-1\}$, and 3-regular means every vertex has exactly three neighbours. Each vertex carries a qubit; a computational basis state is a bit string $z = z_0 \cdots z_{n-1}$. For an edge $\langle jk\rangle$ the clause $C_{\langle jk\rangle}(z)$ is $1$ if $z_j \neq z_k$ and $0$ otherwise, and the cut objective is

$$C(z) = \sum_{\langle jk\rangle} C_{\langle jk\rangle}(z),$$

the number of edges cut by the bipartition $z$ defines. As an operator, $C$ is diagonal in the computational basis.

Let $B = \sum_j \sigma^x_j$ and let $|s\rangle = 2^{-n/2}\sum_z |z\rangle$. For angles $\gamma, \beta \in \mathbb R$, the depth-one QAOA state and its expected cut are

$$|\gamma,\beta\rangle = e^{-i\beta B}\, e^{-i\gamma C}\, |s\rangle, \qquad F_1(\gamma,\beta) = \langle\gamma,\beta|\,C\,|\gamma,\beta\rangle = \sum_z |\langle z|\gamma,\beta\rangle|^2\, C(z).$$

The angles may be restricted to $\gamma \in [0, 2\pi]$, $\beta \in [0, \pi]$ by periodicity.

Two kinds of small subgraphs govern the analysis. A crossed square is a set of four vertices spanning exactly five edges (a 4-cycle with one diagonal). An isolated triangle is a triangle whose three outgoing edges end on three distinct vertices. $S$ and $T$ denote their numbers in $G$. Finally, for an edge $\langle jk\rangle$ the subgraph type is the shape of the edge together with its adjacent edges; in a 3-regular graph there are three types $g_4, g_5, g_6$, according as $j$ and $k$ have two, one or no common neighbours. Each type $g$ defines a function $f_g(\gamma, \beta)$, the expectation of the clause of the central edge in the depth-one QAOA state of the subgraph $g$ alone.

Formalization targets

Goal: the depth-one ratio on cubic graphs

For every connected 3-regular graph $G$ there are angles $\gamma \in [0, 2\pi]$, $\beta \in [0, \pi]$ with

$$F_1(\gamma, \beta) \;\ge\; 0.6924 \cdot C(z) \qquad \text{for every bit string } z,$$

that is, $M_1 = \max_{\gamma,\beta} F_1 \ge 0.6924 \cdot \max_z C(z)$. The constant is exactly the paper's $0.6924$, and $K_4$ is included.

Milestones

The paper's argument passes through the following claims, each a milestone:

1. At $p = 1$ each edge term of a 3-regular graph equals $f_{g_4}$, $f_{g_5}$ or $f_{g_6}$ according to its subgraph type (p. 5).
2. In a connected 3-regular graph other than $K_4$, there are $S$ edges of type $g_4$ and $4S + 3T$ of type $g_5$ (pp. 8–9).
3. Equation (32): $F_1 = S f_{g_4} + (4S + 3T) f_{g_5} + (3n/2 - 5S - 3T) f_{g_6}$ (p. 9).
4. $3T + 4S \le n$ (p. 8).
5. Every cut has at most $3n/2 - S - T$ edges (p. 9).
6. For $s, t \ge 0$ with $4s + 3t \le 1$, the scaled ratio (35) $M_1(1, s, t)/(3/2 - s - t)$ is at least $0.6924$ (p. 9).
7. On $K_4$ the depth-one ratio exceeds $0.6924$ (p. 8).

Significance

The result is the first rigorous worst-case guarantee for the QAOA, and the method behind it (the expected objective is a sum of local terms, each depending only on a bounded neighbourhood of an edge) is the template for every later analysis of fixed-depth QAOA on bounded-degree graphs. It shows that a depth-one circuit, of depth independent of $n$, achieves a constant approximation ratio uniformly over an infinite class of graphs.

The paper's proof is complete apart from one numerical step: the minimization of (35) is reported as a numerical evaluation. No machine-checked version of the result exists. A formal proof requires an exact evaluation of the three subgraph functions at suitable angles, an exact combinatorial count of edge types, and a certified inequality in place of the numerical minimization. The margin is small: the exact minimum is $\tfrac12 + \tfrac{1}{3\sqrt 3} \approx 0.692450$, about $5 \cdot 10^{-5}$ above the paper's constant.

Difficulty

The light-cone reduction (milestone 1) is the conceptual step: one must show that conjugating a two-qubit clause by $e^{-i\gamma C}$ and $e^{-i\beta B}$ leaves an operator that involves only the qubits adjacent to the edge, and that the remaining qubits contribute a factor of one. In matrix form on $2^n$-dimensional space this is a statement about tensor-product structure that the definitions do not make visible. The combinatorial count (milestones 2–4) needs a careful case analysis of how triangles sit in a cubic graph, including the exceptional graph $K_4$, where the count fails. The final inequality (milestone 6) has a margin of order $10^{-4}$, so crude bounds on the trigonometric functions $f_{g}$ do not suffice.

Formalization scope

• Representation. Bit strings are Qubits n = Fin n → Bool from the published QAlgorithms layer, with true the bit $1$. States are vectors in EuclideanSpace ℂ (Qubits n); $|s\rangle$, $C$ as a diagonal operator, $B$ and the QAOA unitary are the published definitions uniformState, problemHamiltonian, qaoaMixer, qaoaUnitary. The latter takes mixer angles before phase angles.
• Conventions. Graphs are SimpleGraph (Fin n) with decidable adjacency; "3-regular" is IsRegularOfDegree 3. The cut counts each edge once. $F_1$ is defined as $\sum_z \Pr[z]\,C(z)$, which equals $\langle\gamma,\beta|C|\gamma,\beta\rangle$ because $C$ is diagonal. The constant $0.6924$ is the exact rational $1731/2500$.
• Added hypotheses. Milestones 2 and 3 assume $G$ connected and $n \ne 4$, which excludes $K_4$, the case the paper sets aside on p. 8. No other hypothesis is added.
• Out of scope. The goal concerns the expected cut at good angles, which is what the paper's analysis bounds. Measuring the state, repeating, and the claim that a cut of that size is then found with high probability are not formalized; nor are running time, circuit depth, or the search for optimal angles.
• Ruled-out trivializations. A cut objective counting each edge twice, or an unnormalized state, would leave the ratio statement formally intact but about the wrong objects; the setting counts each edge once and uses the normalized uniform superposition. The goal quantifies over all bit strings, so it cannot be satisfied by bounding a particular cut.
• Contributions welcome. Reusable lemmas on the light-cone locality of conjugated Pauli operators, closed forms of the depth-one MaxCut expectation, and counting lemmas for triangles in cubic graphs all serve beyond this mission.

Selected references

• E. Farhi, J. Goldstone, S. Gutmann, A Quantum Approximate Optimization Algorithm, arXiv preprint, 2014. https://arxiv.org/abs/1411.4028
• Z. Wang, S. Hadfield, Z. Jiang, E. G. Rieffel, Quantum approximate optimization algorithm for MaxCut: A fermionic view, Phys. Rev. A 97, 022304, 2018. https://arxiv.org/abs/1706.02998
• M. X. Goemans, D. P. Williamson, Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming, J. ACM 42(6), 1995. https://doi.org/10.1145/227683.227684

Certifying a prepared quantum state

Experiments that prepare many-body entangled states (GHZ, W, stabilizer, cluster and matrix product states) need a way to check that the device produced the intended state. Full quantum state tomography answers the question but its cost grows with the dimension $d = 2^n$ of an $n$-qubit system: a reconstruction needs on the order of $d^2$ measurement settings. Entanglement witnesses are cheap but exist only for special states.

Direct fidelity estimation (S. T. Flammia and Y.-K. Liu, arXiv:1104.4695, Phys. Rev. Lett. 106, 230501, 2011; the same idea appears in M. P. da Silva, O. Landon-Cardinal and D. Poulin, arXiv:1104.3835) estimates only the one number the experimentalist needs, the fidelity of the prepared state $\sigma$ to the target pure state $\rho$. It measures a constant number of randomly chosen Pauli observables, independent of $n$, and needs only single-qubit measurements. The method has since become a standard benchmarking tool in experimental quantum information.

Setting

Consider $n$ qubits, $d = 2^n$. Let $W_k$, $k$ ranging over the $d^2 = 4^n$ labels in $\{0,1,2,3\}^n$, be the $n$-fold tensor products of the single-qubit matrices $I, \sigma_x, \sigma_y, \sigma_z$. The characteristic function of a $d\times d$ matrix $\rho$ is

$$\chi_\rho(k) = \mathrm{tr}(\rho W_k/\sqrt d).$$

The target $\rho$ is a pure state, $\rho = |\psi\rangle\langle\psi|$ with $\|\psi\| = 1$; the prepared $\sigma$ is an arbitrary state (positive semidefinite, trace one). For pure $\rho$ the fidelity is $F(\rho,\sigma) = \mathrm{tr}(\rho\sigma)$, and $\mathrm{tr}(\rho\sigma) = \sum_k\chi_\rho(k)\chi_\sigma(k)$.

Given an additive error $\varepsilon>0$ and a failure probability $\delta>0$, the protocol runs in two stages.

1. Importance sampling. Draw $\ell = \lceil 1/(\varepsilon^2\delta)\rceil$ labels $k_1,\dots,k_\ell$ independently with probability $\Pr(k) = \chi_\rho(k)^2$. The ideal estimator is $Y = \frac1\ell\sum_i X_i$, $X_i = \chi_\sigma(k_i)/\chi_\rho(k_i)$.
2. Finite precision. For each $i$, measure the observable $W_{k_i}$ on

$$m_i = \Big\lceil\frac{2}{d\,\chi_\rho(k_i)^2\,\ell\,\varepsilon^2}\log(2/\delta)\Big\rceil$$

copies of $\sigma$. Each measurement gives an outcome $A_{ij}\in\{1,-1\}$ with mean $\mathrm{tr}(\sigma W_{k_i}) = \sqrt d\,\chi_\sigma(k_i)$, independently. The output is

$$\tilde Y = \frac1\ell\sum_{i=1}^\ell\tilde X_i,\qquad \tilde X_i = \frac{1}{m_i\sqrt d\,\chi_\rho(k_i)}\sum_{j=1}^{m_i}A_{ij}.$$

Formalization targets

Goal: the direct-fidelity-estimation guarantee (p. 2)

For every $n$, every pure $\rho$, every state $\sigma$ and every $\varepsilon,\delta>0$,

$$\Pr\Big[\,\mathrm{tr}(\rho\sigma)\in[\tilde Y-2\varepsilon,\ \tilde Y+2\varepsilon]\,\Big]\ \ge\ 1-2\delta ,$$

the probability being over both stages of the protocol.

Milestones

• the fidelity formula (1) and the Pauli expansion (2) (p. 1), and the normalization of (3) (footnote [6], p. 4);
• unbiasedness $\mathbb E X = \mathrm{tr}(\rho\sigma)$ and the variance bound $\mathrm{Var}(X)\le\mathrm{tr}(\sigma^2)-[\mathrm{tr}(\rho\sigma)]^2\le1$ ((12)–(14), p. 6);
• the ideal-estimator bound (5), $\Pr[|Y-\mathrm{tr}(\rho\sigma)|\ge\varepsilon]\le\delta$;
• Hoeffding's bound (16)–(17), $\Pr[|\tilde Y - Y|\ge t]\le 2\exp(-2t^2/C)$, the computation (18), $C\le2\varepsilon^2/\log(2/\delta)$, and the finite-precision bound (8), $\Pr[|\tilde Y - Y|\ge\varepsilon]\le\delta$ for every fixed $k_1,\dots,k_\ell$;
• the resource bounds (9)–(10) on the expected number of copies and the deterministic bound $m_i\le1+2\log(2/\delta)/(\alpha^2\ell\varepsilon^2)$ for well-conditioned states.

Significance

The guarantee says that $\ell = \lceil1/(\varepsilon^2\delta)\rceil$ Pauli settings suffice to estimate the fidelity of any $n$-qubit state to any pure target, whatever $n$. The number of copies of $\sigma$ is $O(d)$ in expectation in the worst case and constant for stabilizer states, while the paper's lower bounds show that full tomography with Pauli measurements needs a number of copies polynomial in $d$. The same scheme, applied to the Choi state, certifies unitary channels and Clifford circuits.

The result is proved on paper but has not been machine-checked. A formal proof requires the Pauli-basis machinery (orthogonality and completeness of the $n$-qubit Pauli operators), the Born-rule model of repeated Pauli measurements, and the combination of a second-moment bound with a sub-Gaussian bound through a two-stage union bound. The formalization also corrects a printed slip: the paper's equality (13) holds only as an inequality (see the milestone's note), which does not affect the result.

Difficulty

Each individual step is classical: Chebyshev's inequality for the first stage, Hoeffding's inequality for the second. The difficulty lies in the bookkeeping that the informal proof leaves implicit. The first-stage estimator involves $1/\chi_\rho(k)$, which is undefined at labels the sampling never produces, so every probability must be weighted by $\Pr(k)$. The second-stage bound holds conditionally on the labels, and its sample sizes $m_i$ depend on them, so the two stages cannot be treated as one product of independent variables. The constant in Hoeffding's bound must be tracked through the $\sqrt d$ factors of $\chi$ and of $\mathbb E A_{ij}$, and through the ceiling in $m_i$. Finally, the Pauli expansion (2) requires the trace orthogonality $\mathrm{tr}(W_kW_{k'}) = d\,\delta_{kk'}$ of $n$-fold tensor products, which is not in Mathlib.

Formalization scope

• Basis labels are Q n := Fin n → Fin 2, Pauli labels P n := Fin n → Fin 4; matrices are Matrix (Q n) (Q n) ℂ, and $W_k$ is the entrywise product $\prod_i(P_{k_i})_{x_iy_i}$. $d$ is the real number $2^n$.
• Traces are real parts of complex traces (real on Hermitian matrices); $\chi_\rho(k)$ is real-valued.
• States are WildeQIT.IsDensityOperator (positive semidefinite, trace one), referenced from the platform; purity is $\rho = \psi\psi^\dagger$ with $\psi^\dagger\psi = 1$.
• $\lceil\cdot\rceil$ is Nat.ceil, $\log$ the natural logarithm.
• The first stage is a finite sum over label tuples weighted by $\prod_i\chi_\rho(k_i)^2$. The second stage is an explicit product measure: each $A_{ij}$ is $+1$ with probability $(1+\mathrm{tr}(\sigma W_{k_i}))/2$ and $-1$ otherwise. This Born-rule law is the unique $\pm1$ law with the page's mean $\sqrt d\,\chi_\sigma(k_i)$. The outcomes are not arbitrary random variables with hypothesised means, which would make the goal vacuous or false.
• Statements that divide by $\chi_\rho(k_i)$ either weight by $\Pr(k_i)$ or assume $\chi_\rho(k_i)\neq0$; none quantifies over all labels without weights.
• (9), (10), (18) and the well-conditioned bound assume $\delta<1$, so that $\log(2/\delta)>0$; the goal, (5) and (8) carry no such hypothesis.
• The goal does not mention variances, Chebyshev, Hoeffding's constant or (15), and it quantifies over every $n$, pure $\rho$, state $\sigma$ and $\varepsilon,\delta>0$. It cannot be discharged by a special case or a degenerate measure.

A complete development needs the Pauli-basis lemmas (Hermiticity, $W_k^2 = I$, trace orthogonality and the expansion of a matrix in the Pauli basis), a Born-rule lemma for $\pm1$ observables, and Hoeffding and Chebyshev bounds specialised to finite product measures. The Pauli-basis lemmas are reusable well beyond this mission (stabilizer formalism, shadow tomography, randomized benchmarking). Proofs of any milestone, and of auxiliary Pauli-basis facts, are welcome.

Selected references

• S. T. Flammia and Y.-K. Liu, Direct fidelity estimation from few Pauli measurements, Phys. Rev. Lett. 106, 230501 (2011); arXiv:1104.4695v3. https://arxiv.org/abs/1104.4695
• M. P. da Silva, O. Landon-Cardinal and D. Poulin, Practical characterization of quantum devices without tomography, Phys. Rev. Lett. 107, 210404 (2011). https://arxiv.org/abs/1104.3835
• R. Jozsa, Fidelity for mixed quantum states, J. Mod. Opt. 41, 2315 (1994). https://doi.org/10.1080/09500349414552171
• W. Hoeffding, Probability inequalities for sums of bounded random variables, J. Amer. Statist. Assoc. 58, 13–30 (1963). https://doi.org/10.1080/01621459.1963.10500830

Motivation

Determining an unknown quantum state of $n$ qubits to good accuracy requires, in general, a number of copies of the state exponential in $n$; this follows from Holevo's theorem. One way around this barrier is to restrict the class of states. Stabilizer states are the natural candidate: they are the states produced from $|0^n\rangle$ by Clifford circuits, they underlie quantum error-correcting codes, measurement-based computation and randomized benchmarking, and there are $2^{\Theta(n^2)}$ of them, so $\Omega(n)$ copies are necessary to identify one.

Timeline.

• Aaronson and Gottesman (2008, Identifying stabilizer states, talk, http://pirsa.org/08080052/) described a procedure identifying an unknown stabilizer state from $O(n^2)$ copies with single-copy measurements, and a variant using $O(n)$ copies with measurements collective across all copies.
• Low (2009, arXiv:0907.2833) showed that a Clifford unitary can be identified from $O(n^2)$ uses, or $O(n)$ with access to its inverse.
• Rocchetto (2017, arXiv:1705.00345) showed that stabilizer states are PAC-learnable efficiently.
• Montanaro (2017, arXiv:1707.04012) gave the algorithm of this mission: $O(n)$ copies, collective measurements on at most two copies at a time, failure probability exponentially small in $n$. Zhao, Pérez-Delgado and Fitzsimons obtained a related $O(n)$-copy algorithm for graph states independently (arXiv:1510.03742).

Bell sampling became a standard tool after this paper, for instance in stabilizer testing (Gross, Nezami and Walter, arXiv:1712.08628), so a machine-checked version of its analysis is a reusable base.

Setting

A state of $n$ qubits is a vector $\psi:\{0,1\}^n\to\mathbb C$; its complex conjugate $\psi^*$ is taken entrywise in the computational basis. The paper uses the four $2\times2$ matrices

$$\sigma_{00}=\begin{pmatrix}1&0\\0&1\end{pmatrix},\ \sigma_{01}=\begin{pmatrix}0&1\\1&0\end{pmatrix},\ \sigma_{10}=\begin{pmatrix}1&0\\0&-1\end{pmatrix},\ \sigma_{11}=\sigma_{10}\sigma_{01}=\begin{pmatrix}0&1\\-1&0\end{pmatrix},$$

which are the Pauli matrices up to the factor $-i$ on $\sigma_{11}$. For a string $s\in\{0,1\}^{2n}$, $\sigma_s=\sigma_{s_1s_2}\otimes\cdots\otimes\sigma_{s_{2n-1}s_{2n}}$; strings are added bitwise, $s\oplus t$.

The Bell basis of $\mathbb C^4$ is $|\sigma_{00}\rangle=\frac1{\sqrt2}(|00\rangle+|11\rangle)$, $|\sigma_{01}\rangle=\frac1{\sqrt2}(|01\rangle+|10\rangle)$, $|\sigma_{10}\rangle=\frac1{\sqrt2}(|00\rangle-|11\rangle)$, $|\sigma_{11}\rangle=\frac1{\sqrt2}(|01\rangle-|10\rangle)$. Bell sampling on $2n$ qubits $A_1,\dots,A_n,B_1,\dots,B_n$ measures each pair $A_iB_i$ in the Bell basis and returns a string $r\in\{0,1\}^{2n}$. On two copies $|\psi\rangle|\psi\rangle$ (first copy on the $A$'s) the outcome $r$ has probability $p_\psi(r)=|\langle\sigma_r|\,\psi\otimes\psi\rangle|^2$.

A stabilizer state is $\psi=U|0^n\rangle$ for a Clifford unitary $U$ (a unitary normalising the Pauli group). Its stabilizer set $T(\psi)\subseteq\mathbb F_2^{2n}$ is the set of strings $t$ for which $\psi$ is an eigenvector of $\sigma_t$, i.e. those $\sigma_t$ that lie in the stabilizer group of $\psi$ up to a phase.

Algorithm 1. Bell-sample two fresh copies to get $r_0$; repeat $2n$ times to get $r_1,\dots,r_{2n}$; find a basis $B$ of $\operatorname{span}\{r_i\oplus r_0\}$; for each element of $B$ measure one copy of $\psi$ in the eigenbasis of the corresponding (Hermitian) Pauli matrix $M$ to learn whether $M|\psi\rangle=+|\psi\rangle$ or $-|\psi\rangle$. It uses $5n+2$ copies.

Formalization targets

Goal: Theorem 1, explicit form

For every $n$ and every $n$-qubit stabilizer state $\psi$, with the $2n+1$ Bell samples independent,

$$\Pr\bigl[\operatorname{span}\{r_i\oplus r_0:1\le i\le 2n\}=T(\psi)\bigr]\ \ge\ 1-2^{-n},$$

and for every basis $b_1,\dots,b_n$ of $T(\psi)$ with Hermitian Paulis $M_j$, each $M_j\psi=\pm\psi$ and every vector with the same eigenvalues under all $M_j$ is a scalar multiple of $\psi$. Together: Algorithm 1 identifies $\psi$ except with probability at most $2^{-n}$.

Milestones

1. $\sigma_s\sigma_t=\pm\sigma_{s\oplus t}$.
2. Lemma 2: $p_\psi(r)=|\langle\psi|\sigma_r|\psi^*\rangle|^2/2^n$.
3. The Bell-sampling probabilities of a unit vector sum to $1$.
4. For a stabilizer state, $|\psi^*\rangle=c\,\sigma_{10}^{\otimes S}|\psi\rangle$ with $|c|=1$.
5. Eqn (1): $p_\psi(r)=|\langle\psi|\sigma_r\sigma_{10}^{\otimes S}|\psi\rangle|^2/2^n$.
6. $T(\psi)$ is an $n$-dimensional subspace of $\mathbb F_2^{2n}$.
7. $\langle\psi|\sigma_t|\psi\rangle=0$ for $t\notin T(\psi)$.
8. $p_\psi$ is uniform on a coset $\{t\oplus s:t\in T\}$.
9. For two independent outcomes, $r_1\oplus r_2$ is uniform on $T$.
10. $T$ and the signs on a basis of $T$ determine $\psi$ up to a scalar.
11. $2n$ uniform samples of an $n$-dimensional $\mathbb F_2$-space fail to span it with probability at most $2^{-n}$.

Significance

The theorem gives a learning algorithm whose copy complexity $O(n)$ is optimal and whose measurements are simple: one Bell measurement on corresponding qubits of two copies. Its analysis isolates a structural fact about stabilizer states, that Bell sampling on two copies produces a uniformly random element of a coset of the stabilizer subspace, which is the engine of later work on stabilizer testing and on learning states with few non-Clifford gates.

The result is proved in the paper; no machine-checked proof of it is known. A complete formalization adds: the stabilizer formalism in a form usable from the definition "$U|0^n\rangle$ for a Clifford $U$" (the subspace $T$, its dimension, vanishing expectations off $T$, determination by signs); the conjugation identity, which the paper takes from a normal form cited from the literature; and the probabilistic bookkeeping of the algorithm with its exact constants.

Difficulty

The probability calculations (Lemma 2, eqn (1), the union bound) are finite sums. The difficulty lies in the stabilizer structure. The platform's definition of a stabilizer state is the image of $|0^n\rangle$ under a Clifford unitary; from it one must derive that the strings whose $\sigma_t$ fixes $\psi$ up to phase form an $n$-dimensional subspace, that all other Pauli expectations vanish, and that $\psi^*$ differs from $\psi$ by a diagonal Pauli. The paper obtains the last fact from the Dehaene–De Moor normal form $\psi\propto\sum_{x\in A}i^{\ell(x)}(-1)^{q(x)}|x\rangle$, a cited theorem whose proof is not on the page; formalizing either that normal form or a direct substitute is the central step. The natural shortcut, treating $T$ as given with "uniform outcomes on $T$" as a hypothesis, proves only the counting lemma and is ruled out below.

Formalization scope

• States are StabilizerRank.QState n = (Fin n → Bool) → ℂ and stabilizer states are StabilizerRank.IsStabilizerState (published platform definition, referenced). Qubit $i$ is coordinate $i$, false $=0$.
• Strings $\{0,1\}^{2n}$ are encoded as Fin n → ZMod 2 × ZMod 2, coordinate $i$ the pair $(s_{2i-1},s_{2i})$ of qubit $i$; $\oplus$ is +.
• $\sigma_{11}$ is the page's $\begin{pmatrix}0&1\\-1&0\end{pmatrix}$, not the Pauli $Y$. The "corresponding Pauli matrix" of step 5 is the Hermitian $(-i)^{\#\{i:t_i=11\}}\sigma_t$; the page does not fix this phase.
• The Bell outcome law is the Born rule with $\psi(x)\psi(y)$ the amplitude of $|\psi\rangle|\psi\rangle$ at $|x\rangle_A|y\rangle_B$.
• Algorithm 1 is modelled by its outcome law: the $2n+1$ samples are independent (fresh copies), and an event has probability $\sum \mathbf 1_E\,p_\psi(r_0)\prod_i p_\psi(r_i)$. Step 5 is deterministic once a basis of $T$ is known, and is stated as a property of every such basis.
• The explicit constants of p. 2 replace "$O(n)$" and "exponentially small": $2n+1$ Bell samples, success probability at least $1-2^{-n}$ (the page's "fails with probability at most $2^{-n}$", in a form that a mis-normalised outcome law cannot satisfy). The count $5n+2$ and "at most two copies at a time" are properties of the model, not separate clauses. The running time $O(n^3)$ is not formalized.
• Lemma 2 is stated for every vector, not only unit vectors (the identity is homogeneous). The conjugation identity carries a unit phase $c$, which the page omits. "$\langle\psi|M|\psi\rangle=0$ for $M\notin G$" is stated for strings outside $T$.
• Ruled out: $T$ as a hypothesis (it is always computed from $\psi$), dropping the reference sample $r_0$ or the independence of the samples, a degenerate outcome law, and reading "identifies" as "the samples span $T$" without the sign step.

Needed infrastructure: Kronecker-product manipulations of $\sigma_s$ indexed by bit strings, the Bell basis as an orthonormal basis of $(\mathbb C^2\otimes\mathbb C^2)^{\otimes n}$, the stabilizer formalism over $\mathbb F_2^{2n}$, and counting hyperplanes of finite $\mathbb F_2$-spaces. The stabilizer-formalism layer and the union bound are reusable beyond this mission. Contributions to any milestone are welcome, in particular direct proofs of milestones 4, 6 and 7 from the Clifford definition.

Selected references

• A. S. Holevo, Bounds for the quantity of information transmitted by a quantum communication channel, Problems of Information Transmission 9:177–183, 1973.
• D. Gross, S. Nezami and M. Walter, Schur–Weyl duality for the Clifford group with applications: property testing, a robust Hudson theorem, and de Finetti representations, Comm. Math. Phys. 385:1325–1393, 2021. https://arxiv.org/abs/1712.08628
• A. Montanaro, Learning stabilizer states by Bell sampling, arXiv preprint, 2017. https://arxiv.org/abs/1707.04012
• S. Aaronson and D. Gottesman, Identifying stabilizer states, PIRSA talk, 2008. http://pirsa.org/08080052/
• R. Low, Learning and testing algorithms for the Clifford group, Phys. Rev. A 80:052314, 2009. https://arxiv.org/abs/0907.2833
• A. Rocchetto, Stabiliser states are efficiently PAC-learnable, arXiv preprint, 2017. https://arxiv.org/abs/1705.00345
• L. Zhao, C. Pérez-Delgado and J. Fitzsimons, Fast graph operations in quantum computation, Phys. Rev. A 93:032314, 2016. https://arxiv.org/abs/1510.03742
• J. Dehaene and B. De Moor, Clifford group, stabilizer states, and linear and quadratic operations over GF(2), Phys. Rev. A 68:042318, 2003. https://arxiv.org/abs/quant-ph/0304125
• M. Van den Nest, Classical simulation of quantum computation, the Gottesman–Knill theorem, and slightly beyond, Quantum Inf. Comput. 10:258, 2010. https://arxiv.org/abs/0811.0898
• S. Aaronson, The learnability of quantum states, Proc. R. Soc. A 463:3089, 2007. https://arxiv.org/abs/quant-ph/0608142