論文の概要: Neuro-Symbolic Reasoning for Vulnerability Detection

• arxiv url: http://arxiv.org/abs/2607.03963v1
• Date: Sat, 04 Jul 2026 17:44:53 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-07-07 22:26:29.773901
• Title: Neuro-Symbolic Reasoning for Vulnerability Detection
• Title（参考訳）: 脆弱性検出のためのニューロシンボリック推論
• Abstract要約: LeanGuardはニューロシンボリックなフレームワークで、それぞれの行為をそれに対応するサイドに割り当てます。 予防策は、よりよい推進ではなく、役割の分離である、と我々は主張する。
• 参考スコア（独自算出の注目度）: 12.515374118940246
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Ask a large language model (LLM) whether a pointer dereference is safe, and it can often produce a plausible justification for ``yes''. The difficulty is that a fluent justification is not a proof. This gap is precisely where automated vulnerability detection lives: deciding, for a given operation in source code, whether a memory safety defect such as a null dereference, use-after-free, or double free can actually occur. We trace the unreliability of LLM-based vulnerability detection to a mechanism, the premature discharge of safety obligations, and argue that the remedy is not better prompting but a separation of roles: the component that interprets the code must not also be the one that decides a safety obligation is met. In this paper, we present LeanGuard, a neuro-symbolic framework that assigns each act to the side equipped for it. On the neural side, an LLM serves strictly as a semantic filter over candidate facts extracted from the abstract syntax tree (AST): it prunes spurious facts and keeps the real ones, but never discharges an obligation or decides the verdict on its own. On the symbolic side, the surviving facts are compiled into a verification model in Lean 4 (a formal proof assistant whose kernel accepts a conclusion only when it is formally proved), where every dangerous operation must be matched by a guard that provably covers it in scope; absent such a guard, the obligation stays open rather than being argued away. Because a function rarely arrives with full context, this symbolic model is necessarily partial: an unproved obligation is not yet a defect. An evidence-aware adjudicator therefore weighs the symbolic and neural verdicts by the quality of each. We instantiate the framework on five CWE classes to ask how far this division of labor can be pushed.
• Abstract（参考訳）: 大きな言語モデル(LLM)にポインタの参照が安全かどうかを問うと、しばしば `yes'' に対する妥当な正当性を生み出す。 難点は、流動的な正当化が証明ではないことだ。 このギャップは、ソースコード内の特定の操作に対して、nullの参照や利用後フリー、ダブルフリーといったメモリ安全性の欠陥が実際に発生するかどうかを判断する自動脆弱性検出の場所である。 我々は、LSMベースの脆弱性検出の信頼性の欠如をメカニズム、早期の安全義務の解除に遡り、予防策はより良い推進力ではなく役割の分離であると主張する:コードの解釈を行うコンポーネントは、安全義務を決定するコンポーネントでなければならない。 本稿では,脳神経シンボルの枠組みであるLeanGuardについて述べる。 神経面では、LLMは抽象構文木(AST)から抽出された候補事実に対するセマンティックフィルタとして厳密に機能する。 象徴的な側面では、生き残った事実はLean 4(公式に証明されたときのみカーネルが結論を受け入れる形式的な証明アシスタント)の検証モデルにコンパイルされます。 関数が完全なコンテキストで現れることはめったにないので、この象徴的モデルは必ずしも部分的である:未証明の義務はまだ欠陥ではない。 したがって、エビデンスを意識した判断者は、それぞれの品質による象徴的および神経的な判断を重み付けする。 5つのCWEクラスのフレームワークをインスタンス化し、この分業がどこまで進めるかを問う。

関連論文リスト

• Autoformalizing Argumentative Material Inferences [26.35292656634472]
  我々は、ガード補完として議論材料推論のための自己形式化を開発する。 GUARDは、証明された信条を大幅に改善する。 シンボル的ソフトな批判と明示的な仮定層がこれらの利益の大部分を担っていることを示す。
  論文  参考訳（メタデータ） (2026-09-15T11:05:26Z)
• Refuse without Refusal: A Structural Analysis of Safety-Tuning Responses for Reducing False Refusals in Language Models [7.073710587892435]
  また, 否定文は, 表面的手がかりに依存することによって, 有害問合せと良性問合せの正確な識別を阻害することを示した。 また,合理性のみを訓練することで,同等の安全性能を維持しながら誤認を低減できることを示す。
  論文  参考訳（メタデータ） (2026-09-04T04:37:10Z)
• Knowing When to Quit: Diagnosing and Training LLMs to Abort Futile Reasoning [109.33717747526583]
  大規模言語モデルは、計算コストが高くても意味論的に無効な推論を、能力を超えたタスクで生成する。 textbfCaRL(textbfCapability-textbfaligned textbfReinforcement textbfL)を導入し、振る舞いを機能境界に合わせる。 実験は、タスクの難易度を超えて性能を保ちながら、無駄な推論を大幅に削減することを示した。
  論文  参考訳（メタデータ） (2026-07-31T09:30:33Z)
• Mark, Don't Erase: Token Inoculation for Dual-Use Knowledge in LLMs [54.96236442484317]
  リスクのある知識はモデルに保持でき、特権制御トークンによって行動的に守られることを示す。 Token Inoculation という手法はバインディング・アンド・ブランチ方式を導入している。
  論文  参考訳（メタデータ） (2026-07-21T02:15:39Z)
• AgentSecBench: Measuring Prompt Injection, Privacy Leakage, and Tool-Use Integrity in LLM Agents [0.2864713389096699]
  本稿では,AgentSecBenchを,この問題に対する正式なセキュリティフレームワークの実証的なインスタンス化として紹介する。 3つのゲーム・インストラクション・インテリジェンス・インテリジェンス・インテリジェンス・インテリジェンス・インテリジェンス・インテリジェンス・インテリジェンス・インテリジェンス(英語版)・インテリジェンス・インテリジェンス・インテリジェンス・インテリジェンス・インテリジェンス(英語版)・インテリジェンス・インテリジェンス・インテリジェンス・インテリジェンス・インテリジェンス・インテリジェンス・インテリジェンス(英語版)を定めている。 これは、承認された観察と能力に対するプロジェクションとしてのアプリケーションポリシーを表し、プロジェクションの即時アノテーションとプロジェクションの強化を区別し、敵のアドバンテージと、防衛が生成前に関連するモデル可視チャネルを閉鎖するかどうかを計測する。
  論文  参考訳（メタデータ） (2026-05-25T18:53:22Z)
• Securing LLM Agents Need Intent-to-Execution Integrity [49.490963596514185]
  我々は, LLMエージェントの確保には, エージェントの実行がユーザの意図を忠実に反映した場合に規定するエンドツーエンドの正当性を定義する必要があると主張している。 LLMエージェントはコンパイラと構造的に類似しており、セキュリティ違反はユーザ意図を保存しない誤った実行に対応する。 emphTool整合性、emph命令整合性、emphJudgment整合性、emphData整合性。
  論文  参考訳（メタデータ） (2026-05-16T12:53:31Z)
• AdversarialCoT: Single-Document Retrieval Poisoning for LLM Reasoning [115.3243260783674]
  Retrieval-augmented Generation (RAG) は、外部文書を取得することにより、大きな言語モデル(LLM)推論を強化する。 攻撃者が悪意のあるコンテンツを検索コーパスに注入するRAGにおける知識ベース中毒攻撃について検討した。 AdversarialCoTは、コーパス内の1つのドキュメントだけを毒化するクエリ固有の攻撃である。
  論文  参考訳（メタデータ） (2026-04-14T02:10:23Z)
• ProofSketcher: Hybrid LLM + Lightweight Proof Checker for Reliable Math/Logic Reasoning [0.0]
  大規模言語モデル(LLMs)は、数学的および論理的分野における説得的議論を生み出す可能性がある。 LeanとCoqは、構文的および意味的ステートメントがプログラム内のすべての構文的および意味的ステップをパスできるステートメントのみを受け入れることを保証することで、厳格な信頼性を持つ。 本稿では,LLMがコンパクトDSLの型付き証明スケッチを生成し,軽量な信頼できるカーネルがスケッチを明示的な証明義務に拡張するハイブリッドパイプラインを提案する。
  論文  参考訳（メタデータ） (2026-04-07T19:33:54Z)
• Beyond Content Safety: Real-Time Monitoring for Reasoning Vulnerabilities in Large Language Models [14.927545906619295]
  大規模言語モデルは、複雑なタスクを解決するために明示的なチェーン・オブ・シンク(CoT)推論にますます依存している。 LLMの安全性に関する既存の研究は、コンテンツ安全性に焦点を当てている。 我々は、推論の安全性をセキュリティの側面として認識する:モデルの推論の軌道が論理的に一貫したものであるという要求。
  論文  参考訳（メタデータ） (2026-03-26T13:08:56Z)
• Hiding in Plain Text: Detecting Concealed Jailbreaks via Activation Disentanglement [13.976796671311066]
  大規模言語モデル (LLM) は、リーチでセマンティックに一貫性のあるジェイルブレイクプロンプトに対して脆弱なままである。 本稿では,LLMアクティベーションにおけるセマンティックファクタペアを推論時にアンタングリングするための自己教師型フレームワークを提案する。 次に、フレーミング表現で動作する異常検出器であるFrameShieldを提案し、モデルに依存しない検出を改善する。
  論文  参考訳（メタデータ） (2026-02-23T00:11:30Z)
• ARMOR: Aligning Secure and Safe Large Language Models via Meticulous Reasoning [64.32925552574115]
  ARMORは、jailbreak戦略を分析し、コアインテントを抽出する、大規模な言語モデルである。 ARMORは最先端の安全性能を達成し、平均有害率は0.002であり、高度な最適化ベースのジェイルブレイクに対する攻撃成功率は0.06である。
  論文  参考訳（メタデータ） (2025-07-14T09:05:54Z)
• Is the Top Still Spinning? Evaluating Subjectivity in Narrative Understanding [40.78154629252038]
  曖昧なクレームにバイナリラベルを強制すると、評価の信頼性が低下する。 請求項のニュアンス評価を提供する方法として,LCM生成した要約の編集を紹介する。 我々は,ARMが主張の忠実性に関するアノテータ合意において,絶対的な21%の改善をもたらすことを示す。
  論文  参考訳（メタデータ） (2025-04-01T19:08:24Z)
• Towards Copyright Protection for Knowledge Bases of Retrieval-augmented Language Models via Reasoning [58.57194301645823]
  大規模言語モデル(LLM)は、現実のパーソナライズされたアプリケーションにますます統合されている。 RAGで使用される知識基盤の貴重かつしばしばプロプライエタリな性質は、敵による不正使用のリスクをもたらす。 これらの知識基盤を保護するための透かし技術として一般化できる既存の方法は、一般的に毒やバックドア攻撃を含む。 我々は、無害な」知識基盤の著作権保護の名称を提案する。
  論文  参考訳（メタデータ） (2025-02-10T09:15:56Z)
• Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
  LLMの複雑な推論には2行のアプローチが採用されている。 1行の作業は様々な推論構造を持つLLMを誘導し、構造出力は自然に中間推論ステップと見なすことができる。 他方の行では、LCMのない宣言的解法を用いて推論処理を行い、推論精度は向上するが、解法のブラックボックスの性質により解釈性に欠ける。 具体的には,Prologインタプリタが生成した中間検索ログにアクセスし,人間可読推論に解釈可能であることを示す。
  論文  参考訳（メタデータ） (2023-11-16T11:26:21Z)
• Measuring Association Between Labels and Free-Text Rationales [60.58672852655487]
  解釈可能なNLPでは、説明された例に対するモデルの意思決定プロセスを反映した忠実な理性が必要です。 情報抽出型タスクに対する忠実な抽出合理化のための既存のモデルであるパイプラインは、自由テキスト合理化を必要とするタスクに確実に拡張されないことを示す。 我々は、信頼が確立されていない自由文合理化のための、広く使われている高性能モデルのクラスである、共同予測と合理化のモデルに目を向ける。
  論文  参考訳（メタデータ） (2020-10-24T03:40:56Z)

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

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