当前位置：首页 > news >正文

Visual Model Checking Graph-Based Inference of Visual Routines for Image Retrieval

news 2026/3/27 8:34:37

Visual Model Checking: Graph-Based Inference of Visual Routines for Image Retrieval

Authors:Adrià Molina, Oriol Ramos Terrades, Josep Lladós

Deep-Dive Summary:

可视化模型检测：基于图的图像检索视觉程序推理

摘要：信息检索是现代数字产业的基础。虽然自然语言搜索近年来在基于嵌入（embedding）的模型和大规模预训练的推动下取得了显著进展，但该领域仍面临巨大挑战。特别是涉及复杂关系、对象组合或精确约束（如身份、计数和比例）的查询，在当前框架下往往难以解决或不可靠。本文提出了一种新型框架，通过将基于图的验证方法与神经代码生成相结合，将形式化验证（formal verification）整合到基于深度学习的图像检索中。该方法旨在支持开放词汇的自然语言查询，同时生成既可靠又可验证的结果。通过将检索结果建立在形式化推理系统之上，我们超越了矢量表示中常见的模糊性和近似性。该框架不再被动接受不确定性，而是显式地根据检索内容验证用户查询中的每个原子事实（atomic truth）。这使我们不仅能返回匹配结果，还能识别并标记满足或未满足的具体约束，从而提供更透明、更负责的检索过程，同时提升了主流嵌入式方法的检索效果。

关键词：图像检索 · 知识表示与推理

1 引言

图像搜索在现代数字生态系统中发挥着基础性作用。随着基于嵌入的检索系统能力增强，人们越来越依赖它们来解释复杂场景和满足开放式查询。然而，这些系统通常优先考虑近似性而非精确性。

图 1. 提出的可视化搜索框架的视觉摘要。系统采用模型检测方法：首先将文本查询转换为结构化系统规范（图）。针对每个局部规范，生成相应的视觉程序（代码）。候选图像根据其满足这些视觉程序的程度进行排名（剪枝），从而实现数字环境中视觉内容的局部或完全验证。

本研究是对图像检索中灵活性与可靠性之间矛盾的回应。通过将形式化验证引入检索过程，自然语言查询的每个组件（以逻辑三元组表示）都可以针对候选图像进行独立测试。这使系统能够明确指出哪些约束被满足、哪些被违反。在事实准确性至关重要的场景中，这种可验证性将视觉搜索从模糊的近似过程转变为透明的结构化推理机制。

我们受模型检测（model checking）框架的启发，提出了一种新方法（见图 1）。查询被解释为系统规范，据此构建世界模型，并与具体实例进行比较。查询定义了世界模型的理想规范，这些规范通过“视觉程序”（visual routine）实例化——这是一种视觉语法，从“世界应该是什么样子”的具体实例中抽象出结构。

本工作的主要贡献包括：

引入了一个形式化的视觉语法框架，将模型检测技术适配于图像检索任务。
提出了一个性能足以媲美最先进（SOTA）视觉搜索方法的系统。
提供了广泛的定性评估，突出了该方法在不同视觉搜索场景下的优势和常见局限。

图 2. 受到 [4] 启发的视觉程序模型检测方法布局。

2 相关工作

近年来，图像搜索领域由基于嵌入的自监督多模态编码器（如 CLIP）主导。虽然这些方法很高效，但在处理涉及多方面或组合性描述的文本查询时往往表现不佳。

最近在视觉与符号推理交叉领域的工作尝试通过程序合成将高层语义理解与视觉感知联系起来（如 Pix2Code, ViperGPT, VisProg）。ViperGPT 和 VisProg 引入了零样本框架，通过生成调用预训练感知模型 API 的 Python 程序来回答视觉查询。受此启发，我们将形式化验证原则应用于视觉检索，目标不是回答特定查询，而是通过图像对逻辑三元组集合的满足程度来进行排名检索。

3 方法论

3.1 符号表示

提出的框架由以下元素构成：

系统规范：表现为自然语言查询q qq。
系统描述：由视觉元素v vv（图像）表示。
系统解析函数：P ( q ) = ϕ P(q) = \phiP(q)=ϕ，将查询转换为图结构：{ ( s 1 , p 1 , o 1 ) , … , ( s n , p n , o n ) } \{(s_1, p_1, o_1), \dots, (s_n, p_n, o_n)\}{(s1,p1,o1),…,(sn,pn,on)}。该图将规范编码为一组主-谓-宾三元组ϕ i \phi_iϕi。

图 3. 对于( m a n , r i d i n g , h o r s e ) (man, riding, horse)(man,riding,horse)的实际视觉程序示例，系统合成了程序以识别抽象语句，且与具体图像无关。

函数合成模型：将三元组ϕ i \phi_iϕi映射到关联程序π i \pi_iπi的映射M : ϕ → Π \mathrm{M}: \phi \rightarrow \PiM:ϕ→Π。
视觉程序集Π \PiΠ：满足ϕ \phiϕ中三元组的专门程序集π i : V → { T r u e , F a l s e } \pi_i : V \rightarrow \{\mathrm{True}, \mathrm{False}\}πi:V→{True,False}。

如果且仅当每个元素π i ∈ Π \pi_i \in \Piπi∈Π在应用于图像v vv时评估为T r u e \mathrm{True}True，则该图像满足规范ϕ \phiϕ。

3.2 检索方法

排名得分（Ranking score）：这种布尔验证框架通过“部分验证”扩展到排名机制。我们通过计算图像满足的程序比例来对图像进行排名，生成反映图像合规程度的真值分数。

视觉程序作为重排器（Re-Rankers）：我们采用混合方案，利用视觉程序对原始检索结果进行重排。得分公式如下：
R e R a n k S c o r e i = ( K − i ) × # V e r i f i e d T r i p l e t s # T o t a l o f T r i p l e t s ( 1 ) \mathrm{ReRankScore}_i = (K - i) \times \frac{\#\mathrm{VerifiedTriplets}}{\#\mathrm{TotalofTriplets}} \quad (1)ReRankScorei=(K−i)×#TotalofTriplets#VerifiedTriplets(1)

流水线（Pipeline）：工作流从解析用户查询q qq开始，生成逻辑规范ϕ \phiϕ。为了避免状态爆炸，每个三元组构成一个视觉程序π \piπ的基础。模型M ( ϕ ) \mathrm{M}(\phi)M(ϕ)将这些逻辑三元组转换为可执行的 Python 程序（见图 3）。这些程序利用大型语言模型（LLM）合成，并通过开放词汇视觉检测模型（如 OWL-v2）执行。

4 实验设置

4.1 数据与评估

使用 MS-COCO Captions 2017 验证集。为了解决评估偏差，我们将验证集划分为COCO-Easy和COCO-Hard。Easy 包含 CLIP 表现最好的前 25% 样本，而 Hard 包含 CLIP 表现最差的后 25%（通常涉及组合性、文本识别或计数任务）。

4.2 实现细节

系统部署在多 GPU 分布式环境中。流水线包含三个阶段：使用 Microsoft Phi-4 解析查询；合成基于 Python 的视觉程序；使用 OWL-v2 执行程序进行符号验证。

5 结果与讨论

定量评估：如表 1 所示，该方法在 Recall@1, 5, 10 上取得了具有竞争力的性能。在 COCO-Hard 划分中，该方法表现出明显优势，这归功于其验证文本内容、空间组合和基础数值推理的能力。

表 1. 本方法与其他基于嵌入方法的召回率比较。在零样本方法中表现出竞争力。
(注：表格数据展示了本方法及其与 CLIP、BEIT、ALIGN 结合后的性能提升)

表 2. 本方法作为传统嵌入方法的重排器。可以观察到 LLM 的常识知识在零样本场景中提供了帮助。
(注：表格展示了在 COCO-All 上的 Recall 提升情况)

图 4. 来自 MS-COCO 数据集的简单（Easy）和困难（Hard）实例示例。较难的例子往往涉及复杂的描述，包括对象计数、文本识别和实体间关系的推理。

定性评估：如图 6 所示，可验证视觉搜索具有三大优势：

精确识别：能够区分细微差别（如“人”与“人们”的数量）和识别特定文本（如指示牌方向）。
组合推理：能够将图像分解为基础组件，实现更精确的匹配。
处理多方面查询：独立评估标题的每个组件，避免 CLIP 偏向主导特征而忽略次要元素的问题。

图 5. 使用本方法（正方形）对基于嵌入的内容（圆形）进行重排的效果。

此外，该方法的错误是全流程可追溯且可解释的（见表 3），这与 CLIP 等模型的黑盒性质形成鲜明对比。

总结：我们的基于验证的方法为传统图像检索提供了一个极具竞争力的替代方案，特别是在需要精细推理、组合性理解、数值计算和文本识别的场景中。虽然代码合成和视觉检测中引入的噪声会影响部分增益，但其带来的透明度和可靠性是显著的。

Original Abstract:Information retrieval lies at the foundation of the modern digital industry. While natural language search has seen dramatic progress in recent years largely driven by embedding-based models and large-scale pretraining, the field still faces significant challenges. Specifically, queries that involve complex relationships, object compositions, or precise constraints such as identities, counts and proportions often remain unresolved or unreliable within current frameworks. In this paper, we propose a novel framework that integrates formal verification into deep learning-based image retrieval through a synergistic combination of graph-based verification methods and neural code generation. Our approach aims to support open-vocabulary natural language queries while producing results that are both trustworthy and verifiable. By grounding retrieval results in a system of formal reasoning, we move beyond the ambiguity and approximation that often characterize vector representations. Instead of accepting uncertainty as a given, our framework explicitly verifies each atomic truth in the user query against the retrieved content. This allows us to not only return matching results, but also to identify and mark which specific constraints are satisfied and which remain unmet, thereby offering a more transparent and accountable retrieval process while boosting the results of the most popular embedding-based approaches.

PDF Link:2602.17386v1