LLMs versus the Halting Problem: Revisiting Program Termination Prediction

TL;DR

This paper evaluates large language models' ability to predict program termination, showing they perform well but struggle with complex programs and providing proofs, highlighting their potential and limitations in reasoning about undecidable problems.

Contribution

The study demonstrates that LLMs can effectively predict program termination, approaching the performance of specialized tools, and explores their limitations in proof generation and handling complex programs.

Findings

LLMs perform remarkably well at predicting termination, close to top tools.

Performance drops with increased program length and complexity.

LLMs often fail to produce valid proofs or witnesses for termination.

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 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 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 and complexity increases. We hope these insights motivate further research into program termination and the broader potential of LLMs for reasoning about undecidable problems.