Source-linked AI summary
Think-Verify-Revise: Neuro-Symbolic Visual Reasoning with Vision-Language Models and Dynamic Logic Tensor Networks
Homayoun Afshari, Pietro Basci, Alessandro Russo, Lia Morra
TL;DR
Visual reasoning needs both visual perception and formal relational reasoning, but existing neural and symbolic approaches leave this combination incomplete. The paper couples VLM-based FOL rule induction with differentiable D-LTN verification in a feedback loop, recovering valid Sudoku constraints from three examples and showing logically equivalent rule discovery across benchmark domains.
Problem
Visual reasoning requires jointly applying formal relational constraints to visual content, while pure neural systems struggle with logical chaining and traditional NeSy systems often require hand-crafted rules.
Method
A VLM proposes grammar-constrained FOL rules, a dynamically assembled D-LTN verifies them on CNN-derived visual embeddings, and verification feedback guides iterative revision.
Results
The framework recovers valid Sudoku constraints from three labelled examples and converges to logically equivalent formulations across MNIST, EMNIST, and KMNIST domains.
Takeaways & Limitations
The results support automatic discovery of interpretable visual reasoning rules through coupled VLM hypothesis generation and differentiable logical verification.
Takeaways & Limitations
The framework currently assumes a fixed alphabet and is evaluated on a single benchmark in a single-rule scenario; FMNIST also produced a syntactically valid but semantically insufficient rule.
Abstract
from arXiv · showhide
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.
1 Introduction
The paper addresses the challenge of combining visual perception with formal relational reasoning by coupling VLM-based FOL rule induction with differentiable D-LTN verification. A closed feedback loop refines candidate rules and enables valid Sudoku constraints to be induced from limited visual examples.
- Motivation: Visual reasoning requires jointly perceiving visual content and applying formal relational constraints, which pure neural and hand-crafted symbolic approaches handle incompletely.VLMs struggle to reliably chain logical rules, while traditional NeSy systems commonly require experts to specify task-specific knowledge.
- Approach: The framework couples a VLM rule inducer with a D-LTN verifier that parses candidate FOL rules, grounds them on CNN visual embeddings, and returns satisfiability feedback.The verifier is dynamically assembled from the induced rule, and its differentiability permits gradients to reach the visual encoder.
- Approach: Grammar-constrained prompting steers VLM outputs toward syntactically valid and formally parseable FOL rules compatible with downstream verification.The strategy is intended to reduce hallucinations and preserve compatibility with the D-LTN verifier.
- Evaluation: Three labelled training examples and 3–19 VLM iterations suffice to induce valid Sudoku constraint rules in the reported setting.The evaluation uses visually encoded 4×4 Sudoku boards from MNIST, EMNIST, KMNIST, and FMNIST domains.
- Evaluation: The CNN+D-LTN architecture matches or outperforms NeuPSL and LTN-IND A/B/C across all four visual domains.This comparison is reported for the independent evaluation of the induced symbolic rules.
2 Related Work
Related work combines neural perception with symbolic rule learning through LLMs, VLMs, agents, and discrete solvers. The proposed framework differs by using a differentiable symbolic verifier that propagates gradients into visual perception.
- Visual reasoning benchmarks: Visual reasoning benchmarks combine visual perception with symbolic relational constraints, including ViSudo-PC, which evaluates visually rendered Sudoku grids.Other cited benchmarks include VAR, VideoABC, Raven’s Progressive Matrices, and CLEVR.
- Existing NeSy approaches: Prior systems use multimodal generators, LLM reasoners, VLM verifiers, ILP, ASP, or interactive induction-deduction-abduction loops for symbolic visual reasoning.The cited approaches vary in whether agents are frozen, rules are discretely solved, or feedback is used interactively.
- Existing NeSy approaches: The proposed framework shares the closed feedback-loop structure of IDEA while grounding verification in a dynamically constructed D-LTN.The comparison connects the system’s induction, deduction, and abduction pattern to prior agent-based work.
- Distinction: Unlike LLM/VLM agents that provide no gradient signal, the D-LTN propagates gradients through the symbolic layer into the visual encoder for end-to-end optimisation.This differentiable connection is the stated distinction from the discrete symbolic layers in the related systems.
3 Methodology
The methodology iteratively generates, parses, grounds, verifies, and revises symbolic rules. A VLM proposes FOL rules from labelled examples, while a CNN and dynamically built D-LTN evaluate their satisfaction against visual data.
- Overview: The framework begins with labelled visual examples and combines neural perception, symbolic rule induction, and differentiable logical reasoning in an iterative loop.Candidate rules are generated, verified against visual evidence, and progressively refined until valid constraints are discovered.
- Architecture: A VLM Rule Generator induces candidate logical rules, a CNN extracts visual representations, and a D-LTN evaluates the rules through differentiable reasoning.A Feedback Loop uses verification outcomes to guide subsequent rule generation.
- Rule verification: Generated FOL rules are syntactically parsed, translated into symbolic representations, and used to dynamically construct an LTN whose predicates are grounded in CNN visual representations.The verifier computes how strongly the generated rules are satisfied by the visual evidence.
- Rule induction: The Rule Generator produces symbols, FOL statements, and groundings that define the semantics of logical constants, predicates, and functions.Few-shot and Chain-of-Thought prompting combines textual instructions, visual examples, and intermediate feedback for VLM rule induction.
- Rule induction: A post-processing stage extracts formal symbolic content from raw VLM responses before forwarding rules and groundings to verification.Predefined patterns and regular expressions discard auxiliary reasoning text.
- Feedback handling: A rule with truth value t is accepted when t ≥ τ; otherwise, its evaluation and parsing feedback are inserted into the next prompt until acceptance or the iteration limit.The threshold τ is a user-defined hyperparameter, and syntactically invalid rules are returned with parsing errors rather than evaluated by the D-LTN.
4 Experimental Setup
The experiments evaluate visual Sudoku verification against prior neuro-symbolic systems while detailing the VLM rule-generation loop, differentiable training, and CNN configuration selection.
- Benchmark and evaluation: ViSudo-PC evaluation uses visually encoded Sudoku boards from MNIST, EMNIST, KMNIST, and FMNIST domains.Each board pair contains one valid and one corrupted 4 × 4 board, with 100 pairs in each split.
- Benchmark and evaluation: The method is compared with NeuPSL and three LTN variants: LTN-IND A, LTN-IND B, and LTN-IND C.Baseline results are taken from the original published works under the same benchmark setting.
- Benchmark and evaluation: Performance is measured with AUC, aggregated independently across the benchmark’s ten evaluation splits for comparability with prior work.AUC measures discrimination between valid and corrupted boards without selecting a classification threshold.
- Rule generation: The VLM generates one FOL rule per iteration using predefined grounded predicates, while previous rules and verification scores guide subsequent refinement.The prompt constrains the rule grammar and records trial errors, extracted rules, and conformity ratios.
- Training and tuning: The visual encoder trains end-to-end with the Rule Verifier, allowing gradients from differentiable logical constraints to update CNN parameters.The objective uses board labels and the composed CNN–D-LTN model to encourage logical satisfaction for valid boards and non-satisfaction for invalid boards.
- Training and tuning: CNN hyperparameters are searched across four data sources using an initial hand-crafted FOL rule, and the configuration with the highest average AUC is selected.The hand-crafted rule is used only for hyperparameter tuning and not in subsequent experiments.
5 Results
The framework discovers logically valid Sudoku rules across MNIST, EMNIST, and KMNIST, with performance matching or outperforming baselines across four domains. FMNIST exposes a semantic failure, while the broader results support differentiable verification as a complement to VLM rule generation.
- Visual encoder selection: 0.9560 average test AUC and 85.50% accuracy identify the selected CNN encoder used for subsequent rule-verification experiments.The configuration used cnn_dims=(32,64), kernel_dims=(4,4), embed_dims=(64,), drop_prob=0.2, and use_softmax=True.
- Symbolic rule discovery: MNIST, EMNIST, and KMNIST yielded syntactically different FOL rules that are logically equivalent and encode the same Sudoku constraint.The constraint prohibits distinct cells sharing a row, column, or block from containing the same value.
- Symbolic rule discovery: The framework did not discover a valid FMNIST rule within the 20-iteration limit, producing a syntactically valid but semantically incomplete constraint.The discovered FMNIST rule omitted the block relation and therefore only partially represented the target Sudoku constraint.
- Visual reasoning performance: The proposed method consistently matches or outperforms baselines across all four ViSudo-PC visual domains.Table 2 reports test AUC ± std., averaged over the first 10 benchmark splits.
- Visual reasoning performance: Performance differences from LTN-IND are not attributable to symbolic knowledge because the induced rule is logically equivalent to theirs.The paper attributes gains to the visual encoder, embedding-space grounding, and broader hyperparameter search.
- Discussion: Combining VLM hypothesis generation with differentiable logical verification discovers interpretable visual reasoning rules from limited supervision.The framework searches for valid symbolic explanations rather than reproducing one predefined formula exactly.
- Limitations and future work: The current framework assumes a fixed alphabet, a single benchmark, and a single-rule scenario, limiting its scope for broader visual reasoning tasks.The paper identifies automatic symbol discovery and multi-rule theories as future extensions.
6 Conclusion
The framework combines VLM-based FOL rule induction with D-LTN verification in a feedback loop, recovering valid Sudoku constraints from visual data while reducing reliance on manually specified knowledge.
- The architecture integrates VLM-based FOL rule induction with D-LTN differentiable verification in a closed iterative feedback loop.This combines neural perception, logical reasoning, and feedback-driven refinement.
- Using only a small set of labeled visual examples, the system generates, validates, and progressively improves candidate rules.
- The framework recovered valid Sudoku constraints in MNIST, EMNIST, and KMNIST, converging to logically equivalent formulations despite syntactic variations.
- The findings indicate that VLMs can support symbolic rule induction when coupled with formal verification, reducing the need for manually specified knowledge.