想象一下，你是一位身处高风险法庭的法官，但你裁决的不是某人是否犯罪，而是判断一辆自动驾驶汽车是否足够安全，可以驶上公路。在工程领域，这不仅仅是一种直觉；这是一个被称为“保证案例”（Assurance Case）的正规过程。你可以将保证案例想象成一个巨大的逻辑谜题，工程师们通过堆叠证据——如测试结果、代码审查和安全检查——来构建一座证明之塔，以此宣告：“我们确信这个系统不会伤害任何人。”
长期以来，工程师们一直难以衡量这种“信心”。有些人试图变得极其精确，分配像“93.4% 信心”这样的精确数字。但这很棘手。93.4% 足够了吗？93.3% 会是一场灾难吗？这就像试图仅用一把尺子来描述草莓的味道；这些数字显得冰冷、令人困惑，且极易被误解。另一些人则使用“相当确定”或“非常担心”这类模糊的词汇，但这样很难进行数学运算，以观察整个证明之塔是否稳固。核心问题在于：我们如何将数学的精确性与人类感知风险时那种自然的、模糊的思维方式结合起来？
就在这时，一个名为 Certus 的新工具登场了。这篇论文将 Certus 介绍为一种特殊的“语言”，旨在帮助工程师以一种既符合直觉又具备数学逻辑的方式来讨论信心。Certus 不再强迫工程师去选择像 0.87 这样的特定数字，而是允许他们使用“高”、“低”或“极低”等模糊词汇。但其中的魔力在于：Certus 将这些词汇视为“模糊集”（fuzzy sets）。想象一下一个滑动刻度，其中“高”不仅仅是一个点，而是一个与“中等”相重叠的软性可能性云团。这使得系统能够对这些“云团”进行计算，并将这种“模糊性”一路传递到论证之塔顶端的最终裁决。
作者 Simon Diemert 和 Jens H. Weber 指出，这种方法解决了几个难题。首先，它阻止了人们对数字的误读（不再为 0.07% 的失败概率而恐慌）。其次，它承认人类的判断本质上是模糊的，并允许工程师在不丢失这种细微差别的情况下表达这种微妙感。第三，它处理了“反驳因素”（defeaters）——这些就像是试图推倒论证之塔的小型“抓包”论据。Certus 有一种特殊的方法，可以让这些“抓包”论据在不破坏整个系统的情况下，从信心值中进行扣减。
为了测试他们的想法，团队构建了一个 Certus 的原型，并将其应用于一个现实世界的案例：汽车自适应巡航控制（ACC）系统的安全论证。他们展示了这种语言如何将简单的陈述（如“代码审查的信心水平非常高”）与“硬件可能会失效”相结合，从而产生最终的、计算出的信心水平。当他们将 Certus 的模糊结果与一种使用严格数字的旧方法进行比较时，结果相似，但 Certus 感觉更加直观且透明。
这篇论文并未声称 Certus 是一个已经完工、可以立即投入每个工厂使用的完美产品。相反，它表明这是一个充满前景的新方向。作者承认，他们还需要做更多工作，才能将这个原型转化为工程师日常使用的工具，包括创建更好的可视化图表，以及证明其结果在涉及生死攸关的决策时足够可靠。但就目前而言，Certus 为构建对即将驾驶我们的机器的信任，提供了一种既有趣又强大的新途径。
技术摘要：Certus —— 一种用于保证案例中置信度评估的领域特定语言
问题陈述
保证案例（Assurance Cases, ACs）是用于证明关键系统满足安全性或安全性等质量属性的结构化论证。虽然存在各种记法来组织这些论证（例如，目标结构化记法 GSN、主张-论据-证据模型），但确定这些论证有效性的“置信度”（confidence）仍然是一个挑战。现有的定量置信度评估方法（CAMs）试图分配数值，但面临着显著的采用障碍。本文识别了当前定量 CAMs 的五个主要局限性：
- 解释性： 数值输出（如 0.93）在关于可接受性阈值方面难以解释，且容易被非专家误解。
- 主观性： 强迫专家对模糊判断分配精确数字，忽略了人类推理中的自然变异性，并丢失了定性的细微差别。
- 扩展性： 诸如 Dempster-Shafer 理论之类的方法需要过多的输入参数（例如，每个叶节点需要四个值），这使得大规模 AC 的应用变得不切实际。
- 削弱因素（Defeaters）： 很少有方法能妥善处理“削弱因素”（即引入怀疑或负面置信度的辩证推理）。
- 可信度： 复杂的数学框架往往表现为“黑盒”，降低了从业者的信任，且缺乏实证验证来证明这些方法产生的结果符合直觉。
方法论
本文介绍了 Certus，一种旨在通过结合**模糊集理论（fuzzy set theory）**与可编程语法进行置信度传播来解决上述局限性的领域特定语言（DSL）。
- 利用模糊集建模置信度： Certus 不使用精确数字，而是允许用户使用语言术语（如“高”、“极低”、“确定”）来分配置信度。这些术语被建模为定义在定义域 β=[0,1] 上的模糊集（隶属函数）。该语言包含了预定义的规范集合（零、极低、低、中、高、极高、确定），并允许用户定义自定义的凸归一化模糊集。这种方法捕捉了工程判断中固有的模糊性，同时保持了数学上的严谨性。
- 置信度传播： 置信度从有向无环图（DAG）的叶子节点（证据）递归地评估到根节点（顶层主张）。Certus 使用
cases 表达式来定义传播规则。这些规则通过匹配子节点的模糊集条件（使用 is、contains、overlaps、>、< 等运算符），并将结果映射为父节点的模糊集。
- 处理削弱因素： 削弱因素被建模为降低置信度的负面前提。Certus 包含一个“预检”系统，通过静态分析验证用户定义的传播规则（包括由宏生成的规则）是否符合处理削弱因素的 12 条既定规则，从而确保辩证推理被正确集成。
- 通过宏实现可扩展性： 为了支持扩展，Certus 允许定义参数化传播算子和宏。宏（通过 Python 等脚本接口实现）可以根据论证结构动态展开为
cases 表达式，从而减少大规模 AC 的手动工作量。此外，还提供了一个内置的 FUSE 宏，用于平衡和合并多个模糊集。
核心贡献
- Certus 语言： 提出了首个使用模糊集对 AC 置信度进行建模，并通过结构化论证使用用户定义表达式进行传播的 DSL。
- 语言化置信度的形式化： 突破了以往仅提出语言化置信度概念而缺乏形式化的研究，Certus 提供了一种为节点分配模糊集并定义传播逻辑的语法。
- 削弱因素集成： 一种能够显式建模并在论证结构中传播“负面置信度”的机制，并经过针对削弱因素规则的验证。
- 透明度： 通过使用简单、可检查的表达式（
cases 算子）而非晦涩的数学公式，Certus 旨在提高从业者的可信度和理解能力。
结果
本文展示了将 Certus 应用于汽车自适应巡航控制（ACC）保证案例片段的证明概念实现。
- 应用： 该示例演示了如何使用参数化算子（
invert、boundedInvert）和 FUSE 宏来处理复杂的推理步骤，包括证据和削弱因素的集成。
- 对比： 作者将 Certus 的结果与之前对同一片段进行的贝叶斯网络（BBN）分析进行了比较。BBN 得出了 0.39 的数值置信度。Certus 的结果与该值一致（解释为一个对应于低到中等置信度水平的模糊集），这表明该方法在提供不同表示形式的同时，与现有的定量方法保持了一致性。
意义与主张
作者将 Certus 定位为并非旨在取代定性或定量方法，而是作为一种解决现有定量 CAMs 特定弱点的工具。这项工作的意义在于：
- 弥合差距： 允许专家以具有语言意义的方式表达置信度（解决主观性问题），同时保留计算和传播置信度的能力（解决定量评估的需求）。
- 提高信任： 通过使传播规则显式化且可检查，Certus 旨在减少当前工具的“黑盒”性质。
- 可扩展性： 宏和可重用算子的使用旨在使大规模、复杂的保证案例进行定量评估成为可能。
论文结论较为谦逊，承认 Certus 目前仍处于原型阶段。未来的工作包括创建形式化规范、开发图形化表示以提高可读性，以及开展实证研究以验证其可用性和可信度。
每周获取最佳 electrical engineering 论文。
受到斯坦福、剑桥和法国科学院研究人员的信赖。
请查收邮箱确认订阅。
出了点问题，再试一次？
无垃圾邮件，随时退订。