論文の概要: From Ambiguity to Explicitness: NLP-Assisted 5G Specification Abstraction for Formal Analysis

• arxiv url: http://arxiv.org/abs/2308.03277v1
• Date: Mon, 7 Aug 2023 03:37:31 GMT
• ステータス: 処理完了
• システム内更新日: 2023-08-08 15:20:34.205750
• Title: From Ambiguity to Explicitness: NLP-Assisted 5G Specification Abstraction for Formal Analysis
• Title（参考訳）: 曖昧さから明示性:形式解析のためのNLP支援5G仕様抽象化
• Authors: Shiyu Yuan, Jingda Yang, Sudhanshu Arya, Carlo Lipizzi, Ying Wang
• Abstract要約: 我々はNLPツールを用いてデータを構築し、構築されたデータを用いて識別子と形式的特性を抽出する2段階パイプラインを提案する。 最適モデルの結果は,抽出精度が39%,形式的特性の同定精度が42%に達している。
• 参考スコア（独自算出の注目度）: 5.526122280732959
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formal method-based analysis of the 5G Wireless Communication Protocol is crucial for identifying logical vulnerabilities and facilitating an all-encompassing security assessment, especially in the design phase. Natural Language Processing (NLP) assisted techniques and most of the tools are not widely adopted by the industry and research community. Traditional formal verification through a mathematics approach heavily relied on manual logical abstraction prone to being time-consuming, and error-prone. The reason that the NLP-assisted method did not apply in industrial research may be due to the ambiguity in the natural language of the protocol designs nature is controversial to the explicitness of formal verification. To address the challenge of adopting the formal methods in protocol designs, targeting (3GPP) protocols that are written in natural language, in this study, we propose a hybrid approach to streamline the analysis of protocols. We introduce a two-step pipeline that first uses NLP tools to construct data and then uses constructed data to extract identifiers and formal properties by using the NLP model. The identifiers and formal properties are further used for formal analysis. We implemented three models that take different dependencies between identifiers and formal properties as criteria. Our results of the optimal model reach valid accuracy of 39% for identifier extraction and 42% for formal properties predictions. Our work is proof of concept for an efficient procedure in performing formal analysis for largescale complicate specification and protocol analysis, especially for 5G and nextG communications.
• Abstract（参考訳）: 5gワイヤレス通信プロトコルの形式的手法に基づく分析は、論理的脆弱性の特定や、特に設計段階でのセキュリティ評価の促進に不可欠である。 自然言語処理(NLP)は技術を支援し、ほとんどのツールは業界や研究コミュニティでは広く採用されていない。 数学のアプローチによる従来の形式的検証は、手動の論理的抽象化に大きく依存しており、時間的消費とエラーが発生しやすい。 NLP支援法が産業研究に適用されなかったのは、プロトコル設計の自然言語の曖昧さが、形式的検証の明示性に異論があるためかもしれない。 本研究では,プロトコル設計において形式的手法を採用するという課題に対処し,自然言語で記述された3gppプロトコルを対象とし,プロトコル分析を合理化するハイブリッド手法を提案する。 まず、NLPツールを用いてデータを構築し、次にNLPモデルを用いて、構築されたデータを用いて識別子と形式的特性を抽出する2ステップパイプラインを提案する。 識別子と形式的性質はさらに形式分析に使用される。 識別子と形式プロパティの異なる依存関係を基準として,3つのモデルを実装した。 最適モデルの結果,識別子抽出では39%,形式的特性予測では42%の精度が得られた。 我々の研究は、特に5GおよびnextG通信において、大規模で複雑な仕様およびプロトコル分析のための形式解析を行うための効率的な手順の実証である。

関連論文リスト

• Networks of Networks: Complexity Class Principles Applied to Compound AI Systems Design [63.24275274981911]
  多くの言語モデル推論コールからなる複合AIシステムは、ますます採用されている。 本研究では,提案した回答の生成と正当性検証の区別を中心に,ネットワークネットワーク(NoN)と呼ばれるシステムを構築した。 我々は,Kジェネレータを備えた検証器ベースの判定器NoNを導入し,"Best-of-K"あるいは"judge-based"複合AIシステムのインスタンス化を行う。
  論文  参考訳（メタデータ） (2024-07-23T20:40:37Z)
