LLMs versus the Halting Problem: Revisiting Program Termination Prediction

• URL: http://arxiv.org/abs/2601.18987v3
• Date: Thu, 29 Jan 2026 04:56:58 GMT
• Title: LLMs versus the Halting Problem: Revisiting Program Termination Prediction
• Authors: Oren Sultan, Jordi Armengol-Estape, Pascal Kesseli, Julien Vanegue, Dafna Shahaf, Yossi Adi, Peter O'Hearn,
• Abstract summary: determining whether a program terminates is a central problem in computer science.<n>Recent success and progress in large language models (LLMs) raises the following question: can LLMs reliably predict program termination?<n>We evaluate LLMs on a diverse set of C programs from the Termination category of the International Competition on Software Verification (SV-Comp) 2025.
• Score: 28.324966803819752
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• Assessing Coherency and Consistency of Code Execution Reasoning by Large Language Models [5.692204231573854]
  This paper proposes CES, a task to evaluate the abilities of LLMs in simulating program execution and using that reasoning in programming tasks.<n>CES introduces the notion of coherence to determine whether the simulation complies with commonsense execution logic, even if the predicted values along the simulations are incorrect.<n>CES also introduces a novel metric to measure reasoning consistency across tests with the same or different prime path coverage in a spectrum: strong, weak, and random.
  arXiv  Detail & Related papers  (2025-10-16T18:48:12Z)
• Do AI models help produce verified bug fixes? [62.985237003585674]
  Large Language Models are used to produce corrections to software bugs.<n>This paper investigates how programmers use Large Language Models to complement their own skills.<n>The results are a first step towards a proper role for AI and LLMs in providing guaranteed-correct fixes to program bugs.
  arXiv  Detail & Related papers  (2025-07-21T17:30:16Z)
• ThrowBench: Benchmarking LLMs by Predicting Runtime Exceptions [4.852619858744873]
  Large Language Models (LLMs) have shown astounding capabilities of code understanding and synthesis.<n>We introduce ThrowBench, a benchmark consisting of over 2,400 short user-written programs written in four different programming languages.<n>We evaluate our benchmark on six state-of-the-art code LLMs and see modest performance ranging from 19 to 38% (F1 score)
  arXiv  Detail & Related papers  (2025-03-06T09:22:23Z)
• Can LLMs Reason About Program Semantics? A Comprehensive Evaluation of LLMs on Formal Specification Inference [0.9319432628663639]
  Large Language Models (LLMs) are increasingly being used to automate programming tasks.<n>This paper introduces FormalBench, a benchmark designed to evaluate LLMs' reasoning abilities on program semantics.<n>Using this benchmark, we evaluated the ability of LLMs in synthesizing consistent and complete specifications.
  arXiv  Detail & Related papers  (2025-02-22T13:27:31Z)
• Autellix: An Efficient Serving Engine for LLM Agents as General Programs [59.673243129044465]
  Large language model (LLM) applications are evolving beyond simple chatbots into dynamic, general-purpose agentic programs.<n>Existing LLM serving systems ignore dependencies between programs and calls, missing significant opportunities for optimization.<n>We introduce Autellix, an LLM serving system that treats programs as first-class citizens to minimize their end-to-end latencies.
  arXiv  Detail & Related papers  (2025-02-19T18:59:30Z)
• Reasoning Runtime Behavior of a Program with LLM: How Far Are We? [25.451857140926943]
  Large language models for code (i.e., code LLMs) have shown strong code understanding and generation capabilities. Code reasoning is one of the most essential abilities of code LLMs. We propose a framework, namely REval, for evaluating code reasoning abilities and consistency of code LLMs with program execution.
  arXiv  Detail & Related papers  (2024-03-25T05:37:16Z)
• Efficient Tool Use with Chain-of-Abstraction Reasoning [63.08202389132155]
  Large language models (LLMs) need to ground their reasoning to real-world knowledge.<n>There remains challenges for fine-tuning LLM agents to invoke tools in multi-step reasoning problems.<n>We propose a new method for LLMs to better leverage tools in multi-step reasoning.
  arXiv  Detail & Related papers  (2024-01-30T21:53:30Z)
• SatLM: Satisfiability-Aided Language Models Using Declarative Prompting [68.40726892904286]
  We propose a new satisfiability-aided language modeling (SatLM) approach for improving the reasoning capabilities of large language models (LLMs) We use an LLM to generate a declarative task specification rather than an imperative program and leverage an off-the-shelf automated theorem prover to derive the final answer. We evaluate SATLM on 8 different datasets and show that it consistently outperforms program-aided LMs in the imperative paradigm.
  arXiv  Detail & Related papers  (2023-05-16T17:55:51Z)
• LEVER: Learning to Verify Language-to-Code Generation with Execution [64.36459105535]
  We propose LEVER, a simple approach to improve language-to-code generation by learning to verify the generated programs with their execution results. Specifically, we train verifiers to determine whether a program sampled from the LLMs is correct or not based on the natural language input, the program itself and its execution results. LEVER consistently improves over the base code LLMs(4.6% to 10.9% with code-davinci) and achieves new state-of-the-art results on all of them.
  arXiv  Detail & Related papers  (2023-02-16T18:23:22Z)
• Fault-Aware Neural Code Rankers [64.41888054066861]
  We propose fault-aware neural code rankers that can predict the correctness of a sampled program without executing it. Our fault-aware rankers can significantly increase the pass@1 accuracy of various code generation models.
  arXiv  Detail & Related papers  (2022-06-04T22:01:05Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.