发表机构
AI Institute of South Carolina; HPE Labs; Indian AI Research Organisation（南卡罗来纳州人工智能研究所; 慧与实验室; 印度人工智能研究组织）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该研究提出神经符号PRM框架，解耦推理为符号有效性与语义接地性，引入反事实符号扰动训练PRM，通过验证器优先搜索提升工具增强型LLM的科学推理可靠性。
AI 中文摘要
尽管工具增强型大型语言模型已显著提升了定量STEM任务中的多步推理能力，但仍存在一类关键的残留失败模式：中间推理步骤在语法上结构良好、数学上可执行且单位一致，但在语义上与上下文脱节。现有方法要么依赖无法评估语义意图的形式验证器，要么让过程奖励模型（PRM）承担检查算术与逻辑的双重任务。本文提出一种神经符号框架，将推理清晰解耦为两个形式维度：符号有效性（V）与语义接地性（G）。我们通过构造保证V，采用确定性符号验证器作为硬过滤器；为评估G，我们在验证器接受的流形上有条件训练PRM。为高效训练该PRM，我们引入反事实符号扰动（CSP）这一新颖的数据合成策略，该策略通过算法生成保留约束的困难负样本（即完美通过验证器但存在逻辑缺陷的步骤）。推理时，我们采用验证器优先的约束搜索，该搜索能保证验证器覆盖操作的执行一致性，同时仅依赖PRM对语义接地性进行排序。通过针对使用工具的强大型语言模型的精确残留错误类别，我们的方法显著提升了推理可靠性，且无需 prior 框架的繁杂启发式规则。
英文摘要
While tool-augmented Large Language Models have significantly improved multi-step reasoning in quantitative STEM tasks, a critical residual failure mode remains: intermediate reasoning steps that are syntactically well-formed, mathematically executable, and unit-consistent, yet contextually ungrounded. Current approaches either rely on formal verifiers that cannot assess semantic intent, or burden Process Reward Models (PRMs) with the dual task of checking both arithmetic and logic. In this paper, we propose a neuro-symbolic framework that cleanly decouples reasoning into two formal dimensions: Symbolic Validity ($V$) and Semantic Groundedness ($G$). We guarantee $V$ by construction using a deterministic symbolic verifier acting as a hard filter. To assess $G$, we train a PRM conditionally on the verifier-accepted manifold. To train this PRM efficiently, we introduce Counterfactual Symbolic Perturbation (CSP), a novel data synthesis strategy that algorithmically generates constraint-preserving hard negatives (steps that perfectly pass the verifier but are logically flawed). At inference, we deploy a verifier-first constrained search that guarantees execution consistency for verifier-covered operations while relying on the PRM solely to rank semantic grounding. By targeting the exact residual error class of strong tool-using LLMs, our method significantly improves reasoning reliability without the sprawling heuristics of prior frameworks.
