这篇文档属于类型a，即报告了一项原创性研究。以下是针对该研究的学术报告：
一、研究作者与机构、发表期刊与时间
本研究的作者包括Mingkuan Xu（卡内基梅隆大学）、Zikun Li（加州大学洛杉矶分校）、Oded Padon（VMware Research）、Sina Lin（微软）、Jessica Pointing（牛津大学）、Auguste Hirth（加州大学洛杉矶分校）、Henry Ma（加州大学洛杉矶分校）、Jens Palsberg（加州大学洛杉矶分校）、Alex Aiken（斯坦福大学）、Umut A. Acar（卡内基梅隆大学）和Zhihao Jia（卡内基梅隆大学）。该研究发表于2022年6月13日至17日在美国圣地亚哥举行的第43届ACM SIGPLAN国际编程语言设计与实现会议（PLDI ‘22）上。
二、学术背景
本研究的主要科学领域是量子计算，具体涉及量子电路优化。量子计算近年来发展迅速，但不同量子设备支持的量子操作集（Instruction Set Architectures, ISAs）存在显著差异，这为量子编译器的设计带来了挑战。现有的量子编译器通常依赖于专家手工设计的电路变换规则，这种方法不仅耗费大量人力，还可能遗漏一些难以手动发现的优化机会。此外，针对某一设备设计的电路变换规则无法直接应用于其他设备，这在量子计算多样化的背景下尤为突出。
为了解决这些问题，本研究提出了Quartz，一种能够自动生成和验证量子电路变换的量子电路超级优化器。Quartz的目标是通过系统化地探索小规模电路，并使用自动化定理证明器验证发现的变换，从而为任意量子门集生成有效的电路优化规则。Quartz还采用基于成本的回溯搜索算法，将已验证的变换应用于量子电路，以实现优化。
三、研究流程
本研究的主要流程包括以下几个步骤：
电路生成与等价类构建
Quartz通过RepGen算法生成候选电路，并构建等价电路类（Equivalent Circuit Classes, ECCs）。ECC是一组功能等效的电路，两个电路来自同一个ECC则构成一个有效的变换。RepGen算法通过逐步扩展电路规模，确保生成的ECC集在给定门集和电路规模下是完备的。具体来说，RepGen从空电路开始，逐步生成更大规模的电路，并通过随机输入为每个电路计算指纹（fingerprint），以识别潜在的等效电路。
电路等价性验证
Quartz使用自动化定理证明器验证候选电路的等价性。由于量子电路可能包含参数化门（如𝑈1、𝑈2等），Quartz计算电路的符号矩阵表示，并将等价性验证问题转化为SMT（Satisfiability Modulo Theories）求解问题。通过消除三角函数和量化交替，Quartz将问题简化为非线性实数算术的量化自由公式，并使用Z3 SMT求解器进行验证。
冗余变换剪枝
在生成完备的ECC集后，Quartz通过ECC简化和公共子电路剪枝进一步消除冗余变换。ECC简化移除未使用的量子比特和参数，而公共子电路剪枝则消除目标电路和重写电路之间在开头或结尾存在公共子电路的变换。
电路优化
Quartz的电路优化器采用基于成本的回溯搜索算法，将已验证的变换应用于输入电路。搜索过程由成本模型引导，成本通常由电路中的门数量决定。优化器通过图表示法匹配目标电路与输入电路的子电路，并应用变换生成新的候选电路。
四、主要结果
本研究在三个流行的量子门集（NAM、IBM和Rigetti）上对Quartz进行了评估，结果表明：
变换生成与验证
Quartz能够在30分钟内（使用128核）为不同门集生成和验证电路变换。生成的变换不仅覆盖了现有优化器使用的手工设计变换，还包括一些新的变换。
电路优化性能
在26个基准电路上，Quartz在NAM、IBM和Rigetti门集上的平均门数量分别减少了29%、30%和49%，优于或匹配现有手工调优的电路优化器。例如，在IBM门集上，Quartz的表现显著优于Qiskit和t|ket⟩；在Rigetti门集上，Quartz的表现远超Quilc和t|ket⟩。
ECC集的完备性
Quartz生成的ECC集在给定门集和电路规模下是完备的，能够涵盖所有可能的电路变换。通过RepGen算法，Quartz显著减少了需要考虑的电路数量，同时保持了ECC集的完备性。
五、结论
本研究提出的Quartz是一种高效、自动化的量子电路超级优化器，能够为任意量子门集生成和验证电路变换。Quartz不仅减少了量子电路的执行成本，还通过自动化方法降低了优化设计的复杂性。其科学价值在于提供了一种系统化的量子电路优化方法，填补了现有优化器在自动化和通用性方面的不足。应用价值则体现在Quartz能够适应多样化的量子设备，为量子计算的实用化提供了重要支持。
六、研究亮点
1. 自动化变换生成与验证：Quartz通过系统化探索和自动化定理证明，显著减少了手工设计变换的需求。
2. ECC集的完备性：Quartz生成的ECC集在给定门集和电路规模下是完备的，确保了优化的全面性。
3. 基于成本的回溯搜索：Quartz的优化器通过成本模型引导搜索，能够发现传统贪婪方法无法触及的优化机会。
4. 通用性与适应性：Quartz支持任意量子门集，能够适应不同量子设备的多样化需求。
七、其他有价值的内容
本研究还探讨了Quartz在有限精度浮点运算下的实现细节，并提出了相应的误差处理机制。此外，Quartz的开源实现（GitHub链接）为后续研究和应用提供了便利。
通过以上报告，我们可以看到Quartz在量子电路优化领域的创新性和实用性，为量子计算的发展提供了重要工具。