論文の概要: Vulnerability Detection: From Formal Verification to Large Language Models and Hybrid Approaches: A Comprehensive Overview

• arxiv url: http://arxiv.org/abs/2503.10784v1
• Date: Thu, 13 Mar 2025 18:22:22 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-03-17 13:04:56.818765
• Title: Vulnerability Detection: From Formal Verification to Large Language Models and Hybrid Approaches: A Comprehensive Overview
• Title（参考訳）: 脆弱性検出:形式検証から大規模言語モデル,ハイブリッドアプローチへ:包括的概要
• Authors: Norbert Tihanyi, Tamas Bisztray, Mohamed Amine Ferrag, Bilel Cherif, Richard A. Dubniczky, Ridhi Jain, Lucas C. Cordeiro,
• Abstract要約: 本稿では,最先端のソフトウェアテストと検証に焦点をあてる。 古典的な形式的手法、LLMに基づく分析、新しいハイブリッド手法の3つの主要なアプローチに焦点を当てている。 LLMによるインサイトとフォーマルリガーを統合することで,ソフトウェア検証の有効性とスケーラビリティが向上するかどうかを解析する。
• 参考スコア（独自算出の注目度）: 3.135279672650891
• License:
• Abstract: Software testing and verification are critical for ensuring the reliability and security of modern software systems. Traditionally, formal verification techniques, such as model checking and theorem proving, have provided rigorous frameworks for detecting bugs and vulnerabilities. However, these methods often face scalability challenges when applied to complex, real-world programs. Recently, the advent of Large Language Models (LLMs) has introduced a new paradigm for software analysis, leveraging their ability to understand insecure coding practices. Although LLMs demonstrate promising capabilities in tasks such as bug prediction and invariant generation, they lack the formal guarantees of classical methods. This paper presents a comprehensive study of state-of-the-art software testing and verification, focusing on three key approaches: classical formal methods, LLM-based analysis, and emerging hybrid techniques, which combine their strengths. We explore each approach's strengths, limitations, and practical applications, highlighting the potential of hybrid systems to address the weaknesses of standalone methods. We analyze whether integrating formal rigor with LLM-driven insights can enhance the effectiveness and scalability of software verification, exploring their viability as a pathway toward more robust and adaptive testing frameworks.
• Abstract（参考訳）: ソフトウェアテストと検証は、現代のソフトウェアシステムの信頼性とセキュリティを確保するために重要である。 伝統的に、モデルチェックや定理証明のような形式的な検証技術は、バグや脆弱性を検出するための厳格なフレームワークを提供してきた。 しかし、これらの手法は複雑な実世界のプログラムに適用する場合、スケーラビリティの問題に直面することが多い。 最近、LLM(Large Language Models)の出現は、ソフトウェア分析のための新しいパラダイムを導入し、安全でないコーディングプラクティスを理解する能力を活用している。 LLMはバグ予測や不変生成といったタスクにおいて有望な機能を示すが、古典的なメソッドの形式的な保証は欠如している。 本稿では,従来の形式的手法,LSMに基づく解析,およびそれらの強みを組み合わせた新しいハイブリッド手法の3つの主要なアプローチに着目し,最先端のソフトウェアテストと検証の総合的研究を行う。 それぞれのアプローチの強み、制限、実践的応用について検討し、スタンドアロンメソッドの弱点に対処するハイブリッドシステムの可能性を強調します。 LLMによるインサイトとフォーマルリガーを統合することで、ソフトウェア検証の有効性とスケーラビリティが向上するかどうかを分析し、より堅牢で適応的なテストフレームワークへの道筋として、その生存可能性を探る。

関連論文リスト

• LLMs in Software Security: A Survey of Vulnerability Detection Techniques and Insights [12.424610893030353]
  大規模言語モデル(LLM)は、ソフトウェア脆弱性検出のためのトランスフォーメーションツールとして登場している。 本稿では,脆弱性検出におけるLSMの詳細な調査を行う。 言語間の脆弱性検出、マルチモーダルデータ統合、リポジトリレベルの分析といった課題に対処する。
  論文  参考訳（メタデータ） (2025-02-10T21:33:38Z)
• Causality can systematically address the monsters under the bench(marks) [64.36592889550431]
  ベンチマークはさまざまなバイアス、アーティファクト、リークに悩まされている。 モデルは、調査の不十分な障害モードのため、信頼できない振る舞いをする可能性がある。 因果関係はこれらの課題を体系的に解決するための 理想的な枠組みを提供します
  論文  参考訳（メタデータ） (2025-02-07T17:01:37Z)
