走向基于 LLM 的代理方法，从非结构化规范进行需求形式化

安全关键系统的早期规范通常用自然语言表达，因此很难导出适合验证和保证安全所需的形式属性。虽然最近基于 大语言模型 (LLM) 的方法可以从文本生成形式工件，但它们主要关注语法正确性，并且不能确保非正式需求和形式可验证属性之间的语义对齐。我们提出了一种代理方法，可以自动从非结构化规范中提取可供验证的属性。模块化管道结合了需求提取、针对目标形式主义的兼容性过滤以及转换为形式属性。三个场景的实验结果表明，该管道生成语法和语义一致的形式属性，准确率达到 77.8%。通过明确考虑建模和验证约束，该方法为利用人工智能（AI）弥合非正式描述和语义上有意义的形式验证之间的差距铺平了一步。