LLMs versus the Halting Problem: Characterizing Program Termination Reasoning
Determining whether a program terminates is a central problem in computer science. Turing's Halting Problem established termination as undecidable, showing that no algorithm can universally determine termination for all programs and inputs. Hence, verification tools approximate termination, sometimes failing to prove or disprove; these tools rely on problem-specific architectures and are usually tied to particular programming languages. Recent advances in LLMs raise a natural question: To what extent can they reason about program termination? We evaluate frontier LLMs on a diverse set of C programs from the International Competition on Software Verification (SV-Comp) 2025. Our results show that GPT-5 and Claude Sonnet-4.5 achieve scores comparable to top-ranked verification tools (with test-time scaling). However, while models often correctly infer whether programs terminate, they frequently fail to construct a witness as formal proof, revealing a gap between semantic recognition and symbolic proof generation. Performance further degrades as code length increases. Beyond witness automaton graphs, we introduce a divergence-precondition formulation that characterizes non-termination conditions as logical constraints. We hope these findings motivate future research on real-world termination benchmarks, neuro-symbolic approaches that combine LLMs with symbolic verification methods, and, more broadly, LLM reasoning on other undecidable problems.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Efficient Transformer-based 3D Object Detection with Dynamic Token Halting
Balancing efficiency and accuracy is a long-standing problem for deploying deep learning models. The trade-off is even more important for real-time safety-critical systems like autonomous vehicles. In this paper, we prop…
3D Object DetectionAutonomous Vehiclesobject-detectionObject DetectionNon-Halting Queries: Exploiting Fixed Points in LLMs
We introduce a new vulnerability that exploits fixed points in autoregressive models and use it to craft queries that never halt, i.e. an LLM output that does not terminate. More precisely, for what we call non-halting q…
Empirically Characterizing Overparameterization Impact on Convergence
A long-held conventional wisdom states that larger models train more slowly when using gradient descent. This work challenges this widely-held belief, showing that larger models can potentially train faster despite the i…
Performance Gains of LLMs With Humans in a World of LLMs Versus Humans
Currently, a considerable research effort is devoted to comparing LLMs to a group of human experts, where the term "expert" is often ill-defined or variable, at best, in a state of constantly updating LLM releases. Witho…
Why Machines Can't Be Moral: Turing's Halting Problem and the Moral Limits of Artificial Intelligence
In this essay, I argue that explicit ethical machines, whose moral principles are inferred through a bottom-up approach, are unable to replicate human-like moral reasoning and cannot be considered moral agents. By utiliz…
Ethics