Neuro-Symbolic Verification on Instruction Following of LLMs

TL;DR

This paper introduces NSVIF, a neuro-symbolic framework that verifies if LLM outputs follow instructions, improving detection of violations and aiding in enhancing LLM instruction-following without retraining.

Contribution

NSVIF is a universal verifier that models instruction-following as a constraint-satisfaction problem, combining logical and semantic reasoning, and is supported by the new VIFBENCH benchmark.

Findings

NSVIF outperforms LLM-based verification methods.

Provides interpretable feedback on instruction adherence.

Feedback from NSVIF improves LLM instruction-following capabilities.

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.