量智信息中心_量科网

无论采用何种编程模型或计算范式，关于量子程序的推理始终是一项基础性挑战。尽管已有大量研究，现有验证技术仍存在不足——即便对于刻意限制经典控制、但仍支撑着当前众多量子算法的量子电路模型而言亦是如此。现有形式化方法大多需要指数级时间和空间来表示和处理断言与判断（的数学表达），导致其难以应用于多量子比特电路。本文提出一种适用于此类场景的推理逻辑SAQR-QC，其全称为“面向量子电路的可扩展近似定量推理”。该逻辑具备三大特征：（1）内置了（人为设计的）精度损失机制；（2）具备控制推理步骤序列中累积精度损失的保障机制；（3）最关键的是，所有推理步骤均采用局部化处理——即每次仅涉及少量量子比特，从而实现可扩展性。研究团队通过两个案例验证了SAQR-QC的有效性：包含非克利福德门的GHZ电路验证，以及作为肖尔大数分解算法核心子程序的量子相位估计分析。