論文の概要: Neuro-Symbolic Software Verification: Hyper-charging Local Language Models with Symbolic Reasoning at Scale

• arxiv url: http://arxiv.org/abs/2606.16886v1
• Date: Mon, 15 Jun 2026 15:59:10 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-16 16:21:34.74377
• Title: Neuro-Symbolic Software Verification: Hyper-charging Local Language Models with Symbolic Reasoning at Scale
• Title（参考訳）: ニューロ・シンボリック・ソフトウェア検証:大規模シンボリック推論を用いた超チャージローカル言語モデル
• Authors: Muhammad A. A. Pirzada, Julian Parsert, Weiqi Wang, Konstantin Korovin, Lucas C. Cordeiro,
• Abstract要約: 局所展開可能なオープンウェイト言語モデルとシンボリック不変量生成を組み合わせた,ニューロシンボリックパイプラインであるVerIbmcを提案する。 すべての推論は、クラウドAPIやプロプライエタリモデルを必要としないオープンウェイトモデルを使用して、単一のローカルマシン上で完全に実行される。
• 参考スコア（独自算出の注目度）: 11.088680803534785
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Loop invariant synthesis remains a central and pivotal bottleneck in formal software verification. Recent LLM-based Neuro-Symbolic tools have achieved impressive solve rates. However, these tools rely on proprietary, often expensive cloud APIs, which constitute a hurdle for privacy-sensitive industrial deployments where the source code cannot leave the organisation or where cost is a factor. We present VerIbmc, a neuro-symbolic pipeline that pairs symbolic invariant generation with locally deployable open-weight language models with the ESBMC verification tool. Our pipeline combines a deterministic symbolic invariant synthesis phase with an iterative LLM refinement loop driven by structured verifier feedback. In addition, we provide two types of pipelines that differ in their prompting strategy: Chain-of-Thought vs. Tree-of-Thought. We conduct an extensive experimental evaluation with five open-weight models (ranging from 7B to 120B parameters) across five benchmark families comprising of 520 problems (499 after excluding 21 with unavoidable overflow). Overall, the best single configuration (GPT-OSS-120B) solves 431 of 499 problems (86.4%). Additionally, on the four benchmark suites shared with the strongest cloud-API tools, VerIbmc is competitive running only on a single local machine. The evaluation shows symbolic invariant synthesis solves 75 problems without any LLM call and yields up to +35 additional problems for the weakest model. Importantly, all inference runs entirely on a single local machine using open-weight models -- no cloud API or proprietary model is required. Overall, we demonstrate that a neuro-symbolic approach based on LLMs can be used effectively for invariant synthesis in a privacy-preserving and energy-efficient manner, without having to resort to expensive proprietary frontier models locked behind APIs.
• Abstract（参考訳）: ループ不変合成は、フォーマルなソフトウェア検証において中心的で重要なボトルネックであり続けている。 最近のLSMベースのNeuro-Symbolicツールは、目覚ましい解決率を達成した。 しかし、これらのツールはプロプライエタリで、しばしば高価なクラウドAPIに依存しており、ソースコードが組織を離れることができないり、コストが要因となるような、プライバシに敏感な産業展開のハードルとなっている。 本稿では, ESBMC検証ツールを用いて, 局所展開可能なオープンウェイト言語モデルとシンボリック不変生成を組み合わせた, ニューロシンボリックパイプラインであるVerIbmcを提案する。 我々のパイプラインは、決定論的シンボリック不変合成相と、構造化された検証器フィードバックによって駆動される反復LLM精製ループを結合する。 さらに、私たちは、そのプロンプト戦略が異なる2つのタイプのパイプラインを提供しています。 我々は,520問題(避けられないオーバーフローを含む21を除いた499)からなる5つのベンチマークファミリーに対して,5つのオープンウェイトモデル(7Bから120Bパラメータ)で広範囲に実験を行った。 全体として、最高の単一構成(GPT-OSS-120B)は499の431の問題を解決している(86.4%)。 さらに、最も強力なクラウドAPIツールと共有される4つのベンチマークスイートでは、VerIbmcは、単一のローカルマシン上でのみ実行される競争力がある。 この評価は、記号的不変合成がLLM呼び出しなしで75の問題を解き、最も弱いモデルに対して最大+35の問題を生じることを示している。 重要なのは、すべての推論がオープンウェイトモデルを使用して単一のローカルマシン上で実行されることだ。クラウドAPIやプロプライエタリモデルを必要としない。 全体として、LLMに基づくニューロシンボリックアプローチは、高価なプロプライエタリなフロンティアモデルに頼らずに、プライバシー保護とエネルギー効率の両面で不変合成に効果的に利用できることを示した。

