LLMs 能见烟不见火：基于 Elenchos 的溯因推理评估

# LLMs Can See the Smoke but not the Fire: Evaluating Abductive Reasoning with Elenchos  
来源: https://arxiv.org/html/2607.12733  

11机构标识：Max\-Planck\-Institute for Biological Cybernetics, Magnetic Resonance Center, Tübingen, Germany  
22机构标识：Dept\. of Biomedical Magnetic Resonance, University Hospital Tübingen, Tübingen, Germany  
Lucas Mahler¹，Gabriele Lohmann¹²  
通讯作者：lohmann@tuebingen\.mpg\.de  

###### 摘要  
大型语言模型（LLMs）擅长模式识别和文本生成，但其进行溯因推理——即推断解释观察行为的潜在假设——的能力仍不明确。本文中，我们引入了 **Elenchos**（以苏格拉底式盘问法命名），这是一个生成式评估框架，将溯因推理建模为结构性逆问题。给定一个参考形式系统（例如 λ\-演算）及其可能发生变异的副本，智能体必须判断是否发生了变异，并推断导致行为差异的规则修改。对前沿和中端LLMs的评估揭示了一种一致的检测与归因分离现象：模型常常能识别系统已被篡改，但难以找出导致观察到的差异的潜在变异。在交互变异情况下，性能显著下降，模型通常只能恢复部分潜在变异。初步证据还表明，增加推理时间推理的收益递减，在更大推理预算下改进有限，不过这一发现仍需进一步验证。  

