Formal Verification of Object Detection

这项工作致力于将形式验证应用于计算机视觉模型，扩展验证范围从图像分类到目标检测，以确保深度神经网络（DNNs）在实际应用中的安全性。我们提出了一种通用的公式，利用形式验证来证明目标检测模型的鲁棒性，并概述了与最先进的验证工具兼容的实现策略。我们的方法使得这些原本设计用于验证分类模型的工具可以应用于目标检测。我们定义了各种攻击方式，说明了对抗性输入可能如何危及神经网络输出。我们在几个常见的数据集和网络上进行了实验，发现目标检测模型存在潜在的错误，突出了系统的漏洞，并强调了扩展形式验证至这些新领域的必要性。这项工作为进一步研究在更广泛的计算机视觉应用中整合形式验证铺平了道路。

论文试图通过形式验证确保计算机视觉模型的安全性，将验证扩展到目标检测，以解决深度神经网络容易出错和遭受对抗性攻击的问题。

论文提出了一个通用的公式，使用形式验证来证明目标检测模型的鲁棒性，并提出了与最先进的验证工具兼容的实现策略，该方法使得这些工具可以用于目标检测。

论文定义了各种攻击目标检测的方式，展示了对抗性输入如何破坏神经网络输出，实验在几个常见的数据集和网络上进行，揭示了目标检测模型的潜在错误，强调了扩展形式验证到这些新领域的必要性。

最近的相关研究包括：Towards Verified Artificial Intelligence，Formal Verification of Neural Networks: A Survey，DeepTest: Automated Testing of Deep-Neural-Network-driven Autonomous Cars