AI 中文总结
本文扩展了位向量抽象验证框架，支持CSS码、高距离表面码及大规模GHZ电路，证明可靠性并验证622个突变体，显著提升量子电路验证的规模与效率。
AI 中文摘要
随着电路规模增大，对量子电路的正式验证变得困难，因为对希尔伯特空间的穷举推理计算代价高昂。在先前的工作[1]中，我们引入了一种位向量抽象，将叠加态跟踪与基态行为分离，从而能够对由H、X和C-NOT门构成的固定规模检错与纠缠电路进行基于SMT的验证。本文在五个方向上扩展了该框架。第一，我们将正确性属性推广到参数化的重复和级联相位翻转码，支持最多101个逻辑元素。第二，我们验证了由任意奇偶校验矩阵指定的CSS码的综合征提取，包括Steane码、[[15,7,3]]汉明码、[[15,1,3]]里德-穆勒码以及距离最高达101的旋转表面码。我们考虑任意错误模式、检测到指定权重以及使用经典解码器的恢复，并提供超出每种码纠错或检测能力的反例。第三，我们刻画了{H,X,C-NOT}片段，在该片段上抽象能忠实表示希尔伯特空间语义。我们证明了可靠性，通过反例展示了必要性，针对态矢量模拟验证了该刻画，并证明了原始工作中的六个引理。第四，一项使用13个算子的突变研究识别了等价突变体，并在所评估的故障模型内检测出全部622个非等价突变体。第五，一个直接的Z3实现在一台16GB笔记本电脑上验证了跨三种拓扑、最多262,144个量子比特的GHZ电路。随机H+C-NOT网络显示，当输出依赖于许多输入时，验证成本随深度急剧上升。该方法不针对通用稳定子电路、Y型稳定子、容错协议或物理噪声；我们指出了解决这些情况所需的扩展。
英文摘要
Formal verification of quantum circuits becomes difficult as circuit size grows because exhaustive reasoning over the Hilbert space is computationally expensive. In previous work [1], we introduced a bit-vector abstraction that separates superposition tracking from basis-state behavior, enabling SMT-based verification of fixed-size error-detection and entanglement circuits built from H, X, and C-NOT gates. This paper extends the framework in five directions. First, we generalise correctness properties to parametrised repetition and concatenated phase-flip codes with up to 101 logical elements. Second, we verify syndrome extraction for CSS codes specified by arbitrary parity-check matrices, including the Steane, [[15,7,3]] Hamming, [[15,1,3]] Reed-Muller, and rotated surface codes with distances up to 101. We consider arbitrary error patterns, detection up to a specified weight, and recovery using a classical decoder, with counterexamples beyond each code's correction or detection capability. Third, we characterize the {H,X,C-NOT} fragment for which the abstraction faithfully represents Hilbert-space semantics. We prove soundness, demonstrate necessity with counterexamples, validate the characterisation against state-vector simulation, and prove the six lemmas from the original work. Fourth, a mutation study using 13 operators identifies equivalent mutants and detects all 622 non-equivalent mutants within the evaluated fault model. Fifth, a direct Z3 implementation verifies GHZ circuits with up to 262,144 qubits across three topologies on a 16GB laptop. Random H+C-NOT networks show verification cost rises sharply with depth when outputs depend on many inputs. The approach does not target general stabilizer circuits, Y-type stabilizers, fault-tolerant protocols, or physical noise; we identify extensions needed to address these cases.
CommentsAccepted for publication in SN Computer Science, final version will be available through journal once published. Abstract is modified to account for arXiv character count
