# LLMs versus the Halting Problem: Characterizing Program Termination Reasoning

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Placed in Reasoning for agents, planning and code, one of 17 directions in LLM reasoning.
- Builds on 17 of its 41 references that are in the map.
- First posted on arXiv 26 Jan 2026.

## Placed in

- LLM reasoning / [Reasoning for agents, planning and code](https://mlsanity.com/lr/reasoning-for-agents-planning-and-code/)

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

- [Qwen3 Technical Report](https://mlsanity.com/paper/2505.09388/) (2025)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [GPT-4o System Card](https://mlsanity.com/paper/2410.21276/) (2024)
- [A Survey of Large Language Models](https://mlsanity.com/paper/2303.18223/) (2023)
- [DeepSeek-V3 Technical Report](https://mlsanity.com/paper/2412.19437/) (2024)
- [A Survey on Large Language Models for Code Generation](https://mlsanity.com/paper/2406.00515/) (2024)
- [GSM-Symbolic: Understanding the Limitations of Mathematical Reasoning in Large Language Models](https://mlsanity.com/paper/2410.05229/) (2024)
- [LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers](https://mlsanity.com/paper/2310.15164/) (2023)
- [LLMs Still Can't Plan; Can LRMs? A Preliminary Evaluation of OpenAI's o1 on PlanBench](https://mlsanity.com/paper/2409.13373/) (2024)
- [CWM: An Open-Weights LLM for Research on Code Generation with World Models](https://mlsanity.com/paper/2510.02387/) (2025)
- [A Survey of Large Language Models for Code: Evolution, Benchmarking, and Future Trends](https://mlsanity.com/paper/2311.10372/) (2023)
- [Have Large Language Models Learned to Reason? A Characterization via 3-SAT Phase Transition](https://mlsanity.com/paper/2504.03930/) (2025)
- [What I cannot execute, I do not understand: Training and Evaluating LLMs on Program Execution Traces](https://mlsanity.com/paper/2503.05703/) (2025)
- [MCP-Solver: Integrating Language Models with Constraint Programming Systems](https://mlsanity.com/paper/2501.00539/) (2024)
- [Combining Constraint Programming Reasoning with Large Language Model Predictions](https://mlsanity.com/paper/2407.13490/) (2024)
- [Reliable Proof Generation with LLMs via Analogical Retrieval and Symbolic Verification: A Case Study in Euclidean Geometry](https://mlsanity.com/paper/2505.14479/) (2025)
- [AProVE: Modular Termination Analysis of Memory-Manipulating C Programs](https://mlsanity.com/paper/2302.02382/) (2023)

## Built on by (most cited first, 2 of 2)

- [Agentic Code Reasoning](https://mlsanity.com/paper/2603.01896/) (2026)
- [Predicting Program Exit Code with LLMs and Programming Language Semantics](https://mlsanity.com/paper/2609.00579/) (2026)

## Abstract (arXiv)

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.