Think-Verify-Revise: Neuro-Symbolic Visual Reasoning with Vision-Language Models

Forum topic · 小凯 · 2026-09-09

Summary

This arXiv paper (2609.05388) by Homayoun Afshari, Pietro Basci, Alessandro Russo, and Lia Morra proposes a neuro-symbolic framework for visual reasoning that combines perception with formal relational constraints. The system couples 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, operating in a closed iterative loop: the VLM proposes candidate FOL rules from a small set of labelled examples (Think), the D-LTN is assembled at runtime and evaluates rules grounded on CNN visual embeddings (Verify), and verification failures guide the VLM toward new hypotheses (Revise). Evaluated on the ViSudo-PC benchmark across four visual domains (MNIST, EMNIST, KMNIST, FMNIST), the system induces valid Sudoku constraint rules from only three training examples. Its AUC matches or exceeds prior methods such as NeuPSL and LTN, demonstrating the potential of automated rule discovery via VLMs.

Paper Overview

Field: Computer Vision (CV) Authors: Homayoun Afshari, Pietro Basci, Alessandro Russo, Lia Morra arXiv: 2609.05388

Introduction

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 Think-Verify-Revise Loop

1. Think: The VLM receives a small set of labelled visual examples and proposes candidate FOL rules conforming to a strict grammar. 2. Verify: The D-LTN is automatically assembled from these rules at runtime and evaluates them, grounding on CNN-produced visual embeddings. 3. Revise: Verification failures are fed back to the VLM, guiding it to generate the next hypothesis.

Results

Evaluated on the ViSudo-PC benchmark across four visual domains: MNIST, EMNIST, KMNIST, and FMNIST.
The system induces valid Sudoku constraint rules using only three training examples.
Achieved AUC scores matching or surpassing prior methods (NeuPSL, LTN), demonstrating the potential of automated rule discovery via VLMs.

Reference

Paper link: https://arxiv.org/abs/2609.05388