• Adversarial Reasoning at Jailbreaking Time [49.70772424278124]
  テスト時間計算による自動ジェイルブレイクに対する逆推論手法を開発した。 我々のアプローチは、LSMの脆弱性を理解するための新しいパラダイムを導入し、より堅牢で信頼性の高いAIシステムの開発の基礎を築いた。
  論文  参考訳（メタデータ） (2025-02-03T18:59:01Z)
• Bringing Order Amidst Chaos: On the Role of Artificial Intelligence in Secure Software Engineering [0.0]
  進化を続ける技術的景観は、機会と脅威の両方を提供し、カオスと秩序が競合する動的な空間を作り出す。 セキュアなソフトウェアエンジニアリング(SSE)は、ソフトウェアシステムを危険にさらす脆弱性に継続的に対処しなければならない。 この論文は、AIの精度に影響を与えるドメイン固有の違いに対処することで、SSEのカオスに秩序をもたらすことを目指している。
  論文  参考訳（メタデータ） (2025-01-09T11:38:58Z)
• FaithEval: Can Your Language Model Stay Faithful to Context, Even If "The Moon is Made of Marshmallows" [74.7488607599921]
  FaithEvalは、コンテキストシナリオにおける大規模言語モデル(LLM)の忠実度を評価するためのベンチマークである。 FaithEvalは4.9Kの高品質な問題で構成され、厳格な4段階のコンテキスト構築と検証フレームワークを通じて検証されている。
  論文  参考訳（メタデータ） (2024-09-30T06:27:53Z)
• Probabilistic ML Verification via Weighted Model Integration [11.812078181471634]
  機械学習モデルの確率形式検証(PFV)はその初期段階にある。 重み付きモデル統合(WMI)に基づくMLシステムのPFV統合フレームワークを提案する。 ML検証文献におけるスケーリング手法が,本来の範囲を超えていかに一般化できるかを示す。
  論文  参考訳（メタデータ） (2024-02-07T14:24:04Z)
• LLbezpeky: Leveraging Large Language Models for Vulnerability Detection [10.330063887545398]
  大規模言語モデル(LLM)は、人やプログラミング言語におけるセムナティクスを理解する大きな可能性を示している。 私たちは、脆弱性の特定と修正を支援するAI駆動ワークフローの構築に重点を置いています。
  論文  参考訳（メタデータ） (2024-01-02T16:14:30Z)
• Testing learning-enabled cyber-physical systems with Large-Language Models: A Formal Approach [32.15663640443728]
  機械学習(ML)をサイバー物理システム(CPS)に統合することは大きな利益をもたらす。 既存の検証と検証技術は、しばしばこれらの新しいパラダイムには不十分である。 本稿では, 基礎確率テストからより厳密なアプローチへ移行し, 正式な保証を実現するためのロードマップを提案する。
  論文  参考訳（メタデータ） (2023-11-13T14:56:14Z)
• CodeLMSec Benchmark: Systematically Evaluating and Finding Security Vulnerabilities in Black-Box Code Language Models [58.27254444280376]
  自動コード生成のための大規模言語モデル(LLM)は、いくつかのプログラミングタスクにおいてブレークスルーを達成した。 これらのモデルのトレーニングデータは、通常、インターネット(例えばオープンソースのリポジトリから)から収集され、障害やセキュリティ上の脆弱性を含む可能性がある。 この不衛生なトレーニングデータは、言語モデルにこれらの脆弱性を学習させ、コード生成手順中にそれを伝播させる可能性がある。
  論文  参考訳（メタデータ） (2023-02-08T11:54:07Z)
• Joint Differentiable Optimization and Verification for Certified Reinforcement Learning [91.93635157885055]
  安全クリティカル制御システムのためのモデルベース強化学習では,システム特性を正式に認定することが重要である。 本稿では,強化学習と形式検証を共同で行う枠組みを提案する。
  論文  参考訳（メタデータ） (2022-01-28T16:53:56Z)
• Practical Machine Learning Safety: A Survey and Primer [81.73857913779534]
  自動運転車のような安全クリティカルなアプリケーションにおける機械学習アルゴリズムのオープンワールド展開は、さまざまなML脆弱性に対処する必要がある。 一般化エラーを低減し、ドメイン適応を実現し、外乱例や敵攻撃を検出するための新しいモデルと訓練技術。 我々の組織は、MLアルゴリズムの信頼性を異なる側面から向上するために、最先端のML技術を安全戦略にマッピングする。
  論文  参考訳（メタデータ） (2021-06-09T05:56:42Z)

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

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