arXiv CSopen access

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 Julius Steiglechner∗2,1 , Lucas Mahler∗1 , and Gabriele Lohmann†1 1

Max-Planck-Institute for Biological Cybernetics, Magnetic Resonance Center, Tübingen, Germany 2 Dept. of Biomedical Magnetic Resonance, University Hospital Tübingen, Tübingen, Germany

arXiv:2607.12733v1 [cs.AI] 14 Jul 2026

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 introduce Elenchos (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 λ-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.

1

Introduction

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. ∗ †

These authors contributed equally. Corresponding author: [email protected]

1

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 [2]. 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 λ-calculus kernel [17, 35, 14]. 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, 26]. This may help reduce reliance on representation-specific heuristics and probe whether performance generalizes beyond λ-calculus-structured inputs.

2

Related 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 [25, 15, 22], graduate-level knowledge [45, 11, 1], and broad capability suites [24, 38, 9] are increasingly saturated for frontier models [2, 51]. This has raised concerns that reported gains partly reflect contamination or memorization rather than invariant reasoning ability [6, 36, 12, 16]. Two complementary responses are particularly relevant: dynamic benchmark generation, which replaces static datasets with procedurally defined distributions to reduce leakage [56], and robustness analyses showing sharp performance degradation under semantics-preserving perturbations. For instance, GSM-Symbolic reports up to a 65% drop in accuracy under prompt perturbations [39]. 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, 61, 20, 57, 46, 27, 65, 64]. In parallel, verification efforts aim to establish the correctness of such kernels themselves, e.g., via certified type checkers in MetaCoq [49, 50] or Lean4Lean for Lean [10]. 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], Altenkirch–Kaposi [3], and smalltt [30]. Mutation testing, fault localization, and abduction. Methodologically, Elenchos builds on differential, mutation, and metamorphic testing traditions [37, 62, 31, 28, 13], which have recently been adapted to evaluate LLMs in software engineering settings [19, 53, 55, 32, 23, 44]. In contrast to these approaches, which primarily assess model robustness or debugging performance 2

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], 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, 29, 59, 58, 60], 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 [8, 5, 47, 4], 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], the xz/liblzma backdoor incident [21], and large-scale failures such as the CrowdStrike kernel-driver outage [18] 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] established intermediate reasoning steps as a first-class object in LLM evaluation, and the subsequent reasoning-trace literature [63, 33] 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] (under perturbation), [7] (memorization critique), and [12, 16] (cognitive interpretation) argue, in different registers, that headline scores can mask shallow pattern reuse. Recent work on reasoning robustness under input perturbation [39, 40] and under software evolution [23, 44] reaches a consistent conclusion: model performance is fragile under controlled changes that preserve task semantics. Our results in Section 5 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.

3

The 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 la-

3

agent

identified?

yes

submission

no next probe

KA

KB OB

OA

Figure 1: The Elenchos audit loop. At each iteration, the agent submits a probe to two blackbox kernels, KA and KB , one of which may be corrupted. The kernels return diagnostic tuples, OA and OB , that summarize how the probe was processed. These tuples constitute the agent’s observations (see Section 4 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. tent 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 λ-calculus kernel detailed in Section 4, the general environment is formalized as follows: Definition 1 (Kernel). A kernel K is a deterministic black-box function K : T → O, where T denotes the space of probes containing all admissible syntactic terms, and O represents the space of observable outputs. Let K denote the set of all such kernels, including the reference kernel Kref 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 blackbox 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 µ is a transformation over kernels, µ : K → K, that modifies the underlying latent rule structure of a kernel. The mutation ontology is defined as the finite set of these primary operators: M = {µ1 , . . . , µn }. For any mutation configuration set S ⊆ M, we define KS ∈ K as the kernel obtained by applying the mutations in S to the reference kernel Kref under a fixed composition policy. Composite mutations. Mutations may interact non-linearly, meaning the behavior of a composite configuration KS 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 4

restrict the evaluation space to a valid configuration family F ⊆ P(M) satisfying a global identifiability condition: for S ∈ F, the mapping S 7→ KS is injective over F , ensuring that each induced kernel uniquely determines its underlying mutation configuration in principle. Elements of P(M) violating this identifiability condition are excluded from F . Let k = |S| denote the number of active mutations. For k ≥ 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 ∅∈F

and {µ} ∈ F,

∀µ ∈ M.

The audit loop. During a session, Elenchos evaluates abductive reasoning as an interactive diagnosis problem (Figure 1). Each instance consists of two kernels (KA , KB ) 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 τ ∈ T and observing outputs (OA , OB ). 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 budget Pmax is exhausted. Evaluation metrics. Kernel identification VK is correct if the predicted and true kernel labels match. Mutation attribution VA is correct if the predicted and true mutation sets are identical, i.e., if all mutations have been correctly identified. After each session, a score V ∈ {0, 1} is returned with V = 1 if both kernel identification and mutation attribution are correct, and V = 0 otherwise. 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 metric EELX ∈ [0, 1.5] that rewards efficiency with a bonus multiplier. It is defined as  3 !! 1 P EELX (V, P ) = V 1 + 1− . (1) 2 Pmax 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 budget Pmax . 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 configuration S ∈ 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], where hypotheses are generated to explain observed phenomena rather than derived from axioms or learned from labeled instances. 5

4

Implementation

Dependently typed λ-calculus. Here we briefly review the core features of the dependently typed λ-calculus used in Elenchos, see also Supplementary Material A. The set of terms T (which encompasses both expressions and types) is defined by the grammar: T ::= x | Type | λx : A.M | M N | Πx : A.B,

(2)

where x denotes a variable, Type represents the universe of types, λx : A.M is a function abstraction with domain type A, M N is a function application, and Πx : A.B is a dependent function type where the result type B may depend on the argument x. Computation proceeds via β-reduction, (λx : A.M ) N −→β M [x 7→ N ],

(3)

with M [x 7→ N ] denoting the capture-avoiding substitution of N for x in M . A term is in β-normal form when no further reductions are possible. Operationally, a λ-calculus kernel acts as a deterministic type checker, validating terms against a typing context Γ that tracks variable assignments. Kernel architecture. We instantiate Elenchos using LambdaPy, a Python-based implementation of a dependently typed λ-calculus kernel adapted from [34]. 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. 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 β-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 by LambdaPy. 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 Material E. Mutation framework. We use a curated ontology of 13 singleton mutations (see Supplementary Material B, especially Table 3). We build the corresponding valid configuration family Fk for k ≤ 3 according to Supplementary Material B.3 and identified additive (+) and interacting (⊗), see Supplementary Figure 6. 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. Rather than modifying kernel source code, mutations are implemented as configurationlevel 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 current LambdaPy context, and submitting an answer. But to prevent benchmark contamination and search-based solutions, web search and code execution 6

Table 1: Detection–attribution dissociation on the “Ladder” experiment, averaged over k ∈ {1, 2} and the three prompt levels (Levels 0–2), with models grouped by family. VK denotes kernel-correct detection; VA denotes exact mutation-set attribution; and VA | VK = 1 denotes exact attribution conditioned on correct kernel detection. Cells display mean point estimates with asymmetric Wilson 95 % confidence intervals in brackets; the Gap column reports VK − VA with paired bootstrap 95 % confidence intervals. Model

VK

VA

VA | VK = 1

Gap (pp)

ministral-3b-2512 ministral-8b-2512 ministral-14b-2512 mistral-large-2512 claude-haiku-4-5 gemini-2.5-flash gemini-2.5-pro gpt-5.4-nano gpt-5.4-mini gpt-5.4 gpt-5.4_low gpt-5.4_medium gpt-5.4_high

0.33 [0.29, 0.38] 0.22 [0.18, 0.26] 0.31 [0.26, 0.36] 0.65 [0.59, 0.69] 0.78 [0.74, 0.82] 0.89 [0.85, 0.92] 0.93 [0.90, 0.95] 0.16 [0.13, 0.20] 0.58 [0.53, 0.63] 0.86 [0.82, 0.90] 0.94 [0.91, 0.96] 0.92 [0.89, 0.94] 0.89 [0.85, 0.92]

0.11 [0.08, 0.14] 0.13 [0.10, 0.17] 0.05 [0.03, 0.08] 0.31 [0.27, 0.36] 0.34 [0.29, 0.39] 0.36 [0.31, 0.41] 0.35 [0.31, 0.41] 0.08 [0.05, 0.11] 0.23 [0.19, 0.28] 0.37 [0.32, 0.42] 0.41 [0.36, 0.47] 0.47 [0.42, 0.52] 0.46 [0.41, 0.51]

0.13 [0.08, 0.20] 0.27 [0.18, 0.38] 0.14 [0.09, 0.22] 0.38 [0.32, 0.44] 0.39 [0.34, 0.45] 0.40 [0.35, 0.46] 0.38 [0.33, 0.43] 0.29 [0.18, 0.41] 0.27 [0.21, 0.34] 0.42 [0.37, 0.48] 0.44 [0.39, 0.50] 0.51 [0.46, 0.57] 0.51 [0.46, 0.57]

0.23 [0.17, 0.28] 0.08 [0.03, 0.13] 0.26 [0.21, 0.30] 0.33 [0.27, 0.40] 0.44 [0.38, 0.50] 0.53 [0.47, 0.58] 0.57 [0.52, 0.63] 0.09 [0.05, 0.12] 0.35 [0.28, 0.41] 0.50 [0.45, 0.55] 0.52 [0.47, 0.57] 0.45 [0.40, 0.50] 0.43 [0.38, 0.48]

Overall

0.65 [0.64, 0.66]

0.28 [0.27, 0.30]

0.39 [0.37, 0.41]

0.37 [0.35, 0.38]

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) 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 Material D. • Level 0. The system prompt includes a curated set of canonical example probes for each of the 13 mutations.1 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 cardinality k of the active mutation set. • Level 1. The system prompt provides the exact cardinality k of the active mutation set, but omits the canonical example probes. • Level 2. The system prompt informs the agent that there are k ≤ 2 active mutations, but does not provide the exact value of k. • Level 3. The system prompt only informs the agent that there are at most three active mutations (k ∈ {0, 1, 2, 3}), and does not provide workflow guidance or hints anymore. 1

The list of constructed probes ΠRSA and expected output of Kref and KS can be provided on request.

7

0.78

0.52

0.55

0.49

0.26

0.09

0.33

0.20

0.00

GPT-5.4 (Medium)

0.71

0.49

0.51

0.49

0.40

0.20

0.33

0.33

0.20

GPT-5.4 (Low)

0.72

0.55

0.37

0.31

0.34

0.14

0.33

0.20

0.00

GPT-5.4

0.74

0.37

0.31

0.54

0.14

0.11

0.27

0.07

0.07

GPT-5.4 Mini

0.35

0.18

0.15

0.23

0.00

0.00

0.00

0.07

0.00

GPT-5.4 Nano

0.20

0.02

0.03

0.00

0.00

0.00

0.00

0.00

0.00

Gemini 2.5 Pro

0.62

0.51

0.28

0.54

0.06

0.00

0.33

0.27

0.00

Gemini 2.5 Flash

0.62

0.32

0.38

0.49

0.26

0.14

0.33

0.13

0.00

Claude Haiku 4.5

0.72

0.31

0.22

0.34

0.20

0.00

0.27

0.13

0.00

Mistral Large 3

0.52

0.18

0.34

0.31

0.09

0.00

0.13

0.00

0.00

Ministral 3 14B

0.09

0.06

0.06

0.03

0.00

0.00

0.00

0.00

0.00

Ministral 3 8B

0.14

0.05

0.11

0.00

0.03

0.00

0.00

0.00

0.00

Ministral 3 3B

0.20

0.02

0.02

0.00

0.00

0.00

0.00

0.00

0.00

0 vel

1 vel

2 vel

0 vel

1 vel

2 vel

0 vel

1 vel

2 vel

Model family Mistral Claude Google OpenAI

Le

Le

k=1

Le

Le

Le

Le

k = 2+

Le

Experiment type (harder )

Le

0.8 0.7 0.6 0.5 0.4

V

Intra family capability (higher )

GPT-5.4 (High)

0.3 0.2 0.1 0.0

Le

k=2

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), and non-additive mutation interactions (+ → ⊗). The reported metric is the averaged exact-match accuracy (V ) across mutation sets, which requires correct identification of whether either kernel is corrupted and, when applicable, the precise attribution of all active mutations.

5

Experiments 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 mutations k affect 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 mutations k ≤ 3) to establish a comparative performance baseline.

5.1

Difficulty Ladder

The “Ladder” experiment evaluates 13 LLMs across two mutation counts (k ∈ {1, 2}) and three prompt levels (Levels 0, 1, and 2). We set the maximum probe budget to Pmax = 50. We use 13 singleton mutations and 10 pair-wise mutations, three of which exhibit non-additive interaction effects (k = 2⊗ ) (see Supplementary Table 6). Each prompt-level and mutation configuration combination is evaluated over 5 independent repetitions. The results are shown in 8

0.5 V = 0.49

92 %

100 % V = 0.18

100 %

92 %

V = 0.14 1 0 0 % % 92 % 100 11 0. V=

100

%

Level 0

0.4

0.4

V = 0.28

V = 0.29

Mean accuracy V across models

0.5 100 %

100

%

0.3 V = 0.26

0.2

100 %

0.1 0.0

V = 0.05 100 %

k=1

V = 0.02

Promp Level 1 t varia nt (ha Level 2 rder )

der har

k = 2+

s(

ion tat

k=2

0.3

0.2

0.1

) 0.0

