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

arXiv: https://arxiv.org/abs/2607.12733 · HTML: https://mlsanity.com/paper/2607.12733/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning.
- Builds on 27 of its 65 references that are in the map.
- First posted on arXiv 14 Jul 2026.

## Placed in

- LLM reasoning / [Reasoning benchmarks and evaluation](https://mlsanity.com/lr/reasoning-benchmarks-and-evaluation/)

## Builds on (most cited first, 27 of 27)

- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [Let's Verify Step by Step](https://mlsanity.com/paper/2305.20050/) (2023)
- [Tree of Thoughts: Deliberate Problem Solving with Large Language Models](https://mlsanity.com/paper/2305.10601/) (2023)
- [GPQA: A Graduate-Level Google-Proof Q&A Benchmark](https://mlsanity.com/paper/2311.12022/) (2023)
- [GAIA: a benchmark for General AI Assistants](https://mlsanity.com/paper/2311.12983/) (2023)
- [GSM-Symbolic: Understanding the Limitations of Mathematical Reasoning in Large Language Models](https://mlsanity.com/paper/2410.05229/) (2024)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Abductive Commonsense Reasoning](https://mlsanity.com/paper/1908.05739/) (2019)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [LiveBench: A Challenging, Contamination-Limited LLM Benchmark](https://mlsanity.com/paper/2406.19314/) (2024)
- [FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AI](https://mlsanity.com/paper/2411.04872/) (2024)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023)
- [FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models](https://mlsanity.com/paper/2505.02735/) (2025)
- [Lean4Lean: Verifying a Typechecker for Lean, in Lean](https://mlsanity.com/paper/2403.14064/) (2024)
- [LLMorpheus: Mutation Testing using Large Language Models](https://mlsanity.com/paper/2404.09952/) (2024)
- [GEAR: A General Evaluation Framework for Abductive Reasoning](https://mlsanity.com/paper/2509.24096/) (2025)
- [Better Debugging: Combining Static Analysis and LLMs for Explainable Crashing Fault Localization](https://mlsanity.com/paper/2408.12070/) (2024)
- [Wiring the 'Why': A Unified Taxonomy and Survey of Abductive Reasoning in LLMs](https://mlsanity.com/paper/2604.08016/) (2026)
- [Integrating Various Software Artifacts for Better LLM-based Bug Localization and Program Repair](https://mlsanity.com/paper/2412.03905/) (2024)
- [Do Language Models Follow Occam's Razor? An Evaluation of Parsimony in Inductive and Abductive Reasoning](https://mlsanity.com/paper/2509.03345/) (2025)
- [MILE: A Mutation Testing Framework of In-Context Learning Systems](https://mlsanity.com/paper/2409.04831/) (2024)
- [Test Case Generation from Bug Reports via Large Language Models: A Cognitive Layered Evaluation Framework](https://mlsanity.com/paper/2510.05365/) (2025)
- [Evaluating LLM-Based Test Generation Under Software Evolution](https://mlsanity.com/paper/2603.23443/) (2026)
- [Touring the MetaCoq Project (Invited Paper)](https://mlsanity.com/paper/2107.07670/) (2021)

## Abstract (arXiv)

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 lambda-calculus, and a potentially mutated counterpart, agents must determine whether a mutation has occurred and infer the rule modifications responsible for the resulting behavioral differences. Evaluating frontier and mid-tier LLMs reveals a consistent detection-attribution dissociation: models often recognize that a system has been altered but struggle to identify the latent mutations causing the observed discrepancies. Performance degrades substantially under interacting mutations, where models frequently recover only a subset of the underlying mutations. Preliminary evidence also suggests diminishing returns from increased inference-time reasoning, with only modest improvements under larger reasoning budgets, though this finding requires further validation.