arXiv:2505.03863v1 交叉公告类型 摘要：在医疗保健、航空电子设备和自动驾驶车辆等关键安全领域，计算物理系统（CPS）相当普遍。因此，对其运行安全的形式验证至关重要。本文针对反证问题进行研究，重点在于寻找系统中的不安全执行情况，而不是证明其不存在。本文的贡献是一个框架，该框架（a）将CPS的反证与其所使用的深度神经网络（DNN）的反证联系起来，（b）利用决策树固有的可解释性来加快CPS的反证速度。这通过以下方式实现：（1）为测试的CPS构建一个代理模型，既可以是DNN模型，也可以是决策树模型，（2）应用各种DNN反证工具对CPS进行反证，以及（3）根据从CPS模型的决策树代理中提取的安全违规解释提出的一种新型反证算法。所提出的框架有可能利用专门设计用于反证DNN鲁棒性属性的各种\emph{对抗性攻击}算法，以及最先进的DNN反证算法。尽管所介绍的方法适用于可以通用执行/模拟的系统，但我们特别展示了其在CPS中的有效性。我们展示了我们作为工具\textsc{FlexiFal}实现的框架，可以在具有线性和非线性动力学的CPS中检测难以发现的反证例子。决策树指导的反证在ARCH-COMP 2024反证基准测试中有效地找到了多个反证例子，展示了显著的结果~\cite{khandait2024arch}。