Embedding search returns plausible images. This work returns verifiable ones — checking each atomic claim in a query against the picture, and naming exactly what is satisfied and what is not.
CLIP and its descendants are extraordinary at vibes. They are unreliable at constraints — counts, identities, proportions, spatial relations, and text on a sign.
A vector search asks one fuzzy question: does this image, as a whole, feel close to this sentence, as a whole? That works beautifully for "a dog on a beach." It quietly fails for "two giraffes while a third eats from a tree," or "a sign that reads Norfolk," because the dominant visual feature drowns out the secondary constraints. The result is confident but unaccountable: you get a ranked list with no statement of which part of your request it actually honoured.
An embedding model scores that whole sentence against a whole image. If the picture has one monitor and three cups, it may still rank highly — the global match is "close enough." The paper's wager is that we can do better by refusing to collapse the query into a single point, and instead treating every noun and relation as a claim that must be checked.
In hardware/software verification, a specification is a logical formula and you machine-check whether a system satisfies it. The paper maps that whole apparatus onto vision.
A query q becomes a system specification. A parser P(q)=φ breaks it into subject–predicate–object triplets — a graph of independent claims. A synthesiser M:φ→Π turns each triplet into a visual routine πᵢ: a small executable program that returns True/False on any image. An image v satisfies φ only if every routine fires True.
The lineage matters: like ViperGPT and VisProg, an LLM writes Python that calls perception APIs. Unlike them, the goal is not to answer one question but to build a reusable set of logical triplets and rank images by how well they satisfy it — using open-source models (Phi-4 for parsing & synthesis, OWL-V2 for detection) for reproducibility.
The whole method is two functions and a checker. P parses the query into a specification; M maps each claim to a routine; the verifier runs them on the image. Click any box — or press run.
v satisfies the query φ if and only if every routine πᵢ ∈ Π returns True on it. Otherwise the verifier emits a visual counterexample — and, crucially, points to the exact triplet that failed.Click any step to walk through it on the running example. Each stage is a real artefact you could log, audit, or fix — the opposite of an opaque vector.
Granularity & state explosion. One could sample many subgraphs from φ — up to the cartesian product of all constraints, which blows up combinatorially. The paper sidesteps this the same way classical model checking does: compositional reasoning. A global statement is taken as true when its individual triplets are true, so each routine is verified locally and the results are aggregated, never enumerated jointly.
Same query, three candidate images. Pick one: each predicate node turns green (satisfied), amber (partial), or red (missing). The truth score is just the fraction that fired True — and you can always see which node failed.
Verification is binary, but retrieval needs an ordering. The fix: rank by the proportion of routines satisfied — and optionally fold that into an existing embedding ranker as a re-ranker.
For the top-K of a base ranker, each image at position i gets a retrieval weight K − i, scaled by the fraction of verified triplets. The verifiable signal lifts correct images that the embedding under-ranked, without throwing away the embedding's recall.
Why this is honest. An image that scored low on the embedding but verifies 6/6 constraints gets promoted; one that scored high but only verifies 2/6 gets pushed down. The ordering is now traceable to a count of satisfied claims rather than an inscrutable cosine similarity.
COCO was split by CLIP's own performance: Easy (top 25%), Hard (bottom 25% — counting, text, composition), and All. The method shines on Hard and lifts zero-shot embedding models when used as a re-ranker.
Table 2 — re-ranking on COCO-All. Green rows: our method boosts the base embedding model.
| Method | Rec@1 | Rec@3 | Rec@5 | Rec@10 | Zero-shot |
|---|---|---|---|---|---|
| CLIP (ViT-B) | .350 | .474 | .512 | .579 | ✓ |
| CLIP + ours | .355 | .468 | .535 | .621 | ✓ |
| ALIGN | .465 | .665 | .756 | .841 | ✓ |
| ALIGN + ours | .509 | .715 | .812 | .882 | ✓ |
| BEIT-3 (fine-tuned) | .665 | .841 | .891 | .962 | ✗ |
| BEIT + ours | .600 | .815 | .876 | .959 | ✗ |
| ours (base, standalone) | .429 | .606 | .676 | .815 | ✓ |
The honest caveat. On the combined split the gains are partly offset by noise: imperfect code synthesis and detector failures introduce errors. But unlike an embedding model, when this method is wrong, you can read exactly why.
Schematic recreations of the paper's qualitative cases. Green frame = the ground-truth image landed in the Top-3. Pick a query and compare how each system orders the candidates.
Every routine's verdict is auditable. Errors fall into four named buckets, located at distinct pipeline stages. Click a row to see the diagnosis — something a cosine similarity can never offer.
The point of the taxonomy. A failure is never just "wrong." It is a bad triplet (parser), a bad code generation (synthesiser), a bad code execution (detector under-performs), or even a wrong annotation (the dataset, not the model). In the failure case from the paper, the detector mistook skis for a baseball bat — and because that decision is explicit, the wrong promotion is fully explainable. CLIP made a similar mistake on a tennis racket, but only a human guessing could say so.
Future work points at named entities and real-world event context. But the core move is durable: anchoring image search in logic rather than intuition, so that "this matches" can finally be accompanied by "and here is exactly why."