Concept-based Analysis of Neural Networks via Vision-Language Models

TL;DR

This work tackles the challenge of formally analyzing vision-based DNNs by leveraging Vision-Language Models (VLMs) as a semantic lens. It introduces Con_spec, a first-order specification language for expressing model properties in terms of human-understandable concepts, and defines a concept representation map rep implemented via VLMs to enable automated verification in the shared text/image embedding space. A key methodological contribution is the affine alignment r_map between a vision model’s embeddings and a VLM’s embeddings, which, together with a decomposition of the vision model into encoders and heads, reduces verification to linear constraints on the head, enabling scalable, region-focused checks. The paper demonstrates the approach on a ResNet18 classifier trained on RIVAL10 using CLIP, extracting concept directions through CLIP captions, statistically validating rep predicates, and verifying the model against Con_spec properties, thereby illustrating the potential of semantic, scalable DNN verification with multimodal foundations.

Abstract

The 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 build a map between the internal representations of a given vision model and a VLM, leading to an efficient verification procedure of natural-language properties for vision models. We demonstrate our techniques on a ResNet-based classifier trained on the RIVAL-10 dataset using CLIP as the multimodal model.

Figures (14)

• Figure 1: Overview of Approach
• Figure 2: $\texttt{Con}_{\texttt{spec}}$ syntax
• Figure 3: $\texttt{Con}_{\texttt{spec}}$ semantics
• Figure 4: Relevant concepts per class
• Figure 5: Satisfaction probabilities for $rep$ implemented only using CLIP model $g$

Theorems & Definitions (13)

• definition thmcounterdefinition: Satisfaction of specification by model
• definition thmcounterdefinition: Linear $rep$ via VLM
• definition thmcounterdefinition: Linear $rep$ via vision model, $r_{map}$, and VLM
• definition thmcounterdefinition: Faithful alignment of representation spaces
• theorem thmcountertheorem
• proof
• lemma thmcounterlemma
• proof
• lemma thmcounterlemma
• proof