論文の概要: Compositional Loop Invariant Inference for Multiphase Programs via Structured Neurosymbolic Reasoning

• arxiv url: http://arxiv.org/abs/2611.07882v1
• Date: Thu, 05 Nov 2026 12:02:54 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-11-06 21:50:50.673389
• Title: Compositional Loop Invariant Inference for Multiphase Programs via Structured Neurosymbolic Reasoning
• Title（参考訳）: 構造的ニューロシンボリック推論による多相プログラムの構成ループ不変推論
• Abstract要約: 本稿では2つのメカニズム上に構築された多相不変推論のための構造的ニューロシンボリック推論フレームワークを提案する。 まず、CLOVERは、ループをシンボルループ分岐シーケンスに静的に分解する 第2に、CLOVERは逆例をブランチ構造に遡り、どの特定のループ分岐シーケンスが障害を引き起こしたかを特定し、そのサブ不変だけを修復する。
• 参考スコア（独自算出の注目度）: 11.251400340341398
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Loop invariants are essential for deductive program verification, yet automatically inferring them for {multiphase programs}, whose loops contain conditional branches that induce multiple execution phases with distinct behaviors, remains an open problem. Existing LLM-based methods either reason about loops as a whole or use explicit branch information to generate atomic assertions jointly across branches, without maintaining complete candidate sub-invariants for independent generation and targeted repair. We present CLOVER, a structured neurosymbolic reasoning framework for multiphase invariant inference built on two interlinked mechanisms. First, compositional inference: CLOVER statically decomposes a loop into symbolic {loop branch sequences}, conjunctions of the loop guard and branch conditions that characterize distinct execution scenarios, and guides the LLM to generate candidate sub-invariants for each one independently, so that each LLM query focuses on a single execution scenario rather than the entire loop. Second, counterexample-guided localized refinement: when SMT verification rejects a composed disjunctive invariant, CLOVER traces the counterexample back through the branch structure to identify which specific loop branch sequence caused the failure and repairs only that sub-invariant, preserving all correct components. Both mechanisms are unified by a shared symbolic structure derived from the loop's branch semantics, which guides what the LLM generates, how candidates are composed, and where refinement is directed. We evaluate CLOVER on 316 linear arithmetic, 50 nonlinear arithmetic, and 54 multiphase benchmarks. CLOVER solves 35 of 54 multiphase benchmarks, outperforming the best LLM-based baseline (29) by 20.7\% and the best traditional method (22) by 59.1\%. On linear/nonlinear benchmarks, CLOVER remains competitive, solving 355 of 366 programs overall.
• Abstract（参考訳）: ループ不変量は帰納的プログラム検証には不可欠であるが、ループに異なる動作で複数の実行フェーズを誘導する条件分岐を含む {multiphase program} を自動推論することは未解決の問題である。 既存のLCMベースの手法は、ループ全体を推論するか、あるいは明示的な分岐情報を使用して、独立した生成と対象とする修復のための完全な候補部分不変性を維持することなく、枝をまたいでアトミックなアサーションを生成する。 CLOVERは、2つの相互結合機構上に構築された多相不変推論のための構造化されたニューロシンボリック推論フレームワークである。 まず、合成推論: CLOVERは、ループを記号的な {loop branch sequences} に静的に分解し、ループガードと異なる実行シナリオを特徴付ける分岐条件を結合させ、各LLMクエリがループ全体ではなく単一の実行シナリオにフォーカスするように、LSMを独立して候補サブ不変量を生成するように誘導する。 第二に、逆例誘導型局所改善: SMT 検証が合成された解離不変量を拒否したとき、CLOVER は逆例を分岐構造を通して追跡し、どのループ分岐配列が故障の原因となったかを特定し、その部分不変量のみを修復し、すべての正しい成分を保存する。 どちらのメカニズムも、ループの分岐セマンティクスから派生した共有シンボル構造によって統一され、LLMが生成するもの、候補がどのように構成され、どのように洗練されるかを導く。 我々はCLOVERを316の線形算術、50の非線形算術、54の多相ベンチマークで評価した。 CLOVERは54のマルチフェーズベンチマークのうち35を解き、最高のLCMベースのベースライン(29)を20.7\%、伝統的なメソッド(22)を59.1\%で上回っている。 線形/非線形のベンチマークでは、CLOVERは競争力があり、全体的な366プログラムのうち355を解決している。

関連論文リスト

