Formal analysis of vision-based deep neural networks (DNNs) is highly
desirable but it is very challenging due to the difficulty of expressing formal
specifications for vision tasks and the lack of efficient verification
procedures. In this paper, we propose to leverage emerging multimodal,
vision-language, foundation models (VLMs) as a lens through which we can reason
about vision models. VLMs have been trained on a large body of images
accompanied by their textual description, and are thus implicitly aware of
high-level, human-understandable concepts describing the images. We describe a
logical specification language $\texttt{Con}_{\texttt{spec}}$ designed to
facilitate writing specifications in terms of these concepts. To define and
formally check $\texttt{Con}_{\texttt{spec}}$ specifications, we leverage a
VLM, which provides a means to encode and efficiently check natural-language
properties of vision models. We demonstrate our techniques on a ResNet-based
classifier trained on the RIVAL-10 dataset leveraging CLIP as the multimodal
model.

通过多模态的视觉 - 语言基础模型作为一种视角，本文提出了一种逻辑规范语言 Con_spec，用于在这些模型的高级人类可理解概念描述的基础上编写规范并进行形式验证，通过采用 VLM 实现自然语言性质的编码和高效检查，以 ResNet 为基础的分类器在 RIVAL-10 数据集上进行的实验验证了我们的技术。