支持使用大语言模型调试和理解规范需求的工具-计算机科学-人工智能-大语言模型.pdf

支持使用大语言模型调试和理解规范需求的

工具

AlexKleijwegt,SinemGetirYaman,RaduCalinescu

DepartmentofComputerScience,UniversityofYork,UnitedKingdom

I.介绍形式“当触发然后响应”。这样的规则定义了触发器中

的事件发生时所需响应，并且其条件（如果有）得到满

规范要求指明系统必须遵守的社会、法律、伦理、

足。一个规则可以伴随一个或多个击败者，使用“除非”

同理心和文化（SLEEC）准则。为了支持识别SLEEC

结构引入。该语言包含时间构造，允许使用“在内部”结

需求，已经制定了许多标准和法规（例如，[1]）。这些

构进行具有截止日期和超时的响应。

需求通常由具有不同专业知识的非技术系统的利益相

本给定这样的SLEEC规则集，一个名为SLEEC-

关者定义（例如，伦理学家、律师、社会科学家）。因

译此，确保其一致性和管理需求提取过程是复杂且容易出VAL[4]的现有工具将这些规则翻译成一种称为时钟

中错的任务[2],[3]。最近的研究使用领域特定语言来将规CSP的形式语言，这是一种时变过程代数，如图1所

1范要求规定为规则以应对这一挑战，然后可以使用形式示。在CSP中定义的形式语义然后使用FDR模型检查

v

器[8]进行一致性分析。然而，结果（特别是反例）对

4方法分析这些规则的一致性[4]–[7]。

0于非技术人员来说难以理解，例如，规则“1当检测用

5然而，这些方法通常以非技术用户难以理解的方式

5呈现形式验证工具的结果。这阻碍了理解，并使提取和户跌倒然后呼叫紧急支持在内部2分钟除非紧急级别L4

0.然后呼叫紧急支持”和“2当检测用户跌倒和紧急级别L2

7验证这些需求的迭代过程在时间和精力上都变得低效。

0为了解决这个问题，我们引入了SLEEC-LLM，一然后不联系紧急支援在2分钟”是冲突的，工具以以下

5形式报告反例，其中滴答是一个时间单位。

2种利用大型语言模型（LLMs）对与SLEEC规则不一

:

v致性相关的模型检查反例提供自然语言解释的工具[4],DetectUserFallen,emergencyLevel.E1,

i

x[5]。SLEEC-LLM提高了规范需求提取和一致性分析的emergencyLevel.E1,tock,...,tock

r

a效率和可解释性。为了展示其有效性，我们在两个涉及这样的输出对于非技术人员来说不容易理解，并且缺

非技术利益相关者的实际案例研究中对其使用进行了乏对系统探索性解决方案的解释，例如发生了哪种类

总结。型的错误。我们的LLM支持的调试和解决工具（可在

GitHub上公开获取[9]）解决了这个问题。

II.问题描述