論文の概要: Ranking Function Generation with LLMs for Termination

• arxiv url: http://arxiv.org/abs/2610.35523v1
• Date: Mon, 26 Oct 2026 14:41:52 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-27 22:27:14.035337
• Title: Ranking Function Generation with LLMs for Termination
• Title（参考訳）: 終端用LDMを用いたランキング関数生成
• Abstract要約: RAINFALLは、ランク関数合成のためのニューロシンボリックなフレームワークである。 RAINFALLは323プログラム(90.22%)の検証可能なランキング関数を合成し、全ての有望なベースラインを上回っている。 以上の結果から, ランキング関数合成のための汎用的, 健全なフレームワークが提案され, 終点を超えて, LLMが公式にチェック可能なライブネス証明書の合成を支援することが示唆された。
• 参考スコア（独自算出の注目度）: 11.672702691633384
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Ranking functions are a fundamental technique for proving loop termination, but constructing them manually is challenging and requires substantial expertise. We propose RAINFALL, a neuro-symbolic framework which follows the generate-verify-refine paradigm and tightly integrates LLMs with symbolic verification. RAINFALL formulates ranking function synthesis as a code-completion task by inserting placeholders into the input program and constraining the LLM to fill four predefined slots for each loop. The completed program is then checked by a symbolic verifier. If verification succeeds, a valid ranking function is obtained; otherwise, the verifier's diagnostics are translated into natural-language feedback that guides iterative refinement of the LLM's output. We evaluate RAINFALL on two public benchmark suites comprising 358 terminating C programs. Using MiniMax V2.7, RAINFALL synthesizes verifiable ranking functions for 323 programs (90.22%), outperforming all promising baselines. In particular, it solves 12 more programs than PROTON 2.1, the best-performing baseline and winner of the SV-COMP 2026 Termination category. Furthermore, combining RAINFALL with PROTON 2.1 increases the success rate to 96.65% (346/358 programs). We also conduct ablation study confirming individual contributions of placeholder contracts, few-shot examples, symbolic verification, and diagnostic information feedback. Experiments across LLMs further confirm the effectiveness of RAINFALL. Our results suggest a generic, sound framework for ranking-function synthesis and, beyond termination, LLM-assisted synthesis of formally checkable liveness certificates, both of which represent new directions of software engineering research.
• Abstract（参考訳）: ランク付け関数はループ終了を証明するための基本的なテクニックであるが、それらを手動で構築することは困難であり、かなりの専門知識を必要とする。 生成-検証-精細パラダイムに従うニューロシンボリックなフレームワークであるRAINFALLを提案し、シンボル検証とLLMを密に統合する。 RAINFALLは、入力プログラムにプレースホルダーを挿入し、LLMを制約し、ループ毎に予め定義された4つのスロットを埋めることで、ランキング関数合成をコード補完タスクとして定式化する。 完了したプログラムはシンボリック検証器によってチェックされる。 検証が成功すると、有効なランキング関数が得られ、そうでなければ、検証者の診断は自然言語のフィードバックに変換され、LCMの出力の反復的洗練が導かれる。 我々は358のCプログラムを含む2つの公開ベンチマークスイート上でRAINFALLを評価する。 RAINFALLはMiniMax V2.7を使用して323プログラム(90.22%)の検証可能なランキング関数を合成し、全ての有望なベースラインを上回っている。 特に、SV-COMP 2026 終了カテゴリーの最高性能のベースラインと勝者である PROTON 2.1 よりも12のプログラムを解決している。 さらに、RAINFALL と PROTON 2.1 を組み合わせることで、成功率は96.65% (346/358 プログラム)に向上する。 また、プレースホルダー契約の個々の貢献、少数ショット例、シンボリック検証、診断情報フィードバックについて、アブレーション調査を行った。 LLMを横断する実験により、RAINFALLの有効性がさらに確認された。 以上の結果から,ソフトウェア工学研究の新たな方向性を反映した,ランキング関数合成のための汎用的,健全なフレームワークが提案されている。

関連論文リスト

• P$^{3}$: Joint Program-and-Proof Planning for Verified Code Generation [19.3449645807529]
  検証されたコード生成は、プログラムの実行可能プログラムとマシンチェック可能な証明の両方を生成するために、大きな言語モデル(LLM)を要求する。 このシーケンシャルパイプラインは、実際には非効率かつ非効率である可能性があることを観察する。 プログラムとその正当性引数を手作業で開発するべきだというディクストラの見解に触発されて、我々は$P3$を提案する。
  論文  参考訳（メタデータ） (2026-08-10T08:33:18Z)