Mu

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), and the presence of interacting mutations (+ → ⊗). At the most challenging configuration (minimum prompt information combined with interacting mutations), the average accuracy drops to V = 0.02. Table 1, Figure 2, and Figure 3. 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 and 8. Performance gradient. As difficulty increases, accuracies decrease, driven by reduced system prompt information and increasing mutation complexity (overall see Figure 3 per-model see Figure 2). 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 to V = 0.02. The detection–attribution gap. Averaged across all 13 LLMs and over k ∈ {1, 2} and prompt levels, models achieve a kernel detection accuracy of VK = 0.65, but an exact mutation attribution accuracy of only VA = 0.28, revealing a substantial detection–attribution gap (Table 1 visualized in Supplementary Figure 8). 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).

9

For k = 2 and conditioned on correct kernel detection (VK = 1), providing mutation-count information shifts attribution failures: models are more likely to hallucinate mutations when k is known and more likely to omit mutations when it is not (Supplementary Table 9). In other words, when k is known, the model seems to feel compelled to fill all slots, leading to hallucinated mutation identities. When k is not known, the model leaves mutations unreported. Effects of interacting mutations. Performance decreases substantially when mutations exhibit non-additive interactions (Figure 2 and across prompt levels in Supplementary Table 7). At k = 2 with Level-2 prompts, most models fail completely, with only two exceptions: gpt-5.4_medium with V = 0.20 and gpt-5.4 with V = 0.07. Notably, the highest reasoningbudget 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-mini and gemini-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). Probe budget limitations. In 86.5 % of cases where models correctly detected the corrupt kernel but failed exact attribution (VK = 1, VA = 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). Baselines comparison. A random mutation-selection baseline over the 13-mutation ontology achieves accuracies of 1/13 ≈ 0.077 for k = 1 and 1/64 ≈ 0.016 for k = 2, so most models substantially exceed chance performance. Randomly selecting the corrupted kernel among {A, B, neither} yields a 1/3 baseline accuracy. A naive exhaustive-search baseline is computationally infeasible due to the combinatorial size of the probe space T .

5.2

Wide-Panel Benchmark

The wide-panel “Benchmark” evaluates 30 LLMs under a fixed baseline configuration (Level-3 system prompt) across mutation set cardinality k ∈ {0, 1, 2, 3}. We use 6 singleton, 3 pair-wise additive, and 3 triplet additive mutation sets (see Supplementary Table 6). 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. However, we separately tested one interacting mutation set (k = 2⊗ ). For each (LLM, S) pair, we evaluate 5 independent sessions with a maximum probe budget of Pmax = 65. Figure 4 shows the resulting performance leaderboard, and Table 2 shows the results averaged across all LLMs included in the leaderboard. Supplementary Table 11 and Figure 9 provides a detailed evaluation. Findings regarding the probe budget limitations are supported by Supplementary Figure 10. The Simple Reflex Agent. The Simple Reflex Agent (RSA) is a deterministic baseline that does not generate custom probes, but instead relies exclusively on the static example probes ΠRSA provided in the Level-0 system prompt. By construction, these probes, together with the expected output of reference and corrupted kernels (Oref , OS ), serve as an analytical oracle that yields perfect identification and attribution accuracy at k = 1 and additive sets. Crucially, none of the evaluated LLMs was capable of generating structurally similar probes autonomously to achieve V = 1 in the “Benchmark”. Furthermore, even when explicitly provided with these 10

Simple Reflex Agent Gemini 3.5 Flash (Preview) Gemini 3.1 Pro (Preview) Claude Sonnet 4.6 (High) Claude Opus 4.7 (High) GPT-5.5 (xHigh) Claude Sonnet 4.6 (Low) GPT-5.5 (High) GPT-5.5 (Medium) GPT-5.5 (Low) GPT-5.4 (Medium) GPT-5.4 (Low) Claude Sonnet 4.6 GPT-5.4 (High) GPT-5.5 Magistral Medium 1.2 GPT-5.4 GPT-5.4 (xHigh) Claude Haiku 4.5 Mistral Medium 3.5 Mistral Large 3 Gemini 2.5 Flash Gemini 2.5 Pro GPT-5.4 Mini GPT-5.4 Nano Magistral Small 1.2 Mistral Small 4 Ministral 3 8B Ministral 3 3B Ministral 3 14B Mistral Medium 3.1

k=1 k = 2+ k = 3+ mean 0.0

0.2

0.4

0.6

Performance: V

0.8

1.0

Figure 4: Performance leaderboard across models and mutation orders in “Benchmark”. For this comparison, only additive k + composite mutations have been used. k ≥ 2⊗ interacting mutations have been excluded since the performance on these sets has been close to 0 across all models (see Supplementary Table 11). The Simple Reflex Agent denotes 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). Hence, it reaches an accuracy of V = 1. 11

Table 2: Marginal accuracy by mutation count k on the wide-panel “Benchmark”. Exact correctness V , kernel detection VK , exact attribution VA , Jaccard partial credit VAJ , and conditional attribution correctness VA | VK = 1. For k ≥ 2, superscripts indicate whether the mutations are additive (+) or interacting (⊗). Values are averaged numbers across models, system prompt levels, and mutation sets with bootstrap 95 % confidence intervals in brackets. k

n

0 1 2+ 3+ 2⊗

155 930 465 465 155

V

VK

VA

VAJ

VA | VK = 1

0.90 [0.85, 0.94] 0.32 [0.29, 0.35] 0.15 [0.12, 0.18] 0.15 [0.12, 0.19] 0.03 [0.01, 0.06]

0.90 [0.85, 0.94] 0.77 [0.75, 0.80] 0.63 [0.58, 0.67] 0.67 [0.63, 0.71] 0.74 [0.67, 0.81]

0.97 [0.94, 0.99] 0.33 [0.30, 0.36] 0.15 [0.12, 0.18] 0.15 [0.12, 0.19] 0.03 [0.01, 0.06]

0.97 [0.94, 0.99] 0.36 [0.34, 0.40] 0.28 [0.25, 0.32] 0.32 [0.29, 0.35] 0.27 [0.23, 0.32]

1.00 [1.00, 1.00] 0.42 [0.38, 0.46] 0.24 [0.19, 0.29] 0.23 [0.19, 0.28] 0.04 [0.01, 0.09]

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 and RSA, see Supplementary Material B.2. Identifying the null case. At k = 0, the correct kernel classification is neither, indicating that both kernels are sound. Across all 30 models and RSA and 155 experimental sessions, models achieved a null-case specificity of 0.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 submit neither very early, whereas others do so only after exhausting the available budget. The former may indicate overconfidence, while the latter may reflect difficulty distinguishing the null case from hard-to-detect mutation configurations (Supplementary Table 10). Scalability and the multi-mutation collapse. Average exact accuracy V declines sharply as the number of mutations increases, dropping from 0.90 → 0.32 → 0.15 → 0.15 for k = 0, 1, 2+ , 3+ , respectively. For the interacting set, the average accuracy is 0.03, see Table 2. There are two severe performance collapses occurring between k = 1 and k ≥ 2 and between additive and interacting combinations, which aligns with the single-mutation bias identified in the “Ladder” experiment. While basic change detection remains relatively stable beyond k = 1, causal attribution remains the primary failure mode. This trend is further substantiated by the Jaccard similarity scores, which reach their lowest point at k = 2⊗ (VAJ = 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). Effects of inference-time compute. Supplementary Figure 7 displays the effect of scaling inference-time compute (or “reasoning effort”) across three models: gpt-5.4, gpt-5.5, and claude-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⊗ ) was very small (one mutation configuration with n = 5 per model and reasoning effort), these results remain preliminary, and further evaluation is required to substantiate this trend.

12

6

Discussion

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 order k is missing in the system prompt. Because attribution failures are overwhelmingly dominated by underreporting 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.1

Limitations

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 of k = 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. 13

• 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.2

Broader Impact and Applications

Although Elenchos is instantiated here using a dependently typed λ-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.3

Future 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 λ-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.

14

References [1] Humanity’s Last Exam. https://agi.safe.ai/, 2025. [2] M. Akhtar and et al. When AI benchmarks plateau: A systematic study of benchmark saturation. arXiv, 2026. doi: arXiv:2602.16763. [3] T. Altenkirch and A. Kaposi. Normalisation by Evaluation for Dependent Types. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), volume 52 of LIPIcs, 2016. https://doi.org/10.4230/LIPIcs.FSCD.2016.6. [4] G. Authors. GEAR: A General Evaluation Framework for Abductive Reasoning. arXiv, 2025. arXiv:2509.24096 (verify author list at camera-ready). [5] I. Authors. A Benchmark for Inductive and Abductive Reasoning over Synthetic Ontology Trees. arXiv, 2024. arXiv:2509.03345 (working title pending publication; verify before camera-ready). [6] E. Bender, T. Gebru, A. McMillan-Major, and S. Shmitchell. On the Dangers of Stochastic Parrots: Can Language Models Be Too Big? In ACM Conference on Fairness, Accountability, and Transparency, 2021. doi:10.1145/3442188.3445922. [7] E. M. Bender, T. Gebru, A. McMillan-Major, and S. Shmitchell. On the Dangers of Stochastic Parrots: Can Language Models Be Too Big? In Proc. ACM Conf. on Fairness, Accountability, and Transparency (FAccT), 2021. https://doi.org/10.1145/3442188.3445922. [8] C. Bhagavatula, R. Le Bras, C. Malaviya, K. Sakaguchi, A. Holtzman, H. Rashkin, D. Downey, W.-t. Yih, and Y. Choi. Abductive Commonsense Reasoning. In International Conference on Learning Representations (ICLR), 2020. arXiv:1908.05739. [9] BIG-bench authors. Beyond the Imitation Game: Quantifying and Extrapolating the Capabilities of Language Models. Transactions on Machine Learning Research, 2023. https://openreview.net/forum?id=uyTL5Bvosj. [10] M. Carneiro. Lean4Lean: Verifying a Typechecker for Lean, in Lean. https://doi.org/10.48550/arXiv.2403.14064.

arXiv, 2025.

[11] Center for AI Safety, Scale AI, and HLE Contributors Consortium. A benchmark of expert-level academic questions to assess AI capabilities. Nature, 649:1139–1146, 2026. https://doi.org/10.1038/s41586-025-09962-4. [12] E. Chen, M. Belkin, L. Bergen, and D. Danks. Does AI already have human-level intelligence? The evidence is clear. Nature, 650, 2026. https://www.nature.com/articles/d41586026-00285-6. [13] T. Chen, F.-C. Kuo, H. Liu, P.-L. Poo, D. Towey, and Z. Tse, T.H. Zhou. Metamorphic testing: A review of challenges and opportunities. ACM Comput. Surv., 51(1), 2018. https://doi.org/10.1145/3143561. [14] A. Church. A set of postulates for the foundation of logic. Annals of Mathematics, Series 2, 32(2):346–366, 1932. [15] 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. Training Verifiers to Solve Math Word Problems. arXiv preprint arXiv:2110.14168, 2021.

15

[16] K. Collins and J. Tenenbaum. Expert-level test is a head-scratcher for AI. Nature, 649, 2026. [17] T. Coquand and G. Huet. The Calculus of Constructions. Information and Computation, 76, 1988. [18] CrowdStrike. External Technical Root Cause Analysis – Channel File 291, 2024. https://www.crowdstrike.com/wp-content/uploads/2024/08/Channel-File-291-IncidentRoot-Cause-Analysis-08.06.2024.pdf. [19] R. Degiovanni and M. Papadakis. µBert: Mutation Testing using Pre-Trained Language Models. In 15th IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW), 2022. https://doi.org/10.1109/ICSTW55395.2022.00040. [20] E. First, M. Rabe, T. Ringer, and Y. Brun. Baldur: Whole-Proof Generation and Repair with Large Language Models. arXiv, 2023. arXiv:2303.04910, https://doi.org/10.48550/ arXiv.2303.04910. [21] A. Freund. Backdoor in upstream xz/liblzma leading to ssh server compromise, 2024. https://www.openwall.com/lists/oss-security/2024/03/29/4. [22] E. Glazer and et al. FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AI. arXiv, 2025. https://doi.org/10.48550/arXiv.2411.04872. [23] S. Haroon, M. T. Khan, and M. A. Gulzar. Evaluating LLM-Based Test Generation Under Software Evolution. arXiv, 2026. arXiv:2603.23443. [24] D. Hendrycks, C. Burns, S. Basart, A. Zou, M. Mazeika, D. Song, and J. Steinhardt. Measuring Massive Multitask Language Understanding. Proceedings of the International Conference on Learning Representations (ICLR), 2021. [25] D. Hendrycks, C. Burns, S. Kadavath, A. Arora, S. Basart, E. Tang, D. Song, and J. Steinhardt. Measuring Mathematical Problem Solving With the MATH Dataset. In NeuRIPS, 2021. [26] J. Hindley and J. Seldon. Lambda-Caluculus and Combinators – an Introduction. Cambridge University Press, 2008. [27] T. Hubert, A. Banino, and Google DeepMind Theorem Proving Team. Olympiad-Level Formal Mathematical Reasoning with Reinforcement Learning. Nature, 2025. https:// doi.org/10.1038/s41586-025-09833-y. [28] Y. Jia and M. Harman. An Analysis and Survey of the Development of Mutation Testing. IEEE Trans on Software Engineering, 37(5), 2011. [29] S. Kang, G. An, and S. Yoo. A Quantitative and Qualitative Evaluation of LLM-Based Explainable Fault Localization. Proceedings of the ACM on Software Engineering, 1(FSE), 2024. https://doi.org/10.1145/3660771. [30] A. Kovács. smalltt: a Minimal Dependent Type Theory Elaborator. https://github.com/ AndrasKovacs/smalltt, 2023. Accessed 2026-05. [31] V. Le, M. Afshari, and Z. Su. Compiler Validation via Equivalence Modulo Inputs. In Proc. 35th ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI ’14), pages 216–226, 2014. https://doi.org/10.1145/2594291.2594334.

