Symbolic Execution for Quantum Error Correction Programs

TL;DR

This work extends symbolic execution to quantum programs with classical control by introducing Quantum Symbolic Execution (QSE) and symbolic stabilizer states, enabling scalable analysis and verification of quantum error correction (QEC) programs. It proves soundness and adequacy theorems and implements a prototype, QuantumSE.jl, capable of handling stabilizer codes such as repetition codes, Kitaev's toric codes, and quantum Tanner codes with over 1000 qubits. By using symbolic measurements and symbolic Pauli gates, QSE avoids exponential path explosion from both measurement outcomes and error enumeration, and it supports conditional Pauli operations without forking paths. Experimental results show competitive bug-finding capability, favorable scaling relative to sampling-based approaches, and a clear roadmap for solver- and technique-driven improvements in future work.

Abstract

We define QSE, a symbolic execution framework for quantum programs by integrating symbolic variables into quantum states and the outcomes of quantum measurements. The soundness of QSE is established through a theorem that ensures the correctness of symbolic execution within operational semantics. We further introduce symbolic stabilizer states, which symbolize the phases of stabilizer generators, for the efficient analysis of quantum error correction (QEC) programs. Within the QSE framework, we can use symbolic expressions to characterize the possible discrete Pauli errors in QEC, providing a significant improvement over existing methods that rely on sampling with simulators. We implement QSE with the support of symbolic stabilizer states in a prototype tool named QuantumSE.jl. Our experiments on representative QEC codes, including quantum repetition codes, Kitaev's toric codes, and quantum Tanner codes, demonstrate the efficiency of QuantumSE.jl for debugging QEC programs with over 1000 qubits. In addition, by substituting concrete values in symbolic expressions of measurement results, QuantumSE.jl is also equipped with a sampling feature for stabilizer circuits. Despite a longer initialization time than the state-of-the-art stabilizer simulator, Google's Stim, QuantumSE.jl offers a quicker sampling rate in the experiments.

Figures (11)

• Figure 1: A QEC program (Lines 4-12) for the three-qubit bit-flip code with code distance $3$. Ensuring the program is bug-free requires that for any initial state $\alpha\lvert 000\rangle+\beta\lvert 111\rangle$ within the code space, the final state remains $\alpha\lvert 000\rangle+\beta\lvert 111\rangle$ after error injection (Lines 1-3) and execution of the QEC program (Lines 4-12). Error injection injects errors that the QEC code can tolerate into the quantum state, and then the QEC program corrects these errors. Here, the possible errors correspond to variables $e_1,e_2,e_3 \in\{0,1\}$ that satisfy $e_1+e_2+e_3 \leq 1$ (up to one $X$ error occurs). We also refer to the errors $X^{e_1}, X^{e_2}, X^{e_3}$ introduced during error injection as "adversarial" because of their potential to disrupt the integrity of information in quantum states.
• Figure 2: Illustration of symbolic execution for the quantum program in \ref{['fig:running_example_decoder']}.
• Figure 3: Transition rules for operational semantics. For external call $\bar{y} \coloneqq{} F(\bar{x})$ with $\bar{x} = x_1,x_2,\ldots,x_m$ and $\bar{y} = y_1,y_2,\ldots, y_n$, we use $\sigma[F(\sigma(\bar{x}))/\bar{y}]$ as a shorthand for $\sigma[f_1/y_1,f_2/y_2,\ldots,f_n/y_n]$ provided by $(f_1, f_2, \ldots, f_n) = F(\sigma(x_1), \sigma(x_2), \ldots, \sigma(x_m))$. For sequential composition $S_1;S_2$, we make convention that $\downarrow;S_2 = S_2$.
• Figure 4: Symbolic execution rules for quantum programs. For external call $\bar{y} \coloneqq{} F(\bar{x})$, $C_{F}(\widetilde{\sigma}(\bar{x}), \bar{s}_{\bar{y}})$ is the condition that the input and output should satisfy for $F$, i.e., $C_{F}(\bar{x}, F(\bar{x})) \equiv \texttt{true}$ for any concrete values $\bar{x}$, where $\bar{s}_{\bar{y}} = s_{y_1}, s_{y_2}, \ldots, s_{y_n}$ is a list of newly introduced symbols for output variables $\bar{y} = y_1,y_2,\ldots,y_n$.
• Figure 5: An example of QEC programs evaluated in RQ1 and the performance results of RQ1.

Theorems & Definitions (17)

• definition 1: Symbolic Quantum State
• definition 2: Quantum operations over symbolic quantum states
• definition 3: Instantiation
• lemma 1: Correctness of function $ut$
• lemma 2: Correctness of function $m$
• theorem 1: Soundness of QSE
• definition 4: Symbolic stabilizer state
• definition 5: Quantum operations over symbolic stabilizer states
• lemma 3
• theorem 2: Adequacy of symbolic stabilizer states