## 1 引言  
大型语言模型在前向推理方面表现出色：预测序列、推导结果或根据已知规则生成输出。然而，许多现实世界中的认知任务——从调试软件、诊断系统故障到生成科学假设——都需要逆向操作：从观察到的行为推断隐藏原因。我们将这种能力称为溯因推理。为测量这一能力，我们引入了 **Elenchos**，一个在仅允许黑盒访问的条件下，对规则修改进行溯因推理的评估框架。该任务被形式化为一个关于底层规则系统上组成的变异类别的有限假设空间的推理问题。智能体将获得一个参考内核和一个潜在变异的副本。在有限的查询预算下，它们必须利用观察到的行为差异来推断导致任何差异的潜在规则变化。这里，“智能体”指在Elenchos框架内执行推理的实体，如LLM、人类参与者或其他计算系统。与允许访问内部源代码的程序分析设置不同，Elenchos将推理局限在一个精心策划的可能变异本体上，且仅提供纯黑盒访问，从而实现对诊断难度的严格可控扩展。使用该框架对前沿和中端LLMs的评估揭示了稳定的检测与归因分离现象。虽然大多数模型能轻松检测到系统已被修改，但它们无法识别导致观察到的行为变化的潜在变异。打个比方，模型能看见烟雾，却找不到火源。当多个变异非线性地交互时，这一差距会进一步扩大。初步观察还表明，即使增加推理时间计算量，这一局限可能仍然存在，暗示溯因推理对当前推理系统构成了一个独特的挑战。  
Elenchos 的设计还旨在解决静态评估套件的一个常见局限：实例重用和隐式适应 [1 (https://arxiv.org/html/2607.12733#bib.bib67)]。由于评估实例是通过规则变异组合的方式程序化生成的，可能问题的空间在组合上是巨大的，并且可以在不改变底层评估方法的情况下扩展。这减少了对重复或记忆实例的依赖，确保评估对泛化能力而非固定测试集的暴露保持敏感，同时保持潜在规则修改的可识别性。  
我们用一个依赖类型的 λ\-演算内核 [16 (https://arxiv.org/html/2607.12733#bib.bib13),35 (https://arxiv.org/html/2607.12733#bib.bib36),13 (https://arxiv.org/html/2607.12733#bib.bib18)] 来实例化 Elenchos。该框架在抽象评估过程的层面上定义，原则上可以在多种替代计算底物上实例化，例如 SKI 组合子演算 [48 (https://arxiv.org/html/2607.12733#bib.bib3),25 (https://arxiv.org/html/2607.12733#bib.bib1)]。这可能有助于减少对具表征特定启发式的依赖，并探查性能是否能泛化到 λ\-演算结构化的输入之外。  

## 2 相关工作  
Elenchos 借鉴了四个方面的文献：(i) 静态推理基准的饱和化，(ii) 作为形式系统上智能体的 LLMs，(iii) 差分、变异和蜕变测试，以及 (iv) 故障定位和溯因推理。它围绕一个核心的结构性逆问题重新组合了这些方面：形式系统本身被视为诊断的对象，而不是一个可信的预言机。  

#### 基准饱和与推理鲁棒性  
涵盖数学 [24 (https://arxiv.org/html/2607.12733#bib.bib29),14 (https://arxiv.org/html/2607.12733#bib.bib54),21 (https://arxiv.org/html/2607.12733#bib.bib23)]、研究生级知识 [45 (https://arxiv.org/html/2607.12733#bib.bib68),10 (https://arxiv.org/html/2607.12733#bib.bib28),27 (https://arxiv.org/html/2607.12733#bib.bib72)] 以及广泛能力套件 [23 (https://arxiv.org/html/2607.12733#bib.bib35),38 (https://arxiv.org/html/2607.12733#bib.bib52),8 (https://arxiv.org/html/2607.12733#bib.bib48)] 的静态推理基准对前沿模型而言正日趋饱和 [1 (https://arxiv.org/html/2607.12733#bib.bib67),51 (https://arxiv.org/html/2607.12733#bib.bib8)]。这引发了担忧，即报告中的改进部分源于污染或记忆，而非不变的推理能力 [5 (https://arxiv.org/html/2607.12733#bib.bib11),36 (https://arxiv.org/html/2607.12733#bib.bib37),11 (https://arxiv.org/html/2607.12733#bib.bib14),15 (https://arxiv.org/html/2607.12733#bib.bib43)]。两种互补的应对措施尤其相关：动态基准生成，即用程序化定义的分布取代静态数据集以减少泄漏 [56 (https://arxiv.org/html/2607.12733#bib.bib71)]；以及鲁棒性分析，表明在保持语义不变的扰动下性能会急剧下降。例如，GSM\-Symbolic 报告在提示扰动下准确率下降高达 65% [39 (https://arxiv.org/html/2607.12733#bib.bib66)]。Elenchos 采纳了类似的动态哲学，但将扰动的焦点从输入转移到评估底物本身，从而在潜在规则修改上构建了一个结构性分布。  

#### 形式系统上的智能体与内核验证  
大量工作研究 LLMs 作为在形式系统（如证明助手）上的智能体，其目标是在固定且可信的内核下构造推导 [43 (https://arxiv.org/html/2607.12733#bib.bib78),61 (https://arxiv.org/html/2607.12733#bib.bib79),19 (https://arxiv.org/html/2607.12733#bib.bib80),57 (https://arxiv.org/html/2607.12733#bib.bib82),46 (https://arxiv.org/html/2607.12733#bib.bib84),26 (https://arxiv.org/html/2607.12733#bib.bib85),65 (https://arxiv.org/html/2607.12733#bib.bib65),64 (https://arxiv.org/html/2607.12733#bib.bib22)]。并行地，验证工作旨在确立这些内核本身的正确性，例如通过 MetaCoq [49 (https://arxiv.org/html/2607.12733#bib.bib86),50 (https://arxiv.org/html/2607.12733#bib.bib87)] 中的认证类型检查器，或用于 Lean 的 Lean4Lean [9 (https://arxiv.org/html/2607.12733#bib.bib63)]。Elenchos 则偏离了这两种范式：内核既不是一个可信的预言机，也不是一个要被正式验证的系统，而是一个可能被破坏的对象，其完整性必须仅通过行为来推断。我们的参考系统遵循双向、通过求值归一化的依赖类型理论实现谱系，例如 LambdaPi [34 (https://arxiv.org/html/2607.12733#bib.bib7)]、Altenkirch–Kaposi [2 (https://arxiv.org/html/2607.12733#bib.bib88)] 和 smalltt [30 (https://arxiv.org/html/2607.12733#bib.bib89)]。  

#### 变异测试、故障定位与溯因  
在方法论上，Elenchos 建立在差分、变异和蜕变测试传统之上 [37 (https://arxiv.org/html/2607.12733#bib.bib90),62 (https://arxiv.org/html/2607.12733#bib.bib20),31 (https://arxiv.org/html/2607.12733#bib.bib91),28 (https://arxiv.org/html/2607.12733#bib.bib31),12 (https://arxiv.org/html/2607.12733#bib.bib38)]，这些方法最近被改编用于评估软件工程环境中的 LLMs [18 (https://arxiv.org/html/2607.12733#bib.bib94),53 (https://arxiv.org/html/2607.12733#bib.bib92),55 (https://arxiv.org/html/2607.12733#bib.bib93),32 (https://arxiv.org/html/2607.12733#bib.bib96),22 (https://arxiv.org/html/2607.12733#bib.bib97),44 (https://arxiv.org/html/2607.12733#bib.bib98)]。与这些主要评估模型在外部引入故障下的鲁棒性或调试性能的方法不同，Elenchos 将变异视为要推断的潜在变量，而非观察到的扰动。在与基于变异的 LLM 评估框架（如 LLMorpheus [53 (https://arxiv.org/html/2607.12733#bib.bib92)]）的比较中，这一区别尤为明显：在那些框架中，变异的程序作为模型推理的测试用例。而在 Elenchos 中，变异作用于形式系统的求值与类型规则层面，活跃的变异配置对应一个从有限假设类中抽取的潜在真实元素。与旨在识别故障程序位置或修复目标 [41 (https://arxiv.org/html/2607.12733#bib.bib105),29 (https://arxiv.org/html/2607.12733#bib.bib99),59 (https://arxiv.org/html/2607.12733#bib.bib100),58 (https://arxiv.org/html/2607.12733#bib.bib101),60 (https://arxiv.org/html/2607.12733#bib.bib102)] 的经典故障定位方法不同，Elenchos 要求从预定义本体中识别抽象的变异类别。交互变异的出现在可观察系统中引入了组合行为，防止捷径消除策略，并将诊断转化为有限假设空间上一种结构化的溯因推理形式。与基于非正式叙事的溯因 NLP 基准 [7 (https://arxiv.org/html/2607.12733#bib.bib106),4 (https://arxiv.org/html/2607.12733#bib.bib107),47 (https://arxiv.org/html/2607.12733#bib.bib108),3 (https://arxiv.org/html/2607.12733#bib.bib109)] 相比，Elenchos 在完全可执行的环境中运行，其中每个假设都可以对底层内核进行确定性验证，从而减少对人类或基于模型判断的依赖。  

#### 信任信任与被破坏的系统  
关于被破坏计算底物的推理问题在安全和系统研究中早已被认识。Thompson 的“信任信任”攻击 [52 (https://arxiv.org/html/2607.12733#bib.bib70)]、xz/liblzma 后门事件 [20 (https://arxiv.org/html/2607.12733#bib.bib73)] 以及类似 CrowdStrike 内核驱动宕机的大规模故障 [17 (https://arxiv.org/html/2607.12733#bib.bib50)] 都说明了，可信计算基础中的故障在其根本原因被定位之前，可能早已被观察到了。虽然 Elenchos 是一个基础研究框架而非安全系统，但这些例子激励了更广泛的问题：学习型智能体是否能对底层系统完整性进行行为诊断。从这个视角出发，Elenchos 应被理解为对核心认知能力的评估：从有限交互中推断规则支配系统中的潜在结构性损坏的能力。遵循 Kerckhoffs 原则，变异本体完全公开；仅在评估期间隐藏活跃配置，确保性能反映的是诊断推理而非信息不对称。  

#### 推理评估：思维链与鲁棒性  
思维链提示 [54 (https://arxiv.org/html/2607.12733#bib.bib110)] 将中间推理步骤确立为 LLM 评估中的一等公民，随后的推理轨迹文献 [63 (https://arxiv.org/html/2607.12733#bib.bib111),33 (https://arxiv.org/html/2607.12733#bib.bib112)] 证明，在结构化推理时间搜索下，在数学和符号任务上取得了巨大提升。然而，由此产生的轨迹是否构成真正的演绎推理一直受到积极质疑：[39 (https://arxiv.org/html/2607.12733#bib.bib66)]（在扰动下）、[6 (https://arxiv.org/html/2607.12733#bib.bib113)]（记忆批评）以及 [11 (https://arxiv.org/html/2607.12733#bib.bib14),15 (https://arxiv.org/html/2607.12733#bib.bib43)]（认知解释）从不同角度论证，标题分数可能掩盖浅层的模式复用。最近关于输入扰动下推理鲁棒性的工作 [39 (https://arxiv.org/html/2607.12733#bib.bib66),40 (https://arxiv.org/html/2607.12733#bib.bib114)] 以及软件演化下的推理鲁棒性 [22 (https://arxiv.org/html/2607.12733#bib.bib97),44 (https://arxiv.org/html/2607.12733#bib.bib98)] 得出一致结论：在保留任务语义的受控变化下，模型性能是脆弱的。我们在第5节 (https://arxiv.org/html/2607.12733#S5) 的结果在一个不同的机制中呼应了这一发现：单变异偏差和检测与归因差距可以认为是依赖类型等价于 GSM\-Symbolic 的扰动下降。框架上的区别在于，Elenchos 是在完全可验证的预言机下程序化生成的，并且扰动作用于评估器而非输入——从而闭合了迄今为止在独立社区中进行的变异测试、故障定位与推理评估之间的循环。  

参见图注  
**图1：Elenchos 审计循环。**  
在每次迭代中，智能体向两个黑盒内核 \(K_A\) 和 \(K_B\)（其中可能有一个被破坏）提交一个探针。内核返回诊断元组 \(O_A\) 和 \(O_B\)，它们总结了探针的处理方式。这些元组构成了智能体的观察（详见第4节 (https://arxiv.org/html/2607.12733#S4.SS0.SSS0.Px2)）。利用积累的观察，智能体评估是否有足够的证据来识别被破坏的内核及其活跃变异集合。如果证据不足，智能体发出另一个探针；否则，它输出一个假设，指定被破坏的内核和推断出的变异。  

## 3 Elenchos 框架  
Elenchos 框架通过将系统诊断建模为一个结构性逆问题来评估智能体的溯因推理能力。它包含三个核心组成部分：(i) 定义查询空间的形式系统底物，(ii) 定义潜在变异配置空间的变异本体，以及 (iii) 一个交互式审计协议，智能体在有限的探针预算下通过该协议诊断这些配置。为了在部分可观察的条件下隔离这种能力，我们独立于任何特定形式主义对底层规则支配的系统进行抽象。虽然我们的主要评估使用第4节 (https://arxiv.org/html/2607.12733#S4.SS0.SSS0.Px1) 中详述的依赖类型 λ\-演算内核来实例化这一设置，但通用环境形式化如下：