16

[32] Z. Li and D. Shin. Mutation-Based Consistency Testing for Evaluating the Code Understanding Capability of LLMs. In Proc. IEEE/ACM 3rd Int. Conf. on AI Engineering – Software Engineering for AI, pages 150–159, 2024. [33] H. Lightman, V. Kosaraju, Y. Burda, H. Edwards, B. Baker, T. Lee, J. Leike, J. Schulman, I. Sutskever, and K. Cobbe. Let’s Verify Step by Step. arXiv, 2023. arXiv:2305.20050. [34] A. Löh, C. McBride, and W. Swierstra. A Tutorial Implementation of a Dependently Typed Lambda Calculus. Fundamenta Informaticae, 102:177–207, 2010. https://doi.org/10.3233/FI-2010-304. [35] P. Martin-Löf. Intuitionistic Type Theory. Bibliopolis, Naples, 1984. Notes by Giovanni Sambin, Studies in Proof Theory. [36] T. McIntosh, T. Susnjak, N. Arachchilage, T. Liu, D. Xu, P. Watters, and M. Halgamuge. Inadequacies of large language model benchmarks in the era of generative artificial intelligence. IEEE Transactions on Artificial Intelligence, 7(1):22–39, 2026. doi: 10.1109/TAI.2025.3569516. [37] W. M. McKeeman. Differential Testing for Software. Digital Technical Journal 10(1), Digital Equipment Corporation, 1998. [38] G. Mialon, C. Fourrier, C. Swift, T. Wolf, Y. LeCun, and T. Scialom. GAIA: a benchmark for General AI Assistants. arXiv:2311.12983, 2023. [39] I. Mirzadeh, K. Alizadeh, H. Shahrokhi, O. Onutlu, O. Tuzel, S. Samet, and S.-M. Samadi. GSM-Symbolic: Understanding the Limitations of Mathematical Reasoning in Large Language Models. arXiv preprint arXiv:2410.05229, 2024. [40] I. Mirzadeh, K. Alizadeh, H. Shahrokhi, O. Tuzel, S. Bengio, and M. Farajtabar. GSM-NoOp: A Stress Test for the Reasoning Robustness of LLMs. arXiv, 2024. https://arxiv.org/abs/2410.05229. [41] M. Papadakis and Y. Le Traon. Metallaxis-FL: Mutation-Based Fault Localization. Software Testing, Verification and Reliability, 25(5-7):605–628, 2015. https://doi.org/10.1002/ stvr.1509. [42] C. S. Peirce. Pragmatism as the logic of abduction. In P. E. Project, editor, The Essential Peirce, Volume 2. Indiana University Press, 1998. Originally delivered as a Harvard lecture, 1903. [43] S. Polu and I. Sutskever. Generative Language Modeling for Automated Theorem Proving. In arXiv, 2020. arXiv:2009.03393, https://doi.org/10.48550/arXiv.2009.03393. [44] I. S. Qureshi and Z. M. J. Jiang. Test Case Generation from Bug Reports via Large Language Models: A Cognitive Layered Evaluation Framework. arXiv, 2025. arXiv:2510.05365. [45] D. Rein, B. Hou, A. Stickland, J. Jackson, S. Bowman, et al. GPQA: A Graduate-Level Google-Proof Q&A Benchmark. arXiv preprint arXiv:2311.12022, 2023. [46] Z. Ren, Z. Shao, J. Song, H. Xin, H. Wang, W. Zhao, L. Zhang, Z. Fu, Q. Zhu, D. Yang, Z. Wu, Z. Gou, S. Ma, H. Tang, Y. Liu, W. Gao, D. Guo, and C. Ruan. DeepSeek-ProverV2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition. arXiv, 2025. arXiv:2504.21801, https://doi.org/10.48550/arXiv.2504. 21801.

17

[47] M. Salimi, S. Adim, D. Parnian, N. Alighardashi, M. Siavoshani, and M. Rohban. Wiring the ‘Why’: A Unified Taxonomy and Survey of Abductive Reasoning in LLMs. arXiv, 2026. arXiv:2604.08016. [48] M. Schönfinkel. Über die Bausteine der mathematischen Logik. Mathematische Annalen, 92(3–4):305–316, 1924. doi:10.1007/BF01448013. [49] M. Sozeau, S. Boulier, Y. Forster, N. Tabareau, and T. Winterhalter. Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq. Proceedings of the ACM on Programming Languages, 4(POPL), 2020. https://doi.org/10.1145/3371076. [50] M. Sozeau, Y. Forster, M. Lennon-Bertrand, J. B. Nielsen, N. Tabareau, and T. o. Winterhalter. Touring the MetaCoq Project. Electronic Proceedings in Theoretical Computer Science (EPTCS), 2021. arXiv:2107.07670, https://doi.org/10.48550/arXiv.2107.07670. [51] Stanford HAI. The 2026 AI Index Report: https://hai.stanford.edu/ai-index/2026-ai-index-report.

Technical Performance,

2026.

[52] K. Thompson. Reflections on trusting trust. Communications of the ACM, 1984. [53] F. Tip, J. Bell, and M. Schäfer. LLMorpheus: Mutation Testing using Large Language Models. arXiv, 2024. arXiv:2404.09952, https://doi.org/10.48550/arXiv.2404.09952. [54] J. Wei, X. Wang, D. Schuurmans, M. Bosma, B. Ichter, F. Xia, E. Chi, Q. V. Le, and D. Zhou. Chain-of-Thought Prompting Elicits Reasoning in Large Language Models. In Advances in Neural Information Processing Systems (NeurIPS), volume 35, pages 24824– 24837, 2022. [55] Z. Wei, Y. Zhang, and M. Sun. MILE: A Mutation Testing Framework of In-Context Learning Systems. In arXiv, 2024. arXiv:2409.04831, https://doi.org/10.48550/arXiv. 2409.04831. [56] C. White, S. Dooley, M. Roberts, A. Pal, B. Feuer, S. Jain, et al. Livebench: A challenging, contamination-limited llm benchmark. arXiv preprint arXiv:2406.19314, 2024. [57] H. Xin, D. Guo, Z. Shao, Z. Ren, Q. Zhu, B. Liu, C. Ruan, W. Li, and X. Liang. DeepSeekProver: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data. arXiv, 2024. arXiv:2405.14333, https://doi.org/10.48550/arXiv.2405.14333. [58] J. Yan, J. Huang, C. Fang, J. Yan, and J. Zhang. Better Debugging: Combining Static Analysis and LLMs for Explainable Crashing Fault Localization. arXiv, 2024. arXiv:2408.12070. [59] A. Z. Yang, C. Le Goues, R. Martins, and V. J. Hellendoorn. Large Language Models for Test-Free Fault Localization. In Proc. IEEE/ACM 46th Int. Conf. on Software Engineering (ICSE ’24), 2024. https://doi.org/10.1145/3597503.3623342. [60] B. Yang, H. Tian, J. Ren, H. Zhang, J. Klein, T. F. Bissyandé, C. Le Goues, and S. Jin. Integrating Various Software Artifacts for Better LLM-Based Bug Localization and Program Repair. ACM Transactions on Software Engineering and Methodology, 2025. arXiv:2412.03905. [61] K. Yang, A. Swope, A. Gu, R. Chalamala, P. Song, S. Yu, S. Godil, R. Prenger, and A. Anandkumar. LeanDojo: Theorem Proving with Retrieval-Augmented Language Models. In Advances in Neural Information Processing Systems (NeurIPS), Datasets and Benchmarks Track, 2023. https://doi.org/10.48550/arXiv.2306.15626. [62] X. Yang, Y. Chen, E. Eide, and J. Regehr. Finding and understanding bugs in C compilers. In Proc. 32nd ACM SIGPLAN conf. on Programming language design and implementation - PLDI ’11, pages 283–294, 2011. https://doi.org/10.1145/1993498.19935. 18

