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的稳定子电路采样功能在性能上超越了谷歌最先进的稳定子模拟器Stim。