LLM의 지시 이행에 대한 뉴로-심볼릭 검증

Neuro-Symbolic Verification on Instruction Following of LLMs

거대 언어 모델(LLM)을 주요 애플리케이션에 적용할 때 발생하는 근본적인 문제는 LLM이 항상 지시를 따르지는 않으며, 이러한 위반 사항을 관찰하거나 확인하기 어려운 경우가 많다는 점입니다. LLM 기반의 에이전트 워크플로우에서 이러한 위반은 추론 사슬을 따라 전파되고 증폭되어, 결국 작업 실패나 시스템 사고를 유발할 수 있습니다. 본 논문에서는 LLM의 출력이 프롬프트에 사용된 지시를 따르는지 검증하기 위한 뉴로-심볼릭 프레임워크인 NSVIF를 제안합니다. NSVIF는 보편적인 범용 검증기로서 지시나 LLM에 대해 어떠한 가정도 하지 않습니다. NSVIF는 사용자 지시를 제약 조건으로 모델링하여 지시 이행 검증 과정을 제약 만족 문제로 공식화합니다. 또한 논리적 제약과 의미적 제약을 모두 모델링하며, 논리적 추론과 의미론적 분석을 조율하는 통합 솔버를 통해 제약 조건을 해결합니다. NSVIF를 평가하기 위해, 세밀한 데이터 레이블을 갖춘 지시 이행 검증기용 새로운 벤치마크인 VIFBENCH를 개발했습니다. 실험 결과, NSVIF는 LLM 기반 접근 방식보다 성능이 크게 우수하며 해석 가능한 피드백을 제공하는 것으로 나타났습니다. 또한 NSVIF의 피드백이 사후 학습(post-training) 없이도 LLM의 지시 이행 능력을 향상하는 데 도움이 됨을 입증했습니다.

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.