[63] S. Yao, D. Yu, J. Zhao, I. Shafran, T. L. Griffiths, Y. Cao, and K. Narasimhan. Tree of Thoughts: Deliberate Problem Solving with Large Language Models. In NeurIPS, 2023. arXiv:2305.10601. [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. FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models. arXiv, 2025. https://doi.org/10.48550/arXiv.2505.02735. [65] K. Zheng, J. Han, and S. Polu. MiniF2F: a cross-system benchmark for formal Olympiadlevel mathematics. arXiv:2109.00110, 2021.

19

Supplementary Material

20

A

LambdaPy Surface 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. // LambdaPi surface syntax grammar (Lark Earley) // // Supports both Python-style and Haskell-style syntax: // Python: assume x : T Haskell: assume (x :: T) // Python: let x : T = body Haskell: let x = (body :: T) // Python: e : T Haskell: e :: T // Python: Type 0 Haskell: * (same as Type 0) // // Each statement occupies one logical line ending with NEWLINE. %import common.CNAME -> NAME %import common.INT %import common.NEWLINE %import common.WS_INLINE %ignore WS_INLINE %ignore /--[^\n]*/ start: statement+ // --------------------------------------------------------------------------// Statements (each ends with NEWLINE) // --------------------------------------------------------------------------// Haskell-style: assume (a :: *) (b :: *) or assume a :: * // Python-style: assume x y : T statement: "assume" paren_binding+ NEWLINE -> assume_multi_stmt | "assume" NAME ("::" | ":") term NEWLINE -> assume_single_stmt | "assume" name_list ":" term NEWLINE -> assume_stmt | "let" NAME "=" term NEWLINE -> let_infer_stmt | "let" NAME ":" term "=" term NEWLINE -> let_stmt | "eval" term NEWLINE -> eval_stmt | "check" term NEWLINE -> check_stmt // Parenthesized binding for Haskell-style assume paren_binding: "(" NAME ("::" | ":") term ")" name_list: NAME+ // --------------------------------------------------------------------------// Terms // --------------------------------------------------------------------------term: lam_term | forall_term | app_term "->" term | app_term ("::" | ":") term | app_term

-> arrow -> ann

// Lambda lam_term: "\\" NAME+ "->" term // Universal (forall binder supports both : and ::) forall_term: "forall" binder+ "." term binder: "(" NAME ("::" | ":") term ")" // ---------------------------------------------------------------------------

21

// Application (left-associative) // --------------------------------------------------------------------------app_term: atom+

-> app_chain

// --------------------------------------------------------------------------// Atoms // --------------------------------------------------------------------------atom: "(" term ")" | "Type" INT? | "*" INT? | "Nat" | "Zero" | "Succ" | "NatElim" | "natElim" | "Vec" | "Nil" | "Cons" | "VecElim" | "vecElim" | "Fin" | "FZero" | "FSucc" | "FinElim" | "finElim" | "Eq" | "Refl" | "EqElim" | "eqElim" | NAME

-> paren -> universe -> universe -> nat -> zero -> succ_kw -> nat_elim_kw -> nat_elim_kw -> vec_kw -> nil_kw -> cons_kw -> vec_elim_kw -> vec_elim_kw -> fin_kw -> fzero_kw -> fsucc_kw -> fin_elim_kw -> fin_elim_kw -> eq_kw -> refl_kw -> eq_elim_kw -> eq_elim_kw -> var

22

B

Mutation Taxonomy Table 3: Full mutation taxonomy used in the current |M| = 13 implementation.

ID

Class

Mutation name and description

ID_01

Type Equality

ID_02

Binding Discipline

ID_03

Type Equality

ID_04

Binding Discipline

ID_05

Semantic Environment

ID_06

Semantic Environment

ID_07

Type Equality

ID_08

Semantic Environment

ID_09

Computational Rule

ID_10

Type Equality

ID_11

Semantic Environment

ID_12

Universe Leveling

ID_13

Computational Rule

Equality of Applications Argument Checker strictly enforces equality on both the function and the argument when comparing applications. Fail to Increment Under Lambda A substitution intended for an outer binder can incorrectly replace the inner bound variable. Equality of Bound Indices Bound(0) and Bound(1) are considered definitionally equal; dependent types over adjacent binders collapse. Index Shift Bound(i) lookup uses env[min(i+1, len(env)−1)] instead of env[i]. Causes de Bruijn variable resolution to silently drift by one position. Globals to Zero Unknown globals normalize to Zero rather than staying neutral; type checking proceeds, semantics are junk. Lambda Environment Reversion The binder is placed at the wrong end of the environment. With the existing Bound(i) → env[i] convention, lambda bodies evaluate against a scrambled scope discipline. Equality of Inference Terms Equality of inference terms collapses; all types are judged equal, but inference still succeeds on well-typed terms. Lambda Environment Padding Closure environment is padded with a neutral element, shifting all argument positions by one. Double Application Function is applied a second time to the result of itself. Equality of Free Terms Any two neutral heads become definitionally equal after quotation; unrelated dependent types collapse. Globals to Identity Unknown globals normalize to the identity function rather than staying neutral. Universe Collapse Star(n) returns VStar(n) instead of VStar(n + 1); the universe hierarchy collapses (Typen : Typen ). Argument Dropping Function argument is dropped; VStar(0) (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.

B.1

Class Label Mapping

Per-mutation experimental tables (Figure 5) 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 gives the explicit mapping). 23

Table 4: Mapping between canonical class names and labels in figures and tables. Canonical class

Analysis-time label

Description

Binding Discipline

binding

Semantic Environment Computational Rule Type Equality Universe Leveling

free_name application def_equality universe

Error in variable resolution such as de Bruijn misalignment and binder shifting Altered substitution or closure environments Corruptions of β-reduction Changes to type-level equality or convertability Violations of cumulative universe stratification

B.2

Simple Reflex Agent

The Simple Reflex Agent (RSA) is designed to diagnose all n = 13 mutations defined above (Table 3) assuming singleton mutations k = 1. This is achieved by constructing a probe set ΠRSA ⊂ 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 ∀µ, µ′ ∈ M, µ ̸= µ′ ⇒ ∃τ ∈ ΠRSA : K{µ} (τ ) ̸= K{µ′ } (τ ) ∧ K{µ} (τ ) ̸= Kref (τ )

(4)

By probing both kernels with ΠRSA , the agent can uniquely identify the present mutation by comparing kernels output to the expected observation for KS and Kref .2

B.3

Non-degeneracy Filter k ≥ 2

The candidate family for k = 2 is defined by   M , F̃2 = 2

(5)

which are all possible 2-element combinations of mutations in M. However, not all of them are admissible in the sense that they can be clearly identified. We selected the family of valid combinations F2 by a deterministic three-condition filter against a curated probe library based. Predicate. Let Π ⊂ T denote the probe library: a fixed, ontology-balanced set of LambdaPy source terms that exercises every mutation class. For a k = 2 candidate pair S = {µi , µj } ∈ F̃2 , the divergence vector div(S) of KS against Kref on Π is defined as OS (τ ) = (Kref (τ ), KS (τ ), τ ) ,

(6)

div(S) = {OS (τ ) : τ ∈ Π} .

(7)

The pair is admissible if 1. Non-collapse. div(S) ̸= div(∅). KS has to be distinguishable from Kref . Additionally, uniformly rejecting or uniformly accepting pairs are excluded as “total logical collapse”: ∃ τm , τn ∈ Π such that τm ̸= τn ∧ KS (τm ) ̸= KS (τn ). 2. Non-subsumption. div(S) ̸= div({µ}) ∀ µ ∈ M in particular for µi , µj . Pairs whose composite divergence is indistinguishable from either singleton are excluded as “symptomatic subsumption” according to Occam’s razor. 3. Identifiability. div(S) ̸= div(S ′ ) ∀ S ′ ∈ F̃2 \ {S}. Two pairs whose divergence vector is indistinguishable are excluded. 2

The list of constructed probes ΠRSA and expected output of Kref and KS can be provided on request.

24

Algorithm. For our implementation, we applied the corresponding mutation flag overrides
13 (Section 4) to each of the 2 = 78 candidate unordered pairs and ran the ΠRSA probe set on both Kref and the merged kernel; each probe under a fresh state which contained only the core in Appendix A. Pairs that fail condition (1) or (2) are rejected. Those failing condition (3) are tested further by extending ΠRSA with probes designed specifically to distinguish the pairs. If this is not successful, both pairs are rejected. The remainder is F2 . Extending to k
> 2. The algorithm has to be applied iteratively for increasing k, / where F̃k = M k . Only condition (2) needs to be generalized for S ∈ F̃k to div(S) ∈ {div(S ′ ) : S ′ ∈ Fk′ , k ′ < k}. The divergence of S must be new, i. e. it must not coincide with the divergence of any set with lower cardinality, in particular to subsets of S.

B.4

Interacting Mutation Sets

We characterized mutation sets S with cardinality k ≥ 2 as additive (highlighted by k + ) if ∀ τ ∈ ΠRSA , ∃ Ssub ⊊ S such that (Ssub is additive ∨ |Ssub | = 1) ∧ OS (τ ) = OSsub (τ ). This basically means, that the behaviour of a corrupted kernel KS can be fully explained by singleton mutations in S and there are no unexpected results. In contrast, we characterize mutation sets as interacting (highlighted by k ⊗ ) 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 our 78 candidate pairs, see Figure 6, and observed three types of mutation sets in our experimental setup, see Table 5. Table 5: Types of mutation pairs in Figure 6. Type +

Admissible, additive (used at k = 2 ) Admissible, interacting (used at k = 2⊗ ) Total collapse (uniform accept/reject) Subsumed by one of {µi , µj } Total

B.5

Colours in Figure 6

Count

blueish green orange, red, purple

55 9 0 14

light grey, dark grey

78

Compound-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.

25

Table 6: Curated mutation sets used in the compound-condition sessions. Order

Mutation Set

k=0

∅

k=1

{ID_01} {ID_02} {ID_03} {ID_04} {ID_05} {ID_06} {ID_07} {ID_08} {ID_09} {ID_10} {ID_11} {ID_12} {ID_13}

✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓

{ID_01,ID_03} {ID_02,ID_04} {ID_02,ID_06} {ID_02,ID_12} {ID_03,ID_10} {ID_04,ID_09} {ID_06,ID_09} {ID_06,ID_10} {ID_07,ID_13}

✓ ✓ ✓

{ID_04,ID_06} {ID_04,ID_08} {ID_09,ID_10}

✓ ✓ ✓

k = 2+

k=2

⊗

k = 3+

{ID_01,ID_03,ID_10} {ID_02,ID_03,ID_06} {ID_07,ID_09,ID_12}

Ladder

Benchmark ✓

✓ ✓ ✓ ✓

✓

✓ ✓ ✓

✓ ✓

✓ ✓

✓

Classes Null baseline def_equality binding def_equality binding free_name binding def_equality binding application def_equality free_name universe application def_equality binding binding universe × binding def_equality application × binding application × binding def_equality × binding def_equality × application

✓

binding binding def_equality × application

✓ ✓ ✓

def_equality def_equality × binding def_equality × application × universe

26

success

0.23 -0.07 -0.03 -0.14 -0.07 -0.30 -0.27 -0.62 0.64 -0.73 -0.28 -0.33 -0.29 -0.17

ID_02: Fail to Increment Under Lambda

-0.45 -0.07 -0.03 0.79 0.08 -0.30 -0.27 0.45 0.51 0.25 0.50 -0.33 0.96 0.16

ID_06: Lambda Environment Reversion

-0.86 -0.61 -0.83 -0.81 -0.23 -0.30 -0.40 -0.22 -0.71 -0.31 0.24 -0.33 -0.29 -0.44

ID_08: Lambda Environment Padding

-0.04 0.33 -0.43 -0.28 -0.39 -0.06 -0.80 -0.22 -0.84 -0.59 0.24 -0.33 -0.29 -0.28

ID_05: Globals to Zero

0.78 0.87 0.50 0.66 -0.23 1.16 0.93 0.99 0.51 1.36 -0.28 1.47 0.21 0.69

ID_11: Globals to Identity

0.23 0.06 0.10 -0.28 0.24 0.19 0.40 -0.62 0.10 0.67 -0.28 0.12 0.21 0.09

ID_13: Argument Dropping

-0.59 -0.74 -0.57 -0.14 0.08 0.67 -0.80 -0.35 -0.30 -0.31 -0.28 -0.10 0.21 -0.25

ID_09: Double Application

0.78 0.87 0.90 0.92 0.24 -0.30 0.93 0.86 0.78 1.08 1.27 1.24 -0.04 0.73

ID_07: Equality of Inference Terms

-0.32 -0.88 -0.70 -0.94 -0.39 -0.30 -0.80 -0.89 -0.57 -0.59 -0.28 -0.33 -0.29 -0.56

ID_10: Equality of Free Terms

-0.04 -0.07 0.24 -0.28 -0.39 -0.30 0.27 -0.22 -0.44 -0.45 -0.28 -0.33 -0.29 -0.20

0.78 0.87 0.90 1.06 1.66 0.43 0.67 1.12 0.64 0.11 -0.28 -0.33 0.46 0.62

0.0

0.5 1.0 1.5

eH

ud

Mis

Pro

0.5

Fla

2.5

ni mi

Ge

Cla

an

2.5 ni

mi

Ge

T-5 .

4N

ini 4M

T-5 .

GP

GP

) Lo w

T-5 . GP

m)

4(

GP

T-5 .

diu

Hig

Me

4(

4(

T-5 .

T-5 .

GP

GP

1.0

sh aik u4 tra .5 lL Min arge 3 ist ral 3 Min 14B ist ral Min 3 8B ist ral 33 B me an

ID_12: Universe Collapse Mutation classes Binding Free Name Universe Def. Equality Application

o

-0.59 -0.48 -0.16 -0.28 -0.39 -0.30 -0.27 -0.22 -0.17 -0.31 -0.02 -0.33 -0.29 -0.29

4

0.09 -0.07 0.10 -0.28 -0.23 -0.30 0.40 -0.08 -0.17 -0.17 -0.28 -0.10 -0.29 -0.11

ID_03: Equality of Bound Indices

h)

ID_01: Equality of Applications Argument

1.5

z-score of V per model

Mutation ID difficulty ID_04: Index Shift

(a) Per-mutation accuracy VK .

divergence

6.7

6.9

6.3

5.9

7.3

>50

5.5

11.7 14.0

7.5

10.0

3.5

4.0

7.4

ID_02: Fail to Increment Under Lambda

3.5

4.0

4.1

4.9

7.8

4.3

3.9

11.3 13.5 10.8

8.0

>50

2.4

6.6

ID_06: Lambda Environment Reversion

3.7

4.3

4.3

4.7

8.3

5.3

3.9

7.4

11.9 15.7 14.4

>50

2.0

7.2

ID_08: Lambda Environment Padding

3.5

4.5

4.3

4.9

7.2

4.5

7.1

12.3 14.5

9.0

7.4

>50

2.0

6.8

ID_05: Globals to Zero

4.7

3.8

4.5

4.2

2.9

3.2

4.7

6.6

4.0

2.5

1.6

1.3

1.2

3.5

ID_11: Globals to Identity

4.1

4.0

4.3

5.0

2.9

3.6

5.7

6.3

3.5

1.8

4.3

1.7

1.0

3.7

ID_13: Argument Dropping

2.2

2.8

2.9

3.1

6.2

1.9

4.9

9.4

7.7

2.2

11.5

6.0

2.2

4.9

ID_09: Double Application

5.0

4.2

5.6

6.1

3.5

4.0

6.3

12.2

3.9

4.9

5.6

1.8

1.6

5.0

ID_07: Equality of Inference Terms

3.3

2.7

2.6

2.4

2.8

4.7

4.5

2.3

4.6

7.2

6.2

3.8

3.5

3.9

ID_10: Equality of Free Terms

21.3 21.0 17.9

5.6

4.4

>50

9.4

13.1

7.7

8.9

>50

14.2

9.8

12.1

ID_01: Equality of Applications Argument

15.9 16.1 15.0

5.0

9.0

>50

9.5

9.5

14.8

7.7

>50

1.0

1.0

9.5

7.0

16.3 11.6 12.0

>50

3.0

3.0

7.4

13.6 13.0

3.8

6.2

8.7

ID_12: Universe Collapse Mutation classes Binding Free Name Universe Def. Equality Application

1.6

1.7

1.2

1.6

6.3

6.0

4.9

18.6 12.0

8.5

8.1

5.6

d GP ium) T-5 .4 (Lo w) GP T GP -5.4 T-5 .4 GP Mini T-5 .4 Ge Nan o mi n Ge i 2.5 mi Pro ni 2 Cla .5 Fl a ud e H sh aik Mis u 4. 5 tra lL a r g Min e3 ist ral 31 Min 4 ist B ral 3 Min 8 ist B ral 33 B

1.1

15

10

5

0

GP

T-5 .

4(

Me

4(

T-5 .

GP

1.1

20

me an

7.0

Hig h)

ID_03: Equality of Bound Indices

25

# first divergent probe (budget: 50)

Mutation ID difficulty

ID_04: Index Shift

(b) Per-mutation first divergent probe.

Figure 5: Difficulty of n = 13 mutations at order k = 1 based on “Ladder” experiment. Values are averaged across prompt variant conditions. Classes that are consistently hard or easy to determine are shown by striking rows.

27

ID_12: Universe Collapse

+

+

+

+

+

ID_13: Argument Dropping

+

+

+

+

+

+

+

+

+

+

+

ID_11: Globals to Identity

+

+

+

+

+

ID_05: Globals to Zero

+

+

+

+

+

ID_09: Double Application

ID_08: Lambda Environment Padding

+

+

+

+

ID_06: Lambda Environment Reversion

+

+

+

+

ID_04: Index Shift

+

+

+

ID_02: Fail to Increment Under Lambda

+

+

+

+

ID_10: Equality of Free Terms

+

+

ID_07: Equality of Inference Terms ID_03: Equality of Bound Indices

+

+

+

+

+

+

+

+

+

+ +

+ +

+

+

+

+

+

+

+

+

+

+

+

+

+

+

+

+

+

+

+

+

+

+

+

+

+

+

+

+

+

+

+

+

+

+

+

+

+

+

+

+

+

+

+

+

+

+

+

+

+

+

+

+

Categories k=1 Simplifies to k = 1 ID_Y Simplifies to k = 1 ID_X + Both IDs diagnosed ID_X challenging ID_Y challenging Both IDs challenging

ID_

01

:E qu

ali ty ID_ of A 0 p ID_ 3: Eq plica 07 ua tion : E lity s qu o Arg al f B u ID_ 02 ID_1 ity o oun men : Fa 0: f In d I t il t Eq fer ndi o I ua en ces nc lity ce ID_ rem o Te 06 en f Fre rms :L tU eT a nd e ID_ mb 08 da ID_ er L rms : L En 04 am am vir : I bd bd onm nde a aE e x nv nt R Shi ir e ft ID_ onm vers e ID_ 05: G nt Pa ion 11 lo dd ID_ : Glo bals ing 09 bal to Z ID_ : Do s to ero 13 ubl Ide : A e A nt ID_ rgum ppli ity 12 en cat : U t D ion niv ro ers ppi e C ng oll ap se

ID_01: Equality of Applications Argument

+

+

Figure 6: Interaction scheme of mutations. Subsumed mutations (grey) are determined by i) indication of implementation ii) indistinguishable behaviour from k = 1 mutations when facing ΠSRA . All combinations that are coloured are valid. Blueish green (+) is the easiest type of combination: Both mutations are additive and do not interact. There SRA produces V = 1. Two interacting types (⊗) are observed in our setting: i) Partial observability (orange, red). SRA identifies only one mutation. Combinations kernel behaviour is still distinguishable from all others. ii) Emergence (purple, diamond) where kernel shows a fully interacting behaviour.

