We define a symbolic execution framework QSE for quantum programs by integrating symbolic variables into quantum states and the outcomes of quantum measurements. The soundness theorem of QSE is proved. We further introduce symbolic stabilizer states, which facilitate the efficient analysis of quantum error correction programs. Within the QSE framework, we can use symbolic expressions to characterize the possible adversarial errors in quantum error correction, 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. With experiments on representative quantum error correction codes, including quantum repetition codes, Kitaev's toric codes, and quantum Tanner codes, we demonstrate the efficiency of QuantumSE.jl for debugging quantum error correction programs with over 1000 qubits. In addition, as a by-product of QSE, QuantumSE.jl's sampling functionality for stabilizer circuits also outperforms the state-of-the-art stabilizer simulator, Google's Stim, in the experiments.

翻译：我们定义了一个用于量子程序的符号执行框架QSE，通过将符号变量集成到量子态和量子测量结果中，证明了QSE的可靠性定理。进一步引入符号稳定子态，以高效分析量子纠错程序。在QSE框架内，可利用符号表达式刻画量子纠错中可能的对抗性错误，相较于现有依赖模拟器采样的方法，实现了显著提升。我们基于符号稳定子态的支持，在原型工具QuantumSE.jl中实现了QSE。通过对包括量子重复码、Kitaev环面码和量子Tanner码在内的典型量子纠错码的实验，展示了QuantumSE.jl在调试超过1000个量子比特的量子纠错程序方面的效率。此外，作为QSE的副产品，QuantumSE.jl针对稳定子电路的采样功能在实验中优于当前最先进的稳定子模拟器Google Stim。