LLMs versus the Halting Problem: Revisiting Program Termination Prediction

TL;DR

This paper investigates whether large language models (LLMs) can reliably predict program termination, a problem rooted in the undecidability of the Halting Problem. By evaluating open and proprietary LLMs on the SV-Comp 2025 Termination dataset, the authors show that models like GPT-5 and Claude Sonnet-4.5 achieve performance near top symbolic tools, though generating valid non-termination witnesses remains challenging and performance degrades with longer code. The study also introduces a domain-witness alternative for interpretability and demonstrates that LLMs can reason about undecidable properties to a practical degree, suggesting a promising direction for neuro-symbolic termination reasoning. Overall, the results motivate integrating LLMs into termination analysis workflows and exploring hybrid approaches for robust, real-world termination reasoning.

Abstract

Determining whether a program terminates is a central problem in computer science. Turing's foundational result established the Halting Problem as undecidable, showing that no algorithm can universally determine termination for all programs and inputs. Consequently, automatic verification tools approximate termination, sometimes failing to prove or disprove; these tools rely on problem-specific architectures and abstractions, and are usually tied to particular programming languages. Recent success and progress in large language models (LLMs) raises the following question: can LLMs reliably predict program termination? In this work, we evaluate LLMs on a diverse set of C programs from the Termination category of the International Competition on Software Verification (SV-Comp) 2025. Our results suggest that LLMs perform remarkably well at predicting program termination, where GPT-5 and Claude Sonnet-4.5 would rank just behind the top-ranked tool (using test-time-scaling), and Code World Model (CWM) would place just behind the second-ranked tool. While LLMs are effective at predicting program termination, they often fail to provide a valid witness as a proof. Moreover, LLMs performance drops as program length increases. We hope these insights motivate further research into program termination and the broader potential of LLMs for reasoning about undecidable problems.

Figures (13)

• Figure 1: Termination prediction task. Given a program, the task is to predict whether the program halts for all inputs (instantiations of nondeterministic variables). (1) Traditional verification tools like PROTON use multi-component architectures for parsing, input augmentation, and tool-chain management (its architecture image reproduced from metta2024proton under https://creativecommons.org/licenses/by/4.0/). (2) We investigate whether LLMs can match state-of-the-art verification tools, providing a simpler, language-agnostic solution, as illustrated in the example above where the LLM correctly predicts termination. For an example of non-termination see Figure \ref{['fig:witness_example']}.
• Figure 2: LLM non-termination witness prediction. Given a $C$ program, an LLM that predicts non-termination must additionally output a witness automaton as a proof in JSON format (see Figure \ref{['appendix:llm_witness_json']} in the Appendix). The witness automaton models a potentially infinite execution: nodes correspond to program states and edges to transitions. The predicted JSON is converted to GraphML and validated by a witness validator (e.g., UAutomizer). The example illustrates a loop where $i$ is initialized in $[-5,5]$, eventually reaches $0$ (see the assumption on edge E2), and executes indefinitely.
• Figure 3: SV-Comp main results. Mean SV-Comp scores for LLMs (across $100$ bootstraps), top SV-Comp 2025 verification tools, and the max possible scores (minimum score is $-50{,}064$). GPT-5 (TTS) and Claude Sonnet-4.5 (TTS) would place 2nd and 3rd ($3{,}520$ and $3{,}448$), behind the gold medalist PROTON. CWM ranks just below UAutomizer. GPT-4o scores significantly lower: $546$ with TTS, and a negative score without TTS ($-5,145$).
• Figure 4: LLMs mean SV-Comp score vs. code length. Dataset examples are grouped into three equal size bins by code length (measured in tokens using Instruct Llama3 Tokenizer) (x axis). The mean SV-Comp score (y axis) per bin is shown for all models (20 predictions per sample). Scores decrease with code length; GPT-5 leads, followed by Claude and CWM.
• Figure 5: Histogram of input code length in SV-Comp 2025. X axis: code length in tokens. Y axis: frequency in the data. Almost all code samples have at most $20K$ tokens ($\mu=6,080$, $\sigma=10,898$).