一句话：提出 QSE 符号执行框架与符号 stabilizer 态，高效分析量子纠错程序中的 Pauli 错误。
本文针对量子纠错（QEC）程序难以高效调试和分析的问题，提出符号执行框架 QSE。它将符号变量融入量子态与测量结果，并通过操作语义证明其可靠性；进一步定义符号 stabilizer 态，用符号表达式刻画 stabilizer 生成元的相位。基于该框架，可用符号表达式描述 QEC 中可能的离散 Pauli 错误，避免依赖模拟器采样。作者实现原型工具 QuantumSE.jl，并在量子重复码、Kitaev toric 码与量子 Tanner 码上实验，成功调试超过 1000 个量子比特的 QEC 程序。工具还支持 stabilizer 线路采样，虽初始化慢于 Stim，但采样速率更快。
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.