LLM指令遵循的神经符号验证

将大语言模型（LLM）应用于重要任务的一个根本问题在于：LLM并不总是遵循指令，而违规往往难以观察或检查。在基于LLM的Agentic工作流中，此类违规会沿推理链传播和放大，导致任务失败和系统事故。本文提出NSVIF，一个用于验证LLM输出是否遵循其提示所用指令的神经符号框架。NSVIF是通用、一般用途的验证器；它对指令或LLM不作任何假设。NSVIF将指令遵循验证形式化为约束满足问题，将用户指令建模为约束。NSVIF同时建模逻辑约束和语义约束；约束求解由统一求解器完成，它编排逻辑推理与语义分析。为评估NSVIF，我们开发了VIFBENCH，一个带有细粒度数据标注的指令遵循验证器新基准。实验表明，NSVIF显著优于基于LLM的方法，并提供可解释的反馈。我们还表明，NSVIF的反馈无需后训练即可帮助提升LLM的指令遵循能力。