From Ambiguity to Explicitness: NLP-Assisted 5G Specification Abstraction for Formal Analysis

• URL: http://arxiv.org/abs/2308.03277v1
• Date: Mon, 7 Aug 2023 03:37:31 GMT
• Title: From Ambiguity to Explicitness: NLP-Assisted 5G Specification Abstraction for Formal Analysis
• Authors: Shiyu Yuan, Jingda Yang, Sudhanshu Arya, Carlo Lipizzi, Ying Wang
• Abstract summary: We introduce a two-step pipeline that uses NLP tools to construct data and then uses constructed data to extract identifiers and formal properties. Our results of the optimal model reach valid accuracy of 39% for extraction and 42% for formal properties identifier predictions.
• Score: 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.

Related papers

• Networks of Networks: Complexity Class Principles Applied to Compound AI Systems Design [63.24275274981911]
  Compound AI Systems consisting of many language model inference calls are increasingly employed. In this work, we construct systems, which we call Networks of Networks (NoNs) organized around the distinction between generating a proposed answer and verifying its correctness. We introduce a verifier-based judge NoN with K generators, an instantiation of "best-of-K" or "judge-based" compound AI systems.
  arXiv  Detail & Related papers  (2024-07-23T20:40:37Z)
• MetaKP: On-Demand Keyphrase Generation [52.48698290354449]
  We introduce on-demand keyphrase generation, a novel paradigm that requires keyphrases that conform to specific high-level goals or intents. We present MetaKP, a large-scale benchmark comprising four datasets, 7500 documents, and 3760 goals across news and biomedical domains with human-annotated keyphrases. We demonstrate the potential of our method to serve as a general NLP infrastructure, exemplified by its application in epidemic event detection from social media.
  arXiv  Detail & Related papers  (2024-06-28T19:02:59Z)
• Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
  We propose a metric for evaluating the quality of specifications for verification-aware languages. We show that our metric agrees closely on a human-labeled dataset of Dafny specifications for the popular MBPP code-generation benchmark. We also outline formal verification challenges that need to be addressed to apply the technique more widely.
  arXiv  Detail & Related papers  (2024-06-14T06:52:08Z)
• 3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers [5.102523342662388]
  3DGen is a framework that makes use of AI agents to transform mixed informal input into format specifications in a language called 3D. 3DGen produces a 3D specification that conforms to a test suite, and which yields safe, efficient, provably correct, parsing code in C.
  arXiv  Detail & Related papers  (2024-04-16T07:53:28Z)
• NLP Verification: Towards a General Methodology for Certifying Robustness [9.897538432223714]
  We discuss the technical challenge of semantic generalisability of verified subspaces. We propose a general methodology to analyse the effect of the embedding gap. We propose the metric of falsifiability of semantic subspaces as another fundamental metric to be reported as part of the NLP verification pipeline.
  arXiv  Detail & Related papers  (2024-03-15T09:43:52Z)
• Faithful Explanations of Black-box NLP Models Using LLM-generated Counterfactuals [67.64770842323966]
  Causal explanations of predictions of NLP systems are essential to ensure safety and establish trust. Existing methods often fall short of explaining model predictions effectively or efficiently. We propose two approaches for counterfactual (CF) approximation.
  arXiv  Detail & Related papers  (2023-10-01T07:31:04Z)
• Prototype-based Aleatoric Uncertainty Quantification for Cross-modal Retrieval [139.21955930418815]
  Cross-modal Retrieval methods build similarity relations between vision and language modalities by jointly learning a common representation space. However, the predictions are often unreliable due to the Aleatoric uncertainty, which is induced by low-quality data, e.g., corrupt images, fast-paced videos, and non-detailed texts. We propose a novel Prototype-based Aleatoric Uncertainty Quantification (PAU) framework to provide trustworthy predictions by quantifying the uncertainty arisen from the inherent data ambiguity.
  arXiv  Detail & Related papers  (2023-09-29T09:41:19Z)
• Natural Language Processing for Requirements Formalization: How to Derive New Approaches? [0.32885740436059047]
  We present and discuss principal ideas and state-of-the-art methodologies from the field of NLP. We discuss two different approaches in detail and highlight the iterative development of rule sets. The presented methods are demonstrated on two industrial use cases from the automotive and railway domains.
  arXiv  Detail & Related papers  (2023-09-23T05:45:19Z)
• Validation Diagnostics for SBI algorithms based on Normalizing Flows [55.41644538483948]
  This work proposes easy to interpret validation diagnostics for multi-dimensional conditional (posterior) density estimators based on NF. It also offers theoretical guarantees based on results of local consistency. This work should help the design of better specified models or drive the development of novel SBI-algorithms.
  arXiv  Detail & Related papers  (2022-11-17T15:48:06Z)
• A Latent-Variable Model for Intrinsic Probing [93.62808331764072]
  We propose a novel latent-variable formulation for constructing intrinsic probes. We find empirical evidence that pre-trained representations develop a cross-lingually entangled notion of morphosyntax.
  arXiv  Detail & Related papers  (2022-01-20T15:01:12Z)
• Verifiable RNN-Based Policies for POMDPs Under Temporal Logic Constraints [31.829932777445894]
  A major drawback in the application of RNN-based policies is the difficulty in providing formal guarantees on the satisfaction of behavioral specifications. By integrating techniques from formal methods and machine learning, we propose an approach to automatically extract a finite-state controller from an RNN.
  arXiv  Detail & Related papers  (2020-02-13T16:38:38Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.