• LLM-as-a-Verifier: A General-Purpose Verification Framework [74.40111651545979]
  本稿では,汎用検証フレームワーク LLM-as-a-Verifier を紹介する。 追加のトレーニングを必要とせずに、エージェントタスクに対してきめ細かいフィードバックを提供する。 いくつかのベンチマークで最先端のパフォーマンスを達成する。
  論文  参考訳（メタデータ） (2026-07-06T17:59:35Z)
• ClarifyCodeBench: Evaluating LLMs on Clarifying Ambiguous Requirements for Code Generation [54.788849448970154]
  我々はClarifyCodeBenchを紹介した。ClarifyCodeBenchは、要求のあいまいさを解決するためのLarge Language Modelsの機能を評価するための、インタラクティブなベンチマークだ。 ClarifyCodeBenchを用いて、6つの最先端LCMの体系的評価を行う。 1) 能力の疎結合: 強いコード生成性能は本質的には効果的な要求の明確化に変換されない; 2) 推論パラドックス: 計算思考の増大はコードの正確性を高めるが、あいまいさの識別において限界的な利益をもたらす。
  論文  参考訳（メタデータ） (2026-07-01T09:58:59Z)
• Prism: Efficient Test-Time Scaling via Hierarchical Search and Self-Verification for Discrete Diffusion Language Models [96.0074341403456]
  LLM推論を改善するための実用的な方法として、推論時計算が再導入されている。 テスト時間スケーリング(TTS)アルゴリズムの多くは、自動回帰デコーディングに依存している。 そこで我々は,dLLM のための効率的な TTS フレームワーク Prism を提案する。
  論文  参考訳（メタデータ） (2026-02-02T09:14:51Z)
• Evaluating and Achieving Controllable Code Completion in Code LLM [89.64782747840225]
  命令誘導型コード補完ベンチマークである制御可能コード補完ベンチマーク(C3-Bench)を提案する。 コード補完作業中に,オープンソースのプロプライエタリモデルと高度なプロプライエタリモデルの間に,命令追従機能にかなりのギャップがあることを明らかにする。 結果として得られたQwen2.5-Coder-C3は、C3-Bench上で最先端のパフォーマンスを達成する。
  論文  参考訳（メタデータ） (2026-01-22T11:40:04Z)
• SLD-Spec: Enhancement LLM-assisted Specification Generation for Complex Loop Functions via Program Slicing and Logical Deletion [29.231420590756954]
  SLD-Specは、複雑なループ構造を持つプログラムに適したLCM支援仕様生成方法である。 SLD-Specは最先端のAutoSpecよりも5つのプログラムの検証に成功し、ランタイムを23.73%削減した。
  論文  参考訳（メタデータ） (2025-09-12T01:40:27Z)
• CodeARC: Benchmarking Reasoning Capabilities of LLM Agents for Inductive Program Synthesis [6.8081984950459]
  既存の評価プロトコルは、静的なサンプルセットとホールドアウトテストに依存しており、合成された関数が正しくない場合にフィードバックを提供する。 エージェントが隠れたターゲット関数と対話する新しい評価フレームワークであるCodeARCを提案する。 1114の関数を特徴とする汎用帰納的プログラム合成のための,最初の大規模ベンチマークを構築した。
  論文  参考訳（メタデータ） (2025-03-29T16:50:39Z)
• Integrating Expert Knowledge into Logical Programs via LLMs [3.637365301757111]
  ExKLoPは、大規模言語モデルが専門家の知識を論理的推論システムに統合する方法を評価するために設計されたフレームワークである。 この能力は特にエンジニアリングにおいて有用であり、製造業者が推奨する運用範囲などの専門家の知識を、自動化された監視システムに直接組み込むことができる。
  論文  参考訳（メタデータ） (2025-02-17T19:18:23Z)
• ALGO: Synthesizing Algorithmic Programs with LLM-Generated Oracle Verifiers [60.6418431624873]
  大きな言語モデル(LLM)は、機能記述からコードを実装するのに優れているが、アルゴリズムの問題に悩まされている。 我々は,アルゴリズムプログラムを LLM 生成 Oracle で合成するフレームワーク ALGO を提案し,その生成をガイドし,その正確性を検証する。 実験の結果,ALGOを装着すると,Codexモデルよりも8倍,CodeTよりも2.6倍の1サブミッションパス率が得られることがわかった。
  論文  参考訳（メタデータ） (2023-05-24T00:10:15Z)

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

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