Think-Verify-Revise: Neuro-Symbolic Visual Reasoning with Vision-Language Models and Dynamic Logic Tensor Networks

AI summary

Overview

Research area: Neuro-symbolic (NeSy) AI for visual reasoning — specifically the automatic induction of First-Order Logic (FOL) rules from images, verified by a differentiable Logic Tensor Network.

Technical level: Advanced. The paper assumes familiarity with logic programming, fuzzy/t-norm semantics, neural-symbolic grounding, and Vision-Language Model prompting.

Scope in one sentence: The paper proposes and evaluates a closed-loop "Think–Verify–Revise" framework that couples a VLM rule inducer with a Dynamic Logic Tensor Network verifier on the ViSudo-PC benchmark across four visual domains.

What This Paper Is About

Visual reasoning tasks, such as judging whether a visually rendered Sudoku board is valid, require a system to both perceive images and apply formal relational constraints. Pure neural models (including VLMs) struggle to reliably chain logical rules, while traditional neuro-symbolic systems achieve transparency only by having a human expert hand-craft the logical rules for each new task. The goal of this paper is to answer the question of where rules come from: can FOL rules be induced automatically from data in a form that is machine-verifiable and generalisable across visual domains?

Key Contributions

1. A closed-loop framework for automatic induction of FOL rules from visual data, combining VLM-based abductive hypothesis generation with D-LTN-based differentiable verification in an iterative Think–Verify–Revise cycle.
2. A grammar-constrained prompting strategy that steers VLM output toward syntactically valid, formally parseable FOL rules, reducing hallucinations and ensuring compatibility with the D-LTN verifier.
3. Demonstration that valid Sudoku constraint rules can be induced using only three training examples as visual context and a limited number of VLM interactions (the paper reports 3–19 iterations).
4. Evidence that the standalone CNN+D-LTN architecture matches or outperforms existing state-of-the-art methods — including NeuPSL and the LTN-IND A/B/C variants — across all four visual domains, independently of the VLM induction component.

Main Findings

• Visual encoder selection: The best configuration from hyperparameter search was cnn_dims=(32,64), kernel_dims=(4,4), embed_dims=(64,), drop_prob=0.2, and use_softmax=True, achieving an average test AUC of 0.9560 and an accuracy of 85.50%.
• Rule discovery succeeded on three of four domains: On the 11th split, the VLM induced valid rules for MNIST (Rule 1, 19 iterations, AUC 0.9974), EMNIST (Rule 2, 13 iterations, AUC 0.9012), and KMNIST (Rule 3, 9 iterations, AUC 0.9517), using 3 training examples as visual context in each case.
• FMNIST failed within the iteration limit: The framework did not discover a valid rule before reaching the maximum of 20 iterations. The VLM produced a syntactically valid but semantically insufficient rule (Rule 4) that encoded only a partial representation of the Sudoku constraint.
• Discovered rules are syntactically different but logically equivalent: Rules 1 and 2 differ only in conjunct ordering (conjunction is commutative); Rule 3 is shown equivalent to the others via the contrapositive and De Morgan's law. All three encode: two distinct cells in the same row, column, or block cannot contain the same value.
• Comparison on the first 10 splits (test AUC ± std.): Ours — MNIST 0.94 ± 0.10, EMNIST 0.93 ± 0.10, KMNIST 0.88 ± 0.10, FMNIST 0.87 ± 0.09. NeuPSL — 0.88 ± 0.02, 0.79 ± 0.09, 0.65 ± 0.12, 0.74 ± 0.04. LTN-IND A — 0.83 ± 0.18, 0.58 ± 0.04, 0.83 ± 0.09, 0.67 ± 0.11. LTN-IND B — 0.84 ± 0.14, 0.58 ± 0.06, 0.85 ± 0.11, 0.76 ± 0.15. LTN-IND C — 0.94 ± 0.10, 0.65 ± 0.14, 0.87 ± 0.09, 0.83 ± 0.11.
• Gains are not explained by symbolic knowledge: The induced rule is logically equivalent to the one used by the LTN-IND variants, so improvements are attributed to (i) the visual encoder producing high-dimensional embeddings rather than digit predictions, and (ii) a broader hyperparameter search. The key architectural difference is the grounding of P_same_value: LTN-IND computes an exponential distance on logit predictions, while this work computes the same exponential distance in a high-dimensional embedding space, which degrades more gracefully on visually harder domains such as EMNIST.
• Termination criterion: The Think–Verify–Revise loop stops when the corresponding D-LTN reaches AUC ≥ 0.95 on the test set, at which point the candidate rule is considered valid.

Methodology in Plain English

The framework has four interconnected parts operating in a loop:

1. Think (Rule Generator). A VLM — specifically Llama-4-Maverick-17B-128E-Instruct, accessed via the Groq API, using a Mixture-of-Experts architecture with 128 experts and a context window of up to one million tokens — receives a textual task description plus a few labelled visual examples, along with few-shot and Chain-of-Thought prompting. It is constrained to output only FOL rules over a fixed vocabulary of pre-grounded predicates (P_same_row, P_same_col, P_same_block, P_same_loc, P_same_value), with constants and functions disallowed, and one rule per iteration. A post-processing stage uses Regular Expressions to strip out reasoning traces and keep only the formal symbolic content.
2. Verify (Rule Verifier). A Rule Parser converts the FOL rule into a syntax tree; an LTN Builder turns tree nodes into custom node classes that form the LTN formula, which is the computation graph itself. Predicates are grounded on visual embeddings from a CNN. Structural predicates use binary similarity; P_same_value uses exponential similarity. Logical connectives use Goguen's product t-norm (AND), Goguen's t-conorm (OR), complement (NOT), Reichenbach's implication, and linear similarity (IFF), with generalized mean w.r.t. the error for FORALL and generalized mean for EXISTS.
3. Visual Encoding. Input tensors of shape B × O × C × W × H (batch, objects per image, channels, width, height) are mapped by the CNN to embeddings of shape B × O × E. Row and column indices are concatenated with the semantic embeddings to add positional information. The CNN is trained end-to-end in all experiments, not frozen.
4. Revise (Feedback Loop). The generated rule, its performance evaluation, and any parsing errors are fed back into the next prompt, including a history of prior trials with their rules and "conforming images" percentages. The process repeats until the rule passes the threshold or the maximum iteration count is reached.

