首次为变分量子线路建立形式化验证框架，解决其对抗性脆弱性问题。
Formal Verification of Variational Quantum Circuits
- 基于抽象解释构建量子线路验证语义框架
- 揭示状态归一化导致变量依赖，挑战传统区间分析方法
- 在标准基准上验证了方法有效性，适合量子机器学习安全研究者
变分量子线路（VQCs）是许多量子机器学习算法的核心组件，其混合量子-经典架构在某些方面可类比于经典深度神经网络。例如，二者均易受对抗输入影响——微小扰动可能导致错误预测。尽管形式化验证技术已在经典模型中广泛应用，但尚无类似框架可用于认证VQCs的鲁棒性。本文首次系统开展VQCs形式化验证的理论与实践研究。受深度学习中抽象解释方法启发，我们分析了区间可达性技术在量子场景下的适用性与局限性。结果表明，量子特有的状态归一化引入了变量间的耦合关系，使得现有方法面临挑战。为此，我们提出一种基于抽象解释的新语义框架，可形式化定义VQC的验证问题并分析其复杂性。最后，我们在标准验证基准上展示了该方法的有效性。
原文摘要 · Abstract (English)
Variational quantum circuits (VQCs) are a central component of many quantum machine learning algorithms, offering a hybrid quantum-classical framework that, under certain aspects, can be considered similar to classical deep neural networks. A shared aspect is, for instance, their vulnerability to adversarial inputs, small perturbations that can lead to incorrect predictions. While formal verification techniques have been extensively developed for classical models, no comparable framework exists for certifying the robustness of VQCs. Here, we present the first in-depth theoretical and practical study of the formal verification problem for VQCs. Inspired by abstract interpretation methods used in deep learning, we analyze the applicability and limitations of interval-based reachability techniques in the quantum setting. We show that quantum-specific aspects, such as state normalization, introduce inter-variable dependencies that challenge existing approaches. We investigate these issues by introducing a novel semantic framework based on abstract interpretation, where the verification problem for VQCs can be formally defined, and its complexity analyzed. Finally, we demonstrate our approach on standard verification benchmarks.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。