LLMs Can See the Smoke but not the Fire: Evaluating Abductive Reasoning with Elenchos

# LLMs Can See the Smoke but not the Fire: Evaluating Abductive Reasoning with Elenchos
Source: [https://arxiv.org/html/2607.12733](https://arxiv.org/html/2607.12733)
11affiliationtext:Max\-Planck\-Institute for Biological Cybernetics, Magnetic Resonance Center, Tübingen, Germany22affiliationtext:Dept\. of Biomedical Magnetic Resonance, University Hospital Tübingen, Tübingen, GermanyLucas Mahler11footnotemark:1Gabriele LohmannCorresponding author: lohmann@tuebingen\.mpg\.de

###### Abstract

Large language models \(LLMs\) excel at pattern recognition and text generation, but their capacity for abductive inference – inferring latent hypotheses that explain observed behavior – remains poorly understood\. Here, we introduceElenchos\(named after the Socratic method of cross\-examination\), a generative evaluation framework that measures abductive reasoning as a structural inverse problem\. Given a reference formal system, such as theλ\\lambda\-calculus, and a potentially mutated counterpart, agents must determine whether a mutation has occurred and infer the rule modifications responsible for the resulting behavioral differences\.

Evaluating frontier and mid\-tier LLMs reveals a consistent detection–attribution dissociation: models often recognize that a system has been altered but struggle to identify the latent mutations causing the observed discrepancies\. Performance degrades substantially under interacting mutations, where models frequently recover only a subset of the underlying mutations\. Preliminary evidence also suggests diminishing returns from increased inference\-time reasoning, with only modest improvements under larger reasoning budgets, though this finding requires further validation\.

## 1Introduction

Large language models excel at forward reasoning: predicting sequences, deriving consequences, or generating outputs from known rules\. However, many real\-world cognitive tasks – from debugging software and diagnosing system failures to generating scientific hypotheses – require the inverse operation: inferring hidden causes from observed behavior\. We refer to this capability as abductive reasoning\.

To measure this ability, we introduce Elenchos, an evaluation framework for abductive resoning over rule modifications under black\-box access\. The task is formulated as an inference problem over a finite hypothesis class of compositional mutations applied to an underlying rule system\. Agents are presented with a reference kernel and a potentially mutated counterpart\. Under a limited query budget, they must use observed behavioral differences to infer the latent rule changes responsible for any discrepancies\. Here, an“agent”denotes the entity performing inference within the Elenchos framework, such as an LLM, a human participant, or another computational system\. Unlike program analysis settings that grant access to internal source code, Elenchos restricts reasoning to a curated ontology of possible mutations under pure black\-box access, enabling tightly controlled scaling of diagnostic difficulty\.

Our evaluations of frontier and mid\-tier LLMs using this framework reveal a consistent detection–attribution dissociation\. While most models easily detect that a system has been modified, they fail to recover the latent mutations responsible for the observed behavioral changes\. Metaphorically, models can see the smoke but struggle to find the fire\. This gap widens when multiple mutations interact nonlinearly\. Preliminary observations further suggest that this limitation may persist even with additional inference\-time compute, hinting that abductive reasoning constitutes a distinct challenge for current reasoning systems\.

Elenchos is also designed to address a common limitation of static evaluation suites: instance reuse and implicit adaptation\[[1](https://arxiv.org/html/2607.12733#bib.bib67)\]\. Because evaluation instances are generated procedurally through compositional rule mutations, the space of possible problems is combinatorially large and can be expanded without altering the underlying evaluation methodology\. This reduces reliance on repeated or memorized instances, ensuring evaluation remains sensitive to generalization rather than exposure to fixed test sets while preserving the identifiability of latent rule modifications\.

We instantiate Elenchos using a dependently typedλ\\lambda\-calculus kernel\[[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)\]\. The framework is defined at the level of an abstract evaluation procedure and, in principle, can be instantiated in a range of alternative computational substrates, e\.g\., the SKI combinator calculus\[[48](https://arxiv.org/html/2607.12733#bib.bib3),[25](https://arxiv.org/html/2607.12733#bib.bib1)\]\. This may help reduce reliance on representation\-specific heuristics and probe whether performance generalizes beyondλ\\lambda\-calculus\-structured inputs\.

## 2Related Work

Elenchos draws on four strands of literature: \(i\) the saturation of static reasoning benchmarks, \(ii\) LLMs as agents over formal systems, \(iii\) differential, mutation, and metamorphic testing, and \(iv\) fault localization and abductive inference\. It recombines these around a single structural inversion: the formal system itself is treated as the object of diagnosis rather than a trusted oracle\.

#### Benchmark saturation and reasoning robustness\.

Static reasoning benchmarks spanning mathematics\[[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)\], graduate\-level knowledge\[[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)\], and broad capability suites\[[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)\]are increasingly saturated for frontier models\[[1](https://arxiv.org/html/2607.12733#bib.bib67),[51](https://arxiv.org/html/2607.12733#bib.bib8)\]\. This has raised concerns that reported gains partly reflect contamination or memorization rather than invariant reasoning ability\[[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)\]\. Two complementary responses are particularly relevant: dynamic benchmark generation, which replaces static datasets with procedurally defined distributions to reduce leakage\[[56](https://arxiv.org/html/2607.12733#bib.bib71)\], and robustness analyses showing sharp performance degradation under semantics\-preserving perturbations\. For instance, GSM\-Symbolic reports up to a65%65\\%drop in accuracy under prompt perturbations\[[39](https://arxiv.org/html/2607.12733#bib.bib66)\]\. Elenchos adopts a similar dynamic philosophy but shifts the locus of perturbation from inputs to the evaluation substrate itself, inducing a structured distribution over latent rule modifications\.

#### Agents over formal systems and kernel verification\.

A substantial body of work studies LLMs as agents operating over formal systems such as proof assistants, where the goal is to construct derivations under a fixed and trusted kernel\[[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)\]\. In parallel, verification efforts aim to establish the correctness of such kernels themselves, e\.g\., via certified type checkers in MetaCoq\[[49](https://arxiv.org/html/2607.12733#bib.bib86),[50](https://arxiv.org/html/2607.12733#bib.bib87)\]or Lean4Lean for Lean\[[9](https://arxiv.org/html/2607.12733#bib.bib63)\]\. Elenchos departs from both paradigms: the kernel is neither a trusted oracle nor a system to be formally verified, but a potentially corrupted object whose integrity must be inferred from behavior alone\. Our reference system follows the bidirectional, normalization\-by\-evaluation lineage of dependent type theory implementations such as LambdaPi\[[34](https://arxiv.org/html/2607.12733#bib.bib7)\], Altenkirch–Kaposi\[[2](https://arxiv.org/html/2607.12733#bib.bib88)\], and smalltt\[[30](https://arxiv.org/html/2607.12733#bib.bib89)\]\.

#### Mutation testing, fault localization, and abduction\.

Methodologically, Elenchos builds on differential, mutation, and metamorphic testing traditions\[[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)\], which have recently been adapted to evaluate LLMs in software engineering settings\[[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)\]\. In contrast to these approaches, which primarily assess model robustness or debugging performance under externally introduced faults, Elenchos treats mutations as latent variables to be inferred rather than observed perturbations\.

This distinction is particularly sharp in comparison to mutation\-based LLM evaluation frameworks such as LLMorpheus\[[53](https://arxiv.org/html/2607.12733#bib.bib92)\], where mutated programs serve as test cases for model reasoning\. In Elenchos, mutations instead operate at the level of the formal system’s evaluation and typing rules, and the active mutation configuration corresponds to a latent ground\-truth element drawn from a finite hypothesis class\.

Unlike classical fault localization methods, which aim to identify faulty program locations or repair targets\[[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 requires identification of abstract mutation classes from a predefined ontology\. The presence of interacting mutations induces combinatorial behavior in the observable system, preventing shortcut elimination strategies and turning diagnosis into a structured form of abductive inference over a finite hypothesis space\. In contrast to abductive NLP benchmarks grounded in informal narratives\[[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 operates in a fully executable environment, where each hypothesis can be deterministically validated against the underlying kernel, reducing reliance on human or model\-based judgment\.

#### Trusting trust and corrupted systems\.

The problem of reasoning about corrupted computation substrates has long been recognized in security and systems research\. Thompson’s "trusting trust" attack\[[52](https://arxiv.org/html/2607.12733#bib.bib70)\], the xz/liblzma backdoor incident\[[20](https://arxiv.org/html/2607.12733#bib.bib73)\], and large\-scale failures such as the CrowdStrike kernel\-driver outage\[[17](https://arxiv.org/html/2607.12733#bib.bib50)\]illustrate how failures in trusted computing bases may be observable long before their root causes are localized\. While Elenchos is a basic research framework rather than a security system, these examples motivate the broader question of whether learned agents can perform behavioral diagnosis of underlying system integrity\.

From this perspective, Elenchos should be understood as an evaluation of a core cognitive capability: the ability to infer latent structural corruption in rule\-governed systems from finite interaction\. Following Kerckhoffs’s principle, the mutation ontology is fully public; only the active configuration is hidden during evaluation, ensuring that performance reflects diagnostic inference rather than information asymmetry\.

#### Reasoning evaluation: chain\-of\-thought and robustness\.

Chain\-of\-thought prompting\[[54](https://arxiv.org/html/2607.12733#bib.bib110)\]established intermediate reasoning steps as a first\-class object in LLM evaluation, and the subsequent reasoning\-trace literature\[[63](https://arxiv.org/html/2607.12733#bib.bib111),[33](https://arxiv.org/html/2607.12733#bib.bib112)\]demonstrated large gains on math and symbolic tasks under structured inference\-time search\. Whether the resulting traces constitute genuine deduction has been actively contested:\[[39](https://arxiv.org/html/2607.12733#bib.bib66)\]\(under perturbation\),\[[6](https://arxiv.org/html/2607.12733#bib.bib113)\]\(memorization critique\), and\[[11](https://arxiv.org/html/2607.12733#bib.bib14),[15](https://arxiv.org/html/2607.12733#bib.bib43)\]\(cognitive interpretation\) argue, in different registers, that headline scores can mask shallow pattern reuse\. Recent work on reasoning robustness under input perturbation\[[39](https://arxiv.org/html/2607.12733#bib.bib66),[40](https://arxiv.org/html/2607.12733#bib.bib114)\]and under software evolution\[[22](https://arxiv.org/html/2607.12733#bib.bib97),[44](https://arxiv.org/html/2607.12733#bib.bib98)\]reaches a consistent conclusion: model performance is fragile under controlled changes that preserve task semantics\. Our results in Section[5](https://arxiv.org/html/2607.12733#S5)echo this finding in a different regime: the single\-mutation bias and the detection–attribution gap are arguably the dependently\-typed analogue of GSM\-Symbolic’s perturbation drop\. The framing distinction is that Elenchos is procedurally generated under a fully verifiable oracle, and the perturbation is to the evaluator rather than the input – closing the loop between mutation testing, fault localization, and reasoning evaluation that has so far been pursued in separate communities\.

![Refer to caption](https://arxiv.org/html/2607.12733v1/x1.png)Figure 1:The Elenchos audit loop\.At each iteration, the agent submits a probe to two black\-box kernels,KAK\_\{A\}andKBK\_\{B\}, one of which may be corrupted\. The kernels return diagnostic tuples,OAO\_\{A\}andOBO\_\{B\}, that summarize how the probe was processed\. These tuples constitute the agent’s observations \(see Section[4](https://arxiv.org/html/2607.12733#S4.SS0.SSS0.Px2)for details\)\. Using the accumulated observations, the agent assesses whether there is sufficient evidence to identify the corrupted kernel and its active mutation set\. If the evidence is insufficient, the agent issues another probe; otherwise, it outputs a hypothesis specifying the corrupted kernel and the inferred mutations\.

## 3The Elenchos Framework

The Elenchos framework evaluates an agent’s capacity for abductive reasoning by framing system diagnosis as a structural inverse problem\. It consists of three core components: \(i\) a formal system substrate defining the query space, \(ii\) a mutation ontology defining the space of latent mutation configurations, and \(iii\) an interactive auditing protocol through which an agent diagnoses those configurations under a limited probe budget\.

To isolate this capacity under partial observability, we abstract the underlying rule\-governed system independently of any particular formalism\. While our primary evaluation instantiates this setup using the dependently typedλ\\lambda\-calculus kernel detailed in Section[4](https://arxiv.org/html/2607.12733#S4.SS0.SSS0.Px1), the general environment is formalized as follows:

###### Definition 1\(Kernel\)\.

A*kernel*KKis a deterministic black\-box function

K:𝒯→𝒪,K:\\mathcal\{T\}\\to\\mathcal\{O\},where𝒯\\mathcal\{T\}denotes the space of probes containing all admissible syntactic terms, and𝒪\\mathcal\{O\}represents the space of observable outputs\. Let𝒦\\mathcal\{K\}denote the set of all such kernels, including the reference kernelKrefK\_\{\\textnormal\{ref\}\}and its mutated variants\.

We assume that each kernel is induced by an underlying latent rule system that is not directly observable\. Mutations operate on this latent representation and induce systematic changes in the observable behavior of the resulting kernel\. Agents, however, have access only to black\-box interactions with this induced behavior, and must infer the latent structure solely through observed input–output discrepancies\.

###### Definition 2\(Mutation Ontology and Configurations\)\.

A*mutation operator*μ\\muis a transformation over kernels,μ:𝒦→𝒦\\mu:\\mathcal\{K\}\\to\\mathcal\{K\}, that modifies the underlying latent rule structure of a kernel\. The mutation ontology is defined as the finite set of these primary operators:

ℳ=\{μ1,…,μn\}\.\\mathcal\{M\}=\\\{\\mu\_\{1\},\\ldots,\\mu\_\{n\}\\\}\.For any mutation configuration setS⊆ℳS\\subseteq\\mathcal\{M\}, we defineKS∈𝒦K\_\{S\}\\in\\mathcal\{K\}as the kernel obtained by applying the mutations inSSto the reference kernelKrefK\_\{\\textnormal\{ref\}\}under a fixed composition policy\.

#### Composite mutations\.

Mutations may interact non\-linearly, meaning the behavior of a composite configurationKSK\_\{S\}cannot generally be predicted from the isolated effects of its constituent mutations\. To ensure that mutation attribution is well\-defined under black\-box access, we restrict the evaluation space to a valid configuration familyℱ⊆𝒫​\(ℳ\)\\mathcal\{F\}\\subseteq\\mathcal\{P\}\(\\mathcal\{M\}\)satisfying a globalidentifiabilitycondition: forS∈ℱS\\in\\mathcal\{F\}, the mapping

is injective overℱ\\mathcal\{F\}, ensuring that each induced kernel uniquely determines its underlying mutation configuration in principle\.

Elements of𝒫​\(ℳ\)\\mathcal\{P\}\(\\mathcal\{M\}\)violating this identifiability condition are excluded fromℱ\\mathcal\{F\}\. Letk=\|S\|k=\|S\|denote the number of active mutations\. Fork≥2k\\geq 2, excluded cases include: \(i\)*logical collapse*, where the induced kernel produces uniform outputs across the probe space, and \(ii\)*symptomatic subsumption*, where a configuration induces the same kernel as one of its proper subsets\. By construction, the configuration family satisfies

∅∈ℱand\{μ\}∈ℱ,∀μ∈ℳ\.\\emptyset\\in\\mathcal\{F\}\\quad\\text\{and\}\\quad\\\{\\mu\\\}\\in\\mathcal\{F\},\\quad\\forall\\mu\\in\\mathcal\{M\}\.

#### The audit loop\.

During a session, Elenchos evaluates abductive reasoning as an interactive diagnosis problem \([Figure 1](https://arxiv.org/html/2607.12733#S2.F1)\)\. Each instance consists of two kernels\(KA,KB\)\(K\_\{A\},K\_\{B\}\)implementing the same formal system, with the guarantee that at least one is sound\. The agent is not informed which kernel, if either, is corrupted; instead, it interacts with both through a restricted query interface, submitting probesτ∈𝒯\\tau\\in\\mathcal\{T\}and observing outputs\(OA,OB\)\(O\_\{A\},O\_\{B\}\)\. From these observations, the agent must determine whether a mutation exists, identify the corrupted kernel, if applicable, and attribute active mutations from the predefined ontology\. The interaction terminates when the agent submits its final hypothesis, either on its own or after the probe budgetPmaxP\_\{\\text\{max\}\}is exhausted\.

#### Evaluation metrics\.

Kernel identificationVKV\_\{K\}is correct if the predicted and true kernel labels match\.Mutation attributionVAV\_\{A\}is correct if the predicted and true mutation sets are identical, i\.e\., ifallmutations have been correctly identified\. After each session, a scoreV∈\{0,1\}V\\in\\\{0,1\\\}is returned withV=1V=1if both kernel identification and mutation attribution are correct, andV=0V=0otherwise\. Because exact\-match attribution conflates missing mutations and spurious predictions, we additionally report conditional accuracy, Jaccard index, precision, and recall\.

#### Inference efficiency score\.

We propose an additional metricEELX∈\[0,1\.5\]E\_\{\\mathrm\{ELX\}\}\\in\[0,1\.5\]that rewards efficiency with a bonus multiplier\. It is defined as

EELX​\(V,P\)=V​\(1\+12​\(1−\(PPmax\)3\)\)\.E\_\{\\mathrm\{ELX\}\}\(V,P\)=V\\left\(1\+\\frac\{1\}\{2\}\\left\(1\-\\left\(\\frac\{P\}\{P\_\{\\max\}\}\\right\)^\{3\}\\right\)\\right\)\.\(1\)
The score assigns zero to incorrect submissions and rewards correct solutions with a bonus that depends on the number of probes used\. The cubic form was chosen to provide only a mild penalty for exploratory probing while rewarding solutions obtained below the probe budgetPmaxP\_\{\\text\{max\}\}\.

#### The task is abductive, not deductive\.

The task is not primarily deductive, since success does not consist of proving statements within a fixed logical system, and it is not a standard supervised induction task, since no labeled training examples are provided within the evaluation\. Rather, we operationalize abductive inference as the problem of recovering a latent mutation configurationS∈ℱS\\in\\mathcal\{F\}that best explains observed behavioral discrepancies between paired kernels under black\-box access\. This corresponds to selecting a hypothesis from a finite configuration space based on partial observational evidence\. This notion of abduction is consistent with its classical formulation in the sense of Peirce\[[42](https://arxiv.org/html/2607.12733#bib.bib76)\], where hypotheses are generated to explain observed phenomena rather than derived from axioms or learned from labeled instances\.

## 4Implementation

#### Dependently typedλ\\lambda\-calculus\.

Here we briefly review the core features of the dependently typedλ\\lambda\-calculus used in Elenchos, see also Supplementary Material[A](https://arxiv.org/html/2607.12733#A1)\. The set of terms𝒯\\mathcal\{T\}\(which encompasses both expressions and types\) is defined by the grammar:

𝒯::=x∣Type∣λx:A\.M∣MN∣Πx:A\.B,\\mathcal\{T\}::=x\\mid\\texttt\{Type\}\\mid\\lambda x:A\.M\\mid M\\,N\\mid\\Pi x:A\.B,\(2\)
wherexxdenotes a variable,Typerepresents the universe of types,λx:A\.M\\lambda x:A\.Mis a function abstraction with domain typeAA,M​NM\\,Nis a function application, andΠx:A\.B\\Pi x:A\.Bis a dependent function type where the result typeBBmay depend on the argumentxx\.

Computation proceeds viaβ\\beta\-reduction,

\(λx:A\.M\)N⟶βM\[x↦N\],\(\\lambda x:A\.M\)\\,N\\longrightarrow\_\{\\beta\}M\[x\\mapsto N\],\(3\)
withM​\[x↦N\]M\[x\\mapsto N\]denoting the capture\-avoiding substitution ofNNforxxinMM\. A term is in*β\\beta\-normal form*when no further reductions are possible\. Operationally, aλ\\lambda\-calculus kernel acts as a deterministic type checker, validating terms against a typing contextΓ\\Gammathat tracks variable assignments\.

#### Kernel architecture\.

We instantiate Elenchos usingLambdaPy, a Python\-based implementation of a dependently typedλ\\lambda\-calculus kernel adapted from\[[34](https://arxiv.org/html/2607.12733#bib.bib7)\]\. The kernel supports parsing, elaboration, bidirectional type checking, and evaluation, providing a deterministic formal substrate for mutation\-based diagnosis\. Kernels are equipped with a persistent state that includes the typing context and the evaluated definitions\. Details of the surface language are provided in Supplementary Material[A](https://arxiv.org/html/2607.12733#A1)\.

Each kernel execution returns a structured diagnostic tuple: \(i\) a success indicator specifying whether execution succeeds, \(ii\) the normalized output value for successful executions \(e\.g\., after applicableβ\\beta\-reductions and other definitional reductions supported by the kernel\), and \(iii\) diagnostic information for failed executions giving the type of error and an error message produced byLambdaPy\. These outputs implement the observation interface exposed to agents during the audit loop\. Three examples of Elenchos’ cross\-examination procedures are provided in the Supplementary MaterialLABEL:app:traces\.

#### Mutation framework\.

We use a curated ontology of1313singleton mutations \(see Supplementary Material[B](https://arxiv.org/html/2607.12733#A2), especially[Table 3](https://arxiv.org/html/2607.12733#A2.T3)\)\. We build the corresponding valid configuration familyℱk\\mathcal\{F\}\_\{k\}fork≤3k\\leq 3according to Supplementary Material[B\.3](https://arxiv.org/html/2607.12733#A2.SS3)and identifiedadditive\(\+\)\(\+\)andinteracting\(⊗\)\(\\otimes\), see Supplementary[Figure 6](https://arxiv.org/html/2607.12733#A2.F6)\.

We evaluate agents on 13 singleton, 12 pairwise, and 3 triplet configurations\. Among the pairwise configurations, 3 exhibit non\-additive interactions, while the triplet configurations are purely additive, see Supplementary[Table 6](https://arxiv.org/html/2607.12733#A2.T6)\.

Rather than modifying kernel source code, mutations are implemented as configuration\-level overrides\. Each mutation corresponds to a dedicated flag within a runtime configuration object, with the default configuration representing the unmutated baseline\. This design enables the dynamic composition of multiple mutations while maintaining isolation across evaluation instances\. By decoupling mutation generation from the core kernel implementation, Elenchos supports scalable benchmark generation with controlled ground truth and reproducible mutation configurations\.

#### Tool use\.

LLMs are permitted task\-specific tool use, such as submitting probes, asking for remaining probe budget, listing currentLambdaPycontext, and submitting an answer\. But to prevent benchmark contamination and search\-based solutions, web search and code execution are disallowed\. Code execution could confound abductive reasoning with tool\-use proficiency, automated hypothesis testing, exhaustive search, and external computational scaffolding\. The resulting evaluations should therefore be interpreted as measuring unaided abductive attribution from observed behavior, rather than the upper bounds achievable by tool\-augmented systems\.

#### The system prompt\.

We evaluate four conditions that vary the level of procedural guidance provided in the system prompt\. These conditions are ordered by increasing difficulty \(Levels 0 through 3\) as the amount of auxiliary information is gradually reduced\. All levels expose the full mutation taxonomy \(Supplementary[Table 3](https://arxiv.org/html/2607.12733#A2.T3)\) and differ solely in the operational hints provided\. While Levels 0, 1, and 2 offer workflow guidance to the model, Level 3 completely omits this information\. The prompts are included in the Supplementary MaterialLABEL:app:prompts\.

- •Level 0\.The system prompt includes a curated set of canonical example probes for each of the 13 mutations\.111The list of constructed probesΠRSA\\Pi\_\{\\texttt\{RSA\}\}and expected output ofKrefK\_\{\\text\{ref\}\}andKSK\_\{S\}can be provided on request\.Each probe is explicitly designed to elicit a distinct behavioral signature that isolates its corresponding mutation from all others\. While the agent receives a complete diagnostic reference suite, it must still infer which specific subset of mutations is active in the current instance\. Additionally, the prompt specifies the exact cardinalitykkof the active mutation set\.
- •Level 1\.The system prompt provides the exact cardinalitykkof the active mutation set, but omits the canonical example probes\.
- •Level 2\.The system prompt informs the agent that there arek≤2k\\leq 2active mutations, but does not provide the exact value ofkk\.
- •Level 3\.The system prompt only informs the agent that there are at most three active mutations \(k∈\{0,1,2,3\}k\\in\\\{0,1,2,3\\\}\), and does not provide workflow guidance or hints anymore\.

![Refer to caption](https://arxiv.org/html/2607.12733v1/x2.png)Figure 2:Performance across experimental configurations \(“Ladder”experiment\)\.Accuracy increases with model capability but decreases with reduced system prompt information \(Levels\), increased mutation complexity\(k\)\(k\), and non\-additive mutation interactions\(\+→⊗\)\(\+\\rightarrow\\otimes\)\. The reported metric is the averaged exact\-match accuracy\(V\)\(V\)across mutation sets, which requires correct identification of whether either kernel is corrupted and, when applicable, the precise attribution of all active mutations\.Table 1:Detection–attribution dissociation on the“Ladder”experiment, averaged overk∈\{1,2\}k\\in\\\{1,2\\\}and the three prompt levels \(Levels 0–2\), with models grouped by family\.VKV\_\{K\}denotes kernel\-correct detection;VAV\_\{A\}denotes exact mutation\-set attribution; andVA∣VK=1V\_\{A\}\\mid V\_\{K\}=1denotes exact attribution conditioned on correct kernel detection\. Cells display mean point estimates with asymmetric Wilson95%95\\,\\%confidence intervals in brackets; the Gap column reportsVK−VAV\_\{K\}\-V\_\{A\}with paired bootstrap95%95\\,\\%confidence intervals\.ModelVKV\_\{K\}VAV\_\{A\}VA∣VK=1V\_\{A\}\\mid V\_\{K\}=1Gap \(pp\)ministral\-3b\-25120\.330\.33\[0\.29,0\.38\]\[0\.29,0\.38\]0\.110\.11\[0\.08,0\.14\]\[0\.08,0\.14\]0\.130\.13\[0\.08,0\.20\]\[0\.08,0\.20\]0\.230\.23\[0\.17,0\.28\]\[0\.17,0\.28\]ministral\-8b\-25120\.220\.22\[0\.18,0\.26\]\[0\.18,0\.26\]0\.130\.13\[0\.10,0\.17\]\[0\.10,0\.17\]0\.270\.27\[0\.18,0\.38\]\[0\.18,0\.38\]0\.080\.08\[0\.03,0\.13\]\[0\.03,0\.13\]ministral\-14b\-25120\.310\.31\[0\.26,0\.36\]\[0\.26,0\.36\]0\.050\.05\[0\.03,0\.08\]\[0\.03,0\.08\]0\.140\.14\[0\.09,0\.22\]\[0\.09,0\.22\]0\.260\.26\[0\.21,0\.30\]\[0\.21,0\.30\]mistral\-large\-25120\.650\.65\[0\.59,0\.69\]\[0\.59,0\.69\]0\.310\.31\[0\.27,0\.36\]\[0\.27,0\.36\]0\.380\.38\[0\.32,0\.44\]\[0\.32,0\.44\]0\.330\.33\[0\.27,0\.40\]\[0\.27,0\.40\]claude\-haiku\-4\-50\.780\.78\[0\.74,0\.82\]\[0\.74,0\.82\]0\.340\.34\[0\.29,0\.39\]\[0\.29,0\.39\]0\.390\.39\[0\.34,0\.45\]\[0\.34,0\.45\]0\.440\.44\[0\.38,0\.50\]\[0\.38,0\.50\]gemini\-2\.5\-flash0\.890\.89\[0\.85,0\.92\]\[0\.85,0\.92\]0\.360\.36\[0\.31,0\.41\]\[0\.31,0\.41\]0\.400\.40\[0\.35,0\.46\]\[0\.35,0\.46\]0\.530\.53\[0\.47,0\.58\]\[0\.47,0\.58\]gemini\-2\.5\-pro0\.930\.93\[0\.90,0\.95\]\[0\.90,0\.95\]0\.350\.35\[0\.31,0\.41\]\[0\.31,0\.41\]0\.380\.38\[0\.33,0\.43\]\[0\.33,0\.43\]0\.570\.57\[0\.52,0\.63\]\[0\.52,0\.63\]gpt\-5\.4\-nano0\.160\.16\[0\.13,0\.20\]\[0\.13,0\.20\]0\.080\.08\[0\.05,0\.11\]\[0\.05,0\.11\]0\.290\.29\[0\.18,0\.41\]\[0\.18,0\.41\]0\.090\.09\[0\.05,0\.12\]\[0\.05,0\.12\]gpt\-5\.4\-mini0\.580\.58\[0\.53,0\.63\]\[0\.53,0\.63\]0\.230\.23\[0\.19,0\.28\]\[0\.19,0\.28\]0\.270\.27\[0\.21,0\.34\]\[0\.21,0\.34\]0\.350\.35\[0\.28,0\.41\]\[0\.28,0\.41\]gpt\-5\.40\.860\.86\[0\.82,0\.90\]\[0\.82,0\.90\]0\.370\.37\[0\.32,0\.42\]\[0\.32,0\.42\]0\.420\.42\[0\.37,0\.48\]\[0\.37,0\.48\]0\.500\.50\[0\.45,0\.55\]\[0\.45,0\.55\]gpt\-5\.4\_low0\.940\.94\[0\.91,0\.96\]\[0\.91,0\.96\]0\.410\.41\[0\.36,0\.47\]\[0\.36,0\.47\]0\.440\.44\[0\.39,0\.50\]\[0\.39,0\.50\]0\.520\.52\[0\.47,0\.57\]\[0\.47,0\.57\]gpt\-5\.4\_medium0\.920\.92\[0\.89,0\.94\]\[0\.89,0\.94\]0\.470\.47\[0\.42,0\.52\]\[0\.42,0\.52\]0\.510\.51\[0\.46,0\.57\]\[0\.46,0\.57\]0\.450\.45\[0\.40,0\.50\]\[0\.40,0\.50\]gpt\-5\.4\_high0\.890\.89\[0\.85,0\.92\]\[0\.85,0\.92\]0\.460\.46\[0\.41,0\.51\]\[0\.41,0\.51\]0\.510\.51\[0\.46,0\.57\]\[0\.46,0\.57\]0\.430\.43\[0\.38,0\.48\]\[0\.38,0\.48\]Overall0\.650\.65\[0\.64,0\.66\]\[0\.64,0\.66\]0\.280\.28\[0\.27,0\.30\]\[0\.27,0\.30\]0\.390\.39\[0\.37,0\.41\]\[0\.37,0\.41\]0\.370\.37\[0\.35,0\.38\]\[0\.35,0\.38\]![Refer to caption](https://arxiv.org/html/2607.12733v1/x3.png)Figure 3:Summary of the“Ladder”results averaged across all evaluated LLMs\.Performance degrades consistently with reductions in system prompt information \(Level\), higher mutation counts\(k\)\(k\), and the presence of interacting mutations\(\+→⊗\)\(\+\\rightarrow\\otimes\)\. At the most challenging configuration \(minimum prompt information combined with interacting mutations\), the average accuracy drops toV=0\.02V=0\.02\.

## 5Experiments and Results

We evaluate Elenchos across two distinct experimental designs:

- •Difficulty Ladder:A deep\-dive evaluation using a select group of LLMs to analyze how varying levels of system prompt scaffolding together with the number of active mutationskkaffect model performance\.
- •Wide\-Panel Benchmark:A broader leaderboard evaluation that tests a diverse array of frontier and mid\-tier LLMs against a fixed baseline difficulty \(system prompt Level 3, and number of active mutationsk≤3k\\leq 3\) to establish a comparative performance baseline\.

### 5\.1Difficulty Ladder

The“Ladder”experiment evaluates 13 LLMs across two mutation counts \(k∈\{1,2\}k\\in\\\{1,2\\\}\) and three prompt levels \(Levels 0, 1, and 2\)\. We set the maximum probe budget toPmax=50P\_\{\\max\}=50\. We use 13 singleton mutations and 10 pair\-wise mutations, three of which exhibit non\-additive interaction effects \(k=2⊗k=2^\{\\otimes\}\) \(see Supplementary[Table 6](https://arxiv.org/html/2607.12733#A2.T6)\)\. Each prompt\-level and mutation configuration combination is evaluated over 5 independent repetitions\. The results are shown in[Table 1](https://arxiv.org/html/2607.12733#S4.T1),[Figure 2](https://arxiv.org/html/2607.12733#S4.F2), and[Figure 3](https://arxiv.org/html/2607.12733#S4.F3)\. A detailed per\-model perspective on the effect of the mutation set complexity and the effect of different hint levels in the system prompt is provided in the Supplementary[Table 7](https://arxiv.org/html/2607.12733#A3.T7)and[8](https://arxiv.org/html/2607.12733#A3.T8)\.

#### Performance gradient\.

As difficulty increases, accuracies decrease, driven by reduced system prompt information and increasing mutation complexity \(overall see[Figure 3](https://arxiv.org/html/2607.12733#S4.F3)per\-model see[Figure 2](https://arxiv.org/html/2607.12733#S4.F2)\)\. This gradient suggests that the difficulty scales as intended: tasks remain achievable under favorable conditions, while progressively challenging frontier models\. In the most challenging configuration \(minimal prompt information with interacting mutations\), average accuracy drops toV=0\.02V=0\.02\.

#### The detection–attribution gap\.

Averaged across all 13 LLMs and overk∈\{1,2\}k\\in\\\{1,2\\\}and prompt levels, models achieve a kernel detection accuracy ofVK=0\.65V\_\{K\}=0\.65, but an exact mutation attribution accuracy of onlyVA=0\.28V\_\{A\}=0\.28, revealing a substantial detection–attribution gap \([Table 1](https://arxiv.org/html/2607.12733#S4.T1)visualized in SupplementaryLABEL:fig:ladder\_heatmap\_detail\)\. This discrepancy persists across all evaluated models; the largest gaps appear among the highest\-performing models \(e\.g\.,gemini\-2\.5\-pro\), while lower\-performing models also retain substantial separation \(e\.g\.,ministral\-3b\-2512\)\.

#### System prompt effects\.

Providing more structural information through Level\-0 system prompts yields substantial performance gains over Level\-1 and Level\-2 prompts\. Weaker models fail almost completely without strong prompt scaffolding \([Figure 2](https://arxiv.org/html/2607.12733#S4.F2)\)\.

Fork=2k=2and conditioned on correct kernel detection \(VK=1V\_\{K\}=1\), providing mutation\-count information shifts attribution failures: models are more likely to hallucinate mutations whenkkis known and more likely to omit mutations when it is not \(Supplementary[Table 9](https://arxiv.org/html/2607.12733#A3.T9)\)\. In other words, whenkkis known, the model seems to feel compelled to fill all slots, leading to hallucinated mutation identities\. Whenkkis not known, the model leaves mutations unreported\.

#### Effects of interacting mutations\.

Performance decreases substantially when mutations exhibit non\-additive interactions \([Figure 2](https://arxiv.org/html/2607.12733#S4.F2)and across prompt levels in Supplementary[Table 7](https://arxiv.org/html/2607.12733#A3.T7)\)\. Atk=2k=2with Level\-2 prompts, most models fail completely, with only two exceptions:gpt\-5\.4\_mediumwithV=0\.20V=0\.20andgpt\-5\.4withV=0\.07V=0\.07\. Notably, the highest reasoning\-budget setting achieves zero accuracy in this case\. The results using a Level\-1 prompt show a similar pattern: performance drops sharply from“additive”to“interacting”mutations with only two exceptions \(gpt\-5\.4\-miniandgemini\-2\.5\-pro\)\.

#### Per\-mutation difficulty\.

Attribution difficulty is highly heterogeneous across the mutation ontology: some mutation classes are recovered by nearly all models, whereas others remain near the performance floor \(Supplementary[Figure 5](https://arxiv.org/html/2607.12733#A2.F5)\)\.

#### Probe budget limitations\.

In86\.5%86\.5\\,\\%of cases where models correctly detected the corrupt kernel but failed exact attribution \(VK=1,VA=0V\_\{K\}=1,V\_\{A\}=0\), the allocated probe budget remained unused\. This suggests that many failures occur before the probe budget becomes a limiting factor, consistent with premature commitment to incorrect hypotheses rather than insufficient interaction opportunities \(Supplementary[Table 9](https://arxiv.org/html/2607.12733#A3.T9)\)\.

#### Baselines comparison\.

A random mutation\-selection baseline over the 13\-mutation ontology achieves accuracies of1/13≈0\.0771/13\\approx 0\.077fork=1k=1and1/64≈0\.0161/64\\approx 0\.016fork=2k=2, so most models substantially exceed chance performance\. Randomly selecting the corrupted kernel among\{A,B,neither\}\\\{A,B,\\mathrm\{neither\}\\\}yields a1/31/3baseline accuracy\. A naive exhaustive\-search baseline is computationally infeasible due to the combinatorial size of the probe space𝒯\\mathcal\{T\}\.

### 5\.2Wide\-Panel Benchmark

![Refer to caption](https://arxiv.org/html/2607.12733v1/x4.png)Figure 4:Performance leaderboard across models and mutation orders in“Benchmark”\.For this comparison, only additivek\+k^\{\+\}composite mutations have been used\.k≥2⊗k\\geq 2^\{\\otimes\}interacting mutations have been excluded since the performance on these sets has been close to0across all models \(see SupplementaryLABEL:tab:full\_benckmark\)\. TheSimple Reflex Agentdenotes a handcrafted agent that does not generate probes of its own, but simply uses the example probes specified with the Level\-0 system prompt \(see Section[B\.2](https://arxiv.org/html/2607.12733#A2.SS2)\)\. Hence, it reaches an accuracy ofV=1V=1\.The wide\-panel“Benchmark”evaluates 30 LLMs under a fixed baseline configuration \(Level\-3 system prompt\) across mutation set cardinalityk∈\{0,1,2,3\}k\\in\\\{0,1,2,3\\\}\. We use 6 singleton, 3 pair\-wise additive, and 3 triplet additive mutation sets \(see Supplementary[Table 6](https://arxiv.org/html/2607.12733#A2.T6)\)\. Importantly, this subset excludes interacting mutations for now, focusing strictly on purely additive configurations\. This restriction was introduced because performance degraded too severely under interacting mutations to yield an informative evaluation, see Section[5\.1](https://arxiv.org/html/2607.12733#S5.SS1)\. However, we separately tested one interacting mutation set \(k=2⊗k=2^\{\\otimes\}\)\. For each\(LLM,S\)\(\\text\{LLM\},S\)pair, we evaluate 5 independent sessions with a maximum probe budget ofPmax=65P\_\{\\max\}=65\.[Figure 4](https://arxiv.org/html/2607.12733#S5.F4)shows the resulting performance leaderboard, and[Table 2](https://arxiv.org/html/2607.12733#S5.T2)shows the results averaged across all LLMs included in the leaderboard\. SupplementaryLABEL:tab:full\_benckmarkandLABEL:fig:leaderboard\_detailedprovides a detailed evaluation\. Findings regarding the probe budget limitations are supported by SupplementaryLABEL:fig:probing\_behavior\.

#### The Simple Reflex Agent\.

TheSimple Reflex Agent \(RSA\)is a deterministic baseline that does not generate custom probes, but instead relies exclusively on the static example probesΠRSA\\Pi\_\{\\texttt\{RSA\}\}provided in the Level\-0 system prompt\. By construction, these probes, together with the expected output of reference and corrupted kernels\(Oref,OS\)\(O\_\{\\text\{ref\}\},O\_\{S\}\), serve as an analytical oracle that yields perfect identification and attribution accuracy atk=1k=1and additive sets\. Crucially, none of the evaluated LLMs was capable of generating structurally similar probes autonomously to achieveV=1V=1in the“Benchmark”\. Furthermore, even when explicitly provided with these diagnostic probes via the system prompt – as evaluated in the“Ladder”experiment – the models failed to utilize them, underperforming significantly despite having access to an optimal query set\. For more details of constructing the oracle probes andRSA, see Supplementary Material[B\.2](https://arxiv.org/html/2607.12733#A2.SS2)\.

#### Identifying the null case\.

Atk=0k=0, the correct kernel classification isneither, indicating that both kernels are sound\. Across all 30 models andRSAand 155 experimental sessions, models achieved a null\-case specificity of0\.900\.90\. This performance provides evidence against trivial shortcut strategies, such as uniformly predicting that a system has been corrupted\. The number of probes expended varies across models: some models submitneithervery early, whereas others do so only after exhausting the available budget\. The former may indicate over\-confidence, while the latter may reflect difficulty distinguishing the null case from hard\-to\-detect mutation configurations \(Supplementary[Table 10](https://arxiv.org/html/2607.12733#A3.T10)\)\.

#### Scalability and the multi\-mutation collapse\.

Average exact accuracyVVdeclines sharply as the number of mutations increases, dropping from0\.90→0\.32→0\.15→0\.15$0\.90$\\to$0\.32$\\to$0\.15$\\to$0\.15$fork=0,1,2\+,3\+k=0,1,2^\{\+\},3^\{\+\}, respectively\. For the interacting set, the average accuracy is0\.030\.03, see[Table 2](https://arxiv.org/html/2607.12733#S5.T2)\. There are two severe performance collapses occurring betweenk=1k=1andk≥2k\\geq 2and between additive and interacting combinations, which aligns with the single\-mutation bias identified in the“Ladder”experiment\. While basic change detection remains relatively stable beyondk=1k=1, causal attribution remains the primary failure mode\.

This trend is further substantiated by the Jaccard similarity scores, which reach their lowest point atk=2⊗k=2^\{\\otimes\}\(VAJ=0\.27V\_\{A\}^\{J\}=$0\.27$\)\. This performance valley confirms that the primary driver of degradation is a localized failure in identifying specific, interacting mutations rather than an inability to detect overall system discrepancies \([Table 2](https://arxiv.org/html/2607.12733#S5.T2)\)\.

Table 2:Marginal accuracy by mutation countkkon the wide\-panel“Benchmark”\.Exact correctnessVV, kernel detectionVKV\_\{K\}, exact attributionVAV\_\{A\}, Jaccard partial creditVAJV\_\{A\}^\{J\}, and conditional attribution correctnessVA∣VK=1V\_\{A\}\\mid V\_\{K\}=1\. Fork≥2k\\geq 2, superscripts indicate whether the mutations are additive\(\+\)\(\+\)or interacting\(⊗\)\(\\otimes\)\. Values are averaged numbers across models, system prompt levels, and mutation sets with bootstrap95%95\\,\\%confidence intervals in brackets\.kknnVVVKV\_\{K\}VAV\_\{A\}VAJV\_\{A\}^\{J\}VA∣VK=1V\_\{A\}\\mid V\_\{K\}=101551550\.900\.90\[0\.85,0\.94\]\[0\.85,0\.94\]0\.900\.90\[0\.85,0\.94\]\[0\.85,0\.94\]0\.970\.97\[0\.94,0\.99\]\[0\.94,0\.99\]0\.970\.97\[0\.94,0\.99\]\[0\.94,0\.99\]1\.001\.00\[1\.00,1\.00\]\[1\.00,1\.00\]119309300\.320\.32\[0\.29,0\.35\]\[0\.29,0\.35\]0\.770\.77\[0\.75,0\.80\]\[0\.75,0\.80\]0\.330\.33\[0\.30,0\.36\]\[0\.30,0\.36\]0\.360\.36\[0\.34,0\.40\]\[0\.34,0\.40\]0\.420\.42\[0\.38,0\.46\]\[0\.38,0\.46\]2\+2^\{\+\}4654650\.150\.15\[0\.12,0\.18\]\[0\.12,0\.18\]0\.630\.63\[0\.58,0\.67\]\[0\.58,0\.67\]0\.150\.15\[0\.12,0\.18\]\[0\.12,0\.18\]0\.280\.28\[0\.25,0\.32\]\[0\.25,0\.32\]0\.240\.24\[0\.19,0\.29\]\[0\.19,0\.29\]3\+3^\{\+\}4654650\.150\.15\[0\.12,0\.19\]\[0\.12,0\.19\]0\.670\.67\[0\.63,0\.71\]\[0\.63,0\.71\]0\.150\.15\[0\.12,0\.19\]\[0\.12,0\.19\]0\.320\.32\[0\.29,0\.35\]\[0\.29,0\.35\]0\.230\.23\[0\.19,0\.28\]\[0\.19,0\.28\]2⊗2^\{\\otimes\}1551550\.030\.03\[0\.01,0\.06\]\[0\.01,0\.06\]0\.740\.74\[0\.67,0\.81\]\[0\.67,0\.81\]0\.030\.03\[0\.01,0\.06\]\[0\.01,0\.06\]0\.270\.27\[0\.23,0\.32\]\[0\.23,0\.32\]0\.040\.04\[0\.01,0\.09\]\[0\.01,0\.09\]
#### Effects of inference\-time compute\.

SupplementaryLABEL:fig:reasoning\_effortdisplays the effect of scaling inference\-time compute \(or“reasoning effort”\) across three models:gpt\-5\.4,gpt\-5\.5, andclaude\-sonnet\-4\-6\. Surprisingly, we do not observe a consistent performance improvement when transitioning from low to high reasoning\-effort configurations\. In the most challenging setting featuring interacting mutations, all evaluated models failed entirely regardless of the allocated compute budget\. However, because the sample size for this particular experiment \(k=2⊗k=2^\{\\otimes\}\) was very small \(one mutation configuration withn=5n=5per model and reasoning effort\), these results remain preliminary, and further evaluation is required to substantiate this trend\.

## 6Discussion

We introduced Elenchos, a framework for studying abductive diagnostic reasoning in LLMs through the inference of latent rule mutations in formal systems\. By framing diagnosis as a structural inverse problem, Elenchos enables the study of a fundamental reasoning capability that remains poorly understood in current AI systems\.

Across two complementary evaluation regimes, our results provide several insights into the capabilities and limitations of contemporary frontier reasoning models:

- •Detection–attribution dissociation:Models consistently detect behavioral anomalies far more reliably than they isolate their underlying causes\. This gap suggests that recognizing the existence of a system discrepancy is a significantly lower cognitive hurdle than constructing a complete, valid explanatory hypothesis for it\.
- •Interacting mutations as a critical failure mode:Non\-additive configurations present an exceptional challenge across all evaluated LLMs\. Performance drops sharply in these regimes, exposing a lack of robust compositional reasoning when navigating overlapping causal effects\.
- •Single\-mutation bias:When multiple mutations are present, models exhibit a strong tendency to terminate their diagnostic search prematurely after identifying a single plausible explanation as soon as the information about the mutation orderkkis missing in the system prompt\. Because attribution failures are overwhelmingly dominated by under\-reporting rather than the hallucination of non\-existent mutations, current systems appear to act as heuristic hypothesis generators rather than exhaustive reasoners\.
- •High sensitivity to prompt scaffolding:Providing structured prompt scaffolding significantly improves attribution accuracy, indicating that the underlying diagnostic capacity is often present but requires explicit environmental conditioning to be fully leveraged\.
- •Tentative insensitivity to inference\-time compute:Preliminary results suggest that moving from low\- to high\-reasoning\-effort configurations yields no statistically significant gains in attribution accuracy\. While this compute\-scaling dimension requires larger\-scale testing to confirm a definitive trend, early data implies that scaling search tokens alone may not resolve fundamental abductive deficits\.

These findings raise a fundamental question: Do these failure modes reflect a fundamental limitation of current AI architectures, or a capability that can be mitigated through training, representation, and reasoning strategies?

### 6\.1Limitations

While Elenchos provides a rigorous framework for isolating abductive capacity, our evaluation is bounded by several specific constraints\.

- •Domain and ontology bounds:Our evaluation is constrained to a restricted formal language and a curated 13\-mutation ontology with maximum mutation counts ofk=3k=3\. Although this constraint ensures precise control over the ground\-truth causal structure, it does not fully mirror the expansive complexity of large\-scale production software or open\-ended adversarial environments\.
- •Sample scaling and edge\-Case performance:Certain auxiliary dimensions warrant broader empirical scaling\. Specifically, our preliminary insights regarding the limited efficacy of inference\-time compute rely on a small sample size that requires deeper validation\. Furthermore, the most challenging configurations, such as pairing minimal prompt context with heavily interacting mutations, require dedicated stress\-testing using the next generation of frontier LLMs\.
- •Confounding formal\-system dynamics:Success in the current benchmark requires a model to simultaneously excel at abductive attribution and symbolic formal reasoning\. The pronounced detection–attribution dissociation observed here motivates the instantiation of the framework across non\-symbolic, rule\-governed environments to cleanly disentangle general deficits in abductive logic from localized limitations in formal semantic parsing\.
- •Prompt sensitivity:Our current protocol relies on fixed prompt scaffolds\. The high variance in accuracy across different prompt conditions highlights a stark sensitivity to elicitation strategies, leaving open the question of how optimal prompting strategies might close the attribution gap\.

### 6\.2Broader Impact and Applications

Although Elenchos is instantiated here using a dependently typedλ\\lambda\-calculus kernel, the underlying capability it measures – inferring hidden structural modifications from behavioral anomalies – is a fundamental component of reasoning in several practical and scientific domains\.

- •Cybersecurity and forensics:Security analysts routinely trace unexpected system behaviors back to root causes under conditions of incomplete information, adversarial masking, and zero\-day exploitation\. By testing a model’s ability to untangle interacting mutations, Elenchos provides a contamination\-resistant environment for evaluating the rigorous forensic reasoning required for automated incident response and vulnerability analysis\.
- •System assurance and autonomous agents:As LLM\-based systems are increasingly deployed in safety\-critical orchestration and monitoring workflows, their ability to perform reliable multi\-fault diagnosis becomes essential\. Assessing whether an agent can move beyond surface\-level anomaly detection toward complete causal attribution is vital for mitigating silent failures and preventing cascading system errors in production environments\.
- •Scientific discovery and hypothesis generation:Many scientific breakthroughs rely on modeling unobservable mechanisms from sparse experimental data\. By isolating abductive reasoning from simple pattern completion, Elenchos offers a controlled testbed to evaluate how effectively frontier models can participate in automated hypothesis generation and the discovery of latent physical or logical laws\.

### 6\.3Future Directions

Disentangling whether the observed detection–\-attribution gap is a persistent architectural barrier or a treatable engineering challenge remains a primary objective\. Addressing this will require systematic evaluation across model scales, training paradigms, and inference\-time reasoning budgets, alongside the development of external scaffolding\.

A further direction is to extend Elenchos beyond the dependently typedλ\\lambda\-calculus setting to other rule\-governed systems and surface languages\. Such extensions would help distinguish general limitations in abductive attribution from difficulties arising from the particular symbolic representations used in the current benchmark\.

Additional directions include studying prompt sensitivity and elicitation effects, developing adaptive verification procedures, exploring automated self\-correction mechanisms, and extending the mutation ontology to larger and more diverse hypothesis spaces\.

### Acknowledgements

This work was supported by the grant DFG SPP\-2041 \(DFG LO1728/2\-1, SCHE 658/17\-1\)\. The authors have no competing interests\.

## References

- \[1\]M\. Akhtar and et al\.\(2026\)When AI benchmarks plateau: A systematic study of benchmark saturation\.arXiv\.External Links:[Document](https://dx.doi.org/arXiv%3A2602.16763)Cited by:[§1](https://arxiv.org/html/2607.12733#S1.p4.1),[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px1.p1.1)\.
- \[2\]T\. Altenkirch and A\. Kaposi\(2016\)Normalisation by Evaluation for Dependent Types\.In1st International Conference on Formal Structures for Computation and Deduction \(FSCD 2016\),LIPIcs, Vol\.52\.Note:[https://doi\.org/10\.4230/LIPIcs\.FSCD\.2016\.6](https://doi.org/10.4230/LIPIcs.FSCD.2016.6)Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px2.p1.1)\.
- \[3\]G\. Authors\(2025\)GEAR: A General Evaluation Framework for Abductive Reasoning\.arXiv\.Note:arXiv:2509\.24096 \(verify author list at camera\-ready\)Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px3.p3.1)\.
- \[4\]I\. Authors\(2024\)A Benchmark for Inductive and Abductive Reasoning over Synthetic Ontology Trees\.arXiv\.Note:arXiv:2509\.03345 \(working title pending publication; verify before camera\-ready\)Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px3.p3.1)\.
- \[5\]E\. Bender, T\. Gebru, A\. McMillan\-Major, and S\. Shmitchell\(2021\)On the Dangers of Stochastic Parrots: Can Language Models Be Too Big?\.InACM Conference on Fairness, Accountability, and Transparency,Note:doi:10\.1145/3442188\.3445922Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px1.p1.1)\.
- \[6\]E\. M\. Bender, T\. Gebru, A\. McMillan\-Major, and S\. Shmitchell\(2021\)On the Dangers of Stochastic Parrots: Can Language Models Be Too Big?\.InProc\. ACM Conf\. on Fairness, Accountability, and Transparency \(FAccT\),Note:[https://doi\.org/10\.1145/3442188\.3445922](https://doi.org/10.1145/3442188.3445922)Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px5.p1.1)\.
- \[7\]C\. Bhagavatula, R\. Le Bras, C\. Malaviya, K\. Sakaguchi, A\. Holtzman, H\. Rashkin, D\. Downey, W\. Yih, and Y\. Choi\(2020\)Abductive Commonsense Reasoning\.InInternational Conference on Learning Representations \(ICLR\),Note:arXiv:1908\.05739Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px3.p3.1)\.
- \[8\]BIG\-bench authors\(2023\)Beyond the Imitation Game: Quantifying and Extrapolating the Capabilities of Language Models\.Transactions on Machine Learning Research\.Note:https://openreview\.net/forum?id=uyTL5BvosjCited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px1.p1.1)\.
- \[9\]M\. Carneiro\(2025\)Lean4Lean: Verifying a Typechecker for Lean, in Lean\.arXiv\.Note:https://doi\.org/10\.48550/arXiv\.2403\.14064Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px2.p1.1)\.
- \[10\]Center for AI Safety, Scale AI, and HLE Contributors Consortium\(2026\)A benchmark of expert\-level academic questions to assess AI capabilities\.Nature649,pp\. 1139–1146\.Note:https://doi\.org/10\.1038/s41586\-025\-09962\-4Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px1.p1.1)\.
- \[11\]E\.K\. Chen, M\. Belkin, L\. Bergen, and D\. Danks\(2026\)Does AI already have human\-level intelligence? The evidence is clear\.\.Nature650\.Note:https://www\.nature\.com/articles/d41586\-026\-00285\-6Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px1.p1.1),[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px5.p1.1)\.
- \[12\]T\.Y\. Chen, F\.\-C\. Kuo, H\. Liu, P\. Poo, D\. Towey, and Z\.Q\. Tse\(2018\)Metamorphic testing: a review of challenges and opportunities\.ACM Comput\. Surv\.51\(1\)\.Note:https://doi\.org/10\.1145/3143561Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px3.p1.1)\.
- \[13\]A\. Church\(1932\)A set of postulates for the foundation of logic\.Annals of Mathematics, Series 232\(2\),pp\. 346–366\.Cited by:[§1](https://arxiv.org/html/2607.12733#S1.p5.2)\.
- \[14\]K\. Cobbe, V\. Kosaraju, M\. Bavarian, M\. Chen, H\. Jun, L\. Kaiser, M\. Plappert, J\. Tworek, J\. Hilton, R\. Nakano, C\. Hesse, and J\. Schulman\(2021\)Training Verifiers to Solve Math Word Problems\.arXiv preprint arXiv:2110\.14168\.Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px1.p1.1)\.
- \[15\]K\.M\. Collins and J\.B\. Tenenbaum\(2026\)Expert\-level test is a head\-scratcher for AI\.Nature649\.Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px1.p1.1),[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px5.p1.1)\.
- \[16\]T\. Coquand and G\. Huet\(1988\)The Calculus of Constructions\.Information and Computation76\.Cited by:[§1](https://arxiv.org/html/2607.12733#S1.p5.2)\.
- \[17\]CrowdStrike\(2024\)External Technical Root Cause Analysis – Channel File 291\.Note:https://www\.crowdstrike\.com/wp\-content/uploads/2024/08/Channel\-File\-291\-Incident\-Root\-Cause\-Analysis\-08\.06\.2024\.pdfCited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px4.p1.1)\.
- \[18\]R\. Degiovanni and M\. Papadakis\(2022\)μ\\muBert: Mutation Testing using Pre\-Trained Language Models\.In15th IEEE International Conference on Software Testing, Verification and Validation Workshops \(ICSTW\),Note:[https://doi\.org/10\.1109/ICSTW55395\.2022\.00040](https://doi.org/10.1109/ICSTW55395.2022.00040)Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px3.p1.1)\.
- \[19\]E\. First, M\.N\. Rabe, T\. Ringer, and Y\. Brun\(2023\)Baldur: Whole\-Proof Generation and Repair with Large Language Models\.arXiv\.Note:arXiv:2303\.04910,[https://doi\.org/10\.48550/arXiv\.2303\.04910](https://doi.org/10.48550/arXiv.2303.04910)Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px2.p1.1)\.
- \[20\]A\. Freund\(2024\)Backdoor in upstream xz/liblzma leading to ssh server compromise\.Note:https://www\.openwall\.com/lists/oss\-security/2024/03/29/4Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px4.p1.1)\.
- \[21\]E\. Glazer and et al\.\(2025\)FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AI\.arXiv\.Note:https://doi\.org/10\.48550/arXiv\.2411\.04872Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px1.p1.1)\.
- \[22\]S\. Haroon, M\. T\. Khan, and M\. A\. Gulzar\(2026\)Evaluating LLM\-Based Test Generation Under Software Evolution\.arXiv\.Note:arXiv:2603\.23443Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px3.p1.1),[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px5.p1.1)\.
- \[23\]D\. Hendrycks, C\. Burns, S\. Basart, A\. Zou, M\. Mazeika, D\. Song, and J\. Steinhardt\(2021\)Measuring Massive Multitask Language Understanding\.Proceedings of the International Conference on Learning Representations \(ICLR\)\.Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px1.p1.1)\.
- \[24\]D\. Hendrycks, C\. Burns, S\. Kadavath, A\. Arora, S\. Basart, E\. Tang, D\. Song, and J\. Steinhardt\(2021\)Measuring Mathematical Problem Solving With the MATH Dataset\.InNeuRIPS,Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px1.p1.1)\.
- \[25\]J\.R\. Hindley and J\.P\. Seldon\(2008\)Lambda\-Caluculus and Combinators – an Introduction\.Cambridge University Press\.Cited by:[§1](https://arxiv.org/html/2607.12733#S1.p5.2)\.
- \[26\]T\. Hubert, A\. Banino, and Google DeepMind Theorem Proving Team\(2025\)Olympiad\-Level Formal Mathematical Reasoning with Reinforcement Learning\.Nature\.Note:[https://doi\.org/10\.1038/s41586\-025\-09833\-y](https://doi.org/10.1038/s41586-025-09833-y)Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px2.p1.1)\.
- \[27\]\(2025\)Humanity’s Last Exam\.Note:[https://agi\.safe\.ai/](https://agi.safe.ai/)Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px1.p1.1)\.
- \[28\]Y\. Jia and M\. Harman\(2011\)An Analysis and Survey of the Development of Mutation Testing\.IEEE Trans on Software Engineering37\(5\)\.Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px3.p1.1)\.
- \[29\]S\. Kang, G\. An, and S\. Yoo\(2024\)A Quantitative and Qualitative Evaluation of LLM\-Based Explainable Fault Localization\.Proceedings of the ACM on Software Engineering1\(FSE\)\.Note:[https://doi\.org/10\.1145/3660771](https://doi.org/10.1145/3660771)Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px3.p3.1)\.
- \[30\]A\. Kovács\(2023\)smalltt: a Minimal Dependent Type Theory Elaborator\.Note:[https://github\.com/AndrasKovacs/smalltt](https://github.com/AndrasKovacs/smalltt)Accessed 2026\-05Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px2.p1.1)\.
- \[31\]V\. Le, M\. Afshari, and Z\. Su\(2014\)Compiler Validation via Equivalence Modulo Inputs\.InProc\. 35th ACM SIGPLAN Conf\. on Programming Language Design and Implementation \(PLDI ’14\),pp\. 216–226\.Note:[https://doi\.org/10\.1145/2594291\.2594334](https://doi.org/10.1145/2594291.2594334)Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px3.p1.1)\.
- \[32\]Z\. Li and D\. Shin\(2024\)Mutation\-Based Consistency Testing for Evaluating the Code Understanding Capability of LLMs\.InProc\. IEEE/ACM 3rd Int\. Conf\. on AI Engineering – Software Engineering for AI,pp\. 150–159\.Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px3.p1.1)\.
- \[33\]H\. Lightman, V\. Kosaraju, Y\. Burda, H\. Edwards, B\. Baker, T\. Lee, J\. Leike, J\. Schulman, I\. Sutskever, and K\. Cobbe\(2023\)Let’s Verify Step by Step\.arXiv\.Note:arXiv:2305\.20050Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px5.p1.1)\.
- \[34\]A\. Löh, C\. McBride, and W\. Swierstra\(2010\)A Tutorial Implementation of a Dependently Typed Lambda Calculus\.Fundamenta Informaticae102,pp\. 177–207\.Note:https://doi\.org/10\.3233/FI\-2010\-304Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px2.p1.1),[§4](https://arxiv.org/html/2607.12733#S4.SS0.SSS0.Px2.p1.1)\.
- \[35\]P\. Martin\-Löf\(1984\)Intuitionistic type theory\.Bibliopolis,Naples\.Note:Notes by Giovanni Sambin, Studies in Proof TheoryCited by:[§1](https://arxiv.org/html/2607.12733#S1.p5.2)\.
- \[36\]T\.R\. McIntosh, T\. Susnjak, N\. Arachchilage, T\. Liu, D\. Xu, P\. Watters, and M\.N\. Halgamuge\(2026\)Inadequacies of large language model benchmarks in the era of generative artificial intelligence\.IEEE Transactions on Artificial Intelligence7\(1\),pp\. 22–39\.Note:doi: 10\.1109/TAI\.2025\.3569516Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px1.p1.1)\.
- \[37\]W\. M\. McKeeman\(1998\)Differential Testing for Software\.Digital Technical JournalTechnical Report10\(1\),Digital Equipment Corporation\.Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px3.p1.1)\.
- \[38\]G\. Mialon, C\. Fourrier, C\. Swift, T\. Wolf, Y\. LeCun, and T\. Scialom\(2023\)GAIA: a benchmark for General AI Assistants\.arXiv:2311\.12983\.Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px1.p1.1)\.
- \[39\]I\. Mirzadeh, K\. Alizadeh, H\. Shahrokhi, O\. Onutlu, O\. Tuzel, S\. Samet, and S\.\-M\. Samadi\(2024\)GSM\-Symbolic: Understanding the Limitations of Mathematical Reasoning in Large Language Models\.arXiv preprint arXiv:2410\.05229\.Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px1.p1.1),[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px5.p1.1)\.
- \[40\]I\. Mirzadeh, K\. Alizadeh, H\. Shahrokhi, Tuzel,O\., S\. Bengio, and M\. Farajtabar\(2024\)GSM\-NoOp: A Stress Test for the Reasoning Robustness of LLMs\.arXiv\.Note:https://arxiv\.org/abs/2410\.05229Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px5.p1.1)\.
- \[41\]M\. Papadakis and Y\. Le Traon\(2015\)Metallaxis\-FL: Mutation\-Based Fault Localization\.Software Testing, Verification and Reliability25\(5\-7\),pp\. 605–628\.Note:[https://doi\.org/10\.1002/stvr\.1509](https://doi.org/10.1002/stvr.1509)Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px3.p3.1)\.
- \[42\]C\. S\. Peirce\(1998\)Pragmatism as the logic of abduction\.InThe Essential Peirce, Volume 2,P\. E\. Project \(Ed\.\),Note:Originally delivered as a Harvard lecture, 1903Cited by:[§3](https://arxiv.org/html/2607.12733#S3.SS0.SSS0.Px5.p1.1)\.
- \[43\]S\. Polu and I\. Sutskever\(2020\)Generative Language Modeling for Automated Theorem Proving\.InarXiv,Note:arXiv:2009\.03393,[https://doi\.org/10\.48550/arXiv\.2009\.03393](https://doi.org/10.48550/arXiv.2009.03393)Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px2.p1.1)\.
- \[44\]I\. S\. Qureshi and Z\. M\. \(\. Jiang\(2025\)Test Case Generation from Bug Reports via Large Language Models: A Cognitive Layered Evaluation Framework\.arXiv\.Note:arXiv:2510\.05365Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px3.p1.1),[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px5.p1.1)\.
- \[45\]D\. Rein, B\.L\. Hou, A\.C\. Stickland, J\. Jackson, S\.R\. Bowman,et al\.\(2023\)GPQA: A Graduate\-Level Google\-Proof Q&A Benchmark\.arXiv preprint arXiv:2311\.12022\.Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px1.p1.1)\.
- \[46\]Z\.Z\. Ren, Z\. Shao, J\. Song, H\. Xin, H\. Wang, W\. Zhao, L\. Zhang, Z\. Fu, Q\. Zhu, D\. Yang, Z\.F\. Wu, Z\. Gou, S\. Ma, H\. Tang, Y\. Liu, W\. Gao, D\. Guo, and C\. Ruan\(2025\)DeepSeek\-Prover\-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition\.arXiv\.Note:arXiv:2504\.21801,[https://doi\.org/10\.48550/arXiv\.2504\.21801](https://doi.org/10.48550/arXiv.2504.21801)Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px2.p1.1)\.
- \[47\]M\. Salimi, S\. Adim, D\. Parnian, N\. Alighardashi, M\.J\. Siavoshani, and M\.H\. Rohban\(2026\)Wiring the ‘Why’: A Unified Taxonomy and Survey of Abductive Reasoning in LLMs\.arXiv\.Note:arXiv:2604\.08016Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px3.p3.1)\.
- \[48\]M\. Schönfinkel\(1924\)Über die Bausteine der mathematischen Logik\.Mathematische Annalen92\(3–4\),pp\. 305–316\.Note:doi:10\.1007/BF01448013Cited by:[§1](https://arxiv.org/html/2607.12733#S1.p5.2)\.
- \[49\]M\. Sozeau, S\. Boulier, Y\. Forster, N\. Tabareau, and T\. Winterhalter\(2020\)Coq Coq Correct\! Verification of Type Checking and Erasure for Coq, in Coq\.Proceedings of the ACM on Programming Languages4\(POPL\)\.Note:[https://doi\.org/10\.1145/3371076](https://doi.org/10.1145/3371076)Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px2.p1.1)\.
- \[50\]M\. Sozeau, Y\. Forster, M\. Lennon\-Bertrand, J\. B\. Nielsen, N\. Tabareau, and T\. o\. Winterhalter\(2021\)Touring the MetaCoq Project\.Electronic Proceedings in Theoretical Computer Science \(EPTCS\)\.Note:arXiv:2107\.07670,[https://doi\.org/10\.48550/arXiv\.2107\.07670](https://doi.org/10.48550/arXiv.2107.07670)Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px2.p1.1)\.
- \[51\]Stanford HAI\(2026\)The 2026 AI Index Report: Technical Performance\.Note:https://hai\.stanford\.edu/ai\-index/2026\-ai\-index\-reportCited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px1.p1.1)\.
- \[52\]K\. Thompson\(1984\)Reflections on trusting trust\.Communications of the ACM\.Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px4.p1.1)\.
- \[53\]F\. Tip, J\. Bell, and M\. Schäfer\(2024\)LLMorpheus: Mutation Testing using Large Language Models\.arXiv\.Note:arXiv:2404\.09952,[https://doi\.org/10\.48550/arXiv\.2404\.09952](https://doi.org/10.48550/arXiv.2404.09952)Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px3.p1.1),[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px3.p2.1)\.
- \[54\]J\. Wei, X\. Wang, D\. Schuurmans, M\. Bosma, B\. Ichter, F\. Xia, E\. Chi, Q\. V\. Le, and D\. Zhou\(2022\)Chain\-of\-Thought Prompting Elicits Reasoning in Large Language Models\.InAdvances in Neural Information Processing Systems \(NeurIPS\),Vol\.35,pp\. 24824–24837\.Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px5.p1.1)\.
- \[55\]Z\. Wei, Y\. Zhang, and M\. Sun\(2024\)MILE: A Mutation Testing Framework of In\-Context Learning Systems\.InarXiv,Note:arXiv:2409\.04831,[https://doi\.org/10\.48550/arXiv\.2409\.04831](https://doi.org/10.48550/arXiv.2409.04831)Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px3.p1.1)\.
- \[56\]C\. White, S\. Dooley, M\. Roberts, A\. Pal, B\. Feuer, S\. Jain,et al\.\(2024\)LiveBench: a challenging, contamination\-limited llm benchmark\.arXiv preprint arXiv:2406\.19314\.Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px1.p1.1)\.
- \[57\]H\. Xin, D\. Guo, Z\. Shao, Z\. Ren, Q\. Zhu, B\. Liu, C\. Ruan, W\. Li, and X\. Liang\(2024\)DeepSeek\-Prover: Advancing Theorem Proving in LLMs through Large\-Scale Synthetic Data\.arXiv\.Note:arXiv:2405\.14333,[https://doi\.org/10\.48550/arXiv\.2405\.14333](https://doi.org/10.48550/arXiv.2405.14333)Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px2.p1.1)\.
- \[58\]J\. Yan, J\. Huang, C\. Fang, J\. Yan, and J\. Zhang\(2024\)Better Debugging: Combining Static Analysis and LLMs for Explainable Crashing Fault Localization\.arXiv\.Note:arXiv:2408\.12070Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px3.p3.1)\.
- \[59\]A\. Z\.H\. Yang, C\. Le Goues, R\. Martins, and V\. J\. Hellendoorn\(2024\)Large Language Models for Test\-Free Fault Localization\.InProc\. IEEE/ACM 46th Int\. Conf\. on Software Engineering \(ICSE ’24\),Note:[https://doi\.org/10\.1145/3597503\.3623342](https://doi.org/10.1145/3597503.3623342)Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px3.p3.1)\.
- \[60\]B\. Yang, H\. Tian, J\. Ren, H\. Zhang, J\. Klein, T\. F\. Bissyandé, C\. Le Goues, and S\. Jin\(2025\)Integrating Various Software Artifacts for Better LLM\-Based Bug Localization and Program Repair\.ACM Transactions on Software Engineering and Methodology\.Note:arXiv:2412\.03905Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px3.p3.1)\.
- \[61\]K\. Yang, A\.M\. Swope, A\. Gu, R\. Chalamala, P\. Song, S\. Yu, S\. Godil, R\. Prenger, and A\. Anandkumar\(2023\)LeanDojo: Theorem Proving with Retrieval\-Augmented Language Models\.InAdvances in Neural Information Processing Systems \(NeurIPS\), Datasets and Benchmarks Track,Note:[https://doi\.org/10\.48550/arXiv\.2306\.15626](https://doi.org/10.48550/arXiv.2306.15626)Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px2.p1.1)\.
- \[62\]X\. Yang, Y\. Chen, E\. Eide, and J\. Regehr\(2011\)Finding and understanding bugs in C compilers\.InProc\. 32nd ACM SIGPLAN conf\. on Programming language design and implementation \- PLDI ’11,pp\. 283–294\.Note:https://doi\.org/10\.1145/1993498\.19935Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px3.p1.1)\.
- \[63\]S\. Yao, D\. Yu, J\. Zhao, I\. Shafran, T\. L\. Griffiths, Y\. Cao, and K\. Narasimhan\(2023\)Tree of Thoughts: Deliberate Problem Solving with Large Language Models\.InNeurIPS,Note:arXiv:2305\.10601Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px5.p1.1)\.
- \[64\]Z\. Yu, R\. Peng, K\. Ding, Y\. Li, Z\. Peng, M\. Liu, Y\. Zhang, Z\. Yuan, H\. Xin, W\. Huang, Y\. Wen, G\. Zhang, and W\. Liu\(2025\)FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models\.arXiv\.Note:https://doi\.org/10\.48550/arXiv\.2505\.02735Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px2.p1.1)\.
- \[65\]K\. Zheng, J\.M\. Han, and S\. Polu\(2021\)MiniF2F: a cross\-system benchmark for formal Olympiad\-level mathematics\.arXiv:2109\.00110\.Cited by:[§2](https://arxiv.org/html/2607.12733#S2.SS0.SSS0.Px2.p1.1)\.

Supplementary Material

## Appendix ALambdaPySurface Grammar

The surface syntax accepted by the kernel is defined by the Lark grammar reproduced below \(lambdapy/grammar\.lark\)\. Source strings are parsed with Lark’s Earley algorithm and elaborated to locally\-nameless de Bruijn terms before reaching the bidirectional type checker\.

//LambdaPisurfacesyntaxgrammar\(LarkEarley\)

//

//SupportsbothPython\-styleandHaskell\-stylesyntax:

//Python:assumex:THaskell:assume\(x::T\)

//Python:letx:T=bodyHaskell:letx=\(body::T\)

//Python:e:THaskell:e::T

//Python:Type0Haskell:\*\(sameasType0\)

//

//EachstatementoccupiesonelogicallineendingwithNEWLINE\.

%importcommon\.CNAME\-\>NAME

%importcommon\.INT

%importcommon\.NEWLINE

%importcommon\.WS\_INLINE

%ignoreWS\_INLINE

%ignore/\-\-\[^\\n\]\*/

start:statement\+

//\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-

//Statements\(eachendswithNEWLINE\)

//\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-

//Haskell\-style:assume\(a::\*\)\(b::\*\)orassumea::\*

//Python\-style:assumexy:T

statement:"assume"paren\_binding\+NEWLINE\-\>assume\_multi\_stmt

\|"assume"NAME\("::"\|":"\)termNEWLINE\-\>assume\_single\_stmt

\|"assume"name\_list":"termNEWLINE\-\>assume\_stmt

\|"let"NAME"="termNEWLINE\-\>let\_infer\_stmt

\|"let"NAME":"term"="termNEWLINE\-\>let\_stmt

\|"eval"termNEWLINE\-\>eval\_stmt

\|"check"termNEWLINE\-\>check\_stmt

//ParenthesizedbindingforHaskell\-styleassume

paren\_binding:"\("NAME\("::"\|":"\)term"\)"

name\_list:NAME\+

//\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-

//Terms

//\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-

term:lam\_term

\|forall\_term

\|app\_term"\-\>"term\-\>arrow

\|app\_term\("::"\|":"\)term\-\>ann

\|app\_term

//Lambda

lam\_term:"\\\\"NAME\+"\-\>"term

//Universal\(forallbindersupportsboth:and::\)

forall\_term:"forall"binder\+"\."term

binder:"\("NAME\("::"\|":"\)term"\)"

//\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-

//Application\(left\-associative\)

//\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-

app\_term:atom\+\-\>app\_chain

//\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-

//Atoms

//\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-

atom:"\("term"\)"\-\>paren

\|"Type"INT?\-\>universe

\|"\*"INT?\-\>universe

\|"Nat"\-\>nat

\|"Zero"\-\>zero

\|"Succ"\-\>succ\_kw

\|"NatElim"\-\>nat\_elim\_kw

\|"natElim"\-\>nat\_elim\_kw

\|"Vec"\-\>vec\_kw

\|"Nil"\-\>nil\_kw

\|"Cons"\-\>cons\_kw

\|"VecElim"\-\>vec\_elim\_kw

\|"vecElim"\-\>vec\_elim\_kw

\|"Fin"\-\>fin\_kw

\|"FZero"\-\>fzero\_kw

\|"FSucc"\-\>fsucc\_kw

\|"FinElim"\-\>fin\_elim\_kw

\|"finElim"\-\>fin\_elim\_kw

\|"Eq"\-\>eq\_kw

\|"Refl"\-\>refl\_kw

\|"EqElim"\-\>eq\_elim\_kw

\|"eqElim"\-\>eq\_elim\_kw

\|NAME\-\>var

## Appendix BMutation Taxonomy

Table 3:Full mutation taxonomy used in the current\|ℳ\|=13\|\\mathcal\{M\}\|=13implementation\.IDClassMutation name and descriptionID\_01Type EqualityEquality of Applications Argument
Checker strictly enforces equality on both the function and the argument when comparing applications\.ID\_02Binding DisciplineFail to Increment Under Lambda
A substitution intended for an outer binder can incorrectly replace the inner bound variable\.ID\_03Type EqualityEquality of Bound Indices
𝙱𝚘𝚞𝚗𝚍​\(0\)\\mathtt\{Bound\}\(0\)and𝙱𝚘𝚞𝚗𝚍​\(1\)\\mathtt\{Bound\}\(1\)are considered definitionally equal; dependent types over adjacent binders collapse\.ID\_04Binding DisciplineIndex Shift
𝙱𝚘𝚞𝚗𝚍​\(i\)\\mathtt\{Bound\}\(i\)lookup uses𝚎𝚗𝚟​\[min⁡\(i\+1,len​\(𝚎𝚗𝚟\)−1\)\]\\mathtt\{env\}\[\\min\(i\{\+\}1,\\,\\mathrm\{len\}\(\\mathtt\{env\}\)\{\-\}1\)\]instead of𝚎𝚗𝚟​\[i\]\\mathtt\{env\}\[i\]\. Causes de Bruijn variable resolution to silently drift by one position\.ID\_05Semantic EnvironmentGlobals to Zero
Unknown globals normalize to𝚉𝚎𝚛𝚘\\mathtt\{Zero\}rather than staying neutral; type checking proceeds, semantics are junk\.ID\_06Semantic EnvironmentLambda Environment Reversion
The binder is placed at the wrong end of the environment\. With the existing𝙱𝚘𝚞𝚗𝚍​\(i\)→𝚎𝚗𝚟​\[i\]\\mathtt\{Bound\}\(i\)\\rightarrow\\mathtt\{env\}\[i\]convention, lambda bodies evaluate against a scrambled scope discipline\.ID\_07Type EqualityEquality of Inference Terms
Equality of inference terms collapses; all types are judged equal, but inference still succeeds on well\-typed terms\.ID\_08Semantic EnvironmentLambda Environment Padding
Closure environment is padded with a neutral element, shifting all argument positions by one\.ID\_09Computational RuleDouble Application
Function is applied a second time to the result of itself\.ID\_10Type EqualityEquality of Free Terms
Any two neutral heads become definitionally equal after quotation; unrelated dependent types collapse\.ID\_11Semantic EnvironmentGlobals to Identity
Unknown globals normalize to the identity function rather than staying neutral\.ID\_12Universe LevelingUniverse Collapse
𝚂𝚝𝚊𝚛​\(n\)\\mathtt\{Star\}\(n\)returns𝚅𝚂𝚝𝚊𝚛​\(n\)\\mathtt\{VStar\}\(n\)instead of𝚅𝚂𝚝𝚊𝚛​\(n\+1\)\\mathtt\{VStar\}\(n\+1\); the universe hierarchy collapses \(𝚃𝚢𝚙𝚎n:𝚃𝚢𝚙𝚎n\\mathtt\{Type\}\_\{n\}:\\mathtt\{Type\}\_\{n\}\)\.ID\_13Computational RuleArgument Dropping
Function argument is dropped;𝚅𝚂𝚝𝚊𝚛​\(0\)\\mathtt\{VStar\}\(0\)\(𝚃𝚢𝚙𝚎\\mathtt\{Type\}\) is used instead\.Mutation IDs rank differently in difficulty\. There are mutations and classes that are inherently hard or easy regardless of model variants as observed in[Figure 5](https://arxiv.org/html/2607.12733#A2.F5)\.

![Refer to caption](https://arxiv.org/html/2607.12733v1/x5.png)\(a\)Per\-mutation accuracyVKV\_\{K\}\.
![Refer to caption](https://arxiv.org/html/2607.12733v1/x6.png)\(b\)Per\-mutation first divergent probe\.

Figure 5:Difficulty ofn=13n=13mutations at orderk=1k=1based on“Ladder”experiment\.Values are averaged across prompt variant conditions\. Classes that are consistently hard or easy to determine are shown by striking rows\.### B\.1Class Label Mapping

Per\-mutation experimental tables \([Figure 5](https://arxiv.org/html/2607.12733#A2.F5)\) use a coarser secondary grouping —binding,free\_name,application,def\_equality,universe— that was generated at experiment time\. The five\-class taxonomy above \(Binding Discipline, Semantic Environment, Computational Rule, Type Equality, Universe Leveling\) is the canonical one used by the protocol; the coarser labels are an analysis\-time grouping retained for compatibility with the released figures \([Table 4](https://arxiv.org/html/2607.12733#A2.T4)gives the explicit mapping\)\.

Table 4:Mapping between canonical class names and labels in figures and tables\.Canonical classAnalysis\-time labelDescriptionBinding DisciplinebindingError in variable resolution such as de Bruijn misalignment and binder shiftingSemantic Environmentfree\_nameAltered substitution or closure environmentsComputational RuleapplicationCorruptions ofβ\\beta\-reductionType Equalitydef\_equalityChanges to type\-level equality or convertabilityUniverse LevelinguniverseViolations of cumulative universe stratification
### B\.2Simple Reflex Agent

TheSimple Reflex Agent \(RSA\)is designed to diagnose alln=13n=13mutations defined above \([Table 3](https://arxiv.org/html/2607.12733#A2.T3)\) assuming singleton mutationsk=1k=1\. This is achieved by constructing a probe setΠRSA⊂𝒯\\Pi\_\{\\texttt\{RSA\}\}\\subset\\mathcal\{T\}such that each pair of distinct mutations exhibits distinguishable behaviour for at least one probe in the set, while the corresponding mutation is also distinguishable from the reference

∀μ,μ′∈ℳ,μ≠μ′⇒∃τ∈ΠRSA:K\{μ\}\(τ\)≠K\{μ′\}\(τ\)∧K\{μ\}\(τ\)≠Kref\(τ\)\\displaystyle\\forall\\mu,\\mu^\{\\prime\}\\in\\mathcal\{M\},\\mu\\neq\\mu^\{\\prime\}\\Rightarrow\\,\\exists\\tau\\in\\Pi\_\{\\texttt\{RSA\}\}\\,:\\,K\_\{\\\{\\mu\\\}\}\(\\tau\)\\neq K\_\{\\\{\\mu^\{\\prime\}\\\}\}\(\\tau\)\\land K\_\{\\\{\\mu\\\}\}\(\\tau\)\\neq K\_\{\\text\{ref\}\}\(\\tau\)\(4\)By probing both kernels withΠRSA\\Pi\_\{\\texttt\{RSA\}\}, the agent can uniquely identify the present mutation by comparing kernels output to the expected observation forKSK\_\{S\}andKrefK\_\{\\text\{ref\}\}\.222The list of constructed probesΠRSA\\Pi\_\{\\texttt\{RSA\}\}and expected output ofKrefK\_\{\\text\{ref\}\}andKSK\_\{S\}can be provided on request\.

### B\.3Non\-degeneracy Filterk≥2k\\geq 2

The candidate family fork=2k=2is defined by

ℱ~2=\(ℳ2\),\\displaystyle\\tilde\{\\mathcal\{F\}\}\_\{2\}=\\binom\{\\mathcal\{M\}\}\{2\}\\,,\(5\)which are all possible 2\-element combinations of mutations inℳ\\mathcal\{M\}\. However, not all of them are admissible in the sense that they can be clearly identified\. We selected the family of valid combinationsℱ2\\mathcal\{F\}\_\{2\}by a deterministic three\-condition filter against a curated probe library based\.

#### Predicate\.

LetΠ⊂𝒯\\Pi\\subset\\mathcal\{T\}denote the probe library: a fixed, ontology\-balanced set ofLambdaPysource terms that exercises every mutation class\. For ak=2k=2candidate pairS=\{μi,μj\}∈ℱ~2S=\\\{\\mu\_\{i\},\\mu\_\{j\}\\\}\\in\\tilde\{\\mathcal\{F\}\}\_\{2\}, the divergence vectordiv⁡\(S\)\\operatorname\{div\}\(S\)ofKSK\_\{S\}againstKrefK\_\{\\mathrm\{ref\}\}onΠ\\Piis defined as

OS​\(τ\)=\(Kref​\(τ\),KS​\(τ\),τ\),\\displaystyle O\_\{S\}\(\\tau\)=\(K\_\{\\text\{ref\}\}\(\\tau\),K\_\{S\}\(\\tau\),\\tau\)\\,,\(6\)div​\(S\)=\{OS​\(τ\):τ∈Π\}\.\\displaystyle\\mathrm\{div\}\(S\)=\\left\\\{O\_\{S\}\(\\tau\):\\tau\\in\\Pi\\right\\\}\\,\.\(7\)The pair is*admissible*if

1. 1\.Non\-collapse\.div​\(S\)≠div​\(∅\)\\mathrm\{div\}\(S\)\\neq\\mathrm\{div\}\(\\emptyset\)\.KSK\_\{S\}has to be distinguishable fromKrefK\_\{\\text\{ref\}\}\. Additionally, uniformly rejecting or uniformly accepting pairs are excluded as“total logical collapse”:∃τm,τn∈Π​such that​τm≠τn∧KS​\(τm\)≠KS​\(τn\)\\exists\\,\\tau\_\{m\},\\tau\_\{n\}\\in\\Pi\\text\{ such that \}\\tau\_\{m\}\\neq\\tau\_\{n\}\\land K\_\{S\}\(\\tau\_\{m\}\)\\neq K\_\{S\}\(\\tau\_\{n\}\)\.
2. 2\.Non\-subsumption\.div​\(S\)≠div​\(\{μ\}\)​∀μ∈ℳ\\mathrm\{div\}\(S\)\\neq\\mathrm\{div\}\(\\\{\\mu\\\}\)\\;\\forall\\,\\mu\\in\\mathcal\{M\}in particular forμi,μj\\mu\_\{i\},\\,\\mu\_\{j\}\. Pairs whose composite divergence is indistinguishable from either singleton are excluded as“symptomatic subsumption”according to Occam’s razor\.
3. 3\.Identifiability\.div​\(S\)≠div​\(S′\)​∀S′∈ℱ~2∖\{S\}\\mathrm\{div\}\(S\)\\neq\\mathrm\{div\}\(S^\{\\prime\}\)\\;\\forall\\,S^\{\\prime\}\\in\\tilde\{\\mathcal\{F\}\}\_\{2\}\\setminus\\\{S\\\}\. Two pairs whose divergence vector is indistinguishable are excluded\.

#### Algorithm\.

For our implementation, we applied the corresponding mutation flag overrides \(Section[4](https://arxiv.org/html/2607.12733#S4)\) to each of the\(132\)=78\\binom\{13\}\{2\}=78candidate unordered pairs and ran theΠRSA\\Pi\_\{\\texttt\{RSA\}\}probe set on bothKrefK\_\{\\mathrm\{ref\}\}and the merged kernel; each probe under a fresh state which contained only the core in[Appendix A](https://arxiv.org/html/2607.12733#A1)\. Pairs that fail condition \(1\) or \(2\) are rejected\. Those failing condition \(3\) are tested further by extendingΠRSA\\Pi\_\{\\texttt\{RSA\}\}with probes designed specifically to distinguish the pairs\. If this is not successful, both pairs are rejected\. The remainder isℱ2\\mathcal\{F\}\_\{2\}\.

#### Extending tok\>2k\>2\.

The algorithm has to be applied iteratively for increasingkk, whereℱ~k=\(ℳk\)\\tilde\{\\mathcal\{F\}\}\_\{k\}=\\binom\{\\mathcal\{M\}\}\{k\}\. Only condition \(2\) needs to be generalized forS∈ℱ~kS\\in\\tilde\{\\mathcal\{F\}\}\_\{k\}todiv⁡\(S\)∉\{div⁡\(S′\):S′∈ℱk′,k′<k\}\\operatorname\{div\}\(S\)\\notin\\left\\\{\\operatorname\{div\}\(S^\{\\prime\}\):S^\{\\prime\}\\in\\mathcal\{F\}\_\{k^\{\\prime\}\},\\;k^\{\\prime\}<k\\right\\\}\. The divergence ofSSmust be new, i\. e\. it must not coincide with the divergence of any set with lower cardinality, in particular to subsets ofSS\.

### B\.4Interacting Mutation Sets

We characterized mutation setsSSwith cardinalityk≥2k\\geq 2asadditive\(highlighted byk\+k^\{\+\}\) if∀τ∈ΠRSA,∃Ssub⊊S​such that​\(Ssub​is additive∨\|Ssub\|=1\)∧OS​\(τ\)=OSsub​\(τ\)\\forall\\,\\tau\\in\\Pi\_\{\\texttt\{RSA\}\},\\ \\exists\\,S\_\{\\text\{sub\}\}\\subsetneq S\\text\{ such that \}\\left\(S\_\{\\text\{sub\}\}\\text\{ is additive \}\\lor\\;\|S\_\{\\text\{sub\}\}\|=1\\right\)\\;\\land\\;O\_\{S\}\(\\tau\)=O\_\{S\_\{\\text\{sub\}\}\}\(\\tau\)\. This basically means, that the behaviour of a corrupted kernelKSK\_\{S\}can be fully explained by singleton mutations inSSand there are no unexpected results\. In contrast, we characterize mutation sets asinteracting\(highlighted byk⊗k^\{\\otimes\}\) if they are not additive\. Note that there are different types of interacting sets based on a fixed probe set: They can be partially additive \(one mutation is still seen, the other not\), deceptive \(a singleton mutation is seen that is not active\), or causing new behaviour \(results can not be assigned to any known mutation\)\.

#### Cardinalities\.

We have analyzed our7878candidate pairs, see[Figure 6](https://arxiv.org/html/2607.12733#A2.F6), and observed three types of mutation sets in our experimental setup, see[Table 5](https://arxiv.org/html/2607.12733#A2.T5)\.

Table 5:Types of mutation pairs in[Figure 6](https://arxiv.org/html/2607.12733#A2.F6)\.TypeColours in[Figure 6](https://arxiv.org/html/2607.12733#A2.F6)CountAdmissible, additive \(used atk=2\+k=2^\{\+\}\)blueish green55Admissible, interacting \(used atk=2⊗k=2^\{\\otimes\}\)orange, red, purple9Total collapse \(uniform accept/reject\)0Subsumed by one of\{μi,μj\}\\\{\\mu\_\{i\},\\mu\_\{j\}\\\}light grey, dark grey14Total78![Refer to caption](https://arxiv.org/html/2607.12733v1/x7.png)Figure 6:Interaction scheme of mutations\.Subsumed mutations \(grey\) are determined by i\) indication of implementation ii\) indistinguishable behaviour fromk=1k=1mutations when facingΠSRA\\Pi\_\{\\texttt\{SRA\}\}\. All combinations that are coloured are valid\. Blueish green\(\+\)\(\+\)is the easiest type of combination: Both mutations are additive and do not interact\. ThereSRAproducesV=1V=1\. Two interacting types\(⊗\)\(\\otimes\)are observed in our setting: i\) Partial observability \(orange, red\)\.SRAidentifies only one mutation\. Combinations kernel behaviour is still distinguishable from all others\. ii\) Emergence \(purple, diamond\) where kernel shows a fully interacting behaviour\.

### B\.5Compound\-Mutation Sets

For our two test settings, Ladder and Benchmark, two different mutation families have been used\. The utilized families are listed and characterized in[Table 6](https://arxiv.org/html/2607.12733#A2.T6)\.

Table 6:Curated mutation sets used in the compound\-condition sessions\.OrderMutation SetLadderBenchmarkClassesk=0k=0∅\\emptyset✓Null baselinek=1k=1\{ID\_01\}✓def\_equality\{ID\_02\}✓✓binding\{ID\_03\}✓def\_equality\{ID\_04\}✓binding\{ID\_05\}✓free\_name\{ID\_06\}✓✓binding\{ID\_07\}✓✓def\_equality\{ID\_08\}✓✓binding\{ID\_09\}✓application\{ID\_10\}✓def\_equality\{ID\_11\}✓✓free\_name\{ID\_12\}✓universe\{ID\_13\}✓✓applicationk=2\+k=2^\{\+\}\{ID\_01,ID\_03\}✓def\_equality\{ID\_02,ID\_04\}✓binding\{ID\_02,ID\_06\}✓binding\{ID\_02,ID\_12\}✓universe×\\timesbinding\{ID\_03,ID\_10\}✓✓def\_equality\{ID\_04,ID\_09\}✓application×\\timesbinding\{ID\_06,ID\_09\}✓application×\\timesbinding\{ID\_06,ID\_10\}✓def\_equality×\\timesbinding\{ID\_07,ID\_13\}✓def\_equality×\\timesapplicationk=2⊗k=2^\{\\otimes\}\{ID\_04,ID\_06\}✓✓binding\{ID\_04,ID\_08\}✓binding\{ID\_09,ID\_10\}✓def\_equality×\\timesapplicationk=3\+k=3^\{\+\}\{ID\_01,ID\_03,ID\_10\}✓def\_equality\{ID\_02,ID\_03,ID\_06\}✓def\_equality×\\timesbinding\{ID\_07,ID\_09,ID\_12\}✓def\_equality×\\timesapplication×\\timesuniverse

## Appendix CDetailed Model\-by\-condition Tables

The Section[5](https://arxiv.org/html/2607.12733#S5)main text reports only the headline inline, e\. g\.[Table 1](https://arxiv.org/html/2607.12733#S4.T1)\. All other per\-model and per\-condition tables are collected here\. The wide tables are set on their own landscape pages\.

#### “Ladder”experiment\.

[Table 7](https://arxiv.org/html/2607.12733#A3.T7)marginalises over scaffold to expose the single vs\. double dissociation as well as the interacting difficulty\. Similarly,[Table 8](https://arxiv.org/html/2607.12733#A3.T8)summarizes the effect of hint levels in the system prompt per model\.[Table 9](https://arxiv.org/html/2607.12733#A3.T9)expands the over/under\-reporting breakdown atk=2k=2\.

Table 7:Per\-model comparison of single vs\. double vs\. interacting mutations\.Marginal accuracy by mutation countkkon the“Ladder”experiment: exact correctnessVV, kernel detectionVKV\_\{K\}, exact attributionVAV\_\{A\}, Jaccard partial creditVAJV\_\{A\}^\{J\}, conditional attribution correctnessVA\|VK=1V\_\{A\}\|V\_\{K\}=1, and ratio of used probesP/PmaxP/P\_\{\\text\{max\}\}\. Numbers are mean values over prompt levels and corresponding mutations sets\. Fork≥2k\\geq 2, superscripts indicate whether the mutations are additive\(\+\)\(\+\)or interacting\(⊗\)\(\\otimes\)\.ModelkknnVVVKV\_\{K\}VAV\_\{A\}VAJV\_\{A\}^\{J\}VA∣VKV\_\{A\}\\mid V\_\{K\}P/PmaxP/P\_\{\\text\{max\}\}ministral\-3b\-2512111950\.0770\.3690\.1900\.1900\.2080\.6162\+2^\{\+\}1050\.0000\.2950\.0000\.0940\.0000\.7272⊗2^\{\\otimes\}450\.0000\.2670\.0000\.0150\.0000\.775ministral\-8b\-2512111950\.0970\.2100\.2000\.2000\.4630\.9662\+2^\{\+\}1050\.0100\.2380\.0670\.1600\.0400\.9882⊗2^\{\\otimes\}450\.0000\.2000\.0000\.0740\.0000\.980ministral\-14b\-2512111950\.0720\.2720\.0820\.0850\.2640\.9992\+2^\{\+\}1050\.0100\.3520\.0190\.1220\.0271\.0002⊗2^\{\\otimes\}450\.0000\.3560\.0000\.0960\.0001\.000mistral\-large\-2512111950\.3490\.6000\.4510\.4510\.5810\.5732\+2^\{\+\}1050\.1330\.6380\.1710\.3630\.2090\.6192⊗2^\{\\otimes\}450\.0440\.8670\.0440\.2740\.0510\.550claude\-haiku\-4\-5111950\.4150\.7740\.4510\.4560\.5360\.7632\+2^\{\+\}1050\.1810\.7430\.2290\.3860\.2440\.8132⊗2^\{\\otimes\}450\.1330\.9110\.1330\.4040\.1460\.852gemini\-2\.5\-flash111950\.4410\.8770\.4460\.4590\.5030\.3782\+2^\{\+\}1050\.2950\.9050\.2950\.4710\.3260\.4702⊗2^\{\\otimes\}450\.1560\.9110\.1560\.3930\.1710\.427gemini\-2\.5\-pro111950\.4670\.9180\.4670\.4950\.5080\.3422\+2^\{\+\}1050\.2000\.9330\.2100\.3790\.2140\.4342⊗2^\{\\otimes\}450\.2000\.9560\.2000\.4300\.2090\.419gpt\-5\.4\-nano111950\.0820\.1740\.1330\.1330\.4710\.1532\+2^\{\+\}1050\.0000\.1240\.0000\.0830\.0000\.1702⊗2^\{\\otimes\}450\.0000\.2000\.0000\.0000\.0000\.152gpt\-5\.4\-mini111950\.2310\.5690\.3180\.3260\.4050\.3042\+2^\{\+\}1050\.0760\.5810\.1520\.2980\.1310\.3282⊗2^\{\\otimes\}450\.0220\.6220\.0220\.2110\.0360\.232gpt\-5\.4111950\.4720\.8510\.4720\.4870\.5540\.3102\+2^\{\+\}1050\.2670\.8480\.2670\.3860\.3150\.3482⊗2^\{\\otimes\}450\.1330\.9560\.1330\.3960\.1400\.325gpt\-5\.4\_low111950\.5490\.9330\.5490\.5740\.5880\.2652\+2^\{\+\}1050\.2670\.9140\.2670\.4210\.2920\.3472⊗2^\{\\otimes\}450\.1781\.0000\.1780\.4780\.1780\.295gpt\-5\.4\_medium111950\.5690\.9080\.5690\.5850\.6270\.3112\+2^\{\+\}1050\.3620\.9050\.3620\.5240\.4000\.4492⊗2^\{\\otimes\}450\.2891\.0000\.2890\.5070\.2890\.404gpt\-5\.4\_high111950\.6210\.9130\.6210\.6280\.6800\.3262\+2^\{\+\}1050\.2760\.8480\.2760\.4000\.3260\.4842⊗2^\{\\otimes\}450\.1780\.8890\.1780\.4190\.2000\.461Table 8:Per\-model comparison of scaffolding level\.Marginal accuracy by prompt level on the“Ladder”experiment: exact correctnessVV, kernel detectionVKV\_\{K\}, exact attributionVAV\_\{A\}, Jaccard partial creditVAJV\_\{A\}^\{J\}, conditional attribution correctnessVA\|VK=1V\_\{A\}\|V\_\{K\}=1, and ratio of used probesP/PmaxP/P\_\{\\text\{max\}\}\. Numbers are mean values over mutations sets\.ModelPromptnnVVVKV\_\{K\}VAV\_\{A\}VAJV\_\{A\}^\{J\}VA∣VKV\_\{A\}\\mid V\_\{K\}P/PmaxP/P\_\{\\text\{max\}\}ministral\-3b\-2512Level 01150\.1130\.4700\.2870\.3780\.2410\.206Level 11150\.0090\.2170\.0090\.0090\.0400\.874Level 21150\.0090\.3130\.0260\.0260\.0280\.932ministral\-8b\-2512Level 01150\.0780\.1740\.2870\.3360\.4500\.936Level 11150\.0350\.2960\.0430\.0780\.1180\.991Level 21150\.0610\.1830\.0700\.1000\.3330\.996ministral\-14b\-2512Level 01150\.0610\.3390\.0870\.1300\.1791\.000Level 11150\.0350\.1910\.0350\.0580\.1820\.998Level 21150\.0350\.3910\.0350\.1040\.0891\.000mistral\-large\-2512Level 01150\.4090\.7910\.5390\.6200\.5160\.331Level 11150\.1300\.4960\.1570\.2230\.2630\.749Level 21150\.1910\.6520\.2430\.3610\.2930\.672claude\-haiku\-4\-5Level 01150\.5480\.9390\.6090\.6780\.5830\.679Level 11150\.2520\.7220\.2610\.3390\.3490\.832Level 21150\.1220\.6870\.1570\.2670\.1770\.859gemini\-2\.5\-flashLevel 01150\.5390\.9570\.5390\.5830\.5640\.172Level 11150\.2780\.8960\.2870\.3590\.3110\.475Level 21150\.2610\.8170\.2610\.4200\.3190\.590gemini\-2\.5\-proLevel 01150\.5570\.9650\.5570\.5910\.5770\.161Level 11150\.3390\.9220\.3480\.4290\.3680\.458Level 21150\.1570\.8960\.1570\.3330\.1750\.520gpt\-5\.4\-nanoLevel 01150\.1130\.2090\.1910\.2140\.5420\.111Level 11150\.0090\.1390\.0090\.0610\.0620\.151Level 21150\.0170\.1390\.0260\.0260\.1250\.212gpt\-5\.4\-miniLevel 01150\.2700\.6870\.3830\.4700\.3920\.141Level 11150\.1130\.5480\.1830\.2460\.2060\.353Level 21150\.0870\.5040\.1220\.1910\.1720\.411gpt\-5\.4Level 01150\.6171\.0000\.6170\.6700\.6170\.176Level 11150\.2610\.7910\.2610\.3280\.3300\.371Level 21150\.2170\.8000\.2170\.3360\.2720\.424gpt\-5\.4\_lowLevel 01150\.5481\.0000\.5480\.6290\.5480\.174Level 11150\.4430\.9040\.4430\.5190\.4900\.346Level 21150\.2520\.9040\.2520\.3970\.2790\.362gpt\-5\.4\_mediumLevel 01150\.5911\.0000\.5910\.6670\.5910\.211Level 11150\.4430\.8960\.4430\.5040\.4950\.423Level 21150\.3740\.8610\.3740\.4970\.4340\.462gpt\-5\.4\_highLevel 01150\.6350\.9740\.6350\.6930\.6520\.231Level 11150\.4000\.8170\.4000\.4460\.4890\.446Level 21150\.3390\.8780\.3390\.4550\.3860\.497Table 9:Fault characterization fork=2k=2double mutation in the“Ladder”experiment\.Per\-model andkk\-hint level prompts, attribution modes are analyzed fornnsessions withVK=1V\_\{K\}=1\. Each entry shows the proportion of responses that were classified as correct, incomplete \(partially correct but missing mutations\), mixed \(partially correct but containing incorrect mutations\), or incorrect\. Proportions sum to one for each model and prompt\.<Pmax<P\_\{\\text\{max\}\}gives the proportion of sessions with probe budget NOT exhausted although incorrect mutation attributionVK=1∧VA=0V\_\{K\}=1\\land V\_\{A\}=0\.ModelPromptnnCorrectIncompleteMixedIncorrect<Pmax<P\_\{\\text\{max\}\}ministral\-3b\-2512Level 0\-1260\.0000\.1920\.1920\.6150\.731Level 2170\.0000\.0000\.0001\.0000\.118ministral\-8b\-2512Level 0\-1250\.0400\.0000\.6800\.2800\.208Level 290\.0000\.7780\.0000\.2220\.222ministral\-14b\-2512Level 0\-1290\.0340\.1380\.4830\.3450\.000Level 2240\.0000\.6250\.0000\.3750\.000mistral\-large\-2512Level 0\-1700\.2290\.0000\.6430\.1290\.926Level 2360\.0000\.7500\.0000\.2500\.917claude\-haiku\-4\-5Level 0\-1820\.3050\.0000\.5730\.1220\.965Level 2370\.0000\.5410\.1350\.3240\.946gemini\-2\.5\-flashLevel 0\-1920\.3590\.0000\.4350\.2070\.898Level 2440\.1140\.7050\.0230\.1590\.923gemini\-2\.5\-proLevel 0\-1930\.3230\.0000\.4300\.2470\.889Level 2480\.0000\.4790\.2080\.3120\.979gpt\-5\.4\-nanoLevel 0\-1120\.0000\.0000\.4170\.5831\.000Level 2100\.0000\.0000\.0001\.0001\.000gpt\-5\.4\-miniLevel 0\-1650\.1380\.0000\.5690\.2921\.000Level 2240\.0000\.2920\.0830\.6250\.958gpt\-5\.4Level 0\-1910\.3190\.0000\.4510\.2311\.000Level 2410\.1220\.3900\.1950\.2931\.000gpt\-5\.4\_lowLevel 0\-1960\.3230\.0000\.5520\.1251\.000Level 2450\.1110\.4440\.1110\.3331\.000gpt\-5\.4\_mediumLevel 0\-1950\.4320\.0000\.4840\.0840\.981Level 2450\.2220\.3780\.1780\.2220\.971gpt\-5\.4\_highLevel 0\-1850\.4000\.0000\.4240\.1760\.922Level 2440\.0680\.3860\.2270\.3180\.976OverallLevel 0–212850\.2160\.1630\.3700\.2510\.865
#### “Benchmark”experiment\.

[Table 10](https://arxiv.org/html/2607.12733#A3.T10)lists per\-model true\-negative rates and probing perseverance on thek=0k=0null condition\.LABEL:tab:full\_benckmarkgives the full per\-\(model, condition\) summary of detailed performance statistics for all benchmark configurations with fork∈\{1,2,3\}k\\in\\\{1,2,3\\\}\.

Table 10:k=0k=0null\-condition coverage in the“Benchmark”experiment\.Per\-model true\-negative rate \(specificity\), number of probes used, and utilization of probe budget\. Point estimates only are given because each per\-model cell isn=5n=5, too few for a useful interval\. Models are sorted as in[Figure 4](https://arxiv.org/html/2607.12733#S5.F4)\. The bottom row aggregates across all155155null sessions\.ModelnnTNFPSpecificityProbesBudget exhaustedministral\-3b\-25125140\.2065\.0magistral\-small\-25095230\.4028\.0ministral\-8b\-25125501\.0065\.0mistral\-medium\-25085501\.0065\.0ministral\-14b\-25125501\.0065\.0mistral\-small\-26035501\.0065\.0gemini\-2\.5\-pro5410\.8061\.0gpt\-5\.4\-nano5501\.006\.4gpt\-5\.4\-mini5501\.0015\.2gpt\-5\.4\_xhigh5230\.4027\.4mistral\-medium\-3\-55320\.6065\.0gemini\-2\.5\-flash5320\.6062\.8mistral\-large\-25125410\.8065\.0claude\-haiku\-4\-55501\.0063\.8gpt\-5\.45501\.0026\.6magistral\-medium\-25095501\.0039\.2gpt\-5\.4\_high5501\.0026\.0gpt\-5\.55501\.0033\.6gpt\-5\.4\_low5501\.0020\.4claude\-sonnet\-4\-65501\.0065\.0gpt\-5\.5\_low5501\.0028\.4gpt\-5\.4\_medium5501\.0022\.4gpt\-5\.5\_medium5501\.0041\.2gpt\-5\.5\_high5501\.0052\.4gpt\-5\.5\_xhigh5501\.0050\.0claude\-sonnet\-4\-6\_low5501\.0063\.2claude\-sonnet\-4\-6\_high5501\.0061\.0claude\-opus\-4\-7\_high5501\.0054\.0gemini\-3\.1\-pro\-preview5501\.0056\.2gemini\-3\.5\-flash5501\.0064\.0simple\_reflex\_agent5501\.0014\.0Overall155139160\.9046\.4Table 11:Summary statistics per model and experiment setting on“Benchmark”\.V is exact\-match correctness; VAJ is the Jaccard partial\-credit score on the mutation set\.kkconsists ofnnmutation sets\. Metrics are exact correctnessVV, kernel detectionVKV\_\{K\}, exact attributionVAV\_\{A\}, Jaccard partial creditVAJV\_\{A\}^\{J\}, conditional attribution correctnessVA\|VK=1V\_\{A\}\|V\_\{K\}=1, precision and recall of attribution, and probing efficiency respresented byEELXE\_\{\\text\{ELX\}\}, ratio of used probesP/PmaxP/P\_\{\\text\{max\}\}, and ratio of in probe budget\. Numbers are averaged values per model andkkacrossnnmutation sets\.ModelkknnVVVKV\_\{K\}VAV\_\{A\}VAJV\_\{A\}^\{J\}VA∣VKV\_\{A\}\\mid V\_\{K\}PrecisionA\\text\{Precision\}\_\{A\}RecallA\\text\{Recall\}\_\{A\}EELXE\_\{\\text\{ELX\}\}P/PmaxP/P\_\{\\text\{max\}\}<Pmax<P\_\{\\text\{max\}\}claude\-haiku\-4\-511300\.300\.970\.300\.330\.310\.330\.370\.370\.830\.902\+2^\{\+\}150\.000\.470\.000\.170\.000\.170\.170\.000\.790\.803\+3^\{\+\}150\.000\.870\.000\.220\.000\.220\.220\.000\.781\.002⊗2^\{\\otimes\}50\.201\.000\.200\.500\.200\.500\.500\.240\.881\.00claude\-sonnet\-4\-611300\.331\.000\.330\.530\.330\.530\.730\.331\.000\.002\+2^\{\+\}150\.330\.870\.330\.460\.380\.460\.470\.331\.000\.073\+3^\{\+\}150\.000\.800\.000\.410\.000\.410\.420\.001\.000\.072⊗2^\{\\otimes\}50\.401\.000\.400\.670\.400\.670\.700\.401\.000\.00claude\-sonnet\-4\-6\_low11300\.571\.000\.570\.620\.570\.620\.670\.780\.590\.932\+2^\{\+\}150\.330\.670\.330\.390\.500\.390\.400\.460\.770\.603\+3^\{\+\}150\.200\.870\.200\.460\.230\.460\.470\.280\.670\.872⊗2^\{\\otimes\}50\.001\.000\.000\.500\.000\.500\.500\.000\.691\.00claude\-sonnet\-4\-6\_high11300\.671\.000\.670\.720\.670\.720\.770\.910\.621\.002\+2^\{\+\}150\.330\.670\.330\.360\.500\.360\.370\.450\.720\.803\+3^\{\+\}150\.270\.870\.270\.570\.310\.570\.580\.370\.680\.872⊗2^\{\\otimes\}50\.001\.000\.000\.500\.000\.500\.500\.000\.601\.00claude\-opus\-4\-7\_high11300\.831\.000\.830\.830\.830\.830\.831\.210\.421\.002\+2^\{\+\}150\.270\.930\.270\.510\.290\.510\.570\.400\.451\.003\+3^\{\+\}150\.131\.000\.130\.510\.130\.510\.530\.200\.351\.002⊗2^\{\\otimes\}50\.001\.000\.000\.500\.000\.500\.500\.000\.681\.00gemini\-2\.5\-flash11300\.230\.930\.230\.260\.250\.260\.300\.330\.421\.002\+2^\{\+\}150\.000\.730\.000\.190\.000\.190\.200\.000\.431\.003\+3^\{\+\}150\.000\.730\.000\.200\.000\.200\.270\.000\.490\.932⊗2^\{\\otimes\}50\.200\.800\.200\.300\.250\.300\.300\.290\.411\.00gemini\-2\.5\-pro11300\.100\.970\.100\.190\.100\.190\.300\.150\.321\.002\+2^\{\+\}150\.000\.870\.000\.220\.000\.220\.270\.000\.371\.003\+3^\{\+\}150\.000\.930\.000\.390\.000\.390\.440\.000\.351\.002⊗2^\{\\otimes\}50\.201\.000\.200\.500\.200\.500\.500\.290\.251\.00gemini\-3\.1\-pro\-preview11300\.801\.000\.800\.800\.800\.800\.801\.100\.581\.002\+2^\{\+\}150\.331\.000\.330\.610\.330\.610\.670\.470\.601\.003\+3^\{\+\}150\.401\.000\.400\.640\.400\.640\.640\.590\.481\.002⊗2^\{\\otimes\}50\.001\.000\.000\.470\.000\.470\.500\.000\.611\.00gemini\-3\.5\-flash11300\.971\.000\.970\.970\.970\.970\.971\.360\.490\.902\+2^\{\+\}150\.400\.670\.400\.490\.600\.490\.530\.590\.601\.003\+3^\{\+\}150\.330\.730\.330\.470\.450\.470\.470\.500\.550\.872⊗2^\{\\otimes\}50\.001\.000\.000\.000\.000\.000\.000\.000\.441\.00gpt\-5\.411300\.301\.000\.300\.320\.300\.320\.330\.450\.171\.002\+2^\{\+\}150\.130\.670\.130\.230\.200\.230\.230\.200\.181\.003\+3^\{\+\}150\.000\.670\.000\.210\.000\.210\.220\.000\.201\.002⊗2^\{\\otimes\}50\.001\.000\.000\.300\.000\.300\.300\.000\.151\.00gpt\-5\.4\-mini11300\.100\.400\.100\.120\.250\.120\.130\.150\.171\.002\+2^\{\+\}150\.000\.400\.000\.230\.000\.230\.230\.000\.171\.003\+3^\{\+\}150\.000\.330\.000\.160\.000\.160\.160\.000\.161\.002⊗2^\{\\otimes\}50\.000\.200\.000\.000\.000\.000\.000\.000\.201\.00gpt\-5\.4\-nano11300\.070\.300\.070\.070\.220\.070\.070\.100\.091\.002\+2^\{\+\}150\.000\.330\.000\.100\.000\.100\.100\.000\.081\.003\+3^\{\+\}150\.000\.000\.000\.04nan0\.040\.040\.000\.101\.002⊗2^\{\\otimes\}50\.000\.000\.000\.00nan0\.000\.000\.000\.091\.00gpt\-5\.4\_low11300\.231\.000\.230\.330\.230\.330\.430\.350\.211\.002\+2^\{\+\}150\.130\.670\.130\.270\.200\.270\.370\.200\.231\.003\+3^\{\+\}150\.330\.730\.330\.420\.450\.420\.420\.500\.241\.002⊗2^\{\\otimes\}50\.001\.000\.000\.270\.000\.270\.300\.000\.181\.00gpt\-5\.4\_medium11300\.401\.000\.400\.480\.400\.480\.570\.590\.331\.002\+2^\{\+\}150\.000\.670\.000\.190\.000\.190\.330\.000\.311\.003\+3^\{\+\}150\.330\.730\.330\.410\.450\.410\.420\.500\.301\.002⊗2^\{\\otimes\}50\.001\.000\.000\.330\.000\.330\.400\.000\.381\.00gpt\-5\.4\_high11300\.270\.970\.270\.350\.280\.350\.430\.390\.421\.002\+2^\{\+\}150\.000\.730\.000\.220\.000\.220\.330\.000\.371\.003\+3^\{\+\}150\.330\.730\.330\.470\.450\.470\.470\.500\.341\.002⊗2^\{\\otimes\}50\.001\.000\.000\.400\.000\.400\.400\.000\.431\.00gpt\-5\.4\_xhigh11300\.100\.570\.100\.100\.180\.100\.100\.140\.281\.002\+2^\{\+\}150\.000\.470\.000\.070\.000\.070\.100\.000\.261\.003\+3^\{\+\}150\.270\.530\.270\.310\.500\.310\.310\.400\.281\.002⊗2^\{\\otimes\}50\.000\.200\.000\.000\.000\.000\.000\.000\.241\.00gpt\-5\.511300\.371\.000\.370\.400\.370\.400\.430\.550\.201\.002\+2^\{\+\}150\.130\.730\.130\.250\.180\.250\.270\.200\.251\.003\+3^\{\+\}150\.001\.000\.000\.180\.000\.180\.180\.000\.191\.002⊗2^\{\\otimes\}50\.001\.000\.000\.300\.000\.300\.300\.000\.211\.00gpt\-5\.5\_low11300\.301\.000\.300\.380\.300\.380\.470\.450\.221\.002\+2^\{\+\}150\.330\.670\.330\.370\.500\.370\.400\.500\.281\.003\+3^\{\+\}150\.130\.730\.130\.280\.180\.280\.310\.200\.261\.002⊗2^\{\\otimes\}50\.001\.000\.000\.100\.000\.100\.100\.000\.231\.00gpt\-5\.5\_medium11300\.431\.000\.430\.450\.430\.450\.470\.640\.361\.002\+2^\{\+\}150\.000\.730\.000\.280\.000\.280\.400\.000\.471\.003\+3^\{\+\}150\.330\.870\.330\.430\.380\.430\.440\.500\.361\.002⊗2^\{\\otimes\}50\.001\.000\.000\.400\.000\.400\.400\.000\.421\.00gpt\-5\.5\_high11300\.401\.000\.400\.400\.400\.400\.400\.590\.451\.002\+2^\{\+\}150\.330\.730\.330\.480\.450\.480\.530\.490\.571\.003\+3^\{\+\}150\.330\.870\.330\.490\.380\.490\.490\.500\.421\.002⊗2^\{\\otimes\}50\.001\.000\.000\.500\.000\.500\.500\.000\.421\.00gpt\-5\.5\_xhigh11300\.430\.900\.430\.450\.480\.450\.470\.610\.611\.002\+2^\{\+\}150\.400\.670\.400\.470\.600\.470\.470\.570\.641\.003\+3^\{\+\}150\.330\.670\.330\.380\.500\.380\.380\.500\.461\.002⊗2^\{\\otimes\}50\.001\.000\.000\.500\.000\.500\.500\.000\.531\.00magistral\-medium\-250911300\.300\.900\.300\.380\.330\.380\.470\.440\.411\.002\+2^\{\+\}150\.130\.800\.130\.320\.170\.320\.370\.190\.461\.003\+3^\{\+\}150\.000\.930\.000\.300\.000\.300\.360\.000\.361\.002⊗2^\{\\otimes\}50\.000\.800\.000\.270\.000\.270\.300\.000\.481\.00magistral\-small\-250911300\.070\.430\.100\.120\.150\.120\.130\.100\.260\.972\+2^\{\+\}150\.000\.870\.000\.210\.000\.210\.230\.000\.191\.003\+3^\{\+\}150\.000\.470\.000\.140\.000\.140\.180\.000\.300\.872⊗2^\{\\otimes\}50\.000\.800\.000\.070\.000\.070\.100\.000\.121\.00ministral\-3b\-251211300\.000\.400\.000\.000\.000\.000\.000\.000\.930\.102\+2^\{\+\}150\.000\.330\.000\.030\.000\.030\.030\.000\.940\.073\+3^\{\+\}150\.000\.470\.000\.000\.000\.000\.000\.001\.000\.002⊗2^\{\\otimes\}50\.000\.400\.000\.000\.000\.000\.000\.001\.000\.00ministral\-8b\-251211300\.000\.130\.030\.030\.000\.030\.030\.001\.000\.002\+2^\{\+\}150\.000\.000\.000\.00nan0\.000\.000\.000\.980\.073\+3^\{\+\}150\.000\.000\.000\.07nan0\.070\.070\.001\.000\.072⊗2^\{\\otimes\}50\.000\.000\.000\.00nan0\.000\.000\.001\.000\.00ministral\-14b\-251211300\.000\.170\.000\.000\.000\.000\.000\.001\.000\.002\+2^\{\+\}150\.000\.000\.000\.00nan0\.000\.000\.001\.000\.003\+3^\{\+\}150\.000\.330\.000\.090\.000\.090\.090\.001\.000\.002⊗2^\{\\otimes\}50\.000\.000\.000\.00nan0\.000\.000\.001\.000\.00mistral\-large\-251211300\.270\.630\.370\.370\.420\.370\.370\.370\.420\.932\+2^\{\+\}150\.000\.470\.000\.230\.000\.230\.230\.000\.380\.933\+3^\{\+\}150\.000\.530\.000\.130\.000\.130\.130\.000\.380\.802⊗2^\{\\otimes\}50\.000\.800\.000\.200\.000\.200\.200\.000\.410\.80mistral\-medium\-250811300\.000\.130\.000\.000\.000\.000\.000\.000\.980\.072\+2^\{\+\}150\.000\.130\.000\.030\.000\.030\.030\.000\.970\.133\+3^\{\+\}150\.000\.070\.000\.070\.000\.070\.070\.000\.890\.132⊗2^\{\\otimes\}50\.000\.000\.000\.00nan0\.000\.000\.001\.000\.00mistral\-medium\-3\-511300\.130\.670\.130\.160\.200\.160\.200\.160\.880\.432\+2^\{\+\}150\.070\.870\.070\.240\.080\.240\.300\.070\.800\.403\+3^\{\+\}150\.070\.730\.070\.340\.090\.340\.360\.090\.820\.532⊗2^\{\\otimes\}50\.000\.600\.000\.200\.000\.200\.200\.001\.000\.00mistral\-small\-260311300\.070\.470\.100\.140\.140\.140\.200\.080\.730\.572\+2^\{\+\}150\.000\.670\.000\.150\.000\.150\.170\.000\.570\.733\+3^\{\+\}150\.000\.600\.000\.180\.000\.180\.180\.000\.720\.472⊗2^\{\\otimes\}50\.000\.400\.000\.200\.000\.200\.200\.000\.820\.40simple\_reflex\_agent11301\.001\.001\.001\.001\.001\.001\.001\.500\.221\.002\+2^\{\+\}151\.001\.001\.001\.001\.001\.001\.001\.500\.221\.003\+3^\{\+\}151\.001\.001\.001\.001\.001\.001\.001\.500\.221\.002⊗2^\{\\otimes\}50\.001\.000\.000\.500\.000\.500\.500\.000\.221\.00Table 11:\(continued\)
#### Supporting figures\.

A visualization of the detection–attribution gap in the“Ladder”experiment is shown inLABEL:fig:ladder\_heatmap\_detail\. Impact of reasoning effort in the“Benchmark”experiment is shown inLABEL:fig:reasoning\_effort\.LABEL:fig:leaderboard\_detailedshows the detailed performance results as bar plots across the benchmark panel\. Thek=1→k=2k=1\\to k=2cliff is universal; cross\-family scaling helps atk=1k=1but flattens atk≥2k\\geq 2, where attribution becomes the binding constraint\. Probing behaviour of LLMs is shown inLABEL:fig:probing\_behaviorfor different success–failure modes\.

![[Uncaptioned image]](https://arxiv.org/html/2607.12733v1/x8.png)![[Uncaptioned image]](https://arxiv.org/html/2607.12733v1/x9.png)
![[Uncaptioned image]](https://arxiv.org/html/2607.12733v1/x10.png)

![[Uncaptioned image]](https://arxiv.org/html/2607.12733v1/x11.png)
![[Uncaptioned image]](https://arxiv.org/html/2607.12733v1/x12.png)
![[Uncaptioned image]](https://arxiv.org/html/2607.12733v1/x13.png)

![[Uncaptioned image]](https://arxiv.org/html/2607.12733v1/x14.png)

## Appendix DSystem prompts

The four prompt levels reported in Section[4](https://arxiv.org/html/2607.12733#S4)correspond to the following system prompts:

Level 0:ladder\_single\_split\_probeandladder\_double\_split\_probe, extending Level 1 with per\-class example probe templates\.

Level 1:ladder\_single\_splitfork=1k=1sessions andladder\_double\_splitfork=2k=2sessions; ontology\-aware,kk\-specific workflow\.

Level 2:ladder\_mix— a single forensic\-auditor prompt coveringk∈\{1,2\}k\\in\\\{1,2\\\}without splitting by mutation count\.

Level 3:stress\_test— the wide\-panel prompt \(k∈\{0,1,2,3\}k\\in\\\{0,1,2,3\\\},Pmax=65P\_\{\\max\}=65\); it omits the workflow and operating\-rules guidance and admits a clean kernel\.

We show the Level 1 \(k=1k=1\) prompt as the base and mark where each other level differs in unified\-diff style: a@@ Levelnn@@header introduces a hunk,green\+linesgive that level’s version \(Level 0’s per\-mutation example probes \(the concrete probes are redacted in this preprint\); Level 2’s unknown11–22mutation framing; Level 3’s wide\-panel rewordings\), andred\-linesmark omissions \(Level 3 drops the workflow and operating\-rules sections and usesPmax=65P\_\{\\max\}=65\)\. The\# Scoreblock quotes the canonical bonus coefficient12\\tfrac\{1\}\{2\}\(see \([1](https://arxiv.org/html/2607.12733#S3.E1)\)\); all scores are recomputed from the replay logs under the same formula\. Thek=2k=2\(double\) variants differ only in count and budget wording\.

\#Role

Youareaprecise,parsimoniousdiagnosticianofadependentlytypedlambda

calculus\(LambdaPi

Youaregivenaccesstotwoblack\-boxkernels,\`K\_A\`and\`K\_B\`,implementing

thesamesurfacelanguage\.Exactlyonekerneliscorrupted\.Thecorrupted

kernelcarriesexactlyonemutationdrawnfromthecatalogbelow\.

YourjobistoidentifywhichkernelisdamagedandwhichcatalogIDbest

@@Level2@@

\+kernelcarries1or2activemutationsdrawnfromthecatalogbelow\.Theymay

\+actindependently\(additively\)orinteractinwaysthatmodifytheircombined

\+effect\.

\+YourjobistoidentifywhichkernelisdamagedandwhichcatalogID\(s\)best

explaintheobservedbehavior\.

@@Level3@@

\+thesamesurfacelanguage\.Atmostonekerneliscorrupted\.Akernelis

\+corruptedifitsoutputdeviatesfromcorrectLambdaPisemantics\.Incaseofan

\+existingcorruptedkernel,thecorruptedkernelcarries1,2,or3activemutations

\+drawnfromthecatalogbelow\.

\+Yourjobistoidentifywhetheranykerneliscorrupted,whichoneitis,and

\+whichcatalogID\(s\)bestexplaintheobservedbehavior\.

Workonlyfrombehavior\.Donotassumeanyimplementationdetailsbeyondwhat

isobservablethroughtheinterface\.

\#Score\-maximiseE\_ELX

E\_ELX=V×\\times\(1\+0\.5×\\times\(1\-\(P/P\_max\)^3\)\),

with\`V=1\`ifthecorruptedkernelANDthemutation\_idarecorrectelse\`V=0\`,

@@Level2@@

\+with\`V=1\`ifthecorruptedkernelANDthefullmutation\_idsetarecorrectelse\`V=0\`,

P=totalprobesissued,\`P\_max=50\`maximumavailableprobebudget\.

Completeandexactcorrectnessismandatory\.Eachredundantprobestrictly

reducesscore;butfindingthecorruptedkernelandcorrectmutationor

excludingmutationcandidatesismuchmoreimportant\.

@@Level2@@

\+Completeandexactcorrectnessismandatory\.Submittingonlyasinglecorrect

\+mutation\_id,eventhoughtwoareactive,orviceversa,resultsin\`V=0\`\.

\+Two\-mutationcasesareaslikelyasone\-mutationcases\.Eachredundantprobe

\+strictlyreducesscore;butfindingthecorruptedkernelandcorrect

\+mutation\(s\)orexcludingmutationcandidatesismuchmoreimportant\.

@@Level3@@

\+with\`V=1\`ifthekernellabelANDthefullmutation\_idsetarecorrect\(empty

\+list\[\]whennokerneliscorrupted\)else\`V=0\`,P=totalprobesissued,

\+\`P\_max=65\`maximumavailableprobebudget\.

\+Completeandexactcorrectnessismandatory\.Submittingonlyasinglecorrect

\+mutation\_id,eventhoughtwoareactive,orviceversa,resultsin\`V=0\`\.

\+Eachredundantprobestrictlyreducesscore;butfindingthecorrectsolution

\+ismuchmoreimportant\.

\#Tools

\-\`probe\`

SendsoneLambdaPisourcestringtobothkernelsandreturnsbothoutputsplusadivergencesummary\.

\-\`list\_context\`

Showsthecurrentpersistentcontextifyouneedtoinspectpriorassumptions/definitions\.

\-\`budget\_left\`

Returnsremainingprobebudget\.Youstartwith50probesandmustsubmitwhenthebudgetdropsto0\.

@@Level3@@

\+Returnsremainingprobebudget\.Youstartwith65probesandmustsubmitwhenthebudgetdropsto0\.

\-\`submit\_answer\`

Finalsubmission\.

@@Level3@@

\-\(thislevelomitsthe"Mandatoryworkflowandoperationaldiagnosesstrategy"section\)

\#Mandatoryworkflowandoperationaldiagnosesstrategy

1\.Probebothkernelswithatargetedsourcestringdesignedtoexposeaspecificmutationclass\.

2\.Readtheresponse:lookat\`diff\`first;if\`identical\`or\`bothrejectwithsameerror\`,redesignbeforeprobingagain\.

3\.Ifconsecutiveprobesreturnnoinformative\`diff\`usethisinformationto

narrowcandidatesbyrulingoutmutationsthatwouldaffecttheprobe's

@@Level2@@

\+narrowcandidatesetbyrulingoutmutationsthatwouldaffecttheprobe's

mutationclass\.Donotsubmitwithoutobserveddivergence\-\-\-absenceof

divergencebasedonyourcurrentprobescaneithermeanyourprobesare

wrong,notthatnomutationexists\.

4\.Onceyouseedivergence,confirmwhichkerneliscorrupted\.Thekernelwhose

outputdeviatesfromcorrectLambdaPisemanticsisthecorruptedone\.

5\.Narrowitdowntomutationcandidates,ruleoutalternatives,andidentify

exactmutationbydesigninghypothesis/mutationcandidatespecific

probes,notjustfindingthemostlikelymutation\.

@@Level2@@

\+exactmutation\(s\)bydesigninghypothesis/mutationcandidatespecific

\+probes,notjustfindingthemostlikelymutation\(s\)\.

6\.Submitonlyafterthesolutionhasbeenuniquelydetermined\(i\.e\.corrupted

kernelandmutationIDaredeterminedwhileallotherhypotheseshavebeen

@@Level2@@

\+kernelandmutationsetaredeterminedwhileallotherhypotheseshavebeen

excluded\)\.

@@Level3@@

\-\(thislevelomitsthe"Operatingrules"section\)

\#Operatingrules

\-Aclaimedmutationmustbesupportedbyatleastonediscriminatingprobe\.

@@Level2@@

\+\-Everyclaimedmutationmustbesupportedbyatleastonediscriminatingprobe\.

\+\-Whenclaimingtwomutations,eachmustbeindependentlyevidencedbya

\+probedesignedforitsspecificmutationclasswheretheothermutation

\+isnottheprimarycause\.Donotassumeoneanomalyexplainseverything\.

\-Neverrepeatanuninformativeprobe\.

\-Distinguishrejectionfromwrongevaluation\.Bothmatter\.

\-Ifbudgetdropstozero,whiletwohypothesescontinuetobeequallysupported,submitthebetter\-evidencedoneanddocumenttheunresolvedambiguityandtheseparatingprobethatwouldresolveit\.

@@Level2@@

\+\-Donotassumemoremutationsthantheevidencerequires,butactivelytestforasecondmutationbeforesubmitting\.

@@Level3@@

\+Identifythecorruptedkernelandactivemutations\.Submityouranswer\.

\#Benchmarklanguage

Statepersistsacrossprobes\.Youstartwithafreshstatewhendiagnosis

begins\.Onlyvalid\`assume\`and\`let\`statementswithouterrorareretained\.

AssumeordinaryLambdaPibehaviorunlessaprobeshowsotherwiseextendedbyauniversehierarchy\.

Aprobeconsistsofanynumberof\`assume\`/\`let\`linesfollowedbyexactlyonefinal\`eval\`line\.

Eachstatementhastobeinasinglelineseparatedby"\\n"\.";"isnotallowed\.

\#\#Statements

assumex:Tdeclareafreevariable

assumexy:Tdeclaremultiplevariablesofthesametype

letname=exprdefinevariable

letname:Type=exprdefinevariablewithexplicittypeannotation

evaltermevaluateandtype\-check

evalterm:typeevaluatewithexplicittypeannotation

\#\#Terms

\\x\-\>bodylambdaabstraction\(backslash\)

forall\(x:A\)\.Bdependentproduct\(Pitype\)

A\-\>Bnon\-dependentfunctiontype

fabapplicationbyjuxtaposition

term:TypeExprannotation

Type,Type0,Type1,\.\.\.universeshierarchy

\#\#Built\-ins

Natnaturalnumbertype

Zerozero\(Zero:Nat\)

Succnsuccessor\(SuccZero:Nat\)

NatElimmotivebasestepnrecursoroverNat

VecAnlength\-indexedvectortype

NilA/ConsAnhtempty/consvectors

VecElimvectoreliminator

EqAxypropositionalequalitytype

ReflAxreflexivityproof\(ReflNatZero:EqNatZeroZero\)

EqElimAmrcxypJeliminator

\#\#Readingprobeoutput

EachprobereturnsaJSONobjectwithfieldsforeachkernelK\_AandK\_B:

sigma"accept"\-kernelacceptedtheterm;outputisin\`result\`

"reject"\-kernelrejectedit;errormessageisin\`epsilon\`

resultThepretty\-printedvalue/normalformandtype,e\.g\."Zero:Nat"

epsilonNormalisederrorstring\(paths/linenumbersstripped\)

diffSummaryofdivergence:

"identical"\-nodivergence,probeuninformative

"resultdivergence:A=\.\.\.,B=\.\.\."\-evaluationdiffers

"sigmadivergence:A=accept,B=reject"\-oneaccepts,onerejects

"errordivergence:A=\.\.\.,B=\.\.\."\-bothrejectbutwithdifferenterrors

@@Level3@@

\+Note:sigmadivergence\(oneaccepts,onerejects\)isasdiagnosticallymeaningfulasresult

\+divergence\.Aprobewherebothkernelsproduceidenticaloutputorbothrejectwithsameerror

\+providesnoevidencefororagainstanymutation\-\-\-itneitherconfirmsnorrulesoutacorrupted

\+kernel\.

\#\#Candidatemutations

Onemutationisactive\.Eachmutationcandidatesuggestsadifferentprobing

strategy\.Treatthedescriptionsbelowassemanticmutationmodels,notas

implementationhints\.Symptomsofmutations,evenacrosscategories,mayappear

identicalonshallowprobes;IDswithsimilarsymptomsoftenrequireatargeted

deeperprobetodistinguish\.

@@Level0@@

\+Foreachmutation,thereisaprobeprovided,thatisguaranteedtoproduce

\+divergenceifthatmutationisactive,andwhosespecificoutputpair

\+\(corruptedkernelresultvs\.correctkernelresult\)uniquelyidentifiesthat

\+mutationamongallcandidates\.

@@Level2@@

\+1or2mutationsareactive\.Eachmutationcandidatesuggestsadifferent

\+probingstrategy\.Treatthedescriptionsbelowassemanticmutationmodels,

\+notasimplementationhints\.Symptomsofmutations,evenacrosscategories,

\+mayappearidenticalonshallowprobes;IDswithsimilarsymptomsoftenrequire

\+atargeteddeeperprobetodistinguish\.

\+Symptomsmaybemisleading\-\-\-whatappearstobeonemutationcouldactuallybe

\+theresultoftwomutationsinteractingwitheachother,andviceversa\.

@@Level3@@

\+0,1,2,or3mutationsareactive\.Eachmutationcandidatesuggestsadifferent

\+probingstrategy\.Treatthedescriptionsbelowassemanticmutationmodels,

\+notasimplementationhints\.

ID\_01\-\-\-Neutralapplicationsignoretheirargumentsindefinitionalequality

Symptom:Typesindexedby\`fa\`and\`fb\`maycompareequalwhenevertheheadisthesame,even

thoughtheargumentsdiffer\.

@@Level0@@

\+Uniqueprobe:<redactedforpreprint\>

ID\_02\-\-\-Failtoincrementthetargetindexunderlambda

Symptom:Substitutioncrossesabinderincorrectly\.Substitutionintoalambdabodymaycontinue

targetingtheoldbindingdepthinsteadofshiftingtoaccountforthenewlyintroducedvariable\.

Avariableintendedforanouterbindercanincorrectlyreplaceaninnerone\.

@@Level0@@

\+Uniqueprobe:<redactedforpreprint\>

ID\_03\-\-\-Definitionalequalityignoreswhichbinderavariablerefersto

Symptom:Termsortypesthatdifferonlybywhichnearbybinderisreferencedcanbetreatedas

equal\.

@@Level0@@

\+Uniqueprobe:<redactedforpreprint\>

ID\_04\-\-\-Indexdriftinboundlookup

Symptom:Bound\-variablelookupusesthewrongselectionundernestedbinding\.Inatermwith

multiplebinders,afunctionmayreturnorusethewrongboundvariable\.Multi\-argumentfunctions

canbehaveasifonereferencepointstoanearbyouterbinderinsteadoftheintendedone\.

@@Level0@@

\+Uniqueprobe:<redactedforpreprint\>

ID\_05\-\-\-Unknownnamesbehavelikeafixedcanonicalconstant

Symptom:Afreenamethatshouldremainwithnodefinitioninsteadcollapsescomputationstoward

aconstantvalue\.Expressionsheadedbyanunknownnamenormalizefurtherthantheyshould\.

@@Level0@@

\+Uniqueprobe:<redactedforpreprint\>

ID\_06\-\-\-Nestedfunctionsmixupinnerandouterarguments

Symptom:Single\-argumentfunctionsmaylookfine,butfunctionsreturningfunctionscanswapthe

rolesofinnerandouterboundvalues\.

@@Level0@@

\+Uniqueprobe:<redactedforpreprint\>

ID\_07\-\-\-Definitionalequalityinthecontextwheretypesarebeingcompared

@@Level3@@

\+ID\_07\-\-\-Definitionalequalitybypassduringtypecomparison

Symptom:Typecheckingacceptstermsbecausestructurallydifferentexpressionswhichthetype

canbereadoffaretreatedasdefinitionallyequalevenwhentheyshouldnotbe\.

@@Level0@@

\+Uniqueprobe:<redactedforpreprint\>

ID\_08\-\-\-Functionbodiescanseeaspuriousextravalue

Symptom:Underlambdaapplication,someboundreferencesbehaveasifanextraunrelatedvalue

hasappearedinscope\.Resultsmaycontainadefault\-likeorneutral\-lookingtermwhereagenuine

argumentorcapturedvalueshouldhavebeenused\.

@@Level0@@

\+Uniqueprobe:<redactedforpreprint\>

ID\_09\-\-\-Functionapplicationrepeatsself\-feeding

Symptom:Asingleapplicationcancontinuebyfeedingthesameargumentinagain\.Termsmay

reduceonesteptoofar,asifthefirstresultwereappliedagaintotheoriginalargument\.

@@Level0@@

\+Uniqueprobe:<redactedforpreprint\>

ID\_10\-\-\-Distinctfreeheadscomparedefinitionallyequal

Symptom:Twodependenttypesindexedbydifferentfreevariablesmaybetreatedas

interchangeablemerelybecausebothheadsareunresolvednames\.

@@Level0@@

\+Uniqueprobe:<redactedforpreprint\>

ID\_11\-\-\-Unknownnamesbehavelikeidentity

Symptom:Applyinganunknownnametoanargumentreturnsthatargument,asifthemissinghead

wereanidentityfunction\.Applicationswithnodefinitionsimplifywhentheyshouldremain

neutral\.

@@Level0@@

\+Uniqueprobe:<redactedforpreprint\>

ID\_12\-\-\-Universestratificationcollapses

Symptom:Universetypingistoopermissive\.Universesbecomeself\-typedinsteadofstratified\.

Auniversemaybeacceptedatitsownlevelinsteadofonlyatahigherone\.Thesystembehaves

asthough\`Typen:Typen\`insteadof\`Typen\+1\`\.

@@Level0@@

\+Uniqueprobe:<redactedforpreprint\>

ID\_13\-\-\-Functionapplicationignoresitsargument

Symptom:Applyingafunctioncanproducearesultthatdoesnotdependonthesuppliedargument

evenwhenitobviouslyshould\.

@@Level0@@

\+Uniqueprobe:<redactedforpreprint\>

\#\#Submissionformat

Call\`submit\_answer\`with:

corrupted\_kernel"A"or"B"\-\-\-thekernelwhoseoutputdeviatesfromcorrectLambdaPisemantics\.

mutation\_idslistofoneID,e\.g\.\["ID\_03"\],thatbestexplainstheobservedbehavior\.

@@Level2@@

\+mutation\_idslistofoneortwoIDs,e\.g\.\["ID\_02"\]or\["ID\_01","ID\_03"\],thatbestexplaintheobservedbehavior\.

@@Level3@@

\+corrupted\_kernel"A"or"B"\-\-\-thekernelwhoseoutputdeviatesfromcorrectLambdaPisemantics,or"neither"

\+mutation\_idslistofone,two,orthreeIDs,e\.g\.\["ID\_02"\],\["ID\_01","ID\_03"\],or\["ID\_01","ID\_03","ID\_12"\],thatbestexplaintheobservedbehavior\.Ifnokerneliscorrupted,submitanemptylist\.

justificationconciseprobe\-basedargumentnamingwhichkernelproducedwhichbehavior\.

@@Level2@@

\+Ifacombinedmutationeffectproducesasymptomthatisnotindividuallydescribed

\+byeitherID,notethisinjustification\.

minimal\_probeTheSHORTESTsourcestringinwhichyouobserveddivergence\.

@@Level3@@

\+Provideevidenceforeveryclaimedmutation\.

\+minimal\_probeTheSHORTESTsourcestringinwhichyouobserveddivergence\.Ifnodivergencewasobserved,submittheshortestprobe\.

explanatory\_probeCiteasecondprobeyoualreadyranthatconfirmsthe

semanticconsequence\-e\.g\.acomputationthatgivesa

provablywrongansweronthecorruptedkernel\.

## Appendix EFailure Case Traces

We provide three annotated failure traces from thek=2k=2Level 2 \(double\_mix\) condition, each showing the same canonical failure mode reported in Section[5](https://arxiv.org/html/2607.12733#S5): the agent correctly identifies the corrupted kernel, but submits only one of the two active mutations\. Traces were selected byanalysis/pick\_failure\_traces\.pyfromresults\_260520/records\.csvsubject to \(V=0V=0,VK=1V\_\{K\}=1,kground truth=2k\_\{\\text\{ground truth\}\}=2,ksubmission=1k\_\{\\text\{submission\}\}=1\); one is drawn per model family\.

#### gpt\-5\.4 — under\-reporting atk=2k=2\.

- •Ground truth:corrupted kernelKBK\_\{B\}, mutations\{\\\{ID\_01, ID\_03\}\\\}\.
- •Submission:corrupted kernelKBK\_\{B\}, mutations\{\\\{ID\_01\}\\\}after 28 probes\.

First 8 probes \(source⇒\\Rightarrowdivergence\):

\[1\]evalType0:Type0

=\>bothrejectwithsameerror

\[2\]assumeA:Type\\nassumexy:A\\neval\(\\z\-\>z\)x:A

=\>bothrejectwithsameerror

\[3\]assumeA:Type\\nassumex:A\\neval\(\(\\z\-\>z\):A\-\>A\)x

=\>identical

\[4\]assumeA:Type\\nassumexy:A\\neval\(\(\(\\u\-\>\\v\-\>u\):A\-\>A\-\>A\)x\)y

=\>identical

\[5\]assumeA:Type\\nassumexy:A\\neval\(\(\(\\u\-\>\\v\-\>v\):A\-\>A\-\>A\)x\)y

=\>identical

\[6\]assumeA:Type\\nassumexy:A\\neval\(\(\(\\u\-\>\\v\-\>uv\):\(A\-\>A\)\-\>A\-\>A\)\(\\w\-\>w:A\-\>A\)\)x

=\>bothrejectwithsameerror

\[7\]assumeA:Type\\nassumef:A\-\>A\\nassumex:A\\nevalfx

=\>identical

\[8\]assumeA:Type\\nassumexy:A\\neval\(\(\(\\u\-\>\\v\-\>u\):A\-\>A\-\>A\)y\)x:A

=\>identical

#### claude\-haiku\-4\-5 — under\-reporting atk=2k=2\.

- •Ground truth:corrupted kernelKBK\_\{B\}, mutations\{\\\{ID\_02, ID\_06\}\\\}\.
- •Submission:corrupted kernelKBK\_\{B\}, mutations\{\\\{ID\_02\}\\\}after 40 probes\.

First 8 probes \(source⇒\\Rightarrowdivergence\):

\[1\]evalZero:Nat

=\>identical

\[2\]evalSuccZero:Nat

=\>identical

\[3\]assumef:Nat\-\>Nat\\nassumex:Nat\\nevalfx

=\>identical

\[4\]assumef:Nat\-\>Nat\-\>Nat\\nassumexy:Nat\\nevalfxy

=\>identical

\[5\]eval\\x\-\>x:Nat\-\>Nat

=\>bothrejectwithsameerror

\[6\]eval\(\\x\-\>x\):Nat\-\>Nat

=\>identical

\[7\]eval\(\(\\x\-\>x\)Zero\):Nat

=\>bothrejectwithsameerror

\[8\]eval\(\(\(\\x\-\>x\):Nat\-\>Nat\)Zero\)

=\>identical

#### gemini\-2\.5\-flash — under\-reporting atk=2k=2\.

- •Ground truth:corrupted kernelKAK\_\{A\}, mutations\{\\\{ID\_02, ID\_08\}\\\}\.
- •Submission:corrupted kernelKAK\_\{A\}, mutations\{\\\{ID\_02\}\\\}after 17 probes\.

First 8 probes \(source⇒\\Rightarrowdivergence\):

\[1\]evalNat

=\>identical

\[2\]evalZero:Nat

=\>identical

\[3\]eval\\x:Nat\-\>x:Nat\-\>Nat

=\>bothrejectwithsameerror

\[4\]eval\\x:Nat\-\>x

=\>bothrejectwithsameerror

\[5\]evalNat\-\>Nat

=\>identical

\[6\]eval\\x\-\>x:Nat\-\>Nat

=\>bothrejectwithsameerror

\[7\]eval\(\\x\-\>x\):Nat\-\>Nat

=\>identical

\[8\]evalType0:Type0

=\>bothrejectwithsameerror

#### Reading the traces\.

In each session the divergence signal is observable within the first44–88probes, but the agent commits to a single salient mutation and either stops or spends the remaining budget hunting for additional evidence that confirms its first hypothesis rather than testing it\. This is the empirical correlate of the single\-mutation bias discussed in Section[6](https://arxiv.org/html/2607.12733#S6): the model finds*a*consistent explanation, not the*complete*one\.