通过模糊处理和严谨方法革新量子模拟器

《Proceedings of the ACM on Programming Languages》：Shaking Up Quantum Simulators with Fuzzing and Rigour

量子计算模拟器验证存在形式方法与测试生成结合不足的问题，FuzzQ框架通过Alloy建模QASM 3.0语义，结合差分基准测试、变异测试和不变式检查，在Qiskit和Cirq上验证发现8个错误（6个新问题），并规划噪声混合状态扩展。

　　

摘要

量子计算平台在硬件执行之前依赖模拟器来建模电路行为，其中的不一致性可能导致代价高昂的错误。虽然现有的形式化验证方法通常针对特定的编译器组件来管理状态爆炸问题，但它们往往无法发现关键错误。与此同时，传统的测试方法缺乏对边界情况和真实执行场景的系统性探索，从而导致误报和漏报。

我们提出了FuzzQ这一新型框架，它通过将形式化方法与结构化测试生成和模糊测试相结合，填补了这一空白。我们的方法采用差分基准测试，并辅以变异测试和不变量检查。FuzzQ的核心是使用基于Alloy的形式化模型来描述QASM 3.0，该模型编码了量子电路的语义，从而实现自动化分析，并生成具有保证特性的结构多样、受约束指导的量子电路。我们引入了几种测试方法来评估Alloy对QASM 3.0的建模能力以及模拟器的正确性，包括基于不变量的检查、统计分布测试，以及一种新颖的跨模拟器幺正一致性检查，该检查可以验证在跨平台差分测试中标准状态向量比较未能发现的差异。

我们在Qiskit和Cirq两个平台上对FuzzQ进行了评估，证明了其平台无关性。通过执行超过80万个量子电路，我们评估了吞吐量、代码和电路覆盖率以及模拟器的性能指标，包括灵敏度、正确性和内存开销。我们的分析发现了8个模拟器错误，其中6个是之前未记录的。我们还概述了扩展该框架以支持在真实噪声模型下的混合态模拟的路径。