28

C

Detailed Model-by-condition Tables

The Section 5 main text reports only the headline inline, e. g. Table 1. 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 marginalises over scaffold to expose the single vs. double dissociation as well as the interacting difficulty. Similarly, Table 8 summarizes the effect of hint levels in the system prompt per model. Table 9 expands the over/under-reporting breakdown at k = 2. “Benchmark” experiment. Table 10 lists per-model true-negative rates and probing perseverance on the k = 0 null condition. Table 11 gives the full per-(model, condition) summary of detailed performance statistics for all benchmark configurations with for k ∈ {1, 2, 3}.

29

Table 7: Per-model comparison of single vs. double vs. interacting mutations. Marginal accuracy by mutation count k on the “Ladder” experiment: exact correctness V , kernel detection VK , exact attribution VA , Jaccard partial credit VAJ , conditional attribution correctness VA |VK = 1, and ratio of used probes P/Pmax . Numbers are mean values over prompt levels and corresponding mutations sets. For k ≥ 2, superscripts indicate whether the mutations are additive (+) or interacting (⊗). Model

k

n

V

VK

VA

VAJ

VA | VK

P/Pmax

ministral-3b-2512

1 2+ 2⊗

195 105 45

0.077 0.000 0.000

0.369 0.295 0.267

0.190 0.000 0.000

0.190 0.094 0.015

0.208 0.000 0.000

0.616 0.727 0.775

ministral-8b-2512

1 2+ 2⊗

195 105 45

0.097 0.010 0.000

0.210 0.238 0.200

0.200 0.067 0.000

0.200 0.160 0.074

0.463 0.040 0.000

0.966 0.988 0.980

ministral-14b-2512

1 2+ 2⊗

195 105 45

0.072 0.010 0.000

0.272 0.352 0.356

0.082 0.019 0.000

0.085 0.122 0.096

0.264 0.027 0.000

0.999 1.000 1.000

mistral-large-2512

1 2+ 2⊗

195 105 45

0.349 0.133 0.044

0.600 0.638 0.867

0.451 0.171 0.044

0.451 0.363 0.274

0.581 0.209 0.051

0.573 0.619 0.550

claude-haiku-4-5

1 2+ 2⊗

195 105 45

0.415 0.181 0.133

0.774 0.743 0.911

0.451 0.229 0.133

0.456 0.386 0.404

0.536 0.244 0.146

0.763 0.813 0.852

gemini-2.5-flash

1 2+ 2⊗

195 105 45

0.441 0.295 0.156

0.877 0.905 0.911

0.446 0.295 0.156

0.459 0.471 0.393

0.503 0.326 0.171

0.378 0.470 0.427

gemini-2.5-pro

1 2+ 2⊗

195 105 45

0.467 0.200 0.200

0.918 0.933 0.956

0.467 0.210 0.200

0.495 0.379 0.430

0.508 0.214 0.209

0.342 0.434 0.419

gpt-5.4-nano

1 2+ 2⊗

195 105 45

0.082 0.000 0.000

0.174 0.124 0.200

0.133 0.000 0.000

0.133 0.083 0.000

0.471 0.000 0.000

0.153 0.170 0.152

gpt-5.4-mini

1 2+ 2⊗

195 105 45

0.231 0.076 0.022

0.569 0.581 0.622

0.318 0.152 0.022

0.326 0.298 0.211

0.405 0.131 0.036

0.304 0.328 0.232

gpt-5.4

1 2+ 2⊗

195 105 45

0.472 0.267 0.133

0.851 0.848 0.956

0.472 0.267 0.133

0.487 0.386 0.396

0.554 0.315 0.140

0.310 0.348 0.325

gpt-5.4_low

1 2+ 2⊗

195 105 45

0.549 0.267 0.178

0.933 0.914 1.000

0.549 0.267 0.178

0.574 0.421 0.478

0.588 0.292 0.178

0.265 0.347 0.295

gpt-5.4_medium

1 2+ 2⊗

195 105 45

0.569 0.362 0.289

0.908 0.905 1.000

0.569 0.362 0.289

0.585 0.524 0.507

0.627 0.400 0.289

0.311 0.449 0.404

gpt-5.4_high

1 2+ 2⊗

195 105 45

0.621 0.276 0.178

0.913 0.848 0.889

0.621 0.276 0.178

0.628 0.400 0.419

0.680 0.326 0.200

0.326 0.484 0.461

30

Table 8: Per-model comparison of scaffolding level. Marginal accuracy by prompt level on the “Ladder” experiment: exact correctness V , kernel detection VK , exact attribution VA , Jaccard partial credit VAJ , conditional attribution correctness VA |VK = 1, and ratio of used probes P/Pmax . Numbers are mean values over mutations sets. Model

Prompt

n

V

VK

VA

VAJ

VA | VK

P/Pmax

ministral-3b-2512

Level 0 Level 1 Level 2

115 115 115

0.113 0.009 0.009

0.470 0.217 0.313

0.287 0.009 0.026

0.378 0.009 0.026

0.241 0.040 0.028

0.206 0.874 0.932

ministral-8b-2512

Level 0 Level 1 Level 2

115 115 115

0.078 0.035 0.061

0.174 0.296 0.183

0.287 0.043 0.070

0.336 0.078 0.100

0.450 0.118 0.333

0.936 0.991 0.996

ministral-14b-2512

Level 0 Level 1 Level 2

115 115 115

0.061 0.035 0.035

0.339 0.191 0.391

0.087 0.035 0.035

0.130 0.058 0.104

0.179 0.182 0.089

1.000 0.998 1.000

mistral-large-2512

Level 0 Level 1 Level 2

115 115 115

0.409 0.130 0.191

0.791 0.496 0.652

0.539 0.157 0.243

0.620 0.223 0.361

0.516 0.263 0.293

0.331 0.749 0.672

claude-haiku-4-5

Level 0 Level 1 Level 2

115 115 115

0.548 0.252 0.122

0.939 0.722 0.687

0.609 0.261 0.157

0.678 0.339 0.267

0.583 0.349 0.177

0.679 0.832 0.859

gemini-2.5-flash

Level 0 Level 1 Level 2

115 115 115

0.539 0.278 0.261

0.957 0.896 0.817

0.539 0.287 0.261

0.583 0.359 0.420

0.564 0.311 0.319

0.172 0.475 0.590

gemini-2.5-pro

Level 0 Level 1 Level 2

115 115 115

0.557 0.339 0.157

0.965 0.922 0.896

0.557 0.348 0.157

0.591 0.429 0.333

0.577 0.368 0.175

0.161 0.458 0.520

gpt-5.4-nano

Level 0 Level 1 Level 2

115 115 115

0.113 0.009 0.017

0.209 0.139 0.139

0.191 0.009 0.026

0.214 0.061 0.026

0.542 0.062 0.125

0.111 0.151 0.212

gpt-5.4-mini

Level 0 Level 1 Level 2

115 115 115

0.270 0.113 0.087

0.687 0.548 0.504

0.383 0.183 0.122

0.470 0.246 0.191

0.392 0.206 0.172

0.141 0.353 0.411

gpt-5.4

Level 0 Level 1 Level 2

115 115 115

0.617 0.261 0.217

1.000 0.791 0.800

0.617 0.261 0.217

0.670 0.328 0.336

0.617 0.330 0.272

0.176 0.371 0.424

gpt-5.4_low

Level 0 Level 1 Level 2

115 115 115

0.548 0.443 0.252

1.000 0.904 0.904

0.548 0.443 0.252

0.629 0.519 0.397

0.548 0.490 0.279

0.174 0.346 0.362

gpt-5.4_medium

Level 0 Level 1 Level 2

115 115 115

0.591 0.443 0.374

1.000 0.896 0.861

0.591 0.443 0.374

0.667 0.504 0.497

0.591 0.495 0.434

0.211 0.423 0.462

gpt-5.4_high

Level 0 Level 1 Level 2

115 115 115

0.635 0.400 0.339

0.974 0.817 0.878

0.635 0.400 0.339

0.693 0.446 0.455

0.652 0.489 0.386

0.231 0.446 0.497

31

Table 9: Fault characterization for k = 2 double mutation in the “Ladder” experiment. Per-model and k-hint level prompts, attribution modes are analyzed for n sessions with VK = 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 gives the proportion of sessions with probe budget NOT exhausted although incorrect mutation attribution VK = 1 ∧ VA = 0. Model

Prompt

n

Correct

Incomplete

Mixed

Incorrect

< Pmax

ministral-3b-2512

Level 0-1 Level 2

26 17

0.000 0.000

0.192 0.000

0.192 0.000

0.615 1.000

0.731 0.118

ministral-8b-2512

Level 0-1 Level 2

25 9

0.040 0.000

0.000 0.778

0.680 0.000

0.280 0.222

0.208 0.222

ministral-14b-2512

Level 0-1 Level 2

29 24

0.034 0.000

0.138 0.625

0.483 0.000

0.345 0.375

0.000 0.000

mistral-large-2512

Level 0-1 Level 2

70 36

0.229 0.000

0.000 0.750

0.643 0.000

0.129 0.250

0.926 0.917

claude-haiku-4-5

Level 0-1 Level 2

82 37

0.305 0.000

0.000 0.541

0.573 0.135

0.122 0.324

0.965 0.946

gemini-2.5-flash

Level 0-1 Level 2

92 44

0.359 0.114

0.000 0.705

0.435 0.023

0.207 0.159

0.898 0.923

gemini-2.5-pro

Level 0-1 Level 2

93 48

0.323 0.000

0.000 0.479

0.430 0.208

0.247 0.312

0.889 0.979

gpt-5.4-nano

Level 0-1 Level 2

12 10

0.000 0.000

0.000 0.000

0.417 0.000

0.583 1.000

1.000 1.000

gpt-5.4-mini

Level 0-1 Level 2

65 24

0.138 0.000

0.000 0.292

0.569 0.083

0.292 0.625

1.000 0.958

gpt-5.4

Level 0-1 Level 2

91 41

0.319 0.122

0.000 0.390

0.451 0.195

0.231 0.293

1.000 1.000

gpt-5.4_low

Level 0-1 Level 2

96 45

0.323 0.111

0.000 0.444

0.552 0.111

0.125 0.333

1.000 1.000

gpt-5.4_medium

Level 0-1 Level 2

95 45

0.432 0.222

0.000 0.378

0.484 0.178

0.084 0.222

0.981 0.971

gpt-5.4_high

Level 0-1 Level 2

85 44

0.400 0.068

0.000 0.386

0.424 0.227

0.176 0.318

0.922 0.976

Overall

Level 0–2

1285

0.216

0.163

0.370

0.251

0.865

32

Table 10: k = 0 null-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 is n = 5, too few for a useful interval. Models are sorted as in Figure 4. The bottom row aggregates across all 155 null sessions. Model

n

TN

FP

Specificity

Probes

ministral-3b-2512 magistral-small-2509 ministral-8b-2512 mistral-medium-2508 ministral-14b-2512 mistral-small-2603 gemini-2.5-pro gpt-5.4-nano gpt-5.4-mini gpt-5.4_xhigh mistral-medium-3-5 gemini-2.5-flash mistral-large-2512 claude-haiku-4-5 gpt-5.4 magistral-medium-2509 gpt-5.4_high gpt-5.5 gpt-5.4_low claude-sonnet-4-6 gpt-5.5_low gpt-5.4_medium gpt-5.5_medium gpt-5.5_high gpt-5.5_xhigh claude-sonnet-4-6_low claude-sonnet-4-6_high claude-opus-4-7_high gemini-3.1-pro-preview gemini-3.5-flash simple_reflex_agent

5 5 5 5 5 5 5 5 5 5 5 5 5 5 5 5 5 5 5 5 5 5 5 5 5 5 5 5 5 5 5

1 2 5 5 5 5 4 5 5 2 3 3 4 5 5 5 5 5 5 5 5 5 5 5 5 5 5 5 5 5 5

4 3 0 0 0 0 1 0 0 3 2 2 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0

0.20 0.40 1.00 1.00 1.00 1.00 0.80 1.00 1.00 0.40 0.60 0.60 0.80 1.00 1.00 1.00 1.00 1.00 1.00 1.00 1.00 1.00 1.00 1.00 1.00 1.00 1.00 1.00 1.00 1.00 1.00

65.0 28.0 65.0 65.0 65.0 65.0 61.0 6.4 15.2 27.4 65.0 62.8 65.0 63.8 26.6 39.2 26.0 33.6 20.4 65.0 28.4 22.4 41.2 52.4 50.0 63.2 61.0 54.0 56.2 64.0 14.0

155

139

16

0.90

46.4

Overall

33

Budget exhausted

Table 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. k consists of n mutation sets. Metrics are exact correctness V , kernel detection VK , exact attribution VA , Jaccard partial credit VAJ , conditional attribution correctness VA |VK = 1, precision and recall of attribution, and probing efficiency respresented by EELX , ratio of used probes P/Pmax , and ratio of in probe budget. Numbers are averaged values per model and k across n mutation sets. k

n

V

VK

VA

VAJ

VA | VK

PrecisionA

RecallA

EELX

P/Pmax

< Pmax

claude-haiku-4-5

1 2+ 3+ 2⊗

30 15 15 5

0.30 0.00 0.00 0.20

0.97 0.47 0.87 1.00

0.30 0.00 0.00 0.20

0.33 0.17 0.22 0.50

0.31 0.00 0.00 0.20