Training uses a loss that is f(x) when the board label is 0 and 1 − f(x) when the label is 1, where f is the composed CNN–D-LTN model. Because LTNs are differentiable, gradients propagate through the logical constraints back to the CNN. Hyperparameter tuning was performed on the 11th split with an initial hand-crafted FOL rule, used exclusively for that purpose and not in subsequent experiments.

Why This Matters

Impact on research. The work shows that VLMs can serve as abductive symbolic hypothesis generators when paired with a formal, differentiable verifier, rather than as static rule writers. The finding that the framework converges to logically equivalent but syntactically distinct rules suggests it performs a search over valid symbolic explanations rather than reproducing a predefined rule. It also highlights that the choice of grounding space (logit predictions versus high-dimensional embeddings) can substantially affect downstream logical verification, motivating co-design of logic formulation and grounding. Unlike prior LLM-based rule induction systems (Concept-RuleNet, ILP-CoT, VLM+ASP, IDEA), whose symbolic layers are discrete solvers or frozen prompted agents admitting no gradient signal, the D-LTN verifier propagates gradients back into the visual encoder.

Real-world applications (as directions this capability supports):

• Automated compliance and constraint checking on visually encoded data, such as verifying that a scanned form or grid satisfies structural rules.
• Industrial quality inspection, where symbolic constraints over detected parts could be induced rather than hand-coded.
• Document and table validation in which relational rules between visual elements must be enforced.
• Assistive or educational tools that check the validity of puzzle-like or grid-based visual inputs.

Industry relevance. The framework reduces dependence on human experts to hand-craft logical knowledge for each new task, which is a practical bottleneck in deploying neuro-symbolic systems. Its modular structure (VLM inducer, CNN encoder, LTN verifier) allows components to be swapped — the authors note the approach could extend to other NeSy frameworks such as NeuPSL — and tighter integration with libraries like LTNtorch or Uller is identified as a path to lower adoption barriers.

Future Directions

• Automatic symbol discovery: The current approach assumes a fixed alphabet of predicates and groundings is provided a priori; learning which concepts to ground as FOL predicates from raw visual data would broaden applicability.
• Multi-rule theories: Experiments are limited to a single benchmark and a single-rule scenario. Extending to multi-rule knowledge bases would better reflect real-world visual reasoning complexity; the authors note the training objective could then be replaced by the satisfiability of the knowledge base.
• Transfer learning and pretrained perception: The paper does not explore pretraining the perception module, which may further simplify rule discovery and reduce the need for task-specific hyperparameter tuning.
• Learning the query strategy: Although the closed feedback loop structurally resembles reinforcement learning, no formal RL objective is optimized. Policy-gradient or actor-critic methods to train the VLM query strategy could make rule induction more sample-efficient.
• Ecosystem integration: The framework is a standalone prototype; closer integration with established NeSy libraries such as LTNtorch or Uller would facilitate broader comparison and adoption.
• Open question raised by the FMNIST failure: Why did the VLM fail to establish a reliable visual-to-symbolic correspondence for clothing items when it succeeded on digits, letters, and Japanese characters, and how can that gap be closed?

Target Audience

This paper is best suited to neuro-symbolic AI and computer vision researchers, particularly those working on differentiable logic, Logic Tensor Networks, or rule induction from multimodal data. It will also interest practitioners exploring VLM-plus-verifier pipelines for structured reasoning, and graduate students with prior exposure to first-order logic and fuzzy t-norm semantics. A beginner audience would need supplementary background in NeSy grounding and logic programming.

Authors’ abstract

Visual reasoning tasks require a system to jointly perceive visual content and apply formal relational constraints---a combination that neither pure neural nor purely symbolic approaches handle well in isolation. This paper proposes a Neuro-Symbolic (NeSy) framework that closes this gap by tightly coupling a Vision-Language Model (VLM) for automatic First-Order Logic (FOL) rule induction with a Dynamic Logic Tensor Network (D-LTN) for differentiable rule verification, in a closed iterative feedback loop. The VLM receives a small set of labelled visual examples and proposes candidate FOL rules conforming to a strict grammar (Think); the D-LTN is automatically assembled from these rules at runtime and evaluates them grounding on CNN-produced visual embeddings (Verify); and verification failures are fed back to guide the VLM's next hypothesis (Revise). Evaluated on the ViSudo-PC benchmark across four visual domains (MNIST, EMNIST, KMNIST, FMNIST), the system induces valid Sudoku constraint rules using only three training examples as visual context. The proposed method achieves AUC scores matching or outperforming previous methods (NeuPSL, LTN), showing the potential for automatic rule discovery through VLM. Code is available at https://github.com/homayoun-afshari/nesy.