StabQ：基于加权稳定子表示的量子程序分析
StabQ: Quantum Program Analysis via Weighted Stabilizer Representations
AI总结：
本研究提出基于稳定子表示的量子程序分析框架StabQ，通过扩展稳定子符号执行、构建Tableau Chain及整合状态优化机制，在三类基准上验证其可支持多项量子程序分析任务。
AI中文摘要：
量子程序分析因量子程序的指数级大状态空间及精确刻画其执行行为的难度而颇具挑战性。尤其是非克利福德（Clifford）操作会引入额外复杂性，限制了基于稳定子（stabilizer）技术的适用性。尽管稳定子表示能为克利福德电路提供紧凑描述，但其有限的表达能力使其无法直接支持通用量子程序分析。本研究提出StabQ，一种基于稳定子表示的量子程序分析符号执行框架。StabQ通过引入符号状态表示，在保留执行语义的同时捕获并传播量子状态演化，将基于稳定子的符号执行扩展至仅含克利福德的程序之外。基于该表示，StabQ构建了一个Tableau Chain，用于表示程序执行过程中中间符号状态的演化，支持对量子程序执行的可复用分析。此外，StabQ整合了Tableau合并与全局相位恢复机制，以缓解执行过程中符号状态的增长。基于Tableau Chain，StabQ支持多项量子程序分析任务，包括量子状态重构、纠缠分析及克利福德属性检测。我们在三个基准套件——Algorithms、MQT Bench和QASMBench上对StabQ进行评估，结果表明StabQ构建了语义一致的符号模型，准确保留了量子状态演化，且能有效支持各类量子程序的下游分析任务。
英文摘要：
Quantum program analysis remains challenging due to the exponentially large state space of quantum programs and the difficulty of precisely characterizing their execution behavior. In particular, non-Clifford operations introduce additional complexity that limits the applicability of stabilizer-based techniques. Although stabilizer representations provide compact descriptions for Clifford circuits, their limited expressiveness prevents them from directly supporting general quantum program analysis. In this work, we propose StabQ, a symbolic execution framework for quantum program analysis based on stabilizer representations. StabQ extends stabilizer-based symbolic execution beyond Clifford-only programs by introducing a symbolic state representation that captures and propagates quantum state evolution while preserving execution semantics. Based on this representation, StabQ constructs a Tableau Chain that represents the evolution of intermediate symbolic states throughout program execution and enables reusable analysis of quantum program executions. Furthermore, StabQ incorporates tableau consolidation and global-phase recovery mechanisms to mitigate symbolic state growth during execution. Building upon the Tableau Chain, StabQ supports multiple quantum program analysis tasks, including quantum state reconstruction, entanglement analysis, and Clifford-property detection. We evaluate StabQ on three benchmark suites---Algorithms, MQT Bench, and QASMBench. The results demonstrate that StabQ constructs semantically consistent symbolic models, accurately preserves quantum state evolution, and effectively supports downstream analysis tasks across diverse quantum programs.