0.33 0.17 0.22 0.50

0.37 0.17 0.22 0.50

0.37 0.00 0.00 0.24

0.83 0.79 0.78 0.88

0.90 0.80 1.00 1.00

claude-sonnet-4-6

1 2+ 3+ 2⊗

30 15 15 5

0.33 0.33 0.00 0.40

1.00 0.87 0.80 1.00

0.33 0.33 0.00 0.40

0.53 0.46 0.41 0.67

0.33 0.38 0.00 0.40

0.53 0.46 0.41 0.67

0.73 0.47 0.42 0.70

0.33 0.33 0.00 0.40

1.00 1.00 1.00 1.00

0.00 0.07 0.07 0.00

claude-sonnet-4-6_low

1 2+ 3+ 2⊗

30 15 15 5

0.57 0.33 0.20 0.00

1.00 0.67 0.87 1.00

0.57 0.33 0.20 0.00

0.62 0.39 0.46 0.50

0.57 0.50 0.23 0.00

0.62 0.39 0.46 0.50

0.67 0.40 0.47 0.50

0.78 0.46 0.28 0.00

0.59 0.77 0.67 0.69

0.93 0.60 0.87 1.00

claude-sonnet-4-6_high

1 2+ 3+ 2⊗

30 15 15 5

0.67 0.33 0.27 0.00

1.00 0.67 0.87 1.00

0.67 0.33 0.27 0.00

0.72 0.36 0.57 0.50

0.67 0.50 0.31 0.00

0.72 0.36 0.57 0.50

0.77 0.37 0.58 0.50

0.91 0.45 0.37 0.00

0.62 0.72 0.68 0.60

1.00 0.80 0.87 1.00

claude-opus-4-7_high

1 2+ 3+ 2⊗

30 15 15 5

0.83 0.27 0.13 0.00

1.00 0.93 1.00 1.00

0.83 0.27 0.13 0.00

0.83 0.51 0.51 0.50

0.83 0.29 0.13 0.00

0.83 0.51 0.51 0.50

0.83 0.57 0.53 0.50

1.21 0.40 0.20 0.00

0.42 0.45 0.35 0.68

1.00 1.00 1.00 1.00

gemini-2.5-flash

1 2+ 3+ 2⊗

30 15 15 5

0.23 0.00 0.00 0.20

0.93 0.73 0.73 0.80

0.23 0.00 0.00 0.20

0.26 0.19 0.20 0.30

0.25 0.00 0.00 0.25

0.26 0.19 0.20 0.30

0.30 0.20 0.27 0.30

0.33 0.00 0.00 0.29

0.42 0.43 0.49 0.41

1.00 1.00 0.93 1.00

34

Model

Continued on next page

Table 11: (continued) k

n

V

VK

VA

VAJ

VA | VK

PrecisionA

RecallA

EELX

P/Pmax

< Pmax

gemini-2.5-pro

1 2+ 3+ 2⊗

30 15 15 5

0.10 0.00 0.00 0.20

0.97 0.87 0.93 1.00

0.10 0.00 0.00 0.20

0.19 0.22 0.39 0.50

0.10 0.00 0.00 0.20

0.19 0.22 0.39 0.50

0.30 0.27 0.44 0.50

0.15 0.00 0.00 0.29

0.32 0.37 0.35 0.25

1.00 1.00 1.00 1.00

gemini-3.1-pro-preview

1 2+ 3+ 2⊗

30 15 15 5

0.80 0.33 0.40 0.00

1.00 1.00 1.00 1.00

0.80 0.33 0.40 0.00

0.80 0.61 0.64 0.47

0.80 0.33 0.40 0.00

0.80 0.61 0.64 0.47

0.80 0.67 0.64 0.50

1.10 0.47 0.59 0.00

0.58 0.60 0.48 0.61

1.00 1.00 1.00 1.00

gemini-3.5-flash

1 2+ 3+ 2⊗

30 15 15 5

0.97 0.40 0.33 0.00

1.00 0.67 0.73 1.00

0.97 0.40 0.33 0.00

0.97 0.49 0.47 0.00

0.97 0.60 0.45 0.00

0.97 0.49 0.47 0.00

0.97 0.53 0.47 0.00

1.36 0.59 0.50 0.00

0.49 0.60 0.55 0.44

0.90 1.00 0.87 1.00

gpt-5.4

1 2+ 3+ 2⊗

30 15 15 5

0.30 0.13 0.00 0.00

1.00 0.67 0.67 1.00

0.30 0.13 0.00 0.00

0.32 0.23 0.21 0.30

0.30 0.20 0.00 0.00

0.32 0.23 0.21 0.30

0.33 0.23 0.22 0.30

0.45 0.20 0.00 0.00

0.17 0.18 0.20 0.15

1.00 1.00 1.00 1.00

gpt-5.4-mini

1 2+ 3+ 2⊗

30 15 15 5

0.10 0.00 0.00 0.00

0.40 0.40 0.33 0.20

0.10 0.00 0.00 0.00

0.12 0.23 0.16 0.00

0.25 0.00 0.00 0.00

0.12 0.23 0.16 0.00

0.13 0.23 0.16 0.00

0.15 0.00 0.00 0.00

0.17 0.17 0.16 0.20

1.00 1.00 1.00 1.00

gpt-5.4-nano

1 2+ 3+ 2⊗

30 15 15 5

0.07 0.00 0.00 0.00

0.30 0.33 0.00 0.00

0.07 0.00 0.00 0.00

0.07 0.10 0.04 0.00

0.22 0.00 nan nan

0.07 0.10 0.04 0.00

0.07 0.10 0.04 0.00

0.10 0.00 0.00 0.00

0.09 0.08 0.10 0.09

1.00 1.00 1.00 1.00

gpt-5.4_low

1 2+ 3+ 2⊗

30 15 15 5

0.23 0.13 0.33 0.00

1.00 0.67 0.73 1.00

0.23 0.13 0.33 0.00

0.33 0.27 0.42 0.27

0.23 0.20 0.45 0.00

0.33 0.27 0.42 0.27

0.43 0.37 0.42 0.30

0.35 0.20 0.50 0.00

0.21 0.23 0.24 0.18

1.00 1.00 1.00 1.00

35

Model

Continued on next page

Table 11: (continued) k

n

V

VK

VA

VAJ

VA | VK

PrecisionA

RecallA

EELX

P/Pmax

< Pmax

gpt-5.4_medium

1 2+ 3+ 2⊗

30 15 15 5

0.40 0.00 0.33 0.00

1.00 0.67 0.73 1.00

0.40 0.00 0.33 0.00

0.48 0.19 0.41 0.33

0.40 0.00 0.45 0.00

0.48 0.19 0.41 0.33

0.57 0.33 0.42 0.40

0.59 0.00 0.50 0.00

0.33 0.31 0.30 0.38

1.00 1.00 1.00 1.00

gpt-5.4_high

1 2+ 3+ 2⊗

30 15 15 5

0.27 0.00 0.33 0.00

0.97 0.73 0.73 1.00

0.27 0.00 0.33 0.00

0.35 0.22 0.47 0.40

0.28 0.00 0.45 0.00

0.35 0.22 0.47 0.40

0.43 0.33 0.47 0.40

0.39 0.00 0.50 0.00

0.42 0.37 0.34 0.43

1.00 1.00 1.00 1.00

gpt-5.4_xhigh

1 2+ 3+ 2⊗

30 15 15 5

0.10 0.00 0.27 0.00

0.57 0.47 0.53 0.20

0.10 0.00 0.27 0.00

0.10 0.07 0.31 0.00

0.18 0.00 0.50 0.00

0.10 0.07 0.31 0.00

0.10 0.10 0.31 0.00

0.14 0.00 0.40 0.00

0.28 0.26 0.28 0.24

1.00 1.00 1.00 1.00

gpt-5.5

1 2+ 3+ 2⊗

30 15 15 5

0.37 0.13 0.00 0.00

1.00 0.73 1.00 1.00

0.37 0.13 0.00 0.00

0.40 0.25 0.18 0.30

0.37 0.18 0.00 0.00

0.40 0.25 0.18 0.30

0.43 0.27 0.18 0.30

0.55 0.20 0.00 0.00

0.20 0.25 0.19 0.21

1.00 1.00 1.00 1.00

gpt-5.5_low

1 2+ 3+ 2⊗

30 15 15 5

0.30 0.33 0.13 0.00

1.00 0.67 0.73 1.00

0.30 0.33 0.13 0.00

0.38 0.37 0.28 0.10

0.30 0.50 0.18 0.00

0.38 0.37 0.28 0.10

0.47 0.40 0.31 0.10

0.45 0.50 0.20 0.00

0.22 0.28 0.26 0.23

1.00 1.00 1.00 1.00

gpt-5.5_medium

1 2+ 3+ 2⊗

30 15 15 5

0.43 0.00 0.33 0.00

1.00 0.73 0.87 1.00

0.43 0.00 0.33 0.00

0.45 0.28 0.43 0.40

0.43 0.00 0.38 0.00

0.45 0.28 0.43 0.40

0.47 0.40 0.44 0.40

0.64 0.00 0.50 0.00

0.36 0.47 0.36 0.42

1.00 1.00 1.00 1.00

gpt-5.5_high

1 2+ 3+ 2⊗

30 15 15 5

0.40 0.33 0.33 0.00

1.00 0.73 0.87 1.00

0.40 0.33 0.33 0.00

0.40 0.48 0.49 0.50

0.40 0.45 0.38 0.00

0.40 0.48 0.49 0.50

0.40 0.53 0.49 0.50

0.59 0.49 0.50 0.00

0.45 0.57 0.42 0.42

1.00 1.00 1.00 1.00

36

Model

Continued on next page

Table 11: (continued) k

n

V

VK

VA

VAJ

VA | VK

PrecisionA

RecallA

EELX

P/Pmax

< Pmax

gpt-5.5_xhigh

1 2+ 3+ 2⊗

30 15 15 5

0.43 0.40 0.33 0.00

0.90 0.67 0.67 1.00

0.43 0.40 0.33 0.00

0.45 0.47 0.38 0.50

0.48 0.60 0.50 0.00

0.45 0.47 0.38 0.50

0.47 0.47 0.38 0.50

0.61 0.57 0.50 0.00

0.61 0.64 0.46 0.53

1.00 1.00 1.00 1.00

magistral-medium-2509

1 2+ 3+ 2⊗

30 15 15 5

0.30 0.13 0.00 0.00

0.90 0.80 0.93 0.80

0.30 0.13 0.00 0.00

0.38 0.32 0.30 0.27

0.33 0.17 0.00 0.00

0.38 0.32 0.30 0.27

0.47 0.37 0.36 0.30

0.44 0.19 0.00 0.00

0.41 0.46 0.36 0.48

1.00 1.00 1.00 1.00

magistral-small-2509

1 2+ 3+ 2⊗

30 15 15 5

0.07 0.00 0.00 0.00

0.43 0.87 0.47 0.80

0.10 0.00 0.00 0.00

0.12 0.21 0.14 0.07

0.15 0.00 0.00 0.00

0.12 0.21 0.14 0.07

0.13 0.23 0.18 0.10

0.10 0.00 0.00 0.00

0.26 0.19 0.30 0.12

0.97 1.00 0.87 1.00

ministral-3b-2512

1 2+ 3+ 2⊗

30 15 15 5

0.00 0.00 0.00 0.00

0.40 0.33 0.47 0.40

0.00 0.00 0.00 0.00

0.00 0.03 0.00 0.00

0.00 0.00 0.00 0.00

0.00 0.03 0.00 0.00

0.00 0.03 0.00 0.00

0.00 0.00 0.00 0.00

0.93 0.94 1.00 1.00

0.10 0.07 0.00 0.00

ministral-8b-2512

1 2+ 3+ 2⊗

30 15 15 5

0.00 0.00 0.00 0.00

0.13 0.00 0.00 0.00

0.03 0.00 0.00 0.00

0.03 0.00 0.07 0.00

0.00 nan nan nan

0.03 0.00 0.07 0.00

0.03 0.00 0.07 0.00

0.00 0.00 0.00 0.00

1.00 0.98 1.00 1.00

0.00 0.07 0.07 0.00

ministral-14b-2512

1 2+ 3+ 2⊗

30 15 15 5

0.00 0.00 0.00 0.00

0.17 0.00 0.33 0.00

0.00 0.00 0.00 0.00

0.00 0.00 0.09 0.00

0.00 nan 0.00 nan

0.00 0.00 0.09 0.00

0.00 0.00 0.09 0.00

0.00 0.00 0.00 0.00

1.00 1.00 1.00 1.00

0.00 0.00 0.00 0.00

mistral-large-2512

1 2+ 3+ 2⊗

30 15 15 5

0.27 0.00 0.00 0.00

0.63 0.47 0.53 0.80

0.37 0.00 0.00 0.00

0.37 0.23 0.13 0.20

0.42 0.00 0.00 0.00

0.37 0.23 0.13 0.20

0.37 0.23 0.13 0.20

0.37 0.00 0.00 0.00

0.42 0.38 0.38 0.41

0.93 0.93 0.80 0.80

37

Model

Continued on next page

Table 11: (continued)

38

Model

k

n

V

VK

VA

VAJ

VA | VK

PrecisionA

RecallA

EELX

P/Pmax

< Pmax

mistral-medium-2508

1 2+ 3+ 2⊗

30 15 15 5

0.00 0.00 0.00 0.00

0.13 0.13 0.07 0.00

0.00 0.00 0.00 0.00

0.00 0.03 0.07 0.00

0.00 0.00 0.00 nan

0.00 0.03 0.07 0.00

0.00 0.03 0.07 0.00

0.00 0.00 0.00 0.00

0.98 0.97 0.89 1.00

0.07 0.13 0.13 0.00

