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.

翻译：我们定义了QSE，一种通过将符号变量融入量子态和量子测量结果中的量子程序符号执行框架。通过一个确保操作语义中符号执行正确性的定理，建立了QSE的可靠性。我们进一步引入了符号稳定子状态，以符号化稳定子生成元的相位，用于高效分析量子纠错（QEC）程序。在QSE框架内，我们可以利用符号表达式刻画QEC中可能的离散泡利错误，相较于依赖模拟器采样的现有方法，实现了显著改进。我们借助符号稳定子状态的支持，在原型工具QuantumSE.jl中实现了QSE。在代表性QEC码（包括量子重复码、Kitaev环面码和量子Tanner码）上的实验表明，QuantumSE.jl能够高效调试包含超过1000个量子比特的QEC程序。此外，通过将测量结果的符号表达式中的具体值替换，QuantumSE.jl还配备了用于稳定子电路的采样功能。尽管初始化时间比最先进的稳定子模拟器Google的Stim更长，但QuantumSE.jl在实验中的采样速率更快。