Advanced Equivalence Checking for Quantum Circuits
量子计算将改变我们解决某些问题的方式。它有望大大加快许多化学、金融和机器学习应用的速度。然而，为了利用这些承诺，在能够在实际设备上执行概念量子算法之前，需要使用由编译、分解或映射等步骤组成的复杂设计流程。这导致在不同抽象层次上的描述可能彼此显著不同。底层设计问题的复杂性不仅需要为单个步骤提供有效的解决方案，而且还需要验证在所有抽象级别中保留了最初预期的功能。这激发了量子线路的等价性检验方法。然而，大多数现有方法受到经典领域的启发，并且仅仅被扩展以支持量子线路（即，不仅依赖于0和1，而且还采用叠加和纠缠的电路）。在这项工作中，我们提出了一种先进的方法，它采取不同的范例的量子线路不仅是一种负担，但作为一个机会。事实上，所提出的方法明确地利用了量子计算特有的特性，以克服现有方法的缺点。我们表明，通过利用量子线路的可逆性，复杂性可以保持在许多情况下是可行的。此外，我们表明，在对比的经典领域，模拟是非常强大的验证量子线路。实验评估证实，由此产生的方法允许进行等价性检查显着快于以往任何时候-在许多情况下，只有一个单一的模拟运行是足够的。拟议方法的实施情况可在https://iic.jku.at/eda/research/quantum_verification/上公开查阅。
2020-10-27 cs.ET quant-ph
Equivalence Checking of Sequential Quantum Circuits
我们定义了一个形式化的框架，用于序列量子线路的等价性检验。我们采用的模型是一个量子态机，这是一个自然的量子广义的Mealy机。检验量子线路的一个主要困难（但不存在于检验经典线路中）是量子线路的状态空间是连续的。这个困难是解决我们的主要定理表明，两个量子Mealy机的等价性检查可以与输入序列，是从一些选定的基础（这是有限的），并有一个长度平方的尺寸的状态希尔伯特空间的机器。基于这一理论结果，我们开发了一个（据我们所知，第一个）算法来检查与运行时间$\mathcal{O}(2^{3m+5l}(2^{3m}+2^{3l}))$的顺序量子线路的等价性，其中$m$和$l$分别表示输入和内部量子比特的数量。我们的算法的复杂性是可比的，与已知的算法，用于检查经典的时序电路的意义上，都是指数的（qu）位的数量。几个案例研究和实验。
2022-09-10 quant-ph
Equivalence Checking of Quantum Circuits by Model Counting
本文将量子电路等价性问题图灵归约至加权模型计数，结合Pauli基定理与支持Toffoli门的WMC编码，并开源实现，性能优于基于ZX微积分和决策图的先进工具。
2024-03-27 quant-ph
QuBEC: Boosting Equivalence Checking for Quantum Circuits with QEC Embedding
QuBEC提出基于决策图的量子电路等价性验证方法，通过量子纠错嵌入处理冗余电路，在基准电路上验证时间最高减少271.49倍、节点数最高减少798.31倍，显著提升验证效率。
2023-09-19 cs.ET quant-ph
Towards Equivalence Checking of Classical Circuits Using Quantum Computing
针对经典电路等价性检查问题，本研究提出利用 Grover's algorithm 进行求解，分析了实施过程中的潜在陷阱，并提出了一种量子计算工作概念，为未来相关解决方案奠定基础。
2024-08-26 cs.ET quant-ph
Partial Equivalence Checking of Quantum Circuits
针对现有方法无法验证量子比特部分初始化的量子电路观测等价性的问题，本研究证明了量子电路部分等价性的充要条件，设计了对应验证算法，实验验证了其通用性、效率与有效性，可助力量子程序编译实现更大胆的优化。
2022-08-16 quant-ph
Efficient equivalence checking of Clifford-U circuits with shared single-qubit unitaries
The University of Osaka（大阪大学）；The University of Tokyo（东京大学）
本文提出一种高效算法，用于判断由任意单量子比特层与Clifford层交替构成的电路对，在共享单量子比特层的情况下是否等价，适用于变分量子算法和Trotter分解的哈密顿量模拟。
2026-03-13 quant-ph
Equivalence, Identity, and Unitarity Checking in Black-Box Testing of Quantum Programs
本文提出三种新算法，解决量子程序黑盒测试中的等价性、同一性和幺正性检查问题，并优化参数选择，实验验证其有效性。
2024-05-24 cs.SE quant-ph
Equivalence Checking of Dynamic Quantum Circuits
尽管近年来量子计算发展迅速，但最先进的量子器件仍然只包含非常有限数量的量子比特。在近期量子设备中执行更现实算法的一种可能方法是采用动态量子线路，其中测量可以在电路期间发生，并且其结果用于控制电路的其他部分。这种技术可以帮助显著减少实现量子算法的给定精度所需的资源。然而，由于这种类型的量子线路更灵活，它们的验证更具挑战性。本文给出了动态量子线路的形式定义，并提出用线性算子系综来描述其功能。基于这种新的语义，如果两个动态量子线路具有相同的功能，则它们是等价的。我们进一步提出并实现了两个基于决策树的动态量子线路等价性检验算法。实验表明，将经典逻辑嵌入到传统的量子线路中不会带来显著的时间和空间负担。
2021-06-03 quant-ph
Approximation Methods for Simulation and Equivalence Checking of Noisy Quantum Circuits
University of Chinese Academy of Sciences（中国科学院大学）；School of Informatics, University of Edinburgh（爱丁堡大学信息学院）；Centre for Quantum Software and Information, University of Technology Sydney（悉尼科技大学量子软件与信息研究中心）
本文提出了一种基于张量网络和奇异值分解的近似方法，用于高效模拟和验证具有200个量子比特和20个噪声操作符的QAOA电路，提升了低噪声条件下的可扩展性和速度。
2025-12-11 quant-ph
Model Checking for Verification of Quantum Circuits
在这次演讲中，我们将描述一个基于断言的验证（ABV）的量子线路的框架，通过应用我们以前的工作中开发的量子系统的模型检查技术，其中：（i）无噪声和有噪声的量子线路分别建模为算子和超算子值的过渡系统，这两者都可以进一步表示为张量网络。(ii)量子断言由Birkhoff-von Neumann量子逻辑的时间扩展指定。它们的语义定义的基础上的设计决策：它们将被用于验证的量子线路的模拟经典计算机或人类推理，而不是量子物理实验（例如，测试通过测量）;（iii）可达性分析和模型检查的量子线路的算法开发的基础上收缩张量网络。我们观察到，许多优化技术计算关系产品中使用的BDD为基础的模型检测算法可以概括为收缩张量网络的量子线路。
2021-04-23 cs.AR cs.LO quant-ph
Equivalence checking of quantum circuits by nonlocality
假设两个量子线路芯片位于不同的地方，我们没有任何先验知识，也看不到内部结构。如果我们想确定它们是否具有相同的功能，我们应该怎么做？本文从量子非定域性的观点出发，证明了这一现实问题是完全可以解决的。具体来说，我们设计了一个优雅的协议，检查潜在的量子非局域性，最强的非局域性可以观察到当且仅当两个量子线路是彼此等效的。我们表明，该协议也工作近似，两个量子线路之间的距离可以准确地计算所观察到的量子非局域性的分析方式。此外，我们的协议的计算成本是独立的比较量子线路的大小。最后，我们还讨论了将该协议推广到多部情况的可能性，即，如果我们对多个量子线路进行等价性检验，我们试图一次性解决问题。
2022-08-10 quant-ph
Quantum Circuit Equivalence Checking: A Tractable Bridge From Unitary to Hybrid Circuits
Université Paris-Saclay（巴黎萨克雷大学）；CEA, List（法国原子能和替代能源委员会，列表实验室）；CNRS, CentraleSupélec, ENS Paris-Saclay, Inria, Laboratoire Méthodes Formelles（法国国家科学研究中心，中央理工-高等电力学院，巴黎萨克雷高等师范学院，法国国家信息与自动化研究所，形式方法实验室）
本文提出通过延迟测量和分离投影技术，解决混合量子电路等价性检查问题，提升处理能力并发现 Qiskit 编译器的意外行为。
2025-11-27 cs.PL quant-ph
Equivalence Checking of Parameterized Quantum Circuits: Verifying the Compilation of Variational Quantum Algorithms
变分量子算法已经被引入作为一类有前途的量子-经典混合算法，其已经可以通过采用参数化的量子线路与当今可用的噪声量子计算硬件一起使用。考虑到量子线路编译的非平凡性质和量子计算的微妙之处，验证这些参数化电路是否被正确编译是至关重要的。已经存在处理无参数电路的已建立的等价性检查程序。然而，还没有提出能够处理具有参数的电路的方法。这项工作填补了这一空白表明，验证参数化电路的等价性可以实现在一个纯粹的符号的方式使用基于ZX-演算的等价性检查方法。同时，利用参数化电路固有的自由度，用传统的方法可以有效地证明不等式。我们实现了相应的方法，并证明了所得到的方法是完整的。实验评估（使用Qiskit提供的整个参数化模拟电路库作为基准）证明了所提出的方法的有效性。该实现是开源的，并作为等价性检查工具QCEC（https：//github.com/cda-tum/qcec）的一部分公开提供，该工具是慕尼黑量子工具包（MQT）的一部分。
2022-10-21 cs.SC quant-ph
Approximate Equivalence Checking of Noisy Quantum Circuits
本文研究了在不可避免地存在量子噪声的NISQ（Noisy Intermediate-Scale Quantum）计算领域中等价性检验的基本设计自动化问题。（可能有噪声的）量子线路的近似等价的概念是基于Jamiolkowski保真度定义的，Jamiolkowski保真度测量当随机选择输入时两个超算子的输出状态之间的平均距离。利用张量网络的收缩，针对不同的噪声情况，提出了两种计算理想量子线路与其噪声实现之间保真度的算法.通过对真实NISQ电路的基准测试，验证了算法的有效性。与Qiskit中最先进的实现相比，实验结果表明，所提出的算法在效率和可扩展性方面都优于其他算法。
2021-06-03 cs.DS quant-ph
Manjushri: A Tool for Equivalence Checking of Quantum Circuits
Stony Brook University（石溪大学）；University of Texas at Austin（德克萨斯大学奥斯汀分校）；University of Wisconsin–Madison（威斯康星大学麦迪逊分校）
Manjushri是一种高效的量子电路等价性检查工具，能快速处理大规模量子电路验证。
2026-01-29 quant-ph
Equivalence Checking of Parameterised Quantum Circuits
针对参数化量子电路等价性检查需参数替换的难题，提出基于张量决策图的紧凑表示法，实现无需实例化的等价性验证，兼顾有效性与高效性。
2024-04-29 quant-ph
Fast equivalence checking of quantum circuits of Clifford gates
提出一种基于数学结果的确定性算法，可在O(n·m)时间内检查Clifford门量子电路的等价性，结合Stim模拟器在万级量子比特上实现比现有方法快数个数量级的验证。
2023-08-02 quant-ph
Scalable Equivalence Checking and Verification of Shallow Quantum Circuits
本文研究浅层量子电路的等价性检查问题，提出基于局部投影约束的判定方法，在经典计算机上实现了与量子比特数呈线性关系的时间与空间复杂度，并支持静态与运行时断言检查。
2025-04-02 cs.PL quant-ph
Quantangle-SAT: A Quantum SAT Solver Based on Entanglement and Equivalence Checking
Singapore Institute of Technology（新加坡理工学院）；National Cheng Kung University（国立成功大学）
本文提出基于纠缠和等价检查的新型量子SAT求解器，无需预先知道满足条件的解数量，计算效率高于量子计数，对随机布尔函数的期望时间复杂度为常数。
2026-04-20 quant-ph
Methods for Automated Equivalence Checking of Quantum Error-Correction Codes
Technical University of Munich（慕尼黑工业大学）；Munich Quantum Software Company GmbH（慕尼黑量子软件有限公司）
针对量子纠错码等价性判定问题，该研究提出统一框架与三种判定策略，构建分阶段混合检验器，在不同码规模与等价概念下实现高效检验。
2026-10-14 quant-ph
Quantum Markov chains: description of hybrid systems, decidability of equivalence, and model checking linear-time properties
在本文中，我们研究了一个模型的量子马尔可夫链，这是一个量子模拟的马尔可夫链，并得到取代概率的转移矩阵与量子操作。我们表明，这个模型是非常适合描述的混合动力系统，包括一个量子组件和一个经典的，虽然它具有相同的表达能力，另一个量子马尔可夫模型在文献中提出的。事实上，在量子信息处理中经常会遇到混合系统;例如，量子程序和量子协议都可以被视为混合系统。因此，我们进一步提出了一个称为混合量子自动机（HQA）的模型，可以用来描述这些从外部世界接收输入（动作）的混合系统。我们证明了HQA的语言等价问题是多项式时间可判定的。此外，我们将这个结果应用到量子马尔可夫链的迹等价问题，从而它也是多项式时间可判定的。最后，我们讨论了量子马尔可夫链的线性时间性质的模型检验，并表明可以成功地解决正则安全性的定量分析。
2015-06-30 cs.LO quant-ph
Strong equivalence of reversible circuits is coNP-complete
逻辑电路的等价判定是一个cNP完全问题。作为推论，判定可逆电路的弱等价问题，即忽略辅助位，也是coNP完全的。决定强等价（包括辅助位）的复杂性不太明显，可能取决于门设置。在这里，我们使用巴林顿定理来证明，决定强等价的可逆电路建立从弗雷德金门是coNP完全的。这意味着决定其他常用的通用可逆门集合的强等价性的coNP完全性，包括任何包含Toffoli或Fredkin门的门集合。
2013-07-02 cs.CC quant-ph
VeriQBench: A Benchmark for Multiple Types of Quantum Circuits
在本文中，我们介绍了VeriQBench -一个开源的量子线路的基准测试。它提供了各种电路类型的高级量子电路抽象，包括1）组合，2）动态，3）顺序和4）变化量子线路，其中几乎涵盖了文献中所有现有类型的量子线路。同时，VeriQBench是一个通用的基准，可以用于验证不同应用的量子软件，如现有的工作所证明的，包括量子线路验证（例如，等价性检查[Hon+21 a; WLY 21]和模型检查[Yin 21]），仿真（例如，故障模拟），测试（例如，测试模式生成[CY 22]）和调试（例如，运行时断言[Li+20 b]）。所有电路都在OpenQASM中描述，并在Qiskit和QCOR仿真器上进行了验证。VeriQBench的发布网址是：https://github.com/Veri-Q/Benchmark，希望它能被其他研究人员使用。
2022-06-22 quant-ph
Simple proof of equivalence between adiabatic quantum computation and the circuit model
我们证明了绝热量子计算和量子计算在电路模型中的等价性。给出了一个显式绝热计算程序，该程序生成一个基态，从该基态可以提取答案。通过计算间隙来评估所需的时间量。我们表明，该过程是计算效率。
2007-02-26 quant-ph
Exact Equivalence between Quantum Adiabatic Algorithm and Quantum Circuit Algorithm
我们给出了一个严格的证明，证明了量子线路算法可以转化为量子绝热算法，并且具有完全相同的时间复杂度。这意味着从$L$门的量子线路算法可以构造时间复杂度为$O(L)$的量子绝热算法。此外，我们的构造表明，通过适当地选择演化路径，可以指数地加速一些量子绝热算法。
2018-10-23 quant-ph
Cutoff Theorems for the Equivalence of Parameterized Quantum Circuits (Extended)
针对参数化量子电路优化易出错的问题，本文定义广义参数化电路类，提出基于截断的等价性验证方法及概率变体，可扩展至全局相位模等价性并设计高效采样过程。
2025-07-08 quant-ph
Verifying Results of the IBM Qiskit Quantum Circuit Compilation Flow
在实际物理设备上实现概念量子算法需要算法的量子线路描述经历某些变换，以便遵守硬件施加的所有约束。在这方面，各个高级电路组件首先被合成到量子计算机的支持的低级门集，然后被映射到目标的架构-利用几个优化来改善编译结果。存在用于此复杂任务的专用工具，例如，IBM的Qiskit、Google的Cirq、微软的QDK或Rigetti的Forest。然而，到目前为止，这些工具产生的电路几乎没有得到验证，这主要是由于检查两个量子线路是否确实实现了相同的功能的巨大复杂性。本文提出了一种有效的量子线路等价性检验方案--专门用于验证IBM Qiskit量子线路编译流程的结果。为此，我们结合了量子计算特有的特性，例如，其固有的可逆性以及关于编译的某些知识流入专用的等价性检查策略中。实验评估证实，所提出的方案允许验证即使是大型电路实例，在几秒钟或更短的时间内进行数万次操作，而最先进的技术经常超时或需要更多的运行时间。在https://github.com/iic-jku/qcec上公开了所提出的方法的相应开源实现。
2020-09-04 quant-ph
Phased outcome-complete simulation
NVIDIA（英伟达）；Microsoft Quantum（微软量子）
本文提出了一种能够精确跟踪全局相位的完整模拟方法，扩展了稳定器电路的多项式时间完整模拟算法，适用于包含单量子位旋转的非稳定器电路等重要家族。
2026-03-25 quant-ph
Ultra-Large-Scale Compilation and Manipulation of Quantum Circuits with Pandora
针对量子电路规模与实际应用需求间的巨大差距，提出开源多线程工具Pandora，基于电路重写实现大规模电路编译、等价性检查与流式资源估算，可处理数十亿门，优于TKET、Qiskit及MQT.QCEC。
2025-08-07 quant-ph
Quantum Indistinguishable Obfuscation via Quantum Circuit Equivalence
本文提出基于量子子路径和等价构造通用量子不可区分混淆的方案，通过增量修改子路径实现电路不可区分，并将区分器归约为多项式概率测试以控制安全性损失，为量子知识产权保护和安全委托计算提供新思路。
2024-11-19 quant-ph
Quasilinear Equivalence Checking for Detector Error Models
Unitary Foundation（Unitary基金会）
提出探测器错误模型（DEM）的等式理论，通过拟线性时间归约系统实现结构等价性判定，并应用于量子编译器验证与优化。
2026-06-15 cs.LO cs.PL cs.SE
Quantum-circuit guide to optical and atomic interferometry
原子（量子比特）和光学或微波（模态）相位估计协议在量子线路图方面处于相同的基础上。电路等效性被用来证明协议的等效性，实现海森堡极限，采用纠缠叠加的Fock状态，如N 00 N状态。关键的等价是那些解开电路，使相位信息只写在一个模式或一个量子位上的等价。福克态叠加相位估计电路被转换为使用纠缠相干态叠加;由此产生的协议更适合在实验室中实现，特别是在微波频率的量子位/腔设置中。
2009-09-04 quant-ph
Completeness for Fault Equivalence of Clifford ZX Diagrams
Quantinuum Ltd.（Quantinuum有限公司）；University of Oxford（牛津大学）
本文提出一套Clifford ZX图的完备故障等价重写规则，通过故障装置将图分为无故障部分和有噪声部分，从而为容错电路合成与优化提供正确性保证的框架。
2026-10-14 quant-ph
On the Quantum Circuit Complexity Equivalence
Nielsen \cite{Nielsen05}最近提出了以下问题：“在不使用辅助量子比特的情况下，精确实现指定的$% \mathit{n}$ -量子比特酉操作$U$所需的最小量子线路是多少？“尼尔森能够证明，最小尺寸电路的下界是由恒等式$I$和$U$之间的测地线的长度提供的，其中长度由$SU(2^{n})$上的适当Finsler度量定义。对于给定的Finsler结构$F$，我们证明了模拟$U$的最小电路尺寸与测地线长度和模拟参数成线性关系.作为一个推论，我们证明了$O(\frac{% n^{4}}{p}d_{F_{p}}^{2}(I,U)L_{F_{p}}(I,\tilde{U})) $的最高下限和最低上限的$Ω(n^{4}d_{F_{p}}^{3}(I,U))$，为标准的模拟技术。因此，我们的研究结果表明，通过标准模拟，人们不能期望一个更好的$n^{2}$倍的改善，从尼尔森，道林，顾和多尔蒂\cite{Nielsen06}的结果的上限。此外，我们的等价结果可以应用到流形上的任意路径，包括一个生成的几何。
2007-03-09 quant-ph
Perfect Computational Equivalence between Quantum Turing Machines and Finitely Generated Uniform Quantum Circuit Families
为了建立量子图灵机（QTM）和量子线路族（QCF）之间的计算等价性，利用Yao的量子线路模拟QTM，我们在前面介绍了基于无限基本门集合的一类均匀QCF，它已被证明在有界误差模拟下在计算上等价于多项式时间QTM（适当限制振幅）.这个结果意味着Bernstein和Vazirani为QTM引入的复杂性类BQP等于其对应的均匀QCF。然而，QTM的复杂性类ZQP和EQP似乎并不等于均匀QCF的对应物。本文引入了基于有限个基本门的均匀QCF的一个子类--非线性生成的均匀QCF，并证明了这类非线性生成的均匀QCF与多项式时间QTM完全等价，它们可以精确地相互模拟.这自然意味着BQP以及ZQP和EQP等于可重构生成的均匀QCF的相应复杂度类。
2008-12-05 quant-ph
Equivalence between classical and quantum dynamics. Neutral kaons and electric circuits
给出了有限个基态量子系统的$\mathrm{Schr\ddot{o}dinger}$动力学与经典动力学的等价性。等价是一种同构，它以单义的方式连接两个动力系统。我们处理的特殊情况下的中性K介子，并发现一类电网络唯一相关的K介子系统找到完整的映射之间的矩阵元素的K介子的有效哈密顿量和这些元素的经典动力学的网络。因此，测量K介子系统中的CP破坏的相关$ε$参数完全根据网络参数来确定。
2011-04-11 hep-ph quant-ph
Fault Tolerance by Construction
University of Oxford（牛津大学）
本文提出一种通过构造设计容错量子电路的框架，利用故障等价性确保电路在噪声下的正确性，并验证了其在综合征提取和猫态制备中的高效性。
2026-03-31 quant-ph
Phase transitions in quantum-circuit compilation
Università degli Studi di Padova（帕多瓦大学）；Istituto Nazionale di Fisica Nucleare, Sezione di Padova（意大利国家核物理研究所帕多瓦分部）；Padua Quantum Technologies Research Center（帕多瓦量子技术中心）
该研究将量子电路编译与多体自旋系统热力学关联，发现存在串扰时电路编译会出现相变，移除幺正等价约束后相消失，柯尔莫哥洛夫复杂度可促进有序相涌现。
2026-08-04 cond-mat.stat-mech quant-ph
When Close Enough Is Not Enough: Autoregressive Drift in Quantum Circuit Synthesis
研究容错计算的量子电路优化问题，用带结构化电路令牌化的变压器评估。在参数化电路上混合方法有效，在 Clifford + T 电路上存在自回归漂移致精确等效性下降，推理时策略和数据缩放可缓解但仍有问题。
2026-07-15 cs.AI cs.ET quant-ph
Symmetry-Checking in Band Structure Calculations on a Noisy Quantum Computer
The University of Melbourne（墨尔本大学）；CSIRO（联邦科学与工业研究组织）
本研究提出了一种在噪声量子计算机上识别双层石墨烯带结构交叉点对称性的方法，通过特征检查量子电路和去极化噪声模型评估其鲁棒性。
2025-06-25 quant-ph
Boolean Matching Reversible Circuits: Algorithm and Complexity
本文首次研究可逆电路的布尔匹配问题，证明在输入取反与置换下的等价性可量子多项式时间求解，实现设计自动化的量子指数加速，并给出输入输出同时取反下的不可能性结果。
2024-04-18 quant-ph
Reducing Trust Cost in Quantum Application Development Using AI
National Institute of Advanced Industrial Science and Technology (AIST)（产业技术综合研究所）
本研究针对量子应用开发中生成式AI带来的信任成本问题，提出整合AI与形式化验证的开发方法，通过划分组件降低人类检查负担，并以随机粒子系统时间演化实现为例验证方案。
2026-10-14 quant-ph
CertiQ: A Mostly-automated Verification of a Realistic Quantum Compiler
我们提出了CertiQ，一个验证框架，用于编写和验证Qiskit，最广泛使用的量子编译器的编译器通行证。据我们所知，CertiQ是第一个以最自动化的方式验证真实世界量子编译器通过的努力。在CertiQ接口中编写的带有注释的验证器通道可用于生成验证条件，以及可集成到Qiskit中的可执行代码。CertiQ引入了量子电路演算，通过将这种检查过程编码到SMT问题中来实现量子线路的等效性的有效检查。CertiQ还提供了一个经过验证的广泛使用的数据结构库、电路转换函数以及不同量子数据表示的转换函数。这个经过验证的库不仅可以进行模块化验证，而且还可以为未来的量子编译器设计提供指导。我们已经在CertiQ中重新实现并验证了26个（共30个）Qiskit编译器通道，在此期间，在Qiskit实现中检测到三个错误。我们验证的编译器通过实现通过了所有Qiskit的回归测试，没有显示出明显的性能损失。
2020-11-26 cs.ET cs.PL quant-ph
Quokka#: Quantum Computing with #SAT
Leiden University（莱顿大学）；Delft University of Technology（代尔夫特理工大学）
Quokka#通过将量子电路分析任务转化为加权模型计数(#SAT)实现高效处理，支持通用量子电路和多种门操作，其合成引擎深度优化，适用于实际量子计算。
2026-05-15 quant-ph
Equivalence of maximal and generic reachability for non-universal Variational Quantum Circuits
Karlsruhe Institute of Technology（卡尔斯鲁厄理工学院）
本文证明非通用变分量子电路在任意参考态下最大可达性与一般可达性等价，并给出可达性维度准则，数值验证了该准则对优化成败的决定性作用。
2026-09-24 quant-ph
Local Unitary Equivalence of Tripartite Quantum States In Terms of Trace Identities
本文通过超矩阵代数框架，将局部酉等价性与同时正交等价性的对应关系从双体推广到三体量子态，并利用推广的Specht准则将三体LU等价性问题简化为检查迹恒等式等不变量。
2025-04-22 quant-ph
A Specification Format and a Verification Method of Fault-Tolerant Quantum Circuits
量子计算一般表示为量子线路，其由有序的量子门列表指定。在优化和执行所表达的计算过程中使用所得到的规范。然而，规范格式使得很难验证优化或执行的计算仍然符合初始的门列表规范：在最坏的情况下，显示由不同的量子门列表表示的两个量子线路之间的计算等价性是指数复杂的。为了解决这个问题，这项工作提出了专门为容错量子线路定制的规格格式的推导。电路被认为是完全由单量子位初始化，CNOT门和单量子位测量（ICM形式）组成的形式。在某些假设下，这种格式允许有效地验证优化的（或实现的）计算。提出了两种基于检查稳定器电路结构的验证方法。
2018-07-08 quant-ph
Self-Testing of Quantum Circuits
我们证明了一个量子线路连同测量仪器和EPR源可以完全验证，而不需要参考其他一些可信的量子设备。我们的主要假设是，我们所研究的物理系统由几个可识别的子系统组成，我们可以在这些子系统上局部应用一些给定的门。为了实现我们的目标，我们定义了模拟和等价的概念。模拟的概念是指在测量物理系统时产生正确的概率。为了能够有效地测试量子操作的组成，我们引入了等价的概念。与模拟不同，模拟是指测量的量（即，结果的概率），等价关系数学对象，如状态，子空间或门。使用这两个概念，我们证明了，如果一个系统满足一些模拟条件，那么它是等价的，它是旨在实现。此外，通过我们的形式主义，我们可以证明这些陈述是鲁棒的，并且鲁棒性的程度可以明确（与[DMMS 00]的鲁棒性结果不同）。特别是，我们还证明了EPR测试[MY98]的稳健性。最后，我们设计了一个测试任何量子线路，其复杂性是线性的门和量子比特的数量，多项式的精度要求。
2005-12-14 quant-ph
Quantum Circuit Transformations with a Multi-Level Intermediate Representation Compiler
量子计算承诺处理信息的显着方法，但需要新的工具来将程序表示编译为量子计算机所需的物理指令。在这里，我们提出了一种新的适应的多级中间表示（MLIR）集成到一个量子编译器，可用于检查程序执行。我们首先介绍了MLIR如何使量子线路转换在量子计算设备上高效执行，然后给出了一个基于所谓的镜像电路的编译器转换的例子。我们证明，在编译过程中插入的镜像电路可以通过评估几个超导和离子阱硬件平台上的量子线路精度来测试硬件性能。我们的研究结果验证MLIR作为一种高效和有效的方法，收集硬件相关的诊断，通过自动化的量子线路的转换。
2021-12-20 cs.PL quant-ph
