論文の概要: LLMs versus the Halting Problem: Revisiting Program Termination Prediction

• arxiv url: http://arxiv.org/abs/2601.18987v1
• Date: Mon, 26 Jan 2026 21:44:12 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-01-28 15:26:51.080601
• Title: LLMs versus the Halting Problem: Revisiting Program Termination Prediction
• Title（参考訳）: LLMとハルティング問題:プログラム終了予測の再検討
• Authors: Oren Sultan, Jordi Armengol-Estape, Pascal Kesseli, Julien Vanegue, Dafna Shahaf, Yossi Adi, Peter O'Hearn,
• Abstract要約: プログラムが終了するかどうかを判断することは コンピュータ科学の中心的な問題です 大規模言語モデル(LLM)の最近の成功と進歩は、次の疑問を提起する: LLMはプログラム終了を確実に予測できるか? ソフトウェア検証に関する国際コンペティション(SV-Comp)2025(International Competition on Software Verification, SV-Comp)の終了カテゴリから, C プログラムの多種多様なセットに対する LLM の評価を行った。
• 参考スコア（独自算出の注目度）: 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.
• Abstract（参考訳）: プログラムが終了するかどうかを決定することは、コンピュータ科学の中心的な問題である。 チューリングの基本的な結果はハルティング問題(英語版)を決定不可能と定義し、全てのプログラムと入力の終了を普遍的に決定するアルゴリズムは存在しないことを示した。 これらのツールは問題固有のアーキテクチャや抽象化に依存しており、通常は特定のプログラミング言語に結びついている。 大規模言語モデル(LLM)の最近の成功と進歩は、次の疑問を提起する: LLMはプログラム終了を確実に予測できるか? 本研究では,国際ソフトウェア検証コンペティション(SV-Comp)2025の終了カテゴリーから,多様なCプログラムのLCMを評価した。 GPT-5とClaude Sonnet-4.5がトップクラスのツール(テスト時間スケーリング)のすぐ後ろでランク付けされ、Code World Model(CWM)が2位のツールのすぐ後ろでランク付けされる。 LLMはプログラム終了を予測するのに効果的であるが、証明として有効な証人を提供するのに失敗することが多い。 さらに、LLMはプログラム長が増加するにつれて性能が低下する。 これらの知見が、プログラム終了のさらなる研究と、決定不能な問題に対する推論のためのLLMの幅広い可能性の動機となることを願っている。

関連論文リスト

• Do AI models help produce verified bug fixes? [62.985237003585674]
  大規模言語モデルは、ソフトウェアバグの修正に使用される。 本稿では,プログラマが大規模言語モデルを用いて,自身のスキルを補完する方法について検討する。 その結果は、プログラムバグに対する保証された修正を提供するAIとLLMの適切な役割への第一歩となる。
  論文  参考訳（メタデータ） (2025-07-21T17:30:16Z)
• ThrowBench: Benchmarking LLMs by Predicting Runtime Exceptions [4.852619858744873]
  大規模言語モデル(LLM)は、コード理解と合成の驚くべき能力を示している。 4つの異なるプログラミング言語で書かれた2,400以上の短いユーザ記述プログラムからなるベンチマークであるThrowBenchを紹介する。 我々は6つの最先端コードLLMのベンチマーク評価を行い、19～38%(F1スコア)の適度なパフォーマンスを確認した。
  論文  参考訳（メタデータ） (2025-03-06T09:22:23Z)
• Can LLMs Reason About Program Semantics? A Comprehensive Evaluation of LLMs on Formal Specification Inference [0.9319432628663639]
  大規模言語モデル(LLM)は、プログラミングタスクの自動化にますます使われています。 本稿では,プログラム意味論におけるLLMの推論能力を評価するためのベンチマークであるFormalBenchを紹介する。 このベンチマークを用いて、一貫した仕様と完全な仕様を合成するLLMの能力を評価した。
  論文  参考訳（メタデータ） (2025-02-22T13:27:31Z)
• Autellix: An Efficient Serving Engine for LLM Agents as General Programs [59.673243129044465]
  大規模言語モデル(LLM)アプリケーションは、単純なチャットボットを超えて、動的で汎用的なエージェントプログラムへと進化している。 既存のLLMサービスシステムは、プログラムと呼び出し間の依存関係を無視し、最適化のための大きな機会を欠いている。 プログラムを第一級市民として扱い、エンドツーエンドのレイテンシを最小限に抑えるLLMサービスシステムであるAutellixを紹介する。
  論文  参考訳（メタデータ） (2025-02-19T18:59:30Z)
• Efficient Tool Use with Chain-of-Abstraction Reasoning [63.08202389132155]
  大規模言語モデル(LLM)は、現実世界の知識に対する推論の基礎となる必要がある。 マルチステップ推論問題におけるツールの実行には,微調整LDMエージェントの課題が残されている。 マルチステップ推論におけるツールの活用方法として, LLM の新しい手法を提案する。
  論文  参考訳（メタデータ） (2024-01-30T21:53:30Z)
• LEVER: Learning to Verify Language-to-Code Generation with Execution [64.36459105535]
  本稿では,プログラムの実行結果の検証を学習することで,言語からコードへの生成を改善するシンプルな手法であるLEVERを提案する。 具体的には、LLMからサンプリングされたプログラムが、自然言語入力、プログラム自体とその実行結果に基づいて正しいか否かを判定するために、検証者を訓練する。 LEVER はベースコード LLMs (4.6% から 10.9% まで) を継続的に改善し、それらすべてに対して新しい最先端の結果を得る。
  論文  参考訳（メタデータ） (2023-02-16T18:23:22Z)
• Fault-Aware Neural Code Rankers [64.41888054066861]
  サンプルプログラムの正しさを予測できる故障認識型ニューラルネットワークローダを提案する。 我々のフォールト・アウェア・ローダは、様々なコード生成モデルのpass@1精度を大幅に向上させることができる。
  論文  参考訳（メタデータ） (2022-06-04T22:01:05Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。