量子错误检测与纠缠的位向量抽象形式验证
Bit-Vector Abstractions to Formally Verify Quantum Error Detection & Entanglement
AI总结：
本文提出位向量抽象方法用于验证量子电路，有效分离叠加与功能行为，验证了2-3-9量子码错误检测电路、贝尔态和GHZ态生成电路，展示了方法的高效性和可扩展性。
摘要：
随着量子比特数量的增加，量子电路变得愈加复杂，其状态空间迅速增长，使传统技术难以进行功能验证。本文提出了一种基于位向量抽象的方法，用于形式验证量子电路，能够分离叠加和功能行为。该方法应用于2-3-9量子码错误检测电路、贝尔态和GHZ态生成电路。错误检测电路和贝尔态生成电路在1秒内和25MB内存下完成验证，GHZ电路在3分钟内使用最多23.2GB内存完成验证。结果展示了所提方法的通用性、可扩展性和有效性。
英文摘要：
As the number of qubits increases, quantum circuits become more complex and their state space grows rapidly. This makes functional verification challenging for conventional techniques. Ensuring correctness is especially critical for quantum error correction and entanglement generation. This paper presents a novel application of bit-vector based abstraction methodology for formal verification of quantum circuits where superposition and functional behaviour can be decoupled. The approach is applied to error detection circuits for 2-qubit, 3-qubit, and Shor 9-qubit quantum codes, as well as Bell-state and GHZ-state generation circuits. The error detection circuits and the Bell-state generation circuit are verified in less than a second and 25MB memory. GHZ circuits with up to 8,192 qubits are verified in under three minutes using a maximum of 23.2 GB of memory. The results demonstrate the versatility, scalability, and effectiveness of the proposed approach.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
