东方时讯网
在过去的几十年里，前所未有的技术进步使我们能够升级和现代化大部分基础设施并解决许多长期存在的后勤问题。例如，Babylon Health的AI驱动智能手机应用程序正在帮助评估北伦敦120万患者的优先级，电子转移使我们能够在世界任何地方即时汇款，并且在过去的20年中，GPS彻底改变了我们的导航方式，我们如何跟踪和运送货物，以及我们如何管理交通。
然而，指数增长伴随着必须导航的一系列障碍。最重要的问题是，预测各种技术将如何演变是非常困难的。因此，规划未来并确保实施必要的安全功能变得具有挑战性。
当涉及可能带来存在挑战的技术时，这种不确定性尤其令人担忧 - 例如人工智能。
然而，尽管明天的AI具有不可预测的性质，但某些挑战是可以预见的。例如，无论AI代理商最终采取的发展路径如何，这些系统都需要能够做出明智的决策，使其能够在我们的物理世界中无缝安全地移动。实际上，人工智能最有影响力的用途之一包括自动驾驶汽车，机器人外科医生，用户感知智能电网和飞机控制系统等技术 - 所有这些都将先进的决策过程与运动物理结合起来。
这种系统被称为网络物理系统(CPS)。下一代先进的CPS可以引领我们进入一个安全的新时代，将崩溃率降低90%，每年为世界各国节省数千亿美元- 但前提是这些系统本身正确实施。
这就是卡内基梅隆大学计算机科学副教授安德烈·普拉泽(Andre Platzer)所在的地方.Platzer的研究致力于确保CPS有益于人类并且不会造成伤害。实际上，这意味着确保系统灵活，可靠和可预测。
拥有安全系统意味着什么?
网络物理系统已经以某种形式出现了很长一段时间。例如，空中交通管制系统长期以来一直依赖CPS型技术来避免碰撞，交通管理和许多其他决策任务。但是，Platzer指出，随着CPS的不断发展，以及越来越需要集成更复杂的自动化和学习技术，确保CPS做出可靠和安全的决策变得更加困难。
为了更好地澄清问题的本质，Platzer转向自动驾驶车辆。在像这样的先进系统中，他指出我们需要确保技术足够复杂以实现灵活性，因为它必须能够安全地响应它所面临的任何情况。从这个意义上说，“如果他们不仅仅运行非常简单的[控制系统]，CPS就处于最佳状态，但如果它们运行的是更复杂和先进的系统，”Platzer指出。然而，当CPS利用高级自治时，因为它们非常复杂，所以要证明它们正在进行系统的合理选择变得更加困难。
在这方面，系统越复杂，我们就越不得不牺牲一些可预测性，从而牺牲系统的安全性。正如Platzer所阐述的那样，“在安全方面为您提供可预测性的简单性与您在人工智能方面需要的灵活性有些不一致。”
因此，最终目标是在灵活性和可预测性之间找到平衡 - 在先进学习技术和安全证明之间 - 以确保CPS能够安全有效地执行其任务。Platzer将这一总体目标描述为一种平衡行为，并指出，“利用网络物理系统，为了使复杂性变得可行和可扩展，保持系统尽可能简单也很重要。”
如何使系统安全
导航此问题的第一步是确定研究人员如何验证CPS是否真正安全。在这方面，Platzer指出，他的研究是由这个核心问题所驱动的：如果科学家对自动驾驶汽车或飞机这样的行为有一个数学模型，并且他们有信心控制器的所有行为是安全的，他们如何证明事实确实如此?
答案是一个自动定理证明器，它是一个计算机程序，可以帮助开发严格的数学正确性证明。
对于CPS，最高的安全标准是这样的数学正确性证明，表明系统总是为任何给定的输入产生正确的输出。它通过使用正式的数学方法来证明或反驳系统底层控制算法的正确性。
在确定并创建了这种证明技术之后，Platzer声称下一步是使用它来增强人工智能学习代理的功能 - 增加其复杂性，同时验证其安全性。
最终，Platzer希望这将最终使技术能够让CPS从预期结果未能成为现实的准确模型的情况中恢复过来。例如，如果自动驾驶汽车假设另一辆汽车在实际减速时加速，则需要能够快速纠正此错误并切换到正确的现实数学模型。
这种无缝转换越复杂，它们实现起来就越复杂。但它们是安全性和灵活性的最终融合，换句话说，是人工智能与安全防护技术的最终结合。
创造明天的技术
到目前为止，Platzer研究的最大进展之一是KeYmaera X prover，Platzer将其定义为“我们安全技术可靠性方面的巨大飞跃，远远超出其他任何人的做法。用于分析网络物理系统。“
由Platzer及其团队创建的KeYmaera X证明器是一种工具，允许用户通过易于使用的界面轻松可靠地为CPS构建数学正确性证明。
从技术上讲，KeYmaera X是一个混合系统定理证明器，它将受控系统的控制程序和物理行为分析在一起，以便为复杂的安全验证技术提供有效的计算和必要的支持。最终，这项工作建立在之前称为KeYmaera的技术迭代之上。但是，Platzer表示，为了优化工具并使其尽可能简单，团队基本上“从头开始”。
Platzer强调这些最近的变化有多么引人注目，并指出，在之前的证明中，语句的正确性取决于大约66,000行代码。值得注意的是，这66,000行中的每一行都对判决的正确性至关重要。根据Platzer的说法，这会带来一个问题，因为确保所有线路都能正确实施非常困难。尽管KeYmaera的最新版本最终与之前的版本一样大，但在KeYmaera X中，负责验证正确性的证明器部分仅为2,000行代码。
这使得团队可以比以往更可靠地评估网络物理系统的安全性。“我们确定了这个微内核，这个系统中真正微不足道的部分负责答案的正确性，所以现在我们有更好的机会确保我们不会意外地将任何错误泄漏到推理引擎中，”Platzer说过。同时，他指出，它使用户能够在分析中进行更积极的自动化。Platzer解释说，“如果你有一小部分系统负责正确性，那么你可以做更自由的自动化。它可以更加勇敢，因为它下面有一个完整的安全网。“
对于他的研究的下一阶段，Platzer将开始整合可能将现实描述为CPS的多种数学模型。为了解释这些接下来的步骤，Platzer再次回归自动驾驶汽车：“如果你跟随另一个驾驶员，你不知道驾驶员是否正在寻找停车位，试图快速到达某个地方，或者即将到来改变车道。因此，原则上，在这种情况下，拥有多个可能的模型并遵守可能是对现实的最佳解释的模型是个好主意。“
最终，目标是允许CPS通过在这些多个模型之间切换来增加其灵活性和复杂性，因为它们或多或少可能解释现实。“世界是一个复杂的地方，”普拉泽尔解释说，“所以世界的安全分析也必须是一个复杂的分析。”