論文の概要: A Neurosymbolic Approach to Loop Invariant Generation via Weakest Precondition Reasoning

• arxiv url: http://arxiv.org/abs/2512.15816v1
• Date: Wed, 17 Dec 2025 14:16:59 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-12-19 18:10:31.742614
• Title: A Neurosymbolic Approach to Loop Invariant Generation via Weakest Precondition Reasoning
• Title（参考訳）: ウェイクスト条件推論によるループ不変生成に対するニューロシンボリックアプローチ
• Authors: Daragh King, Vasileios Koutavas, Laura Kovacs,
• Abstract要約: NeuroInvはループ不変生成に対する神経象徴的アプローチである。 我々は150のJavaプログラムの総合ベンチマークでNeuroInvを評価した。
• 参考スコア（独自算出の注目度）: 3.8233569758620054
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Loop invariant generation remains a critical bottleneck in automated program verification. Recent work has begun to explore the use of Large Language Models (LLMs) in this area, yet these approaches tend to lack a reliable and structured methodology, with little reference to existing program verification theory. This paper presents NeuroInv, a neurosymbolic approach to loop invariant generation. NeuroInv comprises two key modules: (1) a neural reasoning module that leverages LLMs and Hoare logic to derive and refine candidate invariants via backward-chaining weakest precondition reasoning, and (2) a verification-guided symbolic module that iteratively repairs invariants using counterexamples from OpenJML. We evaluate NeuroInv on a comprehensive benchmark of 150 Java programs, encompassing single and multiple (sequential) loops, multiple arrays, random branching, and noisy code segments. NeuroInv achieves a $99.5\%$ success rate, substantially outperforming the other evaluated approaches. Additionally, we introduce a hard benchmark of $10$ larger multi-loop programs (with an average of $7$ loops each); NeuroInv's performance in this setting demonstrates that it can scale to more complex verification scenarios.
• Abstract（参考訳）: ループ不変生成は、自動プログラム検証において重要なボトルネックである。 最近の研究は、この分野におけるLarge Language Models (LLMs)の使用を探求し始めているが、既存のプログラム検証理論にはほとんど言及することなく、信頼性と構造化された方法論を欠いている傾向にある。 本稿では,ループ不変生成に対するニューロシンボリックアプローチであるNeuroInvについて述べる。 NeuroInv は,(1) LLM と Hoare 論理を利用する神経推論モジュールを用いて,後方鎖の弱い条件条件推論によって候補不変量を導出・洗練する,(2) OpenJML の逆例を用いて不変量を反復的に修復する検証誘導記号モジュールである。 我々はNeuroInvを150のJavaプログラムの包括的なベンチマークで評価し、単一のループと複数の(逐次)ループ、複数の配列、ランダム分岐、ノイズの多いコードセグメントを含む。 NeuroInvは99.5 %$成功率を獲得し、他の評価されたアプローチよりも大幅に上回っている。 さらに、より大規模なマルチループプログラム(それぞれ平均7ドルループ)のハードベンチマークを導入し、この設定でのNeuroInvのパフォーマンスは、より複雑な検証シナリオにスケールできることを示しています。

関連論文リスト

• Quantization Meets dLLMs: A Systematic Study of Post-training Quantization for Diffusion LLMs [78.09559830840595]
  本稿では拡散に基づく言語モデルの定量化に関する最初の体系的研究について述べる。 異常に大きなアクティベーション値によって特徴付けられるアクティベーションアウトリーチの存在を同定する。 我々は最先端のPTQ手法を実装し、包括的な評価を行う。
  論文  参考訳（メタデータ） (2025-08-20T17:59:51Z)
• Fast Controlled Generation from Language Models with Adaptive Weighted Rejection Sampling [90.86991492288487]
  トークンの制約を評価するのは 違法にコストがかかる LCDは文字列上のグローバル分布を歪め、ローカル情報のみに基づいてトークンをサンプリングすることができる。 我々のアプローチは最先端のベースラインよりも優れていることを示す。
  論文  参考訳（メタデータ） (2025-04-07T18:30:18Z)
• Graph-Structured Speculative Decoding [52.94367724136063]
  投機的復号化は、大規模言語モデルの推論を加速する有望な手法として登場した。 本稿では, 有向非巡回グラフ(DAG)を応用して, 起案された仮説を管理する革新的な手法を提案する。 我々は1.73$times$から1.96$times$に顕著なスピードアップを観察し、標準投機的復号法を大幅に上回った。
  論文  参考訳（メタデータ） (2024-07-23T06:21:24Z)
• An efficient projection neural network for $\ell_1$-regularized logistic regression [10.517079029721257]
  本稿では, $ell_$-regularized logistics regression のための単純な投影ニューラルネットワークを提案する。 提案したニューラルネットワークは、余分な補助変数や滑らかな近似を必要としない。 また、リアプノフ理論を用いて、提案したニューラルネットワークの収束について検討し、任意の初期値を持つ問題の解に収束することを示す。
  論文  参考訳（メタデータ） (2021-05-12T06:13:44Z)
• Incremental Verification of Fixed-Point Implementations of Neural Networks [0.19573380763700707]
  インクリメンタル境界モデル検査(BMC)、満足度変調理論(SMT)、不変推論を用いた新しいシンボル検証フレームワークの開発と評価を行った。 提案手法は,異なる入力画像を考慮した21の試験事例の85.8%,カバー手法に関連する特性の100%を検証・生成することができた。
  論文  参考訳（メタデータ） (2020-12-21T10:03:44Z)
• NeuroLogic Decoding: (Un)supervised Neural Text Generation with Predicate Logic Constraints [75.66980495245926]
  条件付きテキスト生成は、しばしば語彙的な制約を必要とする。 我々は、ニューラルネットワークモデル -- 教師付きか否かに関わらず -- がフロートテキストを生成することを可能にする、シンプルで効果的なアルゴリズムであるNeuroLogic Decodingを提案する。 この結果から,制御可能な微粒化生成のための大規模ニューラルネットワークの限界と,推論時間アルゴリズムの約束が示唆された。
  論文  参考訳（メタデータ） (2020-10-24T11:55:22Z)
• Closed Loop Neural-Symbolic Learning via Integrating Neural Perception, Grammar Parsing, and Symbolic Reasoning [134.77207192945053]
  従来の手法は強化学習アプローチを用いてニューラルシンボリックモデルを学ぶ。 我々は,脳神経知覚と記号的推論を橋渡しする前に,textbfgrammarモデルをテキストシンボリックとして導入する。 本稿では,トップダウンのヒューマンライクな学習手順を模倣して誤りを伝播する新しいtextbfback-searchアルゴリズムを提案する。
  論文  参考訳（メタデータ） (2020-06-11T17:42:49Z)
• Learning Nonlinear Loop Invariants with Gated Continuous Logic Networks (Extended Version) [19.87276407545565]
  我々は、一般SMT学習のための新しいニューラルネットワーク、Gated Continuous Logic Network (G-CLN)を導入する。 G-CLNは継続論理ネットワーク(CLN)アーキテクチャを拡張し、ゲーティングユニットとドロップアウトを提供する。 G-CLNの収束率は2次問題に対して9.7.5%、CLNモデルに対して39.2%である。
  論文  参考訳（メタデータ） (2020-03-17T21:44:37Z)

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

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