基于大语言模型的自动驾驶汽车安全断言生成方法及其在智能城市系统中的应用研究

《IEEE Access》：LLM-Guided Security Claim Generation for Autonomous Vehicle in Smart Urban Systems

本文针对自动驾驶汽车硬件安全验证中人工编写SystemVerilog断言效率低、易出错的问题，研究人员开展了一项LLM引导的安全断言生成研究。通过构建包含四个基准模块的评估框架，并采用结构化提示工程和仿真验证，实验结果表明在完整设计上下文下LLM可生成超过50%的正确断言。该研究为将生成式AI应用于形式化验证、提升智能交通系统安全性提供了新思路。

　　

随着自动驾驶技术和智能城市的快速发展，确保自动驾驶汽车的安全性和可靠性已成为一项至关重要的挑战。自动驾驶汽车的安全不仅依赖于高层次的感知和决策算法，更取决于底层硬件组件的行为正确性。在传统硬件设计流程中，工程师需要手动编写形式化的安全断言，例如SystemVerilog断言，来验证硬件设计是否满足特定的安全属性。然而，这个过程极其耗时、容易出错，并且需要深厚的专业知识，尤其是在系统日益复杂的背景下，这成为了一个显著的瓶颈。

与此同时，大语言模型在代码生成、自然语言理解等任务上展现出强大能力，但在为低层级硬件生成形式化安全断言这一特定领域，其潜力尚未被系统性地探索。现有的自动化验证工具要么缺乏灵活性，要么无法充分利用LLM的语义理解和生成能力。因此，一个核心问题浮现出来：能否利用LLM来自动化地生成准确、可靠的硬件安全断言，从而显著提升自动驾驶汽车硬件验证的效率和可靠性？

为了回答这个问题，研究人员在《IEEE Access》上发表了题为“LLM-Guided Security Claim Generation for Autonomous Vehicle in Smart Urban Systems”的研究论文。这项研究旨在开发一个新颖的评估框架，系统地评估LLM为自动驾驶汽车子系统自动生成形式化安全断言的能力。该研究聚焦于一个尚未被充分探索的领域——硬件级的安全验证，并试图弥合高层AI规划与底层系统安全之间的鸿沟。

研究人员开展了一项严谨的实证研究。他们首先构建了一个全面的基准测试套件，包含了四个与自动驾驶汽车相关的硬件模块，每个模块都对应一个由通用缺陷枚举分类的特定硬件漏洞。这些基准模块包括交通信号灯控制器、AES加密模块、权限级别寄存器控制器以及ADC复位逻辑。研究框架的核心是一个自动化的断言生成管道，它利用LLM根据结构化的自然语言提示生成SystemVerilog断言。该管道还包含了语法校正和基于仿真的验证环节，以评估生成断言的正確性。实验主要使用了OpenAI的Codex模型，并系统性地改变了提供给模型的提示细节水平，从最小上下文到完整设计上下文，以评估不同条件下LLM的推理性能。

研究结果表明，LLM在生成硬件安全断言方面展现出可喜的潜力，但其性能强烈依赖于所提供的上下文信息。当LLM获得完整的设计上下文时，其生成正确断言的比例可以超过50%；然而，当输入信息有限时，性能会显著下降。研究还对断言失败的原因进行了分类，主要分为逻辑错误和语法错误，这为未来改进LLM在此类任务上的表现提供了明确方向。这项研究首次为LLM生成的SystemVerilog断言在自动驾驶系统中的应用建立了系统的基准和评估管道，揭示了生成式模型在支持智能交通和智慧城市基础设施形式化验证方面的潜力。

为开展研究，作者主要应用了以下几项关键技术方法：构建了涵盖四个AV硬件模块的基准测试套件，每个模块对应特定的CWE漏洞类型；设计了分层次的提示工程策略，包括不同详细程度的注释和示例；采用了基于OpenAI Codex的LLM进行SystemVerilog断言生成；开发了自动化的语法校正模块对原始输出进行修复；利用ModelSim仿真器对生成的断言进行编译和功能验证，并与人工编写的黄金断言进行比对以评估正确性。

