論文の概要: LLM For Loop Invariant Generation and Fixing: How Far Are We?
- arxiv url: http://arxiv.org/abs/2511.06552v1
- Date: Sun, 09 Nov 2025 21:47:45 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-11-11 21:18:45.000373
- Title: LLM For Loop Invariant Generation and Fixing: How Far Are We?
- Title（参考訳）: LLM for Loop Invariant Generation and Fixing: どこまで?
- Authors: Mostafijur Rahman Akhond, Saikat Chakraborty, Gias Uddin,
- Abstract要約: ループ不変量の同定は、プログラムの自動安全性評価をサポートするための重要なステップである。
大規模言語モデルの最近の進歩は、多種多様なソフトウェア工学(SE)と形式的検証タスクの可能性を実証している。
本稿では,プログラムの帰納的ループ不変量の推定や誤り不変量の修正において,様々なサイズのオープンソースLLMとクローズドソースLLMの習熟度を評価するための実証的研究を報告する。
- 参考スコア（独自算出の注目度）: 9.510531513586322
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: A loop invariant is a property of a loop that remains true before and after each execution of the loop. The identification of loop invariants is a critical step to support automated program safety assessment. Recent advancements in Large Language Models (LLMs) have demonstrated potential in diverse software engineering (SE) and formal verification tasks. However, we are not aware of the performance of LLMs to infer loop invariants. We report an empirical study of both open-source and closed-source LLMs of varying sizes to assess their proficiency in inferring inductive loop invariants for programs and in fixing incorrect invariants. Our findings reveal that while LLMs exhibit some utility in inferring and repairing loop invariants, their performance is substantially enhanced when supplemented with auxiliary information such as domain knowledge and illustrative examples. LLMs achieve a maximum success rate of 78\% in generating, but are limited to 16\% in repairing the invariant.
- Abstract（参考訳）: ループ不変量はループの実行の前後で真であるループの特性である。
ループ不変量の同定は、プログラムの自動安全性評価をサポートするための重要なステップである。
大規模言語モデル(LLM)の最近の進歩は、多種多様なソフトウェア工学(SE)と形式的検証タスクの可能性を実証している。
しかし、ループ不変量を推測するLLMの性能は認識していない。
本稿では,プログラムの帰納的ループ不変量の推定や誤り不変量の修正において,様々なサイズのオープンソースLLMとクローズドソースLLMの習熟度を評価するための実証的研究を報告する。
その結果,LLMはループ不変量の推論や修復に有効であるが,ドメイン知識やイラストレーション例などの補助情報を補足することで,その性能が大幅に向上することがわかった。
LLMは、生成における最大成功率78\%を達成するが、不変の修復において16\%に制限される。
関連論文リスト
- Reasoning with Confidence: Efficient Verification of LLM Reasoning Steps via Uncertainty Heads [104.9566359759396]
データ駆動の不確実性スコアに基づくステップレベルの推論検証の軽量な代替案を提案する。
本研究は, LLMの内部状態が不確実性を符号化し, 信頼性の高い検証信号として機能することが示唆された。
論文 参考訳（メタデータ） (2025-11-09T03:38:29Z) - LLM-Specific Utility: A New Perspective for Retrieval-Augmented Generation [110.610512800947]
Retrieval-augmented Generation (RAG)は、外部知識を取り入れた大規模言語モデル(LLM)を強化する。
既存の研究はしばしばユーティリティをジェネリック属性として扱い、異なるLLMが同じ通路から異なる利益をもたらすという事実を無視している。
論文 参考訳（メタデータ） (2025-10-13T12:57:45Z) - InvBench: Can LLMs Accelerate Program Verification with Invariant Synthesis? [13.240989975977302]
不変合成におけるLCMの評価のための原理的フレームワークを提案する。
提案手法は,形式的な音質保証を備えた検証器に基づく決定手順を用いる。
我々は,従来の解法UAutomizerに対して,最先端のLLMと既存のLLMベースの検証器を7つ評価した。
論文 参考訳（メタデータ） (2025-09-25T21:47:02Z) - Efficient Real-time Refinement of Language Model Text Generation [65.1937138219008]
大規模言語モデル(LLM)は、幅広い自然言語タスクにおいて顕著な性能を示している。
重要な課題は、時に事実的に誤った答えを生じさせることである。
本稿では,LLM出力の検証と改善の効率化を目的とした新しい手法であるStreaming-VRを提案する。
論文 参考訳（メタデータ） (2025-01-14T03:59:48Z) - Provenance: A Light-weight Fact-checker for Retrieval Augmented LLM Generation Output [49.893971654861424]
検索強化生成(RAG)から非実効出力を検出する軽量な手法を提案する。
私たちは、二項決定を下すためにしきい値にできる事実性スコアを計算します。
実験の結果, ROC曲線 (AUC) の下では, 関連するオープンソースデータセットの広範囲にわたって高い面積を示すことができた。
論文 参考訳（メタデータ） (2024-11-01T20:44:59Z) - Finding Inductive Loop Invariants using Large Language Models [14.846222005558666]
帰納ループ不変量を見つけることは決定不可能な問題である。
実用化に向けた長い研究の歴史にもかかわらず、解決された問題には程遠い。
本稿では,新たなソリューションを提供する上での大規模言語モデルの有用性について検討する。
論文 参考訳（メタデータ） (2023-11-14T06:58:09Z) - Ranking LLM-Generated Loop Invariants for Program Verification [14.7590099354867]
大規模言語モデルは、0ショット設定でプログラムのクラスに対するループ不変量を合成することができる。
これは、不変性を確立するためのプログラム検証者への多数の呼び出しにつながる可能性がある。
我々は正しい帰納的不変量と誤った試みを区別できるランク付け器を設計した。
論文 参考訳（メタデータ） (2023-10-13T18:13:52Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。