XiaoMi-AI文件搜索系统
World File Search SystemSQIR
量子电路的经过验证的优化器
我们提出了使用COQ证明助手编写的第一个用于量子电路的第一个完全验证的优化器。量子电路以简单的低级语言表示为程序，称为SQIR，一种简单的量子中间表示形式，它深层嵌入了COQ中。优化和其他转换表示为COQ函数，相对于SQIR程序的语义，证明是正确的。sqir使用复数矩阵的语义，这是量子计算的标准，但象征性地对待矩阵以推理使用任意数量量子位的程序。SQIR的仔细设计和我们提供的自动化使得在VOQC中编写和验证广泛的优化是可能的，包括来自尖端优化器的全电路转换。
验证的量子序列的汇编-ACM数字库
量子算法通常在经典数据的量子叠加上应用经典操作，例如算术或谓语检查；这些所谓的甲壳通常是量子程序中最大的组成部分。为了简化高效，正确的Oracle功能的构建，本文介绍了VQO，这是COQ证明助手实施的高保证框架。VQO的核心是O QASM，Oracle量子组装语言。o Qasm操作通过量子傅立叶变换在两个不同的基础之间移动量子位，因此承认了重要的优化，但没有引起纠缠和随附的指数爆炸。o QASM的设计使我们能够证明VQO的编译器从一种名为O QIMP到O QASM的简单命令性语言，从O Qasm到SQIR，从O QASM到SQIR，一种通用量子量组装语言 - 允许我们通过基于QuickChick property属性属性的测试框架有效地测试O Qasm程序的质量质量。我们已经使用VQO实施了各种算术和几何操作员，这些算术和几何操作员是重要的Oracles的构建块，包括Shor's和Grover的算法中使用的Oracles。我们发现，与使用lclassicalžGates构建的量子相比，VQO的基于QFT的算术甲壳所需的量子量要少，有时甚至少得多。但是，VQO的后者版本与Quipper生产的Oracles（在Qubit和Gate计数方面）相当或更好，这是一个最先进但未验证的量子编程平台。