• MetaKP: On-Demand Keyphrase Generation [52.48698290354449]
  オンデマンドのキーフレーズ生成は,特定のハイレベルな目標や意図に従うキーフレーズを必要とする新しいパラダイムである。 そこで我々は,4つのデータセット,7500のドキュメント,3760の目標からなる大規模ベンチマークであるMetaKPを紹介した。 ソーシャルメディアからの流行事象検出に応用して,一般のNLP基盤として機能する可能性を示す。
  論文  参考訳（メタデータ） (2024-06-28T19:02:59Z)
• Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
  本稿では,検証対応言語における仕様の質を評価するための指標を提案する。 MBPPコード生成ベンチマークのDafny仕様の人間ラベル付きデータセットに,我々の測定値が密接に一致することを示す。 また、このテクニックをより広く適用するために対処する必要がある正式な検証課題についても概説する。
  論文  参考訳（メタデータ） (2024-06-14T06:52:08Z)
• 3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers [5.102523342662388]
  3DGenは、AIエージェントを使用して、混合非公式入力を3Dと呼ばれる言語でフォーマット仕様に変換するフレームワークである。 3DGenはテストスイートに準拠した3D仕様を生成する。
  論文  参考訳（メタデータ） (2024-04-16T07:53:28Z)
• NLP Verification: Towards a General Methodology for Certifying Robustness [9.897538432223714]
  検証された部分空間のセマンティック・ジェネリシビリティの技術的課題について論じる。 埋め込みギャップの効果を解析するための一般的な手法を提案する。 我々は,NLP検証パイプラインの一部として報告すべきもう一つの基本指標として,意味的部分空間のファルシフィビリティの尺度を提案する。
  論文  参考訳（メタデータ） (2024-03-15T09:43:52Z)
• Faithful Explanations of Black-box NLP Models Using LLM-generated Counterfactuals [67.64770842323966]
  NLPシステムの予測に関する因果的説明は、安全性を確保し、信頼を確立するために不可欠である。 既存の手法は、しばしばモデル予測を効果的または効率的に説明できない。 本稿では, 対物近似(CF)の2つの手法を提案する。
  論文  参考訳（メタデータ） (2023-10-01T07:31:04Z)
• Prototype-based Aleatoric Uncertainty Quantification for Cross-modal Retrieval [139.21955930418815]
  クロスモーダル検索手法は、共通表現空間を共同学習することにより、視覚と言語モダリティの類似性関係を構築する。 しかし、この予測は、低品質なデータ、例えば、腐敗した画像、速いペースの動画、詳細でないテキストによって引き起こされるアレタリック不確実性のために、しばしば信頼性が低い。 本稿では, 原型に基づくAleatoric Uncertainity Quantification (PAU) フレームワークを提案する。
  論文  参考訳（メタデータ） (2023-09-29T09:41:19Z)
• Natural Language Processing for Requirements Formalization: How to Derive New Approaches? [0.32885740436059047]
  我々はNLPの分野における主要な考え方と最先端の方法論について論じる。 我々は2つの異なるアプローチを詳細に議論し、ルールセットの反復的開発を強調した。 提案手法は, 自動車分野と鉄道分野の2つの産業分野において実証された。
  論文  参考訳（メタデータ） (2023-09-23T05:45:19Z)
• Validation Diagnostics for SBI algorithms based on Normalizing Flows [55.41644538483948]
  本研究は,NFに基づく多次元条件(後)密度推定器の検証診断を容易にすることを提案する。 また、局所的な一貫性の結果に基づいた理論的保証も提供する。 この作業は、より良い特定モデルの設計を支援したり、新しいSBIアルゴリズムの開発を促進するのに役立つだろう。
  論文  参考訳（メタデータ） (2022-11-17T15:48:06Z)
• A Latent-Variable Model for Intrinsic Probing [93.62808331764072]
  固有プローブ構築のための新しい潜在変数定式化を提案する。 我々は、事前訓練された表現が言語間交互に絡み合ったモルフォシンタクスの概念を発達させる経験的証拠を見出した。
  論文  参考訳（メタデータ） (2022-01-20T15:01:12Z)
• Verifiable RNN-Based Policies for POMDPs Under Temporal Logic Constraints [31.829932777445894]
  RNNベースのポリシーの適用の大きな欠点は、行動仕様の満足度に関する正式な保証を提供することの難しさである。 形式的手法と機械学習の技法を統合することにより,RNNから有限状態制御器を自動的に抽出する手法を提案する。
  論文  参考訳（メタデータ） (2020-02-13T16:38:38Z)

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

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