量子算法利用量子力学原理，特别是量子叠加和纠缠[1]，展现出与经典算法根本不同的计算能力。量子比特的叠加属性使量子算法能够访问庞大的计算空间，从而解决经典算法难以高效处理的高复杂性问题[2]。例如，Grover算法在加速无序搜索[3]中的应用，以及量子模拟[4]中的应用，都凸显了量子算法的巨大潜力。对量子算法的系统研究始于Deutsch提出的量子图灵机模型和单量子比特Deutsch算法[5]。随后，这项工作扩展到了多量子比特Deutsch-Jozsa算法[6]，展示了量子计算的并行性。
在这些量子算法中，Bernstein-Vazirani（BV）算法[7]因其简单性和效率而脱颖而出。Shor算法依赖于复杂的量子傅里叶变换[8]，而Grover方法则利用概率重复[3]。相比之下，BV算法无需量子纠缠即可实现量子优势[9]。这一独特特性使得BV算法在密码学[10]和机器学习[11]的实际应用中特别有价值。最近的扩展将其应用于量子通信[12]。
然而，由于量子力学的高复杂性[13]，使用传统方法难以验证算法的正确性和可执行性。直接保证量子算法在实际应用中的准确性和可靠性是一个重大挑战[14]。
为了解决这一挑战，量子算法的形式化验证逐渐成为一个重要的研究领域[15]。通过应用严格的数学推理，形式化验证可以在理论层面消除潜在的系统漏洞和安全缺陷[16]，确保量子算法的正确性。近年来，研究人员使用定理证明工具取得了显著进展。Bordg等人[17]在Isabelle/HOL中正式验证了Deutsch-Jozsa算法。Liu等人[18]基于量子Hoare逻辑对Grover算法进行了形式化。Lin等人[19]通过改进的Grover算法将SAT问题的时间复杂度从O(m)降低到O(1)。Chareton和Hietala等人分别使用QBricks和SQIR语言独立验证了量子相位估计[20][21]。Shi等人[22]使用Coq对Deutsch-Jozsa算法和量子传输进行了符号验证。这些结果证明了形式化验证在量子算法中的适用性，为本工作中BV算法的形式化验证提供了重要的参考和实际基础。
此外，Murali等人[23]优化了BV算法的编译，但仅关注硬件调度约束，缺乏对其量子属性的严格数学证明，如量子状态演化的形式化规范或算法的幺正性。Marco Lewis等人[14]使用SilVer框架对BV算法进行了验证。他们的方法结合了Silq-Hybrid编程和SMT求解器来验证程序行为的正确性。尽管这种方法在自动化方面具有一定的优势，但它仅支持固定的输入大小。验证水平仅限于程序的行为正确性，不涉及BV算法的幺正性、幅度变换机制或在任意维度上的正确性的形式化建模或数学证明。
相比之下，我们的工作在HOL Light
1框架内对BV算法的每一步进行了形式化验证，从量子状态和算子的代数定义开始。我们为其正确性提供了归纳证明，适用于任意数量的量子比特。此外，我们将验证结果扩展到量子密钥分发和图像加密等实际应用，实现了算法层面的严格数学验证。我们的主要贡献包括：
•构建了量子力学数学基础的形式化框架。
- •
通过两个实际应用展示了BV算法的实用性和可扩展性。
本文的其余部分组织如下。第2节提供了BV算法基本理论的形式化。第3节概述了BV算法解决的问题，并详细介绍了其形式化建模和验证。第4节基于BV算法，提出了两个示例案例进行说明。最后，我们在第5节总结了本文。
