Neuro-Symbolic Verification on Instruction Following of LLMs

TL;DR

This paper introduces NSVIF, a universal neuro-symbolic verifier that treats instruction-following verification as a constraint-satisfaction problem, combining logic and semantic constraints via a Z3 SMT solver. It also provides VIFBench, a fine-grained benchmark with labeled constraint violations to evaluate verifiers’ reasoning over multiple interacting constraints. Empirical results show NSVIF outperforms LLM-based judges and can provide actionable, constraint-level feedback to improve LLM instruction following without post-training. Overall, the work demonstrates that decomposing instructions into explicit constraints and integrating symbolic reasoning with neural analysis yields more reliable, interpretable verification in agentic LLM workflows.

Abstract

A fundamental problem of applying Large Language Models (LLMs) to important applications is that LLMs do not always follow instructions, and violations are often hard to observe or check. In LLM-based agentic workflows, such violations can propagate and amplify along reasoning chains, causing task failures and system incidents. This paper presents NSVIF, a neuro-symbolic framework for verifying whether an LLM's output follows the instructions used to prompt the LLM. NSVIF is a universal, general-purpose verifier; it makes no assumption about the instruction or the LLM. NSVIF formulates instruction-following verification as a constraint-satisfaction problem by modeling user instructions as constraints. NSVIF models both logical and semantic constraints; constraint solving is done by a unified solver that orchestrates logical reasoning and semantic analysis. To evaluate NSVIF, we develop VIFBENCH, a new benchmark for instruction-following verifiers with fine-grained data labels. Experiments show that NSVIF significantly outperforms LLM-based approaches and provides interpretable feedback. We also show that feedback from NSVIF helps improve LLMs' instruction-following capability without post-training.

Figures (10)

• Figure 1: Overview of the Nsvif framework and the verification workflow.
• Figure 2: Overview of VifBench's data generation
• Figure 3: An example data entry in VifBench
• Figure 4: F1 scores of Nsvif and the baseline by number of constraints in an instruction (using GPT-4.1)
• Figure 5: Workflow of Nsvif improving LLM instruction following via multi-turn feedback.