基准测试套件

研究设计了四个基准模块来评估LLM的性能。BM1是交通信号灯控制器，其安全属性要求黄灯必须在红灯亮起前至少激活一个时钟周期，以避免不安全的直接切换，对应CWE-1245。BM2是AES加密模块，要求确保在加密操作未完成时不能输出数据，防止数据泄漏，对应CWE-1303。BM3是基于CVA6核心的寄存器控制器，需要检测当权限级别低于要求时触发的访问违规，对应CWE-1261。BM4是ADC控制器，要求系统复位时唤醒计时器必须被清零，对应CWE-1221。每个基准都提供了三种设计变体：EmptyDUT（最小上下文）、CorrectDUT（正确设计）和BuggyDUT（包含已知漏洞的设计），以测试LLM在不同信息量下的表现。

评估框架与实验设置

评估框架是一个多阶段的自动化管道。它从提示生成器开始，根据基准模块的安全属性生成结构化的自然语言提示。这些提示随后被输入到LLM中，由其生成候选的SystemVerilog断言。由于初始输出可能存在缺陷，一个专用的语法校正模块会处理这些断言，修复格式错误。最后，仿真器在代表性的硬件设计实例上执行每个校正后的断言，并根据仿真结果将其分类为正确或错误。实验使用OpenAI的Codex模型，并配置了特定的参数，如最大生成长度和温度，以平衡输出的创造性和一致性。

结果分析

整体性能分析显示，LLM生成的断言在编译通过率上普遍较高（超过85%），但功能正确性因基准模块的复杂性而异。BM1和BM4这两个逻辑相对简单的模块取得了最高的正确率，分别为45.2%和50.4%。而涉及复杂时序和条件逻辑的BM2和BM3模块，正确率则较低，分别为32.8%和28.9%。这表明硬件逻辑的复杂性显著影响LLM的成功率。

提示细节的影响非常显著。当提供完整的设计上下文时，断言正确率最高可达65%；而仅提供最小上下文时，正确率骤降至15%。研究还发现，当设计上下文保持在60-70%的完整度时，正确率可以维持在40%以上，这为实际应用提供了实用的阈值参考。

错误分类诊断表明，逻辑错误是导致断言失败的主要原因，占比约40%，其次是语法错误（35%）。逻辑错误多表现为时序操作符使用不当、前提条件触发缺失或时钟边沿同步错误等问题，这在BM2和BM3中尤为常见。

此外，LLM的配置参数也影响结果。较低的温度设置（如0.4）会产生更确定、更准确的结果，而较高的频率惩罚则有助于减少重复并提高正确性。

讨论与结论

该研究证实了LLM在自动化生成硬件安全断言方面的可行性与局限性。LLM在具备充分上下文信息时，能够有效辅助形式化验证过程，尤其适用于逻辑相对直接的场景。然而，对于涉及复杂多条件时序依赖和抽象安全概念的模块，LLM的表现仍有待提升。这凸显了领域特定知识和大规模语料库对于训练专门化模型的重要性。

这项研究的意义在于，它为将生成式人工智能集成到安全关键系统的开发流程中奠定了基础。通过自动化部分繁琐且易出错的形式化断言编写工作，该框架有望显著提高自动驾驶汽车硬件设计的验证效率，加速开发周期，并增强最终系统的可靠性和安全性。这不仅适用于自动驾驶领域，其方法论还可扩展至航空航天、工业控制系统等其他对安全性要求极高的领域。

未来研究的方向包括对LLM进行领域特定的微调，将其与传统的符号化形式验证工具结合形成混合验证框架，以及将基准测试套件扩展至更广泛的自动驾驶组件，如V2X通信模块等。随着智能城市基础设施日益依赖人工智能代理，确保这些系统底层硬件的可验证性和正确性不仅是一个技术挑战，更是一项社会需求。本研究为推动构建更具弹性、可信和可扩展的智能移动系统迈出了重要一步。