# Towards Auto-Modeling of Formal Verification for NextG Protocols: A Multimodal cross- and self-attention Large Language Model Approach

arXiv: https://arxiv.org/abs/2312.17353 · HTML: https://mlsanity.com/paper/2312.17353/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 18 of its 35 references that are in the map.
- First posted on arXiv 28 Dec 2023.

## Builds on (most cited first, 18 of 18)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding](https://mlsanity.com/paper/1810.04805/) (2018)
- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Not what you've signed up for: Compromising Real-World LLM-Integrated Applications with Indirect Prompt Injection](https://mlsanity.com/paper/2302.12173/) (2023)
- [CoQA: A Conversational Question Answering Challenge](https://mlsanity.com/paper/1808.07042/) (2018)
- [Language Models Are Greedy Reasoners: A Systematic Formal Analysis of Chain-of-Thought](https://mlsanity.com/paper/2210.01240/) (2022)
- [Language to Logical Form with Neural Attention](https://mlsanity.com/paper/1601.01280/) (2016)
- [An Empirical Study of the Non-determinism of ChatGPT in Code Generation](https://mlsanity.com/paper/2308.02828/) (2023)
- [RankGen: Improving Text Generation with Large Ranking Models](https://mlsanity.com/paper/2205.09726/) (2022)
- [nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models](https://mlsanity.com/paper/2303.04864/) (2023)
- [A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification](https://mlsanity.com/paper/2305.14752/) (2023)
- [The FormAI Dataset: Generative AI in Software Security Through the Lens of Formal Verification](https://mlsanity.com/paper/2307.02192/) (2023)
- [Formal Specifications from Natural Language](https://mlsanity.com/paper/2206.01962/) (2022)
- [(Security) Assertions by Large Language Models](https://mlsanity.com/paper/2306.14027/) (2023)
- [Using LLMs to Facilitate Formal Verification of RTL](https://mlsanity.com/paper/2309.09437/) (2023)
- [Formal and Fuzzing Amplification: Targeting Vulnerability Detection in 5G and Beyond](https://mlsanity.com/paper/2307.05758/) (2023)
- [Formal-Guided Fuzz Testing: Targeting Security Assurance from Specification to Implementation for 5G and Beyond](https://mlsanity.com/paper/2307.11247/) (2023)
- [From Ambiguity to Explicitness: NLP-Assisted 5G Specification Abstraction for Formal Analysis](https://mlsanity.com/paper/2308.03277/) (2023)

## Built on by (most cited first, 1 of 1)

- [Decision-Theoretic Safety Assessment of Persona-Driven Multi-Agent Systems in O-RAN](https://mlsanity.com/paper/2604.09682/) (2026)

## Abstract (arXiv)

This paper introduces Auto-modeling of Formal Verification with Real-world Prompting for 5G and NextG protocols (AVRE), a novel system designed for the formal verification of Next Generation (NextG) communication protocols, addressing the increasing complexity and scalability challenges in network protocol design and verification. Utilizing Large Language Models (LLMs), AVRE transforms protocol descriptions into dependency graphs and formal models, efficiently resolving ambiguities and capturing design intent. The system integrates a transformer model with LLMs to autonomously establish quantifiable dependency relationships through cross- and self-attention mechanisms. Enhanced by iterative feedback from the HyFuzz experimental platform, AVRE significantly advances the accuracy and relevance of formal verification in complex communication protocols, offering a groundbreaking approach to validating sophisticated communication systems. We compare CAL's performance with state-of-the-art LLM-based models and traditional time sequence models, demonstrating its superiority in accuracy and robustness, achieving an accuracy of 95.94% and an AUC of 0.98. This NLP-based approach enables, for the first time, the creation of exploits directly from design documents, making remarkable progress in scalable system verification and validation.