LogicVal:A Logic-Formalized Benchmark for Constraint Satisfaction in Text-to-Image Generation

Savitha Sam Abraham; Marjan Alirezaie; Hossein Rahnama

cs.AIOct 16, 2026

LogicVal:A Logic-Formalized Benchmark for Constraint Satisfaction in Text-to-Image Generation

Authors: Savitha Sam Abraham, Marjan Alirezaie, Hossein Rahnama

Organizations: City St George’s, University of London · Toronto Metropolitan University · Flybits Labs, Creative AI Hub, Toronto · MIT Media Lab, Massachusetts Institute of Technology

Abstract

Text-to-Image (T2I) generative models have made significant progress in producing high-fidelity images from natural-language prompts. Alongside this progress, numerous benchmarks have been developed to evaluate capabilities such as attribute binding, numeracy, spatial reasoning, and commonsense reasoning. In this work, we propose a new perspective on T2I evaluation by casting it as a constraint-satisfaction problem. We introduce a logical framework that formally specifies the benchmark domain, including objects, attributes, and relations, alongside the constraints that generated images must satisfy. We evaluated four state-of-the-art T2I models across 9 classes of constraints ranging from a single-object-attribute to multi-object relationships constraints involving logical operators ( $\forall, \exists, count, \rightarrow$ ). Our results reveal a substantial gap between single-object and complex conditional multi-object relationship constraint classes, with the best-performing model achieving 98% accuracy on the former and just 53% on the latter. We assess compositional generalisation, finding that the best-performing model`s accuracy drops from 84% on single-constraint prompts to 20% when satisfying multiple constraints simultaneously. Identifying unsatisfiable constraints is also challenging, with the best model correctly recognizing only 23% of such prompts. Building on this framework, we introduce LogicVal, an evaluation methodology that combines neural visual detection with logical reasoning to assess constraint satisfaction in generated images. On CLEVR, LogicVal achieves ROC-AUC scores ranging from 0.88 to 0.98, indicating strong alignment with human judgments. These findings underscore the value of logic-based evaluation for characterizing T2I model capabilities and limitations.

Figures & tables

Panel of Figure 1 — Figure 1: Overview of LogicVal, following one specification (class C6). ① The benchmark: a formal specification (domain and constraint templates) is instantiated and labelled SAT/UNSAT by clingo and verbalised into a prompt. ② Image generation: the prompt is rendered by a T2I model. ③ LogicVal evaluation: scene graph is extracted and checked against the constraint specification with clingo .

Benchmark	Negation	$\forall/\exists$	Counting	Composition	UNSAT	Formal spec.
T2I-CompBench ( 2023 )	–	$\circ$	$\circ$	✓	–	–
GenEval ( 2023 )	–	$\circ$	$\circ$	$\circ$	–	–
GenEval 2 ( 2025 )	–	$\circ$	$\circ$	✓	–	–
GenAI-Bench ( 2024 )	✓	$\circ$	✓	✓	–	–
GeckoNum ( 2024 )	$\circ$	$\circ$	$\circ$	–	–	–
NegT2IBench ( 2026 )	✓	$\circ$	–	$\circ$	–	–

Table 1: Comparison with other T2I benchmarks based on logical operators evaluated, presence of unsatisfiable prompts, a formal specification. ✓ covered,

\circ

partly, – not covered.

Object-level
ID	Name	#T	Abstract Form	Example template instance (ASP)	Natural language
C1	Existential Object	11	$\exists x\,\Phi(x)$	:- #count{X: obj(X), hP(X,color,red)} = 0.	A red object is in the scene.
C2	Universal Object	9	$\forall x\,\Phi(x)$	:- obj(X), hP(X,shape,sphere).	No object is sphere.
C3	Conditional Object	10	$\forall x\,(\Phi(x)\rightarrow\Psi(x))$	:- obj(X), hP(X,color,blue), hP(X,region,r3).	Every blue object is not in r3.
SubGraph-level
C4	Existential	4	$\exists\bar{x}\,(\Phi(\bar{x})\wedge R(\bar{x}))$	:- #count{Z,X1,X2: …, hP(Z,shape,sphere), hP(X1,region,r1), hP(X2,shape,cube), hR(Z,X1,right), hR(Z,X2,behind)} = 0.	There exists a sphere object that is to the right of an object in r1, and also behind a cube object.

Table 2: Primitive constraint classes with their abstract form (notation as in § 3.2 ), the number of templates in the class (#T; Appendix B ), an example template from the class, and its natural language form. In the ASP column, obj , hP and hR abbreviate object , hasProperty and hasRelationship , auxiliary predicates are renamed, “…” omits the object and distinctness atoms, and the anti-vacuity rules (and the corresponding part of the prompt).

	GPT	Gemini	Flux	QwenImage
1SAT	0.577	0.848	0.031	0.017
3SAT	0.200	0.480	0.000	0.000
6SAT	0.000	0.200	0.000	0.000

Table 3: Success rate per model and package (based on human judgement).

	GPT	Flux	QwenImage
1SAT	0.001	0.138	0.507
3SAT	0.000	0.040	0.120
6SAT	0.000	0.040	0.040

Table 4: Rate of images with at least one deformed object (based on human judgement).

Figure 2: Success rate per constraint class (based on human judgement) on 1SAT . C1–C3: single objects; C4–C7: relations under quantifiers; C8–C9: counts.

Figure 3: Success rate on 1SAT : short vs. long prompts.

Figure 4: Satisfaction rate on 1SAT with and without the object-count requirement.

Metric	GPT	Gemini	Flux	QwenImage
ClipScore	-0.081	0.158	0.046	0.009
VLM-Judge	0.127	0.152	0.217	0.160
Soft-TIFA (AM)	0.247	0.128	0.276	0.223
Soft-TIFA (GM)	0.289	0.216	0.246	0.206
LogicVal	0.970	0.700	0.712	0.522

Table 5: Point-biserial correlation with human scores.

Figure 5: ROC-AUC of each metric against the human verdict on 1SAT ; the dashed line marks chance (0.5).

	GPT	Gemini	Flux	QwenImage
1SAT	96.34	90.70	97.61	96.62
3SAT	96	88	100	100
6SAT	100	92	100	100

Table 6: Percentage of images both LogicVal and human accept or reject.

	GPT	Gemini	Flux	QwenImage
1SAT	0.744	0.323	0.154	0.141
3SAT	0.600	0.560	0.040	0.200
6SAT	0.480	0.680	0.160	0.240

Table 7: Scene Graph Extraction Accuracy: percentage of predicted graphs matching human annotations.

Appendix figures & tables6 assets

Supplementary material from the paper’s appendix.

Appendix

C3 (template 1propA_1propC ), $n=4$
ASP	:- object(X), hasProperty(X,color,green), not hasProperty(X,material,metal). :- #count{X: object(X), hasProperty(X,color,green)} = 0.
Short	At least one object is green, and every green object is also metal.
Long	The scene must contain at least one object that is green. Whenever an object is green, it must simultaneously be metal.
C7 (template 1prop_exact ), $n=6$
ASP	:- object(X), hasProperty(X,region,r1), #count{Y: object(Y), X!=Y, hasProperty(Y,material,rubber), hasRelationship(Y,X,behind)} != 3. :- #count{X: object(X), hasProperty(X,region,r1)} = 0.
Short	There must be at least one object that is in r1. Every such object has exactly three rubber objects that are behind it.

Appendix

Table 8: Three 1SAT specifications, each shown with its instantiated ASP rules, its two natural-language forms - a short and a long version. The second ASP rule of each example is the anti-vacuity condition.

Constraints per spec ( $m$ )	SAT	UNSAT	Total
1	355	25	380
3	25	10	35
6	25	69	94
Total	405	104	509
Templates covered ( 1SAT )	71	14

Appendix

Table 9: Number of prompts per package (top) and per constraint class in 1SAT (bottom).

Category	Sub-question	Expected answer
Common sub-questions
Common (SAT)	Is there any shape other than cube, sphere, or cylinder?	No
Common (SAT)	Are all objects among the following colors: gray, red, blue, green, brown, purple, cyan, or yellow?	Yes
Common (SAT)	True or False: All objects are either metal or rubber.	True
Common (SAT)	Is the image an empty scene with a white background?	No
Common (SAT)	How many objects are in the scene?	number_of_objects (from the prompt)

Appendix

Table 10: Common and prompt-specific sub-questions used in Soft-TIFA, along with their expected answers. Expected answers may be template-based, as in

c>0

, where the value of c is obtained from GPT-4o. Subsequent references to

c

, such as in

=c

, are instantiated using the value assigned to

c

based on GPT-4o’s answer to the first sub-question.

Figure 6: The annotation tool, showing the Gemini-3-Pro-Image image of Figure 1 . The object list (centre) and the property editor (right) set each object’s shape, colour and material, and its region is derived from the box. The annotator also marks whether the image is a reasonable scene, or marks it as empty.

Panel of Figure 7 — Figure 7: Images generated by each model for the same prompt (short version), with the human verdict (✓/✗) and, for failures, the reason.

Figure 8: Satisfaction rate per template on 1SAT (short prompts), one panel per class; each cell is computed from five images.

Image Generation Evaluation

Image generation evaluation measures the quality, fidelity, diversity, and instruction-following ability of AI-generated images.

See all 108 papers

Imag-Eval: a language-grounded framework for interpretable Text-to-Image instruction following evaluation
Aug 29, 2026Ibrahim Mohamed Serouis, David Jaramillo DuqueT2I Generation Evaluation Compositional T2I Generation
Talan Research and Innovation Center Toulouse, France · Talan Research and Innovation Center Paris, France
DynEval: Holistic Evaluations of T2I Generative Models in the Wild
Jul 13, 2026Shyam Marjit, Dheeraj Baiju, Anuj Shikarkhane +3VLM Evaluation Automated Evaluation
Indian Institute of Science · VCL, IISc · Hugging Face
TIIF-Bench: How Does Your T2I Model Follow Your Instructions?
Jun 2, 2025Xinyu Wei, Jinrui Zhang, Zeqing Wang +4Vision-Language Model-as-a-Judge T2I Generation Evaluation
The Hong Kong Polytechnic University · OPPO Research Institute · Tsinghua University

Aug 29, 2026J/K move · Enter open · S save

Imag-Eval: a language-grounded framework for interpretable Text-to-Image instruction following evaluation

Ibrahim Mohamed Serouis, David Jaramillo Duque

Talan Research and Innovation Center Toulouse, France · Talan Research and Innovation Center Paris, France

T2I Generation Evaluation Compositional T2I Generation

Open paper AskPDF arXiv

Text-to-Image (T2I) models have recently achieved impressive visual fidelity, yet their evaluation remains constrained by benchmarks that are often difficult to interpret and insufficiently diagnostic. Existing skill-based evaluations tend to overlook critical failure modes that strongly impact usability but fall outside standard taxonomies, such as global incoherence arising from missing parts or physically implausible configurations (e.g., floating objects). In addition, prompt difficulty is typically controlled along a single dimension; either prompt length or the number of elements to generate. To address these limitations, we introduce Imag-Eval, a controlled benchmark designed to assess how T2I models ground compositional natural-language instructions into visual outputs. Unlike prior work that conflates surface linguistic complexity with compositional difficulty, Imag-Eval explicitly seeks to disentangles these factors by independently varying both the number of instances and the combination of constraints (rules), while avoiding error propagation. This design enables fine-grained and interpretable analysis of where cross-modal instruction following fails. Our benchmark comprises 1,140 prompts and 8,842 combined rules, and we evaluate it on several state-of-the-art models. Complementing this analysis with an additional study of over 2,000 prompts from a concurrent benchmark, our results suggest that, for structured skills, compositional difficulty is primarily governed by the number of grounded rules and their binding to instances,, rather than by prompt length alone.

Abstract

Image Generation Evaluation

Explore similar work

Imag-Eval: a language-grounded framework for interpretable Text-to-Image instruction following evaluation

DynEval: Holistic Evaluations of T2I Generative Models in the Wild

TIIF-Bench: How Does Your T2I Model Follow Your Instructions?