• LimICE: Integrating LLM into ICE Framework for Efficient Loop Invariant Inference [10.534386090450276]
  インクリメンタル合成のための新しい学習フレームワークであるインクリメンタルICEを提案する。 本フレームワークはIC3の漸進的哲学を一般的な不変学習フレームワークICEに統合する。 このフレームワークでは、LLMを利用して順序付けられたレムマ列を生成するループ不変合成ツールLimICEをインスタンス化する。
  論文  参考訳（メタデータ） (2026-07-30T02:50:09Z)
• Imputation Meets Clustering: Exploiting Latent Subgroup Structure for Missing Data Recovery [52.29866804948133]
  本稿では、クラスタリングと命令を相互に強化する共最適化プロセスとして再構築するフレームワークであるCAGI(Cluster-Aware Generative Imputation)を提案する。 14のベンチマークデータセットと15の代表的なベースラインの実験は、CAGIの優位性を実証している。
  論文  参考訳（メタデータ） (2026-07-08T02:50:02Z)
• Context Pruning for Coding Agents via Multi-Rubric Latent Reasoning [14.508049757681862]
  LLMベースのコーディングエージェントは、トークンの予算の大部分をリポジトリファイルを読むのに費やしている。 この定式化がモデリングのボトルネックを生み出すことを示す。 コード関連性を2つの解釈可能な品質次元に分解する構造化プルーニングフレームワークであるLaMRを提案する。
  論文  参考訳（メタデータ） (2026-05-14T18:30:10Z)
• F-GRPO: Factorized Group-Relative Policy Optimization for Unified Candidate Generation and Ranking [79.49893545611779]
  大規模言語モデル(LLM)はサブセットを生成し、それを1つの自己回帰パス内で順序付けることができる。 この柔軟性は、新しい最適化課題をもたらす: モデルが出力空間を検索し、完全なランクリストが生成された後にのみユーティリティフィードバックを受けなければならない。 このクレジット割り当てギャップは、エンドツーエンドの最適化を不安定にし、サンプル非効率にする。 本稿では,単一自己回帰的ロールアウト内の両方を実行する統一フレームワークを提案する。
  論文  参考訳（メタデータ） (2026-05-13T04:52:33Z)
• CktFormalizer: Autoformalization of Natural Language into Circuit Representations [23.44745731124114]
  CktFormalizerは、Lean 4.0に組み込まれた依存型HDLを通じてハードウェア生成をリダイレクトするフレームワークである。 VerilogEval(156問題)、RTLLM(50問題)、ResBench(56問題)では、CktFormalizerは直接Verilog生成と競合するシミュレーションパスレートを達成する。
  論文  参考訳（メタデータ） (2026-05-08T14:20:06Z)
• Efficient Test-Time Inference via Deterministic Exploration of Truncated Decoding Trees [68.04613115686509]
  自己整合性は、複数の推論トレースを並列にサンプリングし、投票することで、推論時間のパフォーマンスを向上させる。 そこで本研究では,切り落された標本を伐採木として扱う決定論的復号法であるDLE(Distinct Leafion)を提案する。 DLEは高品質な推論トレースを調査し、数学、コーディング、一般的な推論タスクのパフォーマンスを向上させる。
  論文  参考訳（メタデータ） (2026-04-22T12:42:03Z)
• 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)
• LLM-guided Hierarchical Retrieval [54.73080745446999]
  LATTICEは階層的な検索フレームワークであり、LLMは対数探索の複雑さで大きなコーパスを推論し、ナビゲートすることができる。 LLM誘導探索における中心的な課題は、モデルの関連性判断がノイズが多く、文脈に依存し、階層性に気付かないことである。 我々のフレームワークは、推論集約型BRIGHTベンチマークで最先端のゼロショット性能を実現する。
  論文  参考訳（メタデータ） (2025-10-15T07:05:17Z)
• EquiBench: Benchmarking Large Language Models' Reasoning about Program Semantics via Equivalence Checking [58.15568681219339]
  大規模言語モデル(LLM)を評価するための新しいベンチマークであるEquiBenchを紹介する。 このタスクは、プログラムのセマンティクスについて推論するモデルの能力を直接テストする。 19の最先端LCMを評価し、最も難しいカテゴリでは、最高の精度は63.8%と76.2%であり、50%のランダムベースラインよりわずかに高い。
  論文  参考訳（メタデータ） (2025-02-18T02:54:25Z)

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

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