mistral-medium-3-5

1 2+ 3+ 2⊗

30 15 15 5

0.13 0.07 0.07 0.00

0.67 0.87 0.73 0.60

0.13 0.07 0.07 0.00

0.16 0.24 0.34 0.20

0.20 0.08 0.09 0.00

0.16 0.24 0.34 0.20

0.20 0.30 0.36 0.20

0.16 0.07 0.09 0.00

0.88 0.80 0.82 1.00

0.43 0.40 0.53 0.00

mistral-small-2603

1 2+ 3+ 2⊗

30 15 15 5

0.07 0.00 0.00 0.00

0.47 0.67 0.60 0.40

0.10 0.00 0.00 0.00

0.14 0.15 0.18 0.20

0.14 0.00 0.00 0.00

0.14 0.15 0.18 0.20

0.20 0.17 0.18 0.20

0.08 0.00 0.00 0.00

0.73 0.57 0.72 0.82

0.57 0.73 0.47 0.40

simple_reflex_agent

1 2+ 3+ 2⊗

30 15 15 5

1.00 1.00 1.00 0.00

1.00 1.00 1.00 1.00

1.00 1.00 1.00 0.00

1.00 1.00 1.00 0.50

1.00 1.00 1.00 0.00

1.00 1.00 1.00 0.50

1.00 1.00 1.00 0.50

1.50 1.50 1.50 0.00

0.22 0.22 0.22 0.22

1.00 1.00 1.00 1.00

Supporting figures. A visualization of the detection–attribution gap in the “Ladder” experiment is shown in Figure 8. Impact of reasoning effort in the “Benchmark” experiment is shown in Figure 7. Figure 9 shows the detailed performance results as bar plots across the benchmark panel. The k = 1 → k = 2 cliff is universal; cross-family scaling helps at k = 1 but flattens at k ≥ 2, where attribution becomes the binding constraint. Probing behaviour of LLMs is shown in Figure 10 for different success–failure modes.

GPT-5.4

GPT-5.5

Claude Sonnet 4.6

Experiment types k=0 k=1 k = 2+ k = 3+ k = 2 interacting mean

1.0

Performance V

0.8 0.6 0.4 0.2 0.0 none

low medium high

xhigh

none

low medium high

xhigh

none

low

high

Reasoning effort

0.86

0.88

0.94

0.71

0.89

0.93

0.87

0.87

GPT-5.4 (Medium)

1.00

0.89

0.83

1.00

0.86

0.86

1.00

1.00

GPT-5.4 (Low)

1.00

0.89

0.91

1.00

0.89

0.86

1.00

1.00

GPT-5.4

1.00

0.77

0.78

1.00

0.80

0.74

1.00

0.87

1.00

1.0

GPT-5.4 (High)

0.78

0.52

0.55

0.49

0.26

0.09

0.33

0.20

0.00

1.00

GPT-5.4 (Medium)

0.71

0.49

0.51

0.49

0.40

0.20

0.33

0.33

0.20

1.00

GPT-5.4 (Low)

0.72

0.55

0.37

0.31

0.34

0.14

0.33

0.20

0.00

GPT-5.4

0.74

0.37

0.31

0.54

0.14

0.11

0.27

0.07

0.07

0.8

GPT-5.4 Mini

0.63

0.55

0.52

0.71

0.51

0.51

0.87

0.60

0.40

GPT-5.4 Nano

0.34

0.09

0.09

0.03

0.17

0.17

0.07

0.27

0.27

0.6

Gemini 2.5 Pro

0.98

0.92

0.85

0.97

0.89

0.94

0.87

1.00

1.00

Gemini 2.5 Flash

1.00

0.86

0.77

0.91

0.91

0.89

0.87

1.00

0.87

Claude Haiku 4.5

0.97

0.71

0.65

0.86

0.69

0.69

1.00

0.87

0.87

Mistral Large 3

0.75

0.45

0.60

0.83

0.49

0.60

0.87

0.73

1.00

Ministral 3 14B

0.29

0.20

0.32

0.37

0.20

0.49

0.47

0.13

0.47

Ministral 3 8B

0.20

0.25

0.18

0.17

0.34

0.20

0.07

0.40

Ministral 3 3B

0.54

0.28

0.29

0.37

0.14

0.37

0.40

0.13

Model family Mistral Claude Google OpenAI

k = 2+

Experiment type (harder )

0.48

0.26

0.22

0.37

0.09

0.00

0.00

0.07

0.00

0.34

0.02

0.05

0.00

0.00

0.00

0.00

0.00

0.00

Gemini 2.5 Pro

0.62

0.51

0.28

0.54

0.09

0.00

0.33

0.27

0.00

Gemini 2.5 Flash

0.62

0.34

0.38

0.49

0.26

0.14

0.33

0.13

0.00

Claude Haiku 4.5

0.75

0.32

0.28

0.49

0.20

0.00

0.27

0.13

0.00

Mistral Large 3

0.69

0.23

0.43

0.43

0.09

0.00

0.13

0.00

0.00

Ministral 3 14B

0.12

0.06

0.06

0.06

0.00

0.00

0.00

0.00

0.00

0.13

Ministral 3 8B

0.42

0.06

0.12

0.17

0.03

0.00

0.00

0.00

0.00

0.27

Ministral 3 3B

0.51

0.02

0.05

0.00

0.00

0.00

0.00

0.00

0.00

l0

e Lev

l1

e Lev

l2

e Lev

l0

e Lev

l1

e Lev

l2

e Lev

l0

e Lev

l1

e Lev

el 0 evel 1 evel 2 evel 0 evel 1 evel 2 evel 0 evel 1 evel 2 Lev L L L L L L L L k=1

0.4

GPT-5.4 Mini GPT-5.4 Nano

0.2

0.0

Model family Mistral Claude Google OpenAI

k=2

(a) Kernel accuracy VK .

e Lev

k=1

k = 2+

Experiment type (harder )

l2

0.8 0.7 0.6 0.5 0.4

VA

1.00

Intra family capability (higher )

GPT-5.4 (High)

VK

Intra family capability (higher )

Figure 7: Impact of inference-time compute in the “Benchmark” experiment gpt-5.4, gpt-5.5, and claude-sonnet-4-6 have been evaluated for the performance impact of their reasoning effort for different mutation cardinality.

0.3 0.2 0.1 0.0

k=2

(b) Mutation accuracy VA .

Figure 8: Per-condition accuracy heatmaps in the “Ladder” experiment of 13 models. The Elements configurations of (model, prompt variant, mutation order). The resulting matrices in (a) and (b) are visibly different. While the monotonicity of kernel accuracy (a) is unclear because the models’ performance saturates early, the mutation accuracy (b) shows the canonical ladders for capability and task difficulty, as seen in Figure 2.

39

Simple Reflex Agent Gemini 3.5 Flash (Preview) Gemini 3.1 Pro (Preview) Claude Sonnet 4.6 (High) Claude Opus 4.7 (High) GPT-5.5 (xHigh) Claude Sonnet 4.6 (Low) GPT-5.5 (High) GPT-5.5 (Medium) GPT-5.5 (Low) GPT-5.4 (Medium) GPT-5.4 (Low) Claude Sonnet 4.6 GPT-5.4 (High) GPT-5.5 Magistral Medium 1.2 GPT-5.4 GPT-5.4 (xHigh) Claude Haiku 4.5 Mistral Medium 3.5 Mistral Large 3 Gemini 2.5 Flash Gemini 2.5 Pro GPT-5.4 Mini GPT-5.4 Nano Magistral Small 1.2 Mistral Small 4 Ministral 3 8B Ministral 3 3B Ministral 3 14B Mistral Medium 3.1

Simple Reflex Agent Gemini 3.5 Flash (Preview) Gemini 3.1 Pro (Preview) Claude Sonnet 4.6 (High) Claude Opus 4.7 (High) GPT-5.5 (xHigh) Claude Sonnet 4.6 (Low) GPT-5.5 (High) GPT-5.5 (Medium) GPT-5.5 (Low) GPT-5.4 (Medium) GPT-5.4 (Low) Claude Sonnet 4.6 GPT-5.4 (High) GPT-5.5 Magistral Medium 1.2 GPT-5.4 GPT-5.4 (xHigh) Claude Haiku 4.5 Mistral Medium 3.5 Mistral Large 3 Gemini 2.5 Flash Gemini 2.5 Pro GPT-5.4 Mini GPT-5.4 Nano Magistral Small 1.2 Mistral Small 4 Ministral 3 8B Ministral 3 3B Ministral 3 14B Mistral Medium 3.1

k=1 k = 2+ k = 3+ mean 0.0

0.2

0.4

0.6

Performance: VK

0.8

k=1 k = 2+ k = 3+ mean 0.0

1.0

(a) Kernel accuracy

0.2

0.4

0.6

Performance: VA|VK = 1

0.8

1.0

(b) Mutation accuracy

Simple Reflex Agent Gemini 3.5 Flash (Preview) Gemini 3.1 Pro (Preview) Claude Sonnet 4.6 (High) Claude Opus 4.7 (High) GPT-5.5 (xHigh) Claude Sonnet 4.6 (Low) GPT-5.5 (High) GPT-5.5 (Medium) GPT-5.5 (Low) GPT-5.4 (Medium) GPT-5.4 (Low) Claude Sonnet 4.6 GPT-5.4 (High) GPT-5.5 Magistral Medium 1.2 GPT-5.4 GPT-5.4 (xHigh) Claude Haiku 4.5 Mistral Medium 3.5 Mistral Large 3 Gemini 2.5 Flash Gemini 2.5 Pro GPT-5.4 Mini GPT-5.4 Nano Magistral Small 1.2 Mistral Small 4 Ministral 3 8B Ministral 3 3B Ministral 3 14B Mistral Medium 3.1

k=1 k = 2+ k = 3+ mean 0.0

0.2

0.4

0.6

0.8

1.0

Performance: EELX

1.2

1.4

(c) Probing efficiency

Figure 9: “Benchmark” leaderboard: per-model VK , VA |VK = 1, and EELX across the difficulty levels.

40

Probe Counts vs. Success Categories of Top-2 Models k=1 k=2 k=3

Success Category

K A

K A

K A

0 10 20 30 40 50 60

0 10 20 30 40 50 60

0 10 20 30 40 50 60

Probe Count Pmax = 65 Claude

Model Family Google OpenAI

Mistral

Figure 10: Probe count distribution vs. correctness level for the Top-2 models per family in “Benchmark”.

41

D

System prompts

The four prompt levels reported in Section 4 correspond to the following system prompts: Level 0: ladder_single_split_probe and ladder_double_split_probe, extending Level 1 with per-class example probe templates. Level 1: ladder_single_split for k = 1 sessions and ladder_double_split for k = 2 sessions; ontology-aware, k-specific workflow. Level 2: ladder_mix — a single forensic-auditor prompt covering k ∈ {1, 2} without splitting by mutation count. Level 3: stress_test — the wide-panel prompt (k ∈ {0, 1, 2, 3}, Pmax = 65); it omits the workflow and operating-rules guidance and admits a clean kernel. We show the Level 1 (k = 1) prompt as the base and mark where each other level differs in unified-diff style: a @@ Level n @@ header introduces a hunk, green + lines give that level’s version (Level 0’s per-mutation example probes (the concrete probes are redacted in this preprint); Level 2’s unknown 1–2 mutation framing; Level 3’s wide-panel rewordings), and red - lines mark omissions (Level 3 drops the workflow and operating-rules sections and uses Pmax = 65). The # Score block quotes the canonical bonus coefficient 21 (see (1)); all scores are recomputed from the replay logs under the same formula. The k = 2 (double) variants differ only in count and budget wording. # Role You are a precise, parsimonious diagnostician of a dependently typed lambda calculus (LambdaPi-style) using cumulative universe subtyping. You are given access to two black-box kernels, `K_A` and `K_B`, implementing the same surface language. Exactly one kernel is corrupted. The corrupted kernel carries exactly one mutation drawn from the catalog below. Your job is to identify which kernel is damaged and which catalog ID best @@ Level 2 @@ +kernel carries 1 or 2 active mutations drawn from the catalog below. They may +act independently (additively) or interact in ways that modify their combined +effect. +Your job is to identify which kernel is damaged and which catalog ID(s) best explain the observed behavior. @@ Level 3 @@ +the same surface language. At most one kernel is corrupted. A kernel is +corrupted if its output deviates from correct LambdaPi semantics. In case of an +existing corrupted kernel, the corrupted kernel carries 1, 2, or 3 active mutations +drawn from the catalog below. +Your job is to identify whether any kernel is corrupted, which one it is, and +which catalog ID(s) best explain the observed behavior. Work only from behavior. Do not assume any implementation details beyond what is observable through the interface. # Score - maximise E_ELX E_ELX = V × (1 + 0.5 × (1 - (P / P_max)^3)), with `V=1` if the corrupted kernel AND the mutation_id are correct else `V=0`, @@ Level 2 @@ +with`V=1` if the corrupted kernel AND the full mutation_id set are correct else `V=0`, P = total probes issued, `P_max = 50` maximum available probe budget. Complete and exact correctness is mandatory. Each redundant probe strictly reduces score; but finding the corrupted kernel and correct mutation or excluding mutation candidates is much more important. @@ Level 2 @@ +Complete and exact correctness is mandatory. Submitting only a single correct +mutation_id, even though two are active, or vice versa, results in `V=0`. +Two-mutation cases are as likely as one-mutation cases. Each redundant probe

42

