One of the key steps in quantum algorithms is to prepare an initial quantum superposition state with different kinds of features. These so-called state preparation algorithms are essential to the behavior of quantum algorithms, and complicated state preparation algorithms are difficult to develop correctly and effectively. This paper presents Pqasm: a high-assurance framework implemented with the Coq proof assistant, allowing us to certify our Pqasm tool to correctly reflect quantum program behaviors. The key in the framework is to reduce the program correctness assurance of a program containing a quantum superposition state to the program correctness assurance for the program state without superposition. The reduction allows the development of an effective testing framework for testing quantum state preparation algorithm implementations on a classical computer - considered to be a hard problem with no clear solution until this point. We utilize the QuickChick property-based testing framework to test state preparation programs. We evaluated the effectiveness of our approach over 5 case studies implemented using Pqasm; such cases are not even simulatable in the current quantum simulators.

翻译：量子算法的关键步骤之一是制备具有不同特征的初始量子叠加态。这些所谓的态制备算法对量子算法的行为至关重要，而复杂的态制备算法难以正确且高效地开发。本文提出了Pqasm：一个基于Coq证明助手实现的高可信度框架，使我们能够验证Pqasm工具能正确反映量子程序行为。该框架的核心在于，将包含量子叠加态的程序正确性保障，简化为无叠加态的程序状态正确性保障。这种简化使得在经典计算机上为量子态制备算法实现开发有效的测试框架成为可能——这在此前一直被视为缺乏明确解决方案的难题。我们利用基于属性的测试框架QuickChick对态制备程序进行测试。通过在Pqasm实现的5个案例研究中评估本方法的有效性；这些案例在现有量子模拟器中甚至无法进行模拟。