関連論文リスト

• Knowledge Boundary Probing and Demand-Guided Intervention for LLM-Based Power System Code Generation [8.136015158683694]
  電力系統のコード生成におけるファーストパス障害は, 幻覚関数名, 誤用パラメータ, 不正処理結果表など, 構造化されたAPI知識境界によって支配されていることを示す。 我々は,自然言語演算子クエリとパンダパワーコードと数値基底真理を組み合わせた実行検証ベンチマークジェネレータPowerCodeBenchを紹介する。 また、モデルごとのAPI知識プロファイルを測定するL0-L3ドキュメンテーション駆動のプロファイリング手順も導入する。
  論文  参考訳（メタデータ） (2026-05-29T16:06:34Z)
• Resource-Efficient Iterative LLM-Based NAS with Feedback Memory [49.44875022114861]
  ニューラルアーキテクチャサーチ(NAS)はネットワーク設計を自動化するが、従来の手法ではかなりの計算資源を必要とする。 本稿では,大規模言語モデル(LLM)を活用して,畳み込みニューラルネットワークアーキテクチャを反復的に生成し,評価し,洗練するクローズドループパイプラインを提案する。
  論文  参考訳（メタデータ） (2026-03-12T16:00:22Z)
• Cost-Aware Model Selection for Text Classification: Multi-Objective Trade-offs Between Fine-Tuned Encoders and LLM Prompting in Production [0.0]
  大規模言語モデル(LLM)は、オープンエンド推論や生成言語タスクにおいて強力な機能を示している。 固定ラベル空間を用いた構造化テキスト分類問題に対して、モデル選択は予測性能のみによって駆動されることが多い。 BERTファミリーの細調整エンコーダを用いたモデルでは、競争力があり、しばしば優れた分類性能が得られることを示す。
  論文  参考訳（メタデータ） (2026-02-06T03:54:28Z)
• Framework-Aware Code Generation with API Knowledge Graph-Constructed Data: A Study on HarmonyOS [52.483888557864326]
  APIKG4SYNはAPI指向の質問コードペアの構築にAPIナレッジグラフを活用するように設計されたフレームワークである。 APIKG4SYNを使ったHarmonyOSコード生成のための最初のベンチマークを構築した。
  論文  参考訳（メタデータ） (2025-11-29T08:13:54Z)
• Semantic Agreement Enables Efficient Open-Ended LLM Cascades [18.119677655287607]
  カスケードシステムは、可能な限り小さなモデルに計算要求をルーティングし、必要な時にのみ大きなモデルに遅延する。 我々は,信頼度の高い推論のための訓練自由信号として意味的合意を提案する。 セマンティックカスケードは、40%のコストでターゲットモデル品質に適合または超過し、最大60%のレイテンシを削減している。
  論文  参考訳（メタデータ） (2025-09-26T03:51:28Z)
• Syntactic and Semantic Control of Large Language Models via Sequential Monte Carlo [90.78001821963008]
  広い範囲のLMアプリケーションは、構文的制約や意味論的制約に適合するテキストを生成する必要がある。 我々は、連続モンテカルロ(SMC)に基づく制御LM生成のためのアーキテクチャを開発する。 我々のシステムはLew et al. (2023) のフレームワーク上に構築されており、言語モデル確率型プログラミング言語と統合されている。
  論文  参考訳（メタデータ） (2025-04-17T17:49:40Z)
• Are You Getting What You Pay For? Auditing Model Substitution in LLM APIs [71.7892165868749]
  LLM(Commercial Large Language Model) APIは基本的な信頼の問題を生み出します。 ユーザーは特定のモデルに課金するが、プロバイダが忠実に提供できることを保証することはない。 我々は,このモデル置換問題を定式化し,現実的な逆条件下での検出方法を評価する。 我々は,信頼された実行環境(TEE)を実用的で堅牢なソリューションとして使用し,評価する。
  論文  参考訳（メタデータ） (2025-04-07T03:57:41Z)
• LLMC: Benchmarking Large Language Model Quantization with a Versatile Compression Toolkit [55.73370804397226]
  鍵圧縮技術である量子化は、大きな言語モデルを圧縮し、加速することにより、これらの要求を効果的に軽減することができる。 本稿では,プラグアンドプレイ圧縮ツールキットであるLLMCについて,量子化の影響を公平かつ体系的に検討する。 この汎用ツールキットによって、我々のベンチマークはキャリブレーションデータ、アルゴリズム(3つの戦略)、データフォーマットの3つの重要な側面をカバーしています。
  論文  参考訳（メタデータ） (2024-05-09T11:49:05Z)

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

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