+strictly reduces score; but finding the corrupted kernel and correct +mutation(s) or excluding mutation candidates is much more important. @@ Level 3 @@ +with`V=1` if the kernel label AND the full mutation_id set are correct (empty +list [] when no kernel is corrupted) else `V=0`, P = total probes issued, +`P_max = 65` maximum available probe budget. +Complete and exact correctness is mandatory. Submitting only a single correct +mutation_id, even though two are active, or vice versa, results in `V=0`. +Each redundant probe strictly reduces score; but finding the correct solution +is much more important. # Tools - `probe` Sends one LambdaPi source string to both kernels and returns both outputs plus a divergence summary. - `list_context` Shows the current persistent context if you need to inspect prior assumptions/definitions. - `budget_left` Returns remaining probe budget. You start with 50 probes and must submit when the budget drops to 0. @@ Level 3 @@ + Returns remaining probe budget. You start with 65 probes and must submit when the budget drops to 0. - `submit_answer` Final submission. @@ Level 3 @@ - (this level omits the "Mandatory workflow and operational diagnoses strategy" section) # Mandatory workflow and operational diagnoses strategy 1. Probe both kernels with a targeted source string designed to expose a specific mutation class. 2. Read the response: look at `diff` first; if `identical` or `both reject with same error`, redesign before probing again. 3. If consecutive probes return no informative `diff` use this information to narrow candidates by ruling out mutations that would affect the probe's @@ Level 2 @@ + narrow candidate set by ruling out mutations that would affect the probe's mutation class. Do not submit without observed divergence –- absence of divergence based on your current probes can either mean your probes are wrong, not that no mutation exists. 4. Once you see divergence, confirm which kernel is corrupted. The kernel whose output deviates from correct LambdaPi semantics is the corrupted one. 5. Narrow it down to mutation candidates, rule out alternatives, and identify exact mutation by designing hypothesis/mutation candidate specific probes, not just finding the most likely mutation. @@ Level 2 @@ + exact mutation(s) by designing hypothesis/mutation candidate specific + probes, not just finding the most likely mutation(s). 6. Submit only after the solution has been uniquely determined (i.e. corrupted kernel and mutation ID are determined while all other hypotheses have been @@ Level 2 @@ + kernel and mutation set are determined while all other hypotheses have been excluded). @@ Level 3 @@ - (this level omits the "Operating rules" section) # Operating rules - A claimed mutation must be supported by at least one discriminating probe. @@ Level 2 @@ +- Every claimed mutation must be supported by at least one discriminating probe. +- When claiming two mutations, each must be independently evidenced by a + probe designed for its specific mutation class where the other mutation + is not the primary cause. Do not assume one anomaly explains everything.

43

- Never repeat an uninformative probe. - Distinguish rejection from wrong evaluation. Both matter. - If budget drops to zero, while two hypotheses continue to be equally supported, submit the better-evidenced one and document the unresolved ambiguity and the separating probe that would resolve it. @@ Level 2 @@ +- Do not assume more mutations than the evidence requires, but actively test for a second mutation before submitting. @@ Level 3 @@ +Identify the corrupted kernel and active mutations. Submit your answer. # Benchmark language State persists across probes. You start with a fresh state when diagnosis begins. Only valid `assume` and `let` statements without error are retained. Assume ordinary LambdaPi behavior unless a probe shows otherwise extended by a universe hierarchy. A probe consists of any number of `assume` / `let` lines followed by exactly one final `eval` line. Each statement has to be in a single line separated by "\n". ";" is not allowed. ## Statements assume x : T assume x y : T let name = expr let name : Type = expr eval term eval term : type

declare a free variable declare multiple variables of the same type define variable define variable with explicit type annotation evaluate and type-check evaluate with explicit type annotation

## Terms \x -> body forall (x : A). B A -> B f a b term : TypeExpr Type, Type 0, Type 1, ...

lambda abstraction (backslash) dependent product (Pi type) non-dependent function type application by juxtaposition annotation universes hierarchy

## Built-ins Nat Zero Succ n NatElim motive base step n Vec A n Nil A / Cons A n h t VecElim Eq A x y Refl A x EqElim A m rc x y p

natural number type zero (Zero : Nat) successor (Succ Zero : Nat) recursor over Nat length-indexed vector type empty / cons vectors vector eliminator propositional equality type reflexivity proof (Refl Nat Zero : Eq Nat Zero Zero) J eliminator

## Reading probe output Each probe returns a JSON object with fields for each kernel K_A and K_B: sigma "accept" - kernel accepted the term; output is in `result` "reject" - kernel rejected it; error message is in `epsilon` result The pretty-printed value/normal form and type, e.g. "Zero : Nat" epsilon Normalised error string (paths/line numbers stripped) diff Summary of divergence: "identical" - no divergence, probe uninformative "result divergence: A=..., B=..." - evaluation differs "sigma divergence: A=accept, B=reject" - one accepts, one rejects "error divergence: A=..., B=..." - both reject but with different errors @@ Level 3 @@ +Note: sigma divergence (one accepts, one rejects) is as diagnostically meaningful as result +divergence. A probe where both kernels produce identical output or both reject with same

44

error +provides no evidence for or against any mutation –- it neither confirms nor rules out a corrupted +kernel. ## Candidate mutations One mutation is active. Each mutation candidate suggests a different probing strategy. Treat the descriptions below as semantic mutation models, not as implementation hints. Symptoms of mutations, even across categories, may appear identical on shallow probes; IDs with similar symptoms often require a targeted deeper probe to distinguish. @@ Level 0 @@ +For each mutation, there is a probe provided, that is guaranteed to produce +divergence if that mutation is active, and whose specific output pair +(corrupted kernel result vs. correct kernel result) uniquely identifies that +mutation among all candidates. @@ Level 2 @@ +1 or 2 mutations are active. Each mutation candidate suggests a different +probing strategy. Treat the descriptions below as semantic mutation models, +not as implementation hints. Symptoms of mutations, even across categories, +may appear identical on shallow probes; IDs with similar symptoms often require +a targeted deeper probe to distinguish. +Symptoms may be misleading –- what appears to be one mutation could actually be +the result of two mutations interacting with each other, and vice versa. @@ Level 3 @@ +0, 1, 2, or 3 mutations are active. Each mutation candidate suggests a different +probing strategy. Treat the descriptions below as semantic mutation models, +not as implementation hints. ID_01 –- Neutral applications ignore their arguments in definitional equality Symptom: Types indexed by `f a` and `f b` may compare equal whenever the head is the same, even though the arguments differ. @@ Level 0 @@ + Unique probe: <redacted for preprint> ID_02 –- Fail to increment the target index under lambda Symptom: Substitution crosses a binder incorrectly. Substitution into a lambda body may continue targeting the old binding depth instead of shifting to account for the newly introduced variable. A variable intended for an outer binder can incorrectly replace an inner one. @@ Level 0 @@ + Unique probe: <redacted for preprint> ID_03 –- Definitional equality ignores which binder a variable refers to Symptom: Terms or types that differ only by which nearby binder is referenced can be treated as equal. @@ Level 0 @@ + Unique probe: <redacted for preprint> ID_04 –- Index drift in bound lookup Symptom: Bound-variable lookup uses the wrong selection under nested binding. In a term with multiple binders, a function may return or use the wrong bound variable. Multi-argument functions can behave as if one reference points to a nearby outer binder instead of the intended one. @@ Level 0 @@ + Unique probe: <redacted for preprint> ID_05 –- Unknown names behave like a fixed canonical constant Symptom: A free name that should remain with no definition instead collapses computations toward a constant value. Expressions headed by an unknown name normalize further than they should. @@ Level 0 @@ + Unique probe: <redacted for preprint>

45

ID_06 –- Nested functions mix up inner and outer arguments Symptom: Single-argument functions may look fine, but functions returning functions can swap the roles of inner and outer bound values. @@ Level 0 @@ + Unique probe: <redacted for preprint> ID_07 –- Definitional equality in the context where types are being compared @@ Level 3 @@ +ID_07 –- Definitional equality bypass during type comparison Symptom: Type checking accepts terms because structurally different expressions which the type can be read off are treated as definitionally equal even when they should not be. @@ Level 0 @@ + Unique probe: <redacted for preprint> ID_08 –- Function bodies can see a spurious extra value Symptom: Under lambda application, some bound references behave as if an extra unrelated value has appeared in scope. Results may contain a default-like or neutral-looking term where a genuine argument or captured value should have been used. @@ Level 0 @@ + Unique probe: <redacted for preprint> ID_09 –- Function application repeats self-feeding Symptom: A single application can continue by feeding the same argument in again. Terms may reduce one step too far, as if the first result were applied again to the original argument. @@ Level 0 @@ + Unique probe: <redacted for preprint> ID_10 –- Distinct free heads compare definitionally equal Symptom: Two dependent types indexed by different free variables may be treated as interchangeable merely because both heads are unresolved names. @@ Level 0 @@ + Unique probe: <redacted for preprint> ID_11 –- Unknown names behave like identity Symptom: Applying an unknown name to an argument returns that argument, as if the missing head were an identity function. Applications with no definition simplify when they should remain neutral. @@ Level 0 @@ + Unique probe: <redacted for preprint> ID_12 –- Universe stratification collapses Symptom: Universe typing is too permissive. Universes become self-typed instead of stratified. A universe may be accepted at its own level instead of only at a higher one. The system behaves as though `Type n : Type n` instead of `Type n+1`. @@ Level 0 @@ + Unique probe: <redacted for preprint> ID_13 –- Function application ignores its argument Symptom: Applying a function can produce a result that does not depend on the supplied argument even when it obviously should. @@ Level 0 @@ + Unique probe: <redacted for preprint> ## Submission format Call `submit_answer` with: corrupted_kernel "A" or "B" –- the kernel whose output deviates from correct LambdaPi semantics. mutation_ids list of one ID, e.g. ["ID_03"], that best explains the observed behavior. @@ Level 2 @@ + mutation_ids list of one or two IDs, e.g. ["ID_02"] or ["ID_01","ID_03"], that best

46

explain the observed behavior. @@ Level 3 @@ + corrupted_kernel "A" or "B" –- the kernel whose output deviates from correct LambdaPi semantics, or "neither" + mutation_ids list of one, two, or three IDs, e.g. ["ID_02"], ["ID_01","ID_03"], or ["ID_01","ID_03","ID_12"], that best explain the observed behavior. If no kernel is corrupted, submit an empty list. justification concise probe-based argument naming which kernel produced which behavior. @@ Level 2 @@ + If a combined mutation effect produces a symptom that is not individually described + by either ID, note this in justification. minimal_probe The SHORTEST source string in which you observed divergence. @@ Level 3 @@ + Provide evidence for every claimed mutation. + minimal_probe The SHORTEST source string in which you observed divergence. If no divergence was observed, submit the shortest probe. explanatory_probe Cite a second probe you already ran that confirms the semantic consequence - e.g. a computation that gives a provably wrong answer on the corrupted kernel.

47

E

Failure Case Traces

We provide three annotated failure traces from the k = 2 Level 2 (double_mix) condition, each showing the same canonical failure mode reported in Section 5: the agent correctly identifies the corrupted kernel, but submits only one of the two active mutations. Traces were selected by analysis/pick_failure_traces.py from results_260520/records.csv subject to (V = 0, VK = 1, kground truth = 2, ksubmission = 1); one is drawn per model family. gpt-5.4 — under-reporting at k = 2. • Ground truth: corrupted kernel KB , mutations {ID_01, ID_03}. • Submission: corrupted kernel KB , mutations {ID_01} after 28 probes. First 8 probes (source ⇒ divergence): [1] eval Type 0 : Type 0 => both reject with same error [2] assume A : Type \n assume x y : A \n eval (\z -> z) x : A => both reject with same error [3] assume A : Type \n assume x : A \n eval ((\z -> z) : A -> A) x => identical [4] assume A : Type \n assume x y : A \n eval (((\u -> \v -> u) : A -> A -> A) x) y => identical [5] assume A : Type \n assume x y : A \n eval (((\u -> \v -> v) : A -> A -> A) x) y => identical [6] assume A : Type \n assume x y : A \n eval (((\u -> \v -> u v) : (A -> A) -> A -> A) (\w -> w : A -> A)) x => both reject with same error [7] assume A : Type \n assume f : A -> A \n assume x : A \n eval f x => identical [8] assume A : Type \n assume x y : A \n eval (((\u -> \v -> u) : A -> A -> A) y) x : A => identical

claude-haiku-4-5 — under-reporting at k = 2. • Ground truth: corrupted kernel KB , mutations {ID_02, ID_06}. • Submission: corrupted kernel KB , mutations {ID_02} after 40 probes. First 8 probes (source ⇒ divergence): [1] eval Zero : Nat => identical [2] eval Succ Zero : Nat => identical [3] assume f : Nat -> Nat \n assume x : Nat \n eval f x => identical [4] assume f : Nat -> Nat -> Nat \n assume x y : Nat \n eval f x y => identical [5] eval \x -> x : Nat -> Nat => both reject with same error [6] eval (\x -> x) : Nat -> Nat => identical [7] eval ((\x -> x) Zero) : Nat => both reject with same error [8] eval (((\x -> x) : Nat -> Nat) Zero) => identical

48

gemini-2.5-flash — under-reporting at k = 2. • Ground truth: corrupted kernel KA , mutations {ID_02, ID_08}. • Submission: corrupted kernel KA , mutations {ID_02} after 17 probes. First 8 probes (source ⇒ divergence): [1] eval Nat => identical [2] eval Zero : Nat => identical [3] eval \x : Nat -> x : Nat -> Nat => both reject with same error [4] eval \x : Nat -> x => both reject with same error [5] eval Nat -> Nat => identical [6] eval \x -> x : Nat -> Nat => both reject with same error [7] eval (\x -> x) : Nat -> Nat => identical [8] eval Type 0 : Type 0 => both reject with same error

Reading the traces. In each session the divergence signal is observable within the first 4– 8 probes, 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: the model finds a consistent explanation, not the complete one.

49