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

TL;DR

This paper introduces a graph-based formal verification framework for image retrieval that enhances trustworthiness and transparency in complex, constraint-based natural language queries, complementing existing embedding methods.

Contribution

It presents a novel integration of formal verification with neural image retrieval, enabling explicit validation of query constraints and improving result reliability.

Findings

Supports open-vocabulary natural language queries

Provides verifiable and transparent retrieval results

Enhances existing embedding-based image retrieval methods

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.