面向噪声量子强化学习策略的形式化验证

量子强化学习 (QRL) 旨在利用量子效应创建比经典方法更有效的序列决策策略。然而，QRL 政策面临来自量子测量不确定性和硬件噪声（如比特翻转、相位翻转和去极化误差）的挑战，可能导致不安全行为。现有工作未提供系统性方法以验证训练后的 QRL 政策在特定噪声条件下是否满足安全要求。我们引入 QVerifier，一种形式化验证方法，应用概率模型检查分析训练后的 QRL 政策，包括是否建模量子噪声。QVerifier 构建政策-环境交互的完整模型，将量子不确定性直接纳入转移概率，然后使用 Storm 模型检查器验证安全属性。跨多个 QRL 环境的实验表明，QVerifier precise 测量不同噪声模型对安全性的影响，揭示性能降解以及噪声有助于情形。通过在部署前实现严格的安全验证，QVerifier 解决了关键需求：由于获取量子硬件昂贵，部署前的验证对任何安全关键型 QRL 用途至关重要。QVerifier 目标于经典计算与量子计算之间的潜在甜蜜区，训练后的 QRL 政策可能仍可经典建模以进行概率模型检查。当政策在匹配噪声条件下训练时，该形式模型是 exact的；当在物理硬件上训练时，它构成一种理想化的近似，因为未知硬件噪声防止了精确的政策建模。