CoDefeater: Using LLMs To Find Defeaters in Assurance Cases
作者: Usman Gohar, Michael C. Hunter, Robyn R. Lutz, Myra B. Cohen
分类: cs.SE, cs.AI
发布日期: 2024-07-18 (更新: 2024-08-16)
备注: ASE 2024 NIER
💡 一句话要点
CoDefeater：利用大型语言模型自动发现保障案例中的反驳论证
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 保障案例 反驳论证 大型语言模型 安全关键系统 自动化 安全分析 LLM应用
📋 核心要点
- 保障案例的构建依赖专家经验，且需迭代更新以适应变化的需求和法规，这使得发现潜在的反驳论证成为一项挑战。
- CoDefeater利用大型语言模型自动生成反驳论证，旨在辅助安全分析师识别保障案例中的薄弱环节。
- 实验结果表明，该方法能够有效地发现已知和未预见的反驳论证，从而提高保障案例的完整性和可信度。
📝 摘要（中文）
构建保障案例是广泛使用，有时甚至是强制性的流程，旨在证明安全关键型系统在其计划环境中能够安全运行。为了降低错误和遗漏边缘情况的风险，引入了反驳论证（defeaters）的概念，即挑战保障案例中声明的论点或证据。反驳论证可以及时检测论证中的弱点，促使进一步调查和及时缓解。然而，捕获反驳论证依赖于专家判断、经验和创造力，并且由于不断变化的需求和法规，必须迭代进行。本文提出了CoDefeater，一种利用大型语言模型（LLMs）自动查找反驳论证的过程。在两个系统上的初步结果表明，LLMs可以有效地找到已知和未预见的可行反驳论证，以支持安全分析师增强保障案例的完整性和置信度。
🔬 方法详解
问题定义：论文旨在解决安全关键系统中保障案例构建过程中，人工识别反驳论证效率低、易遗漏的问题。现有方法依赖于专家经验，耗时且难以覆盖所有潜在的反驳情况，尤其是在需求和法规不断变化的情况下。
核心思路：论文的核心思路是利用大型语言模型（LLMs）的强大生成能力，自动生成针对保障案例中各项声明的反驳论证。通过提示LLM扮演攻击者的角色，促使其从不同角度挑战既有论证，从而发现潜在的缺陷和漏洞。
技术框架：CoDefeater的整体流程包括以下几个主要步骤：1) 输入保障案例的结构化表示，包括声明、论据和证据；2) 利用LLM，基于输入的保障案例信息，生成潜在的反驳论证；3) 对生成的反驳论证进行过滤和排序，去除不相关或无效的论证；4) 将筛选后的反驳论证呈现给安全分析师，供其进一步评估和验证。
关键创新：该方法最重要的创新点在于将大型语言模型应用于保障案例的反驳论证生成，实现了自动化和智能化。与传统的人工方法相比，CoDefeater能够更高效、更全面地发现潜在的反驳论证，从而提高保障案例的质量和可靠性。
关键设计：论文中没有详细描述关键的参数设置、损失函数、网络结构等技术细节。但可以推断，关键在于如何设计有效的提示语（prompt），引导LLM生成高质量的反驳论证。这可能涉及到对LLM进行微调，或者采用特定的prompt工程技术。
🖼️ 关键图片
📊 实验亮点
论文在两个不同的系统上进行了实验，结果表明LLMs能够有效地找到已知和未预见的可行反驳论证。虽然论文没有提供具体的性能数据，但强调了CoDefeater能够辅助安全分析师增强保障案例的完整性和置信度，表明了其在实际应用中的潜力。
🎯 应用场景
CoDefeater可应用于航空航天、汽车、医疗等安全关键领域的系统保障案例构建。通过自动发现反驳论证，该方法能够帮助工程师尽早发现系统设计和论证中的缺陷，降低安全风险，并提高系统可靠性。未来，该技术有望集成到现有的保障案例工具链中，实现更智能化的安全分析。
📄 摘要（原文）
Constructing assurance cases is a widely used, and sometimes required, process toward demonstrating that safety-critical systems will operate safely in their planned environment. To mitigate the risk of errors and missing edge cases, the concept of defeaters - arguments or evidence that challenge claims in an assurance case - has been introduced. Defeaters can provide timely detection of weaknesses in the arguments, prompting further investigation and timely mitigations. However, capturing defeaters relies on expert judgment, experience, and creativity and must be done iteratively due to evolving requirements and regulations. This paper proposes CoDefeater, an automated process to leverage large language models (LLMs) for finding defeaters. Initial results on two systems show that LLMs can efficiently find known and unforeseen feasible defeaters to support safety analysts in enhancing the completeness and confidence of assurance cases.