Trusta：用形式化方法与大语言模型对保证案例进行推理
软件工程
2023-09-25 v1 人工智能
摘要
保证案例可用于在安全工程中论证产品的安全性。在安全关键领域，保证案例的构建不可或缺。可信推导树 (TDTs) 通过引入形式化方法增强保证案例，使对保证案例的自动推理成为可能。我们提出可信推导树分析器 (Trusta)，这是一个用于自动构建和验证 TDTs 的桌面应用。该工具后端内置 Prolog 解释器，并得到约束求解器 Z3 和 MONA 的支持。因此，它能求解涉及算术、集合、Horn 子句等的逻辑公式约束。Trusta 还利用大语言模型使保证案例的创建与评估更为便捷，并支持交互式人工审查与修改。我们评估了 ChatGPT-3.5、ChatGPT-4 和 PaLM 2 等顶级语言模型生成保证案例的能力，测试显示机器生成与人工创建的案例之间有 50%–80% 的相似度。此外，Trusta 可从自然语言文本中提取形式化约束，便于解释与验证。该提取过程需人工审查与修正，将自动化的高效与人的洞察力相结合。据我们所知，这标志着大语言模型首次被集成到保证案例的自动创建与推理中，为传统挑战带来新方法。通过若干工业案例研究，Trusta 已证明能快速发现人工检查中常遗漏的细微问题，展现了其在提升保证案例开发流程中的实用价值。
引用
@article{arxiv.2309.12941,
title = {Trusta: Reasoning about Assurance Cases with Formal Methods and Large Language Models},
author = {Zezhong Chen and Yuxin Deng and Wenjie Du},
journal= {arXiv preprint arXiv:2309.12941},
year = {2023}
}
备注
38 pages