SymDiag: Explainable Diagnosis for LLM Reasoning via Neuro-Symbolic Verification
Wenyao Cui, Huaping Zhang, Yongyi Huang, Qiuchi Li, Jian Xu, Cheng-Lin Liu, Chunxiao Gao, Juan Wang, Baohua Zhang
cs.AI
2026-08-10
把 LLM 思考链编译成 Prolog 做步骤级验证,Self-Auditor 区分翻译错与推理错;忠实性检测整体 F1 达 70.7,高于对答案和奖励模型。
LLM 当推理引擎用,有个老问题:最终答案对了,中间的思考链可能根本站不住脚。这种「答案对、推理错」叫不忠实推理(unfaithful reasoning)。现有的验证手段都查不出毛病出在哪一步。对答案(答对了没)只看结果;LLM 当评委给的是主观、无法复核的点评;标量奖励模型(PRM/RM)只给一个分数,不告诉你第几步崩了。所以即便检测到问题,也没法定位、没法修。
SymDiag 把这件事重新定义成结构化的故障诊断。
SymDiag 分两阶段。
第一阶段把自然语言思考链编译成可执行的符号程序。每个推理步 Si 拆成三块:已积累的前提与推导事实 Pi、本步要做的推断 Ii、约束 Ci(领域限制、类型约束、公理),编译成 SWI-Prolog 程序。
这里有个关键设计:双分支符号生成器。形式翻译分支(A)把自然语言编译成形式化表示,归一化数值、单位、等式;批判性重述分支(B)把思考链重新表述成更严格、显式声明范围的句子,逼出隐藏假设。两支各自生成独立的 Prolog 程序。为什么要两套?一个表面上的逻辑违反,可能来自真正的推理缺陷,也可能来自自然语言转符号时的翻译噪声。单路翻译会把翻译错误判成推理错。
Self-Auditor 就是来解决这个混淆的。它做两件事:翻译一致性检查(对比两套程序的事实集与约束,标记对不上的符号目标)和逻辑批判检查(轻量的 sanity test,捕捉即时矛盾和类型错配),然后输出一个二分归因:这个锅是翻译错还是推理错。
归因清楚后做步骤级符号验证:一致性/可满足性检查这步是否引入矛盾(SAT(Pi ∧ Ci)),局部蕴含检查前一步的前提是否真的支持这一步的断言,实现成 UNSAT(前提 ∧ ¬断言)。任一不过,这步就判为不忠实。诊断输出一个三元组:错误标签、可验证证据(反例、unsat core、缺失前提指示器)、修复范围。
第二阶段把诊断转成可执行的修复反馈:孤立缺陷给局部补丁,扩散型故障(比如某个缺失前提连累多步)给全局重写。
| 验证方法 | 整体 F1 |
| 对答案(Answer Matching) | 57.7 |
| 奖励模型(Reward Model) | 57.0 |
| LLM 当评委(大模型档) | 62.8 |
| SymDiag | 70.7 |
SymDiag 在八个数据集(AIME24/25、MATH、AR-LSAT、LogiDed、GPQA、MMLU、MMLU-Pro)上整体 F1 最高,在逻辑推理和通用推理(AR-LSAT、LogiDed、MMLU)上优势最大,因为这些领域答案对但中间步无效的情况最多。这是在 240 条人工审核的精标集上测的,自动构建的全量语料有 437,792 条。
多轮修复上,SymDiag 的提升斜率最陡也最持久。对答案几乎不动(没有定位信息);奖励模型是标量信号,没法显式定位;LLM 评委早期有点用但很快饱和,因为反馈粗、不可复核。
Self-Auditor 自己的效果也站得住:审核前总错误率 46.6%,其中翻译错占 20.1%。三轮迭代后翻译错降到接近零,执行失败从 5.5% 降到 1% 以下,通过率从 53.4% 升到 81.4%。剩下的错误主要是逻辑级、不可归约的批判失败,而不是翻译噪声。
对做推理可靠性的人来说,这给了一个从「打分」升级到「定位加给证据」的框架。它输出的不是「这段推理不好」,而是「第 3 步错了,这里有个反例证明它不成立」。这种可验证证据对自动修复和多轮 self-correction 是直接可用的信号,标量奖励做不到。
适用面要清醒:它依赖把推理编译成 Prolog 可执行的符号形式,所以最契合数学、逻辑、有明确约束的领域。开放域的常识推理,符号化本身就难。
作者自己承认:符号后端用的是 Prolog,不是 Lean/Coq 这类需要专门形式库的重型证明助手,能覆盖的推理类型受 Prolog 表达力限制。240 条精标集规模偏小(尽管是从 43 万条语料里抽的)。Self-Auditor 用双编码一致性来处理自然语言的歧义,但不完美,部分可观测性问题仍在。
另有存疑:主结果 F1 是在 240 条人工审核子集上报的,作者选这个子集是为了评估可信,但小样本 F1 的波动不容忽视,全量 43 万条的自动评估没在正文给对照。推理基座是 GPTOSS-120B/20B,这两个模型的通用性需要独立确认。