面向NextG协议形式化验证的自动建模：一种多模态交叉与自注意力大语言模型方法
系统与控制
2024-01-03 v2 人工智能
机器学习
系统与控制
摘要
本文介绍了AVRE（基于真实世界提示的5G与NextG协议形式化验证自动建模系统），这是一个专为下一代（NextG）通信协议形式化验证设计的新型系统，旨在应对网络协议设计与验证中日益增长的复杂性和可扩展性挑战。利用大语言模型（LLM），AVRE将协议描述转换为依赖图与形式化模型，高效解决歧义并捕捉设计意图。该系统将Transformer模型与LLM集成，通过交叉与自注意力机制自主建立可量化的依赖关系。借助HyFuzz实验平台的迭代反馈增强，AVRE显著提升了复杂通信协议形式化验证的准确性与相关性，为验证复杂通信系统提供了一种开创性方法。我们将CAL的性能与基于LLM的最先进模型及传统时间序列模型进行了比较，证明了其在准确性和鲁棒性上的优越性，达到了95.94%的准确率和0.98的AUC。这种基于NLP的方法首次实现了直接从设计文档生成漏洞利用，在可扩展系统验证与确认方面取得了显著进展。
引用
@article{arxiv.2312.17353,
title = {Towards Auto-Modeling of Formal Verification for NextG Protocols: A Multimodal cross- and self-attention Large Language Model Approach},
author = {Jingda Yang and Ying Wang},
journal= {arXiv preprint arXiv:2312.